*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 22 Nov 2012 15:31:40 +0100*In-reply-to*: <50AE3314.8060002@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>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

Am 22/11/2012 15:13, schrieb Christoph LANGE: > Dear Larry, dear all, > > I'm now back at our auction formalisation and catching up with emails. > > I have taken into account the advice I got from you and the others; basically I > managed to change my statements from > > shows "!i . p x --> q x" > > to > > fixes ... and i > assumes "p x" > shows "q x" Unless you want to give the type of i, you don't need to fix it. > This and similar changes helped to shorten the overall formalisation from 1145 > to 1045 lines (see > http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy). > I'm sure I can do even better. > > I have not yet made any further simplifications, such as doing a lot of things > at once in a style like > > ... by (induct i arbitrary: xs) (case_tac xs, simp_all)+ > > that Chris used in his example of a lemma about lists. At the moment I don't > even know how to get started using such proof methods. > > 2012-11-01 12:03 Lawrence Paulson: >> You should look at the documentation on the induct/induction proof methods. > > Where can I find that documentation? The Tutorial mainly uses > apply(induct_tac), which is probably something else. This is what I suggested to you 3 weeks back: "If you look at the documentation page http://isabelle.in.tum.de/documentation.html you will find that the first document is the relatively new Programming and Proving in Isabelle/HOL, which does cover structured proofs (which is why I wrote it). The Tutorial is now only second choice because of the foucus on "apply"." That is also where you find the induction method. > Is there a single, up to > date reference manual that documents all proof methods? Yes, the reference manual (more or less). > BTW, changing induction proofs to "assumes ... shows ..." did not always make > them shorter. Is there a way of not having to explicitly restate the assumption > for (Suc n) in the induction step? Indeed, for inductions, the most convenient way is stating them as implications (with ==>). The manuals above will also tell you about the naming conventions of assumptions in each case. Tobias > E.g. I have one lemma of the following structure, which proves some property of > a function "fun maximum": > > lemma maximum_sufficient : > fixes n::nat and ... > assumes assm1: "p n" > and assm2: "q n" > and assm3: "r n" > shows "s n" > using assms (* <-- now this became necessary, > otherwise even "case 0" would fail, but why? *) > proof (induct n) > case 0 > then show ?case by simp > next > case (Suc n) > (* and now I have to explicitly restate all assumptions: *) > assume assm1: "p (Suc n)" > assume assm2: "q (Suc n)" > assume assm3: "r (Suc n)" > ... > show "s (Suc n)" ... > qed > > Cheers, and thanks for any help, > > Christoph >

**Follow-Ups**:

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

- Previous by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- 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] ?spam? Re: 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