Re: [isabelle] Aligning full_prf with proof term



Quoting John Munroe <munddr at gmail.com>:
I'm trying to find a clause that is displayed by 'full_prf' in a proof
term. For instance:

[...]

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.

Hi John,

since your theorem has already been stored in the theorem database,
the proof returned by Thm.proof_of has simply the form

  PThm (..., (("Theory_Name.lem1", ..., ...), body))

so you have to use Proofterm.strip_thm to obtain the actual proof. You can
then search for the desired subproof by recursion on the structure of the
proof term datatype (see attached theory).

Greetings,
Stefan




Any assistance or opinions will be much appreciated. Thanks.

John




Attachment: Munroe.thy
Description: Binary data



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