## Stream: Beginner Questions

### Topic: div2 induction example

#### waynee95 (Dec 11 2021 at 20:39):

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!

#### Maximilian Schaeffeler (Dec 13 2021 at 07:35):

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
``````

Last updated: Jul 15 2022 at 23:21 UTC