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

```Dear Christoph,

Consider the proofs:

lemma 1:
"ALL i. i < length xs --> xs ! i = hd (drop i xs)"
proof
fix i
show "i < length xs --> xs ! i = hd (drop i xs)"
proof
assume "i < length xs"
then show "xs ! i = hd (drop i xs)"
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
qed
qed
thm 1
thm 1 [rule_format]

lemma 2:
"!!i. i < length xs ==> xs ! i = hd (drop i xs)"
proof -
fix i
assume "i < length xs"
then show "xs ! i = hd (drop i xs)"
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
qed
thm 2

lemma 3:
assumes "i < length xs"
shows "xs ! i = hd (drop i xs)"
using assms
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
thm 3

```
I hope the example proofs still cover the structure that was important to you (I changed them only to have some lemma I could actually prove). Note the following points:
```
```
1) In lemma 3 we do not explicitly all-quantify i, thus it is handled as "arbitrary but fixed" throughout the proof (and implicitly all-quantified after the proof is finished; in fact "thm 2" and "thm 3" give exactly the same result). This can always be done when we do not need to vary/instantiate i inside the proof itself.
```
```
2) The attribute [rule_format] turns (some) HOL connectives into Pure connectives (which are used to present natural deduction style rules in Isabelle, hence the name).
```
```
3) For Isar proofs (i.e., structured proofs, as opposed to proof-scripts) the style of lemma 3 is the most idiomatic, if such a style is not possible (since we need to generalize a variable like i), then the style of lemma 2 is the next most idiomatic. As Larry already pointed out, the style of lemma 1 is the least idiomatic nowadays.
```
hope that helps,

chris

On 11/01/2012 10:20 AM, Christoph LANGE wrote:
```
```2012-10-31 20:09 Lawrence Paulson:
```
```On 31 Oct 2012, at 18:28, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote:
```
```* In statements such as "!x. p x --> q x" it is tedious (and always
the same) to break their structure down to a level where the actually
interesting work starts.
```
```
It is almost never necessary or helpful to state a theorem in that
format.
```
```

```
```I suggest

lemma "p x ==> q x"

for a straightforward proof, or

lemma assumes "p x" shows "q x"

for a more complicated structured proof.
```
```
… such a structure doesn't always work; I think the proofs will also

The following lemma (reduced to the structural outline) has a
(anti-)pattern that is typical for my formalisation:

lemma skip_index_keeps_non_negativity :
fixes n::nat and v::real_vector
assumes non_empty: "n > 0"
and non_negative: "non_negative_real_vector n v"
shows "\<forall>i::nat . in_range n i \<longrightarrow>
non_negative_real_vector (n-(1::nat)) (skip_index v i)"
proof
fix i::nat
show "in_range n i \<longrightarrow> non_negative_real_vector
(n-(1::nat)) (skip_index v i)"
proof
assume "in_range n i"
...
show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" sorry
qed
qed

How would I have to adapt the proof when rephrasing the statement as
shows "in_range n i \<Longrightarrow> ..." ?

(I'll be happy to accept "RTFM" as an answer, if you could give me a
pointer.)

Cheers, and thanks,

Christoph

```
```

```

• References:

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