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

```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"

```
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. Is there a single, up to date reference manual that documents all proof methods?
```
```
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?
```
```
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

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

```

• Follow-Ups:
• References:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.