author haftmann Fri, 14 Jun 2019 08:34:27 +0000 changeset 70523 c832d431636b parent 70522 48609a6af1a0 child 70524 e939ea997f5f
slightly more stringent ordering of theorems
 src/HOL/Parity.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -548,63 +548,6 @@
qed
qed

-lemma int_parity_induct [case_names zero minus even odd]:
-  "P k" if zero_int: "P 0"
-    and minus_int: "P (- 1)"
-    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
-    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
-proof (cases "k \<ge> 0")
-  case True
-  define n where "n = nat k"
-  with True have "k = int n"
-    by simp
-  then show "P k"
-  proof (induction n arbitrary: k rule: nat_parity_induct)
-    case zero
-    then show ?case
-  next
-    case (even n)
-    have "P (int n * 2)"
-      by (rule even_int) (use even in simp_all)
-    with even show ?case
-  next
-    case (odd n)
-    have "P (1 + (int n * 2))"
-      by (rule odd_int) (use odd in simp_all)
-    with odd show ?case
-  qed
-next
-  case False
-  define n where "n = nat (- k - 1)"
-  with False have "k = - int n - 1"
-    by simp
-  then show "P k"
-  proof (induction n arbitrary: k rule: nat_parity_induct)
-    case zero
-    then show ?case
-  next
-    case (even n)
-    have "P (1 + (- int (Suc n) * 2))"
-      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
-    also have "\<dots> = - int (2 * n) - 1"
-    finally show ?case
-      using even by simp
-  next
-    case (odd n)
-    have "P (- int (Suc n) * 2)"
-      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
-    also have "\<dots> = - int (Suc (2 * n)) - 1"
-    finally show ?case
-      using odd by simp
-  qed
-qed
-
lemma not_mod2_eq_Suc_0_eq_0 [simp]:
"n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
using not_mod_2_eq_1_eq_0 [of n] by simp
@@ -759,6 +702,63 @@
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])

+lemma int_parity_induct [case_names zero minus even odd]:
+  "P k" if zero_int: "P 0"
+    and minus_int: "P (- 1)"
+    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
+    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
+proof (cases "k \<ge> 0")
+  case True
+  define n where "n = nat k"
+  with True have "k = int n"
+    by simp
+  then show "P k"
+  proof (induction n arbitrary: k rule: nat_parity_induct)
+    case zero
+    then show ?case
+  next
+    case (even n)
+    have "P (int n * 2)"
+      by (rule even_int) (use even in simp_all)
+    with even show ?case
+  next
+    case (odd n)
+    have "P (1 + (int n * 2))"
+      by (rule odd_int) (use odd in simp_all)
+    with odd show ?case
+  qed
+next
+  case False
+  define n where "n = nat (- k - 1)"
+  with False have "k = - int n - 1"
+    by simp
+  then show "P k"
+  proof (induction n arbitrary: k rule: nat_parity_induct)
+    case zero
+    then show ?case
+  next
+    case (even n)
+    have "P (1 + (- int (Suc n) * 2))"
+      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
+    also have "\<dots> = - int (2 * n) - 1"
+    finally show ?case
+      using even by simp
+  next
+    case (odd n)
+    have "P (- int (Suc n) * 2)"
+      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
+    also have "\<dots> = - int (Suc (2 * n)) - 1"