# [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.*