*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Aligning full_prf with proof term*From*: John Munroe <munddr at gmail.com>*Date*: Tue, 4 Oct 2011 01:49:10 +0100*In-reply-to*: <CAP0k5J6U0BY9ycKRiba9T00+Mwt+a9et0k_OHzNOi1ySjDk9XQ@mail.gmail.com>*References*: <CAP0k5J6U0BY9ycKRiba9T00+Mwt+a9et0k_OHzNOi1ySjDk9XQ@mail.gmail.com>

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 >

**Follow-Ups**:**Re: [isabelle] Aligning full_prf with proof term***From:*Jasmin Blanchette

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

**Re: [isabelle] Aligning full_prf with proof term***From:*Stefan Berghofer

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

- Previous by Date: Re: [isabelle] Isabelle release candidate
- Next by Date: Re: [isabelle] Aligning full_prf with proof term
- Previous by Thread: [isabelle] Aligning full_prf with proof term
- Next by Thread: Re: [isabelle] Aligning full_prf with proof term
- 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