In prog-prove the following example is used to introduce `rule: something.induct`

:

```
fun div2 :: "nat ⇒ nat" where
"div2 0 = 0" |
"div2 (Suc 0) = 0" |
"div2 (Suc (Suc n)) = Suc (div2 n)"
```

And with `apply (induction n rule: div2.induct)`

we can finish the proof with `auto`

compared to `apply (induction n)`

where the tutorial says that it needs further case analysis in the induction step.

I was wondering how that would look like. At this point there were not many (if any) examples that use case analysis in `apply`

proofs and I could not figure it out myself so far.

Thanks!

Hi,

after `apply (induction n)`

the `n`

in the second subgoal is under a quantifier, so you do a direct case analysis.

You can use `subgoal for m`

to focus on that subgoal and introduce a new variable `m`

that you can split on.

```
lemma "div2 n = n div 2"
apply (induction n)
subgoal by simp
subgoal for m
apply (cases m)
apply simp
sorry
done
```

Still in this case you will not be able to complete the proof, as the induction hypothesis only gives you information about `div2 m`

but you need information about `div2 (m-1)`

. You may instead prove following stronger theorem:

```
lemma "div2 n = n div 2 ∧ div2 (Suc n) = (Suc n) div 2"
apply (induction n)
apply auto
done
```

or use a stronger induction rule:

```
lemma "div2 n = n div 2"
apply (induction n rule: less_induct)
subgoal for n
apply (cases n)
subgoal by simp
subgoal for n'
apply (cases n')
by auto
done
done
```

However, all these proofs can be expressed much better using the Isar language (Chapter 4). I would strongly advise against using such nested apply style proofs.

```
lemma "div2 n = n div 2"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case
proof (cases n)
case 0
then show ?thesis by simp
next
case (Suc m)
then show ?thesis sorry
qed
qed
```

waynee95 has marked this topic as resolved.

Last updated: Sep 22 2023 at 08:19 UTC