[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Grind and automatic rewrites



Hi Pertti,

The :exclude argument to grind seems to work for me, as shown below.
Is this what you meant?

Sam
-------

foo :  

  |-------
{1}   "foo" = "bar"

Rule? (grind)
Rewriting with length
Rewriting with length
Rewriting with length
Rewriting with length
Rewriting with list2finseq
Rewriting with length
Rewriting with length
Rewriting with length
Rewriting with list2finseq
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
foo :  

  |-------
{1}   (LAMBDA (x:
                 below[length(cons(char(102),
                                   cons(char(111),
                                        cons(char(111), null))))]):
         nth(cons(char(102), cons(char(111), cons(char(111), null))), x))
       =
       (LAMBDA (x:
                  below[length(cons(char(98),
                                    cons
                                    (char(97), cons(char(114), null))))]):
          nth(cons(char(98), cons(char(97), cons(char(114), null))), x))

Rule? (undo)y
This will undo the proof to: 
foo :  

  |-------
{1}   "foo" = "bar"
Sure?(Y or N): 
foo :  

  |-------
{1}   "foo" = "bar"

Rule? (grind :exclude "length")
Rewriting with list2finseq
Rewriting with list2finseq
Trying repeated skolemization, instantiation, and if-lifting,
this yields  2 subgoals: 
foo.1 :  

  |-------
{1}   (LAMBDA (x:
                 below[length(cons(char(102),
                                   cons(char(111),
                                        cons(char(111), null))))]):
         nth(cons(char(102), cons(char(111), cons(char(111), null))), x))
       =
       (LAMBDA (x:
                  below[length(cons(char(98),
                                    cons
                                    (char(97), cons(char(114), null))))]):
          nth(cons(char(98), cons(char(97), cons(char(114), null))), x))

Rule? (undo)y
This will undo the proof to: 
foo :  

  |-------
{1}   "foo" = "bar"
Sure?(Y or N): 
foo :  

  |-------
{1}   "foo" = "bar"

Rule? (grind :exclude ("length" "list2finseq"))
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
foo :  

  |-------
[1]   "foo" = "bar"

Rule?