I'd like to prove the following lemma:
lemma mod10_cases:
"P 0 ⟹ P 1 ⟹ P 2 ⟹ P 3 ⟹ P 4 ⟹ P 5 ⟹ P 6 ⟹ P 7 ⟹ P 8 ⟹ P 9 ⟹ P (n mod 10)"
but am finding it surprisingly tricky. The lemma feels straightforward; it just says that in order to prove a property P holds of every number modulo 10, I just need to check that it holds of 0, 1, 2, 3, 4, 5, 6, 7, 8, and 9.
(Wider picture: I want to use my lemma to prove theorems of the form foo(n mod 10), which I intend to start by saying apply (cases rule: mod10_cases).)
My usual trick is to first show n mod 10 ∈ {..<10} (which is trivially proven by simp) and then unfold {..<10} to {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}, which can be done by feeding the right rules to the simplifier:
lemma mod10_induct [case_names 0 1 2 3 4 5 6 7 8 9]:
fixes n :: nat
assumes "P 0" "P 1" "P 2" "P 3" "P 4" "P 5" "P 6" "P 7" "P 8" "P 9"
shows "P (n mod 10)"
proof -
have "n mod 10 ∈ {..<10}"
by simp
also have "{..<10} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9 :: nat}"
by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
finally show ?thesis using assms
by fastforce
qed
Note that the way you wrote your theorem, it has the shape of an induction rule, not a case-splitting rule. A case-splitting rule would look more like this:
lemma mod10_cases [case_names 0 1 2 3 4 5 6 7 8 9]:
fixes n :: nat
obtains "n mod 10 = 0" | "n mod 10 = 1" | "n mod 10 = 2" | "n mod 10 = 3" | "n mod 10 = 4" |
"n mod 10 = 5" | "n mod 10 = 6" | "n mod 10 = 7" | "n mod 10 = 8" | "n mod 10 = 9"
proof -
have "n mod 10 ∈ {..<10}"
by simp
also have "{..<10} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9 :: nat}"
by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
finally show ?thesis using that
by fast
qed
If the obtains here confuses you, the final theorem you get from this looks like this:
theorem mod10_cases:
(?n mod 10 = 0 ⟹ ?thesis) ⟹
(?n mod 10 = 1 ⟹ ?thesis) ⟹
(?n mod 10 = 2 ⟹ ?thesis) ⟹
(?n mod 10 = 3 ⟹ ?thesis) ⟹
(?n mod 10 = 4 ⟹ ?thesis) ⟹
(?n mod 10 = 5 ⟹ ?thesis) ⟹
(?n mod 10 = 6 ⟹ ?thesis) ⟹
(?n mod 10 = 7 ⟹ ?thesis) ⟹
(?n mod 10 = 8 ⟹ ?thesis) ⟹
(?n mod 10 = 9 ⟹ ?thesis) ⟹ ?thesis
You can then use your rules like this:
lemma "P (n mod 10 :: nat)"
apply (induction n rule: mod10_induct)
oops
lemma "P (n mod 10 :: nat)"
apply (cases n rule: mod10_cases)
oops
In most circumstances, however, I would not derive a separate rule for this as you did to begin with – I would simply do the unfolding of {..<10} at the place where I need it instead, since it only takes about 4 lines, and then feed the fact that n mod 10 ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} to my actual goal and hit it with auto.