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

```2012-11-22 16:04 Lars Noschinski:
```
```On 22.11.2012 15:13, Christoph LANGE wrote:
```
```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 (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)"
...
```
```
You don't need to restate your assumptions here: They are all stored in
"Suc" (or Suc.prems, which omits the hypotheses added by induction).
```
```

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

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.