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 longer possible.]

Larry Paulson


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
theorem.  Why?






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