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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and