[isabelle] Aligning full_prf with proof term



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.