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



Hi Makarius,

I'm trying out some instructions  you gave earlier, but I keep getting
an error saying:

"*** reconstruct_proof: minimal proof object
*** At command "full_prf"."

prf a works for me though and gives:

ccontr % _ %% (Lam H: _. ? %% H %% (Lam H: _. zero_less_Suc % _))

Thanks
John

Makarius wrote:
>
> 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.