Re: [isabelle] Aligning full_prf with proof term



Anyone got any idea?

Thanks
John

On Sun, Oct 2, 2011 at 2:51 PM, John Munroe <munddr at gmail.com> wrote:
> Hi,
>
> I'm trying to find a clause that is displayed by 'full_prf' in a proof
> term. For instance:
>
> axiomatization
> f :: "nat => nat"
> where ax: "f 0 = 0"
> and ax': "f 0 = 1"
>
> lemma lem1: "f 0 = 1 | f 0 = 0"
> using ax
> by auto
>
> full_prf lem1
>
> gives the following proof:
>
> equal_elim % True % f 0 = 1 | f 0 = 0 %%
>  (symmetric % TYPE(prop) % f 0 = 1 | f 0 = 0 % True %%
>   (combination % TYPE(bool) % TYPE(prop) % Trueprop % Trueprop %
>     f 0 = 1 | f 0 = 0 %
>     True %%
>     (reflexive % TYPE(bool => prop) % Trueprop) %%
>     (transitive % TYPE(bool) % f 0 = 1 | f 0 = 0 % False | True % True %% ...
>
> Now if I do:
>
> ML {*
> val thm = @{thm "lem1"};
> val prf = Thm.proof_of thm;
> val prop = Thm.full_prop_of thm;
> val prf' = Proofterm.rewrite_proof_notypes ([],[]) prf;
> val prf'' = Reconstruct.reconstruct_proof @{theory} prop prf'
> *}
>
> I get a massive proof term. If I want to find the line "(transitive %
> TYPE(bool) % f 0 = 1 | f 0 = 0 % False | True % True %%", how do I
> extract it from the proof term? I'm just trying to see which disjunct
> is proved, so I thought if I could extract "False | True" then I can
> infer that the second disjunct is proved.
>
> Any assistance or opinions will be much appreciated. Thanks.
>
> John
>





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