Re: [isabelle] Delving into Isabelle.
Am 16/12/2012 02:24, schrieb Layus:
> 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 *)
> 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.
At the end of the simplification process, the simplifier tries to solve the goal
by some trivial means, for example by unifying it with True.
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and