# HG changeset patch
# User haftmann
# Date 1507494502 -7200
# Node ID 93c6632ddf44976fdb594ee28b2a38b6cfe3f8bd
# Parent  a24cde9588bbb59481c391f291192194fa92a730
one uniform type class for parity structures

diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -282,6 +282,9 @@
   "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
   by (simp add: integer_eq_iff)
 
+instance integer :: ring_parity
+  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
 
@@ -927,6 +930,9 @@
   "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
   by (simp add: fun_eq_iff)
 
+instance natural :: semiring_parity
+  by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .
diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>More on quotient and remainder\<close>
 
 theory Divides
-imports Parity
+imports Parity Nat_Transfer
 begin
 
 subsection \<open>Numeral division with a pragmatic type class\<close>
@@ -19,7 +19,7 @@
   and less technical class hierarchy.
 \<close>
 
-class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
+class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -40,29 +40,6 @@
     yields a significant speedup.\<close>
 begin
 
-subclass unique_euclidean_semiring_parity
-proof
-  fix a
-  show "a mod 2 = 0 \<or> a mod 2 = 1"
-  proof (rule ccontr)
-    assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
-    then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
-    have "0 < 2" by simp
-    with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
-    with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
-    with discrete have "1 \<le> a mod 2" by simp
-    with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
-    with discrete have "2 \<le> a mod 2" by simp
-    with \<open>a mod 2 < 2\<close> show False by simp
-  qed
-next
-  show "1 mod 2 = 1"
-    by (rule mod_less) simp_all
-next
-  show "0 \<noteq> 2"
-    by simp
-qed
-
 lemma divmod_digit_1:
   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
@@ -74,7 +51,7 @@
   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
   define w where "w = a div b mod 2"
-  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
   have mod_w: "a mod (2 * b) = a mod b + b * w"
     by (simp add: w_def mod_mult2_eq ac_simps)
   from assms w_exhaust have "w = 1"
@@ -93,7 +70,7 @@
     and "a mod (2 * b) = a mod b" (is "?Q")
 proof -
   define w where "w = a div b mod 2"
-  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
   have mod_w: "a mod (2 * b) = a mod b + b * w"
     by (simp add: w_def mod_mult2_eq ac_simps)
   moreover have "b \<le> a mod b + b"
@@ -318,60 +295,6 @@
 
 declare divmod_algorithm_code [where ?'a = nat, code]
 
-lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
-  by (auto elim: oddE)
-
-lemma even_Suc_div_two [simp]:
-  "even n \<Longrightarrow> Suc n div 2 = n div 2"
-  using even_succ_div_two [of n] by simp
-
-lemma odd_Suc_div_two [simp]:
-  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
-  using odd_succ_div_two [of n] by simp
-
-lemma odd_two_times_div_two_nat [simp]:
-  assumes "odd n"
-  shows "2 * (n div 2) = n - (1 :: nat)"
-proof -
-  from assms have "2 * (n div 2) + 1 = n"
-    by (rule odd_two_times_div_two_succ)
-  then have "Suc (2 * (n div 2)) - 1 = n - 1"
-    by simp
-  then show ?thesis
-    by simp
-qed
-
-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
-    next
-      case False
-      with hyp odd [of "n div 2"] show ?thesis
-        by simp
-    qed
-  qed
-qed
-
-lemma mod_2_not_eq_zero_eq_one_nat:
-  fixes n :: nat
-  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
-  by (fact not_mod_2_eq_0_eq_1)
-
 lemma Suc_0_div_numeral [simp]:
   fixes k l :: num
   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
@@ -708,6 +631,39 @@
 
 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
 
+instance int :: ring_parity
+proof
+  fix k l :: int
+  show "k mod 2 = 1" if "\<not> 2 dvd k"
+  proof (rule order_antisym)
+    have "0 \<le> k mod 2" and "k mod 2 < 2"
+      by auto
+    moreover have "k mod 2 \<noteq> 0"
+      using that by (simp add: dvd_eq_mod_eq_0)
+    ultimately have "0 < k mod 2"
+      by (simp only: less_le) simp
+    then show "1 \<le> k mod 2"
+      by simp
+    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
+      by (simp only: less_le) simp
+  qed
+qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
+
+lemma even_diff_iff [simp]:
+  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
+  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
+  by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
+  using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
+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])
+
 
 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
 
@@ -1495,4 +1451,18 @@
   then show ?thesis ..
 qed
 
+lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
+
+lemma mod_2_not_eq_zero_eq_one_nat:
+  fixes n :: nat
+  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
+  by (fact not_mod_2_eq_0_eq_1)
+
+lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
+  by (fact even_of_nat)
+
+text \<open>Tool setup\<close>
+
+declare transfer_morphism_int_nat [transfer add return: even_int_iff]
+
 end
diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -834,6 +834,10 @@
 
 end
 
+instance star :: (semidom_modulo) semidom_modulo
+  by standard (transfer; simp)
+
+
 
 subsection \<open>Power\<close>
 
@@ -917,14 +921,6 @@
 
 instance star :: (ring_char_0) ring_char_0 ..
 
-instance star :: (semiring_parity) semiring_parity
-  apply intro_classes
-     apply (transfer, rule odd_one)
-    apply (transfer, erule (1) odd_even_add)
-   apply (transfer, erule even_multD)
-  apply (transfer, erule odd_ex_decrement)
-  done
-
 
 subsection \<open>Finite class\<close>
 
diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -218,7 +218,7 @@
 
 lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
   by (auto split: split_root elim!: sgn_power_injE
-      simp: inverse_sgn power_inverse)
+      simp: power_inverse)
 
 lemma real_root_divide: "root n (x / y) = root n x / root n y"
   by (simp add: divide_inverse real_root_mult real_root_inverse)
@@ -715,7 +715,7 @@
     have "x n \<le> sqrt (2 / real n)" if "2 < n" for n :: nat
     proof -
       have "1 + (real (n - 1) * n) / 2 * (x n)\<^sup>2 = 1 + of_nat (n choose 2) * (x n)\<^sup>2"
-        by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd)
+        by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
       also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
         by (simp add: x_def)
       also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -6,19 +6,73 @@
 section \<open>Parity in rings and semirings\<close>
 
 theory Parity
-  imports Nat_Transfer Euclidean_Division
+  imports Euclidean_Division
 begin
 
 subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
 
-class semiring_parity = comm_semiring_1_cancel + numeral +
-  assumes odd_one [simp]: "\<not> 2 dvd 1"
-  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
-  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
-  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
+class semiring_parity = linordered_semidom + unique_euclidean_semiring +
+  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
+    and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
+
+context semiring_parity
 begin
 
-subclass semiring_numeral ..
+lemma of_nat_dvd_iff:
+  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "m = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?Q
+    then show ?P
+      by (auto elim: dvd_class.dvdE)
+  next
+    assume ?P
+    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
+      by simp
+    then have "of_nat n = of_nat (n div m * m)"
+      by (simp add: of_nat_div)
+    then have "n = n div m * m"
+      by (simp only: of_nat_eq_iff)
+    then have "n = m * (n div m)"
+      by (simp add: ac_simps)
+    then show ?Q ..
+  qed
+qed
+
+lemma of_nat_mod:
+  "of_nat (m mod n) = of_nat m mod of_nat n"
+proof -
+  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
+    by (simp add: div_mult_mod_eq)
+  also have "of_nat m = of_nat (m div n * n + m mod n)"
+    by simp
+  finally show ?thesis
+    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
+qed
+
+lemma one_div_two_eq_zero [simp]:
+  "1 div 2 = 0"
+proof -
+  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
+    by (simp only:) simp
+  then show ?thesis
+    by simp
+qed
+
+lemma one_mod_two_eq_one [simp]:
+  "1 mod 2 = 1"
+proof -
+  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
+    by (simp only:) simp
+  then show ?thesis
+    by simp
+qed
 
 abbreviation even :: "'a \<Rightarrow> bool"
   where "even a \<equiv> 2 dvd a"
@@ -26,11 +80,27 @@
 abbreviation odd :: "'a \<Rightarrow> bool"
   where "odd a \<equiv> \<not> 2 dvd a"
 
-lemma even_zero [simp]: "even 0"
-  by (fact dvd_0_right)
+lemma even_iff_mod_2_eq_zero:
+  "even a \<longleftrightarrow> a mod 2 = 0"
+  by (fact dvd_eq_mod_eq_0)
+
+lemma odd_iff_mod_2_eq_one:
+  "odd a \<longleftrightarrow> a mod 2 = 1"
+  by (auto dest: odd_imp_mod_2_eq_1)
 
-lemma even_plus_one_iff [simp]: "even (a + 1) \<longleftrightarrow> odd a"
-  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
+lemma parity_cases [case_names even odd]:
+  assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
+  assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
+  shows P
+  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
+
+lemma not_mod_2_eq_1_eq_0 [simp]:
+  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
+  by (cases a rule: parity_cases) simp_all
+
+lemma not_mod_2_eq_0_eq_1 [simp]:
+  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
+  by (cases a rule: parity_cases) simp_all
 
 lemma evenE [elim?]:
   assumes "even a"
@@ -41,22 +111,107 @@
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
 proof -
-  from assms obtain b where *: "a = b + 1"
-    by (blast dest: odd_ex_decrement)
-  with assms have "even (b + 2)" by simp
-  then have "even b" by simp
-  then obtain c where "b = 2 * c" ..
-  with * have "a = 2 * c + 1" by simp
-  with that show thesis .
+  have "a = 2 * (a div 2) + a mod 2"
+    by (simp add: mult_div_mod_eq)
+  with assms have "a = 2 * (a div 2) + 1"
+    by (simp add: odd_iff_mod_2_eq_one)
+  then show ?thesis ..
+qed
+
+lemma mod_2_eq_odd:
+  "a mod 2 = of_bool (odd a)"
+  by (auto elim: oddE)
+
+lemma one_mod_2_pow_eq [simp]:
+  "1 mod (2 ^ n) = of_bool (n > 0)"
+proof -
+  have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
+    by (induct n) (simp_all add: mod_mult2_eq)
+  then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_mod)
+qed
+
+lemma even_of_nat [simp]:
+  "even (of_nat a) \<longleftrightarrow> even a"
+proof -
+  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
+    by simp
+  also have "\<dots> \<longleftrightarrow> even a"
+    by (simp only: of_nat_dvd_iff)
+  finally show ?thesis .
+qed
+
+lemma even_zero [simp]:
+  "even 0"
+  by (fact dvd_0_right)
+
+lemma odd_one [simp]:
+  "odd 1"
+proof -
+  have "\<not> (2 :: nat) dvd 1"
+    by simp
+  then have "\<not> of_nat 2 dvd of_nat 1"
+    unfolding of_nat_dvd_iff by simp
+  then show ?thesis
+    by simp
 qed
 
-lemma even_times_iff [simp]: "even (a * b) \<longleftrightarrow> even a \<or> even b"
-  by (auto dest: even_multD)
+lemma odd_even_add:
+  "even (a + b)" if "odd a" and "odd b"
+proof -
+  from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
+    by (blast elim: oddE)
+  then have "a + b = 2 * c + 2 * d + (1 + 1)"
+    by (simp only: ac_simps)
+  also have "\<dots> = 2 * (c + d + 1)"
+    by (simp add: algebra_simps)
+  finally show ?thesis ..
+qed
+
+lemma even_add [simp]:
+  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
+  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
+
+lemma odd_add [simp]:
+  "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
+  by simp
+
+lemma even_plus_one_iff [simp]:
+  "even (a + 1) \<longleftrightarrow> odd a"
+  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
+
+lemma even_mult_iff [simp]:
+  "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q
+  then show ?P
+    by auto
+next
+  assume ?P
+  show ?Q
+  proof (rule ccontr)
+    assume "\<not> (even a \<or> even b)"
+    then have "odd a" and "odd b"
+      by auto
+    then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
+      by (blast elim: oddE)
+    then have "a * b = (2 * r + 1) * (2 * s + 1)"
+      by simp
+    also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
+      by (simp add: algebra_simps)
+    finally have "odd (a * b)"
+      by simp
+    with \<open>?P\<close> show False
+      by auto
+  qed
+qed
 
 lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
 proof -
   have "even (2 * numeral n)"
-    unfolding even_times_iff by simp
+    unfolding even_mult_iff by simp
   then have "even (numeral n + numeral n)"
     unfolding mult_2 .
   then show ?thesis
@@ -77,15 +232,26 @@
   then show False by simp
 qed
 
-lemma even_add [simp]: "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
-  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
-
-lemma odd_add [simp]: "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
-  by simp
-
 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto
 
+lemma even_succ_div_two [simp]:
+  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+  by (auto elim!: oddE simp add: add.assoc)
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ [simp]:
+  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+  using mult_div_mod_eq [of 2 a]
+  by (simp add: even_iff_mod_2_eq_zero)
+
 end
 
 class ring_parity = ring + semiring_parity
@@ -93,166 +259,48 @@
 
 subclass comm_ring_1 ..
 
-lemma even_minus [simp]: "even (- a) \<longleftrightarrow> even a"
+lemma even_minus [simp]:
+  "even (- a) \<longleftrightarrow> even a"
   by (fact dvd_minus_iff)
 
-lemma even_diff [simp]: "even (a - b) \<longleftrightarrow> even (a + b)"
+lemma even_diff [simp]:
+  "even (a - b) \<longleftrightarrow> even (a + b)"
   using even_add [of a "- b"] by simp
 
 end
 
-class unique_euclidean_semiring_parity = unique_euclidean_semiring +
-  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
-  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
-  assumes zero_not_eq_two: "0 \<noteq> 2"
-begin
 
-lemma parity_cases [case_names even odd]:
-  assumes "a mod 2 = 0 \<Longrightarrow> P"
-  assumes "a mod 2 = 1 \<Longrightarrow> P"
-  shows P
-  using assms parity by blast
-
-lemma one_div_two_eq_zero [simp]:
-  "1 div 2 = 0"
-proof (cases "2 = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
-  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
-  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
-  then have "1 div 2 = 0 \<or> 2 = 0" by simp
-  with False show ?thesis by auto
-qed
-
-lemma not_mod_2_eq_0_eq_1 [simp]:
-  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
-  by (cases a rule: parity_cases) simp_all
-
-lemma not_mod_2_eq_1_eq_0 [simp]:
-  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
-  by (cases a rule: parity_cases) simp_all
+subsection \<open>Instance for @{typ nat}\<close>
 
-subclass semiring_parity
-proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
-  show "1 mod 2 = 1"
-    by (fact one_mod_two_eq_one)
-next
-  fix a b
-  assume "a mod 2 = 1"
-  moreover assume "b mod 2 = 1"
-  ultimately show "(a + b) mod 2 = 0"
-    using mod_add_eq [of a 2 b] by simp
-next
-  fix a b
-  assume "(a * b) mod 2 = 0"
-  then have "(a mod 2) * (b mod 2) mod 2 = 0"
-    by (simp add: mod_mult_eq)
-  then have "(a mod 2) * (b mod 2) = 0"
-    by (cases "a mod 2 = 0") simp_all
-  then show "a mod 2 = 0 \<or> b mod 2 = 0"
-    by (rule divisors_zero)
-next
-  fix a
-  assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1"
-    using div_mult_mod_eq [of a 2] by simp
-  then show "\<exists>b. a = b + 1" ..
-qed
+instance nat :: semiring_parity
+  by standard (simp_all add: dvd_eq_mod_eq_0)
 
-lemma even_iff_mod_2_eq_zero:
-  "even a \<longleftrightarrow> a mod 2 = 0"
-  by (fact dvd_eq_mod_eq_0)
-
-lemma odd_iff_mod_2_eq_one:
-  "odd a \<longleftrightarrow> a mod 2 = 1"
-  by (simp add: even_iff_mod_2_eq_zero)
-
-lemma even_succ_div_two [simp]:
-  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
-  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
-  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
-  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
-
-lemma even_two_times_div_two:
-  "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ [simp]:
-  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
- 
-end
-
-
-subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
-
-lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
+lemma even_Suc_Suc_iff [simp]:
+  "even (Suc (Suc n)) \<longleftrightarrow> even n"
   using dvd_add_triv_right_iff [of 2 n] by simp
 
-lemma even_Suc [simp]: "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
-  by (induct n) auto
+lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
+  using even_plus_one_iff [of n] by simp
 
-lemma even_diff_nat [simp]: "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
-  for m n :: nat
+lemma even_diff_nat [simp]:
+  "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
 proof (cases "n \<le> m")
   case True
   then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
-  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
-  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
+  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
+  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
   then show ?thesis by auto
 next
   case False
   then show ?thesis by simp
 qed
 
-instance nat :: semiring_parity
-proof
-  show "\<not> 2 dvd (1 :: nat)"
-    by (rule notI, erule dvdE) simp
-next
-  fix m n :: nat
-  assume "\<not> 2 dvd m"
-  moreover assume "\<not> 2 dvd n"
-  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
-    by simp
-  then have "2 dvd (Suc m + Suc n)"
-    by (blast intro: dvd_add)
-  also have "Suc m + Suc n = m + n + 2"
-    by simp
-  finally show "2 dvd (m + n)"
-    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
-next
-  fix m n :: nat
-  assume *: "2 dvd (m * n)"
-  show "2 dvd m \<or> 2 dvd n"
-  proof (rule disjCI)
-    assume "\<not> 2 dvd n"
-    then have "2 dvd (Suc n)" by simp
-    then obtain r where "Suc n = 2 * r" ..
-    moreover from * obtain s where "m * n = 2 * s" ..
-    then have "2 * s + m = m * Suc n" by simp
-    ultimately have " 2 * s + m = 2 * (m * r)"
-      by (simp add: algebra_simps)
-    then have "m = 2 * (m * r - s)" by simp
-    then show "2 dvd m" ..
-  qed
-next
-  fix n :: nat
-  assume "\<not> 2 dvd n"
-  then show "\<exists>m. n = m + 1"
-    by (cases n) simp_all
-qed
-
-lemma odd_pos: "odd n \<Longrightarrow> 0 < n"
-  for n :: nat
+lemma odd_pos:
+  "odd n \<Longrightarrow> 0 < n" for n :: nat
   by (auto elim: oddE)
 
-lemma Suc_double_not_eq_double: "Suc (2 * m) \<noteq> 2 * n"
-  for m n :: nat
+lemma Suc_double_not_eq_double:
+  "Suc (2 * m) \<noteq> 2 * n"
 proof
   assume "Suc (2 * m) = 2 * n"
   moreover have "odd (Suc (2 * m))" and "even (2 * n)"
@@ -260,52 +308,58 @@
   ultimately show False by simp
 qed
 
-lemma double_not_eq_Suc_double: "2 * m \<noteq> Suc (2 * n)"
-  for m n :: nat
+lemma double_not_eq_Suc_double:
+  "2 * m \<noteq> Suc (2 * n)"
   using Suc_double_not_eq_double [of n m] by simp
 
-lemma even_diff_iff [simp]: "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
-  for k l :: int
-  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+  by (auto elim: oddE)
 
-lemma even_abs_add_iff [simp]: "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
-  for k l :: int
-  by (cases "k \<ge> 0") (simp_all add: ac_simps)
+lemma even_Suc_div_two [simp]:
+  "even n \<Longrightarrow> Suc n div 2 = n div 2"
+  using even_succ_div_two [of n] by simp
 
-lemma even_add_abs_iff [simp]: "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
-  for k l :: int
-  using even_abs_add_iff [of l k] by (simp add: ac_simps)
+lemma odd_Suc_div_two [simp]:
+  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
+  using odd_succ_div_two [of n] by simp
 
-instance int :: ring_parity
-proof
-  show "\<not> 2 dvd (1 :: int)"
-    by (simp add: dvd_int_unfold_dvd_nat)
-next
-  fix k l :: int
-  assume "\<not> 2 dvd k"
-  moreover assume "\<not> 2 dvd l"
-  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
-    by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
-  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
-    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
-  then show "2 dvd (k + l)"
+lemma odd_two_times_div_two_nat [simp]:
+  assumes "odd n"
+  shows "2 * (n div 2) = n - (1 :: nat)"
+proof -
+  from assms have "2 * (n div 2) + 1 = n"
+    by (rule odd_two_times_div_two_succ)
+  then have "Suc (2 * (n div 2)) - 1 = n - 1"
     by simp
-next
-  fix k l :: int
-  assume "2 dvd (k * l)"
-  then show "2 dvd k \<or> 2 dvd l"
-    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
-next
-  fix k :: int
-  have "k = (k - 1) + 1" by simp
-  then show "\<exists>l. k = l + 1" ..
+  then show ?thesis
+    by simp
 qed
 
-lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
-  by (simp add: dvd_int_iff)
-
-lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
-  by (simp add: even_int_iff [symmetric])
+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
+    next
+      case False
+      with hyp odd [of "n div 2"] show ?thesis
+        by simp
+    qed
+  qed
+qed
 
 
 subsection \<open>Parity and powers\<close>
@@ -319,6 +373,10 @@
 lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
   by (auto elim: oddE)
 
+lemma uminus_power_if:
+  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
+  by auto
+
 lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
   by simp
 
@@ -396,9 +454,6 @@
   qed
 qed
 
-lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
-  by auto
-
 text \<open>Simplify, when the exponent is a numeral\<close>
 
 lemma zero_le_power_eq_numeral [simp]:
@@ -428,9 +483,4 @@
 
 end
 
-
-subsubsection \<open>Tool setup\<close>
-
-declare transfer_morphism_int_nat [transfer add return: even_int_iff]
-
 end
diff -r a24cde9588bb -r 93c6632ddf44 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -11,7 +11,7 @@
 
 subsection \<open>Truncating bit representations of numeric types\<close>
 
-class semiring_bits = unique_euclidean_semiring_parity +
+class semiring_bits = semiring_parity +
   assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
 begin
 
@@ -27,28 +27,16 @@
   by (simp add: bitrunc_eq_mod)
 
 lemma bitrunc_Suc [simp]:
-  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
+  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + of_bool (odd a)"
 proof -
-  define b and c
-    where "b = a div 2" and "c = a mod 2"
-  then have a: "a = b * 2 + c" 
-    and "c = 0 \<or> c = 1"
-    by (simp_all add: div_mult_mod_eq parity)
-  from \<open>c = 0 \<or> c = 1\<close>
-  have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
-  proof
-    assume "c = 0"
-    moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
-      by (simp add: mod_mult_mult1)
-    ultimately show ?thesis
-      by (simp add: bitrunc_eq_mod ac_simps)
-  next
-    assume "c = 1"
-    with semiring_bits [of b "2 ^ n"] show ?thesis
-      by (simp add: bitrunc_eq_mod ac_simps)
-  qed
-  with a show ?thesis
-    by (simp add: b_def c_def)
+  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
+    if "odd a"
+    using that semiring_bits [of "a div 2" "2 ^ n"]
+      by (simp add: algebra_simps odd_iff_mod_2_eq_one mult_mod_right)
+  also have "\<dots> = a mod (2 * 2 ^ n)"
+    by (simp only: div_mult_mod_eq)
+  finally show ?thesis
+    by (simp add: bitrunc_eq_mod algebra_simps mult_mod_right)
 qed
 
 lemma bitrunc_of_0 [simp]:
@@ -57,11 +45,11 @@
 
 lemma bitrunc_plus:
   "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
-  by (simp add: bitrunc_eq_mod mod_add_eq)
+  by (simp add: bitrunc_eq_mod mod_simps)
 
 lemma bitrunc_of_1_eq_0_iff [simp]:
   "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
-  by (induct n) simp_all
+  by (simp add: bitrunc_eq_mod)
 
 end
 
@@ -113,7 +101,7 @@
 
 lemma signed_bitrunc_Suc [simp]:
   "signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
-  using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
+  by (simp add: odd_iff_mod_2_eq_one signed_bitrunc_eq_bitrunc algebra_simps)
 
 lemma signed_bitrunc_of_0 [simp]:
   "signed_bitrunc n 0 = 0"