src/HOL/Parity.thy
 changeset 58769 70fff47875cd parent 58740 cb9d84d3e7f2 child 58770 ae5e9b4f8daf
```     1.1 --- a/src/HOL/Parity.thy	Wed Oct 22 23:15:40 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
1.3 @@ -353,6 +353,32 @@
1.4  lemma odd_two_times_div_two_Suc:
1.5    "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
1.6    using odd_two_times_div_two_succ [of n] by simp
1.7 +
1.8 +lemma parity_induct [case_names zero even odd]:
1.9 +  assumes zero: "P 0"
1.10 +  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1.11 +  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1.12 +  shows "P n"
1.13 +proof (induct n rule: less_induct)
1.14 +  case (less n)
1.15 +  show "P n"
1.16 +  proof (cases "n = 0")
1.17 +    case True with zero show ?thesis by simp
1.18 +  next
1.19 +    case False
1.20 +    with less have hyp: "P (n div 2)" by simp
1.21 +    show ?thesis
1.22 +    proof (cases "even n")
1.23 +      case True
1.24 +      with hyp even [of "n div 2"] show ?thesis
1.25 +        by (simp add: dvd_mult_div_cancel)
1.26 +    next
1.27 +      case False
1.28 +      with hyp odd [of "n div 2"] show ?thesis
1.29 +        by (simp add: odd_two_times_div_two_Suc)
1.30 +    qed
1.31 +  qed
1.32 +qed
1.33
1.34  text {* Nice facts about division by @{term 4} *}
1.35
```