Re: [isabelle] Induction starting from 1 and beyond

Maybe this is a good point to remind us all of the very nice "induction_schema" method that comes with the function package by Alex Krauss (and the automatic "termination" methods that also come with it, like "lexicographic_order").
```
lemma ind_from_2 [case_names 0 1 2 many]:
fixes P :: "nat â bool"
assumes "P 0"
and "P 1"
and "P 2"
and "âk. k â 2 â P k â P (Suc k)"
shows "P n"
using assms
apply (induction_schema)
apply (case_tac n, force, force)
apply (lexicographic_order)
done

```
the 2nd line of the proof script is a bit awkward in this case, but can often be replaced by "apply (pat_completeness)" (which raises an exception on this specific example).
```
cheers

chris

On 03/24/2015 11:02 PM, Joachim Breitner wrote:
```
```Dear Douglas,

Am Dienstag, den 24.03.2015, 15:37 -0500 schrieb W. Douglas Maurer:
```
```P. S. While I was still in graduate school I co-wrote a paper
containing an inductive proof in which the inductive step, P(k-1)
implies P(k), depended on the fact that k >= 3. Therefore I needed
two basis steps, one for k = 1, which was trivial, and one for k = 2,
which my co-author supplied. How would you do something like that in
Isar?
```
```
remember that inductions schemes are just regular lemmas, so you can
always define precisely the induction rule that you need, and use that:

lemma ind_from_2[case_names 0 1 2 many]:
assumes "P 0"
assumes "P 1"
assumes "P 2"
assumes "â k. k â 2 â P k â P (Suc k)"
shows "P n"
proof(induction n)
case 0 thus ?case by fact
next
case (Suc k)
have "k = 0 â k = 1 â k â 2" by auto
with Suc.IH assms
show ?case by (auto simp add: numeral_eq_Suc)
qed

And later

lemma "foo n"
proof(induction n rule: ind_from_2)
case 0 show ?case...
next
case 1 show ?case...
next
case 2 show ?case...
next
case many show ?case...
qed

I find this separation of concerns makes your proofs much easier to read
and understand.

Greetings,
Joachim

```
```

```

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