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

```On Thu, 22 Nov 2012, Christoph LANGE wrote:

```
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.
```
```
Restating case/assume is not a big deal, it is done occasionally and not bad style, only a bit redundant and less formally checked than could be done otherwise.
```
```
To make it more tight, you can do it via literal fact references or the corresponing "fact" method like this:
```
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

```
BTW, according to the way the logical framework works, you can have redundant 'assume' statements in your proof body, but not redundant 'fix'. The "fix n" is already part of the case (Suc n). Another fix n would postulate a different hyptothetical entity in the context, that is not the same, and its assumptions unrelated to what you have already after invoking the case.
```
```
The funny thing is that textbook logicians often omit the formal "fix n" altogether. I've seen this even in some implementations of logic, where the global absence of a declaration over the whole text is taken as an implicit fix of a local variable.
```

Makarius
```

• References:

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