# Re: [isabelle] Obtaining the instantiation of variables in a proof

On Wed, 15 Apr 2009, Stephy Wong wrote:

`Thanks. What I actually meant is that is it possible to obtain the
``instantiation(s) that Isabelle has found automatically? The example I
``gave is a trivial one that Isabelle can proof automatically, but I'm
``interested in seeing how Isabelle instantiates the theorem. Does this
``need to be done in ML?
`

You need some tiny bit of ML, namely:
ML "proofs := 2";

`Now you can inspect what happens internally, although the details of
``automated tools are often hard to follow. For example:
`
lemma a: "EX x::nat. x > 0" by auto
full_prf a
ccontr % EX x. 0 < x %%
(Lam H: ~ (EX x. 0 < x).
HOL.swap % EX x. 0 < x % False %% H %%
(Lam H: ~ False.
exI % TYPE(nat) % op < 0 % Suc ?a2 %% (zero_less_Suc % ?a2)))

`This is nat too bad: it says in the last line that exI was used with the
``term "Suc ?a2", for an arbitrary ?a2. If you try this with "by arith"
``instead, you get less satisfactory output, though.
`
Makarius

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