[isabelle] Delving into Isabelle.



Hi,

I am currently trying to get a grasp at the internals of Isabelle.
I would like to expose some higher order unification within a proof.

I started with some simple theorem.

theorem Isa : "? P. ( P x & P y )" 
  apply (intro exI)
  apply (intro conjI)
  using [[simp_trace]]
  apply simp
  apply eval (* anything solves True *)
done

This behaves as expected, and shows second order unification,
but I cannot see how the simp tactic gets rid of my first subgoal.

To state it in another way :
What is the magic in HOL that is able to simplify "?P x" into a proven subgoal.

The trace shows nothing except that the second goal changes from "?P x" to "True",
which means that somehow "P" got unified with "%x . True".

Any pointer would be welcome.

Best regards,
Guillaume.


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