# HG changeset patch
# User haftmann
# Date 1414065845 -7200
# Node ID 70fff47875cd71d5a347399852977c130c464e23
# Parent  06dfbfa4b3eab4b1d4c03ecc328334d082f36899
parity induction over natural numbers

diff -r 06dfbfa4b3ea -r 70fff47875cd src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Oct 22 23:15:40 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
@@ -353,6 +353,32 @@
 lemma odd_two_times_div_two_Suc:
   "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
   using odd_two_times_div_two_succ [of n] by simp
+
+lemma parity_induct [case_names zero even odd]:
+  assumes zero: "P 0"
+  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
+  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+  shows "P n"
+proof (induct n rule: less_induct)
+  case (less n)
+  show "P n"
+  proof (cases "n = 0")
+    case True with zero show ?thesis by simp
+  next
+    case False
+    with less have hyp: "P (n div 2)" by simp
+    show ?thesis
+    proof (cases "even n")
+      case True
+      with hyp even [of "n div 2"] show ?thesis
+        by (simp add: dvd_mult_div_cancel)
+    next
+      case False
+      with hyp odd [of "n div 2"] show ?thesis 
+        by (simp add: odd_two_times_div_two_Suc)
+    qed
+  qed
+qed
   
 text {* Nice facts about division by @{term 4} *}