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.