*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Aligning full_prf with proof term*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Tue, 04 Oct 2011 19:37:13 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAP0k5J7RoBpzcb7DWjLE_BQ3kJvQTodf=ZW3X8rDp0Mb71o=cw@mail.gmail.com>*References*: <CAP0k5J6U0BY9ycKRiba9T00+Mwt+a9et0k_OHzNOi1ySjDk9XQ@mail.gmail.com> <CAP0k5J7RoBpzcb7DWjLE_BQ3kJvQTodf=ZW3X8rDp0Mb71o=cw@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

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**

**References**:**[isabelle] Aligning full_prf with proof term***From:*John Munroe

**Re: [isabelle] Aligning full_prf with proof term***From:*John Munroe

- Previous by Date: Re: [isabelle] Aligning full_prf with proof term
- Next by Date: Re: [isabelle] Mutual induction in ML
- Previous by Thread: Re: [isabelle] Aligning full_prf with proof term
- Next by Thread: [isabelle] Mutual induction in ML
- Cl-isabelle-users October 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list