*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]*From*: Makarius <makarius at sketis.net>*Date*: Fri, 23 Nov 2012 14:44:33 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50AE5AD0.2010203@cs.bham.ac.uk>*References*: <50916DB3.4030707@cs.bham.ac.uk> <B342CF2B-EEC3-4932-A98D-193702F57A14@cam.ac.uk> <5091CE53.6020006@cs.bham.ac.uk> <C76381F2-5127-48DF-B198-DE2B3AABEAB1@cam.ac.uk> <50AE3314.8060002@cs.bham.ac.uk> <50AE4CF2.2030809@in.tum.de> <50AE5AD0.2010203@cs.bham.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 22 Nov 2012, Christoph LANGE wrote:

For readability I'd sometimes like to make it explicit to whatassumption I'm referring when there is more than one.When explicitly restating them with 'assume "... (Suc n) ..."' that's noproblem. With "Suc" I found, e.g., Suc.prems(1) to work. A symbolicname, e.g. Suc.prems(foo), if the original statement says 'assumes foo:"..."', would be even nicer – but that's not possible, I suppose.

notepad begin fix n :: nat have "P n" proof (induct n) case 0 then show ?case sorry next case (Suc n) then show ?case sorry qed have "P n" proof (induct n) case 0 show "P 0" sorry next case (Suc n) from `P n` show "P (Suc n)" sorry qed have "P n" proof (induct n) case 0 show "P 0" sorry next case (Suc n) have "P n" by fact then show "P (Suc n)" sorry qed have "P n" proof (induct n) case 0 show "P 0" sorry next case (Suc n) assume "P n" then show "P (Suc n)" sorry qed have "P n" proof (induct n) show "P 0" sorry next fix n assume "P n" then show "P (Suc n)" sorry qed end

Makarius

**References**:**[isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Lawrence Paulson

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Christoph LANGE

**Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]***From:*Lars Noschinski

*From:*Christoph LANGE

- Previous by Date: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Next by Date: Re: [isabelle] Title of "Programming and Proving" [Re: ?spam? Re: Simpler theorem statements, and proofs for them]
- Previous by Thread: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Thread: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Cl-isabelle-users November 2012 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