Re: [isabelle] Obtaining the instantiation of variables in a proof
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 % _))
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and