Does Isabelle support custom case distinctions when proving statements? Let's say I want to prove a statement for all natural numbers n, but the proof is entirely different depending on whether n is even or odd. Is it possible to do that case distinction in a proof, like
proof(cases n)
assume "n mod 2 = 0"
<proof>
next assume "n mod 2 = 1"
<proof>
qed
So far, I'd split the lemma/theorem in two seperate parts (assuming n even/odd) and then use these parts to proof the statement for all natural numbers, but that does not appear to be the optimal solution.
In Isabelle2017, you can prove ad-hoc case distinction rules easily, like so:
lemma "P (n::nat)"
proof -
consider (odd) "odd n" | (even) "even n" by auto
then show ?thesis
proof cases
case odd
then show ?thesis sorry
next
case even
then show ?thesis sorry
qed
qed