In prog-prove the following example is used to introduce
fun div2 :: "nat ⇒ nat" where "div2 0 = 0" | "div2 (Suc 0) = 0" | "div2 (Suc (Suc n)) = Suc (div2 n)"
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.
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