Re: [isabelle] Delving into Isabelle.



Am 16/12/2012 02:24, schrieb Layus:
> 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.

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.

Tobias

> 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.