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)
apply eval (* anything solves True *)
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.