[isabelle] unexpected (for me) output using FOL



Dear ALL x. IsabelleExpert(x):

Sometimes Isabelle returns outputs that I see as somewhat unexpected...

For instance, suppose I want to show that the name of a universally
quantified variable can be changed, and write:

Goalw [iff_def] "(ALL x. P(x)) <-> (ALL y. P(y))";

I would have expected then the output to be a goal such as:

((ALL x. P(x))-->(ALL y. P(y))) & ((ALL y. P(y))-->(ALL x. P(x)))

but Isabelle gives me the following:

Level 0 (1 subgoal)
((ALL x. P(x))<->(ALL y. P(y)))
1. ((All(P)-->All(P))&(All(P)-->All(P)))
val it = [] : Thm.thm list

WHY??

Suppose, moreover, I want to prove that contiguous universal
quantifiers can be exchanged, and write:

Goalw [iff_def] "(ALL x. (ALL y. P(x,y))) <-> (ALL y. (ALL x. P(x,y)))";

Here the output is:

Level 0 (1 subgoal)
(ALL x y. P(x, y)) <-> (ALL y x. P(x, y))
1. ((ALL x. All(P(x))) --> (ALL y x. P(x, y))) &
   ((ALL y x. P(x, y)) --> (ALL x. All(P(x))))
val it = [] : Thm.thm list

WHY does the system exchange some but not all instances of P(x,y) for
P(x), and uses "All" to write the new goal??

I note that these things only occur when I use Goalw plus a rewrite
rule such as iff_def, but not if I simply use Goal to prove my
theorem.  Why?

Thanx in advance for the clarification,
JM

--
My homepages:
http://geocities.com/jm_logica/
http://www.dimap.ufrn.br/~jmarcos/
http://slc.math.ist.utl.pt/jmarcos.html





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.