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: Dec 07 2024 at 16:22 UTC