# [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.*