Re: [isabelle] unexpected (for me) output using FOL
Here (ALL x y. P(x, y)) is internally All(%x. All(%y. P x y)), which
can be collapsed to All(%x. All(P x)), so you see (ALL x y. P(x, y)).
The "collapsing" is actually called eta-contraction and it is
performed by the rewriter.
[Note to Isabelle/HOL users: in FOL, P(x,y) is what you would write
as P x y. Thus this example behaves differently in Isabelle/HOL,
where P(x,y) abbreviates P(Pair x y) and the eta-contraction is no
On 3 Nov 2006, at 01:03, Joao Marcos wrote:
(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
This archive was generated by a fusion of
Pipermail (Mailman edition) and