*To*: Andrew Boyton <Andrew.Boyton at nicta.com.au>*Subject*: Re: [isabelle] Undefined facts in skip_proofs mode*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Date*: Thu, 31 Jul 2014 00:16:38 +0000*Accept-language*: en-AU, en-US*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Lars Hupel <hupel at in.tum.de>, Cornelius Diekmann <c.diekmann at googlemail.com>*In-reply-to*: <D2467C67-1A9A-4E24-9EC8-CB682B77EB60@nicta.com.au>*References*: <53D64E5A.60405@in.tum.de> <37A2927A-1BA9-40A1-9EFD-E797FD62728E@nicta.com.au> <D2467C67-1A9A-4E24-9EC8-CB682B77EB60@nicta.com.au>*Thread-index*: AQHPqmduiaMw5T2XSkC4TS4nZ2yo7Ju01k2AgAETHICAAsONAA==*Thread-topic*: [isabelle] Undefined facts in skip_proofs mode

This may be slightly more addressable. You’d have to look at what oops does for skip_proofs and if it can be caught somehow. Cheers, Gerwin On 29 Jul 2014, at 4:04 pm, Andrew Boyton <andrew.boyton at nicta.com.au> wrote: > The skip-proof semantics are confusing though. > > When processing a theorem, skip_proofs takes a theorem ending with "oops" as a valid theorem, and so if you have two versions > of a lemma in a single file, one that has been oopsed, and one later with the same name which is "done", then the second one fails > to be processed, which is unfortunate. > > Andrew > > > On 28 Jul 2014, at 11:39 pm, Gerwin Klein <gerwin.klein at nicta.com.au> wrote: > >> Isn’t that as specified? The proofs are skipped, so Cons.hyps won’t be generated in the induct call. >> >> Cheers, >> Gerwin >> >> On 28 Jul 2014, at 3:21 pm, Lars Hupel <hupel at in.tum.de> wrote: >> >>> Hello, >>> >>> Cornelius and I noticed an oddity when using the system option >>> "skip_proofs". Consider this simple proof: >>> >>> lemma "(xs::'a list) = xs" >>> proof (induct xs) >>> case Cons >>> thm Cons.hyps >>> from Cons show ?case by auto >>> qed auto >>> >>> Notice the "thm" command in the middle. Without "skip_proofs", this goes >>> through fine. Enabling "skip_proofs" produces this message: >>> >>> *** Undefined fact: "Cons.hyps" (line 8 of >>> "~/tmp/Skip_Proof/Skip_Proof.thy") >>> *** At command "thm" (line 8 of "~/tmp/Skip_Proof/Skip_Proof.thy") >>> >>> I have attached a session demonstrating the difference. Run with >>> >>> $ isabelle build -d . -v Skip_Proof >>> >>> Reproducible in all official releases since 2013-2. >>> >>> Cheers >>> Lars >>> <skip_proofs.zip> >> >> >> ________________________________ >> >> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. >> >

**References**:**[isabelle] Undefined facts in skip_proofs mode***From:*Lars Hupel

**Re: [isabelle] Undefined facts in skip_proofs mode***From:*Gerwin Klein

**Re: [isabelle] Undefined facts in skip_proofs mode***From:*Andrew Boyton

- Previous by Date: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Date: Re: [isabelle] 2014-RC1 issues
- Previous by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Next by Thread: Re: [isabelle] Undefined facts in skip_proofs mode
- Cl-isabelle-users July 2014 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