diff --git a/src/HOL/Euclidean_Division.thy b/src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy
+++ b/src/HOL/Euclidean_Division.thy
@@ -1,1981 +1,1981 @@
 (*  Title:      HOL/Euclidean_Division.thy
     Author:     Manuel Eberl, TU Muenchen
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 section \<open>Division in euclidean (semi)rings\<close>
 
 theory Euclidean_Division
   imports Int Lattices_Big
 begin
 
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
 class euclidean_semiring = semidom_modulo + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   assumes size_0 [simp]: "euclidean_size 0 = 0"
   assumes mod_size_less: 
     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
   assumes size_mult_mono:
     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
 begin
 
 lemma euclidean_size_eq_0_iff [simp]:
   "euclidean_size b = 0 \<longleftrightarrow> b = 0"
 proof
   assume "b = 0"
   then show "euclidean_size b = 0"
     by simp
 next
   assume "euclidean_size b = 0"
   show "b = 0"
   proof (rule ccontr)
     assume "b \<noteq> 0"
     with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
     with \<open>euclidean_size b = 0\<close> show False
       by simp
   qed
 qed
 
 lemma euclidean_size_greater_0_iff [simp]:
   "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0"
   using euclidean_size_eq_0_iff [symmetric, of b] by safe simp
 
 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   by (subst mult.commute) (rule size_mult_mono)
 
 lemma dvd_euclidean_size_eq_imp_dvd:
   assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
     and "b dvd a" 
   shows "a dvd b"
 proof (rule ccontr)
   assume "\<not> a dvd b"
   hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
   then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
   then obtain c where "b mod a = b * c" unfolding dvd_def by blast
     with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
     using size_mult_mono by force
   moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
   have "euclidean_size (b mod a) < euclidean_size a"
     using mod_size_less by blast
   ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
     by simp
 qed
 
 lemma euclidean_size_times_unit:
   assumes "is_unit a"
   shows   "euclidean_size (a * b) = euclidean_size b"
 proof (rule antisym)
   from assms have [simp]: "a \<noteq> 0" by auto
   thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
   from assms have "is_unit (1 div a)" by simp
   hence "1 div a \<noteq> 0" by (intro notI) simp_all
   hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
     by (rule size_mult_mono')
   also from assms have "(1 div a) * (a * b) = b"
     by (simp add: algebra_simps unit_div_mult_swap)
   finally show "euclidean_size (a * b) \<le> euclidean_size b" .
 qed
 
 lemma euclidean_size_unit:
   "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
   using euclidean_size_times_unit [of a 1] by simp
 
 lemma unit_iff_euclidean_size: 
   "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
 proof safe
   assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
   show "is_unit a"
     by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
 qed (auto intro: euclidean_size_unit)
 
 lemma euclidean_size_times_nonunit:
   assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
   shows   "euclidean_size b < euclidean_size (a * b)"
 proof (rule ccontr)
   assume "\<not>euclidean_size b < euclidean_size (a * b)"
   with size_mult_mono'[OF assms(1), of b] 
     have eq: "euclidean_size (a * b) = euclidean_size b" by simp
   have "a * b dvd b"
     by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
   hence "a * b dvd 1 * b" by simp
   with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   with assms(3) show False by contradiction
 qed
 
 lemma dvd_imp_size_le:
   assumes "a dvd b" "b \<noteq> 0" 
   shows   "euclidean_size a \<le> euclidean_size b"
   using assms by (auto elim!: dvdE simp: size_mult_mono)
 
 lemma dvd_proper_imp_size_less:
   assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   shows   "euclidean_size a < euclidean_size b"
 proof -
   from assms(1) obtain c where "b = a * c" by (erule dvdE)
   hence z: "b = c * a" by (simp add: mult.commute)
   from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   with z assms show ?thesis
     by (auto intro!: euclidean_size_times_nonunit)
 qed
 
 lemma unit_imp_mod_eq_0:
   "a mod b = 0" if "is_unit b"
   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
 
 lemma mod_eq_self_iff_div_eq_0:
   "a mod b = a \<longleftrightarrow> a div b = 0" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   with div_mult_mod_eq [of a b] show ?Q
     by auto
 next
   assume ?Q
   with div_mult_mod_eq [of a b] show ?P
     by simp
 qed
 
 lemma coprime_mod_left_iff [simp]:
   "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
   by (rule; rule coprimeI)
     (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
 
 lemma coprime_mod_right_iff [simp]:
   "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
   using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
 
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring
 begin
 
 lemma dvd_diff_commute [ac_simps]:
   "a dvd c - b \<longleftrightarrow> a dvd b - c"
 proof -
   have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
     by (subst dvd_mult_unit_iff) simp_all
   then show ?thesis
     by simp
 qed
  
 end
 
 
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
 
 class euclidean_semiring_cancel = euclidean_semiring +
   assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
   and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
 lemma div_mult_self2 [simp]:
   assumes "b \<noteq> 0"
   shows "(a + b * c) div b = c + a div b"
   using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
 
 lemma div_mult_self3 [simp]:
   assumes "b \<noteq> 0"
   shows "(c * b + a) div b = c + a div b"
   using assms by (simp add: add.commute)
 
 lemma div_mult_self4 [simp]:
   assumes "b \<noteq> 0"
   shows "(b * c + a) div b = c + a div b"
   using assms by (simp add: add.commute)
 
 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
 proof (cases "b = 0")
   case True then show ?thesis by simp
 next
   case False
   have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
     by (simp add: div_mult_mod_eq)
   also from False div_mult_self1 [of b a c] have
     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
       by (simp add: algebra_simps)
   finally have "a = a div b * b + (a + c * b) mod b"
     by (simp add: add.commute [of a] add.assoc distrib_right)
   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
     by (simp add: div_mult_mod_eq)
   then show ?thesis by simp
 qed
 
 lemma mod_mult_self2 [simp]:
   "(a + b * c) mod b = a mod b"
   by (simp add: mult.commute [of b])
 
 lemma mod_mult_self3 [simp]:
   "(c * b + a) mod b = a mod b"
   by (simp add: add.commute)
 
 lemma mod_mult_self4 [simp]:
   "(b * c + a) mod b = a mod b"
   by (simp add: add.commute)
 
 lemma mod_mult_self1_is_0 [simp]:
   "b * a mod b = 0"
   using mod_mult_self2 [of 0 b a] by simp
 
 lemma mod_mult_self2_is_0 [simp]:
   "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
 lemma div_add_self1:
   assumes "b \<noteq> 0"
   shows "(b + a) div b = a div b + 1"
   using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
 
 lemma div_add_self2:
   assumes "b \<noteq> 0"
   shows "(a + b) div b = a div b + 1"
   using assms div_add_self1 [of b a] by (simp add: add.commute)
 
 lemma mod_add_self1 [simp]:
   "(b + a) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
 
 lemma mod_add_self2 [simp]:
   "(a + b) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by simp
 
 lemma mod_div_trivial [simp]:
   "a mod b div b = 0"
 proof (cases "b = 0")
   assume "b = 0"
   thus ?thesis by simp
 next
   assume "b \<noteq> 0"
   hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
     by (rule div_mult_self1 [symmetric])
   also have "\<dots> = a div b"
     by (simp only: mod_div_mult_eq)
   also have "\<dots> = a div b + 0"
     by simp
   finally show ?thesis
     by (rule add_left_imp_eq)
 qed
 
 lemma mod_mod_trivial [simp]:
   "a mod b mod b = a mod b"
 proof -
   have "a mod b mod b = (a mod b + a div b * b) mod b"
     by (simp only: mod_mult_self1)
   also have "\<dots> = a mod b"
     by (simp only: mod_div_mult_eq)
   finally show ?thesis .
 qed
 
 lemma mod_mod_cancel:
   assumes "c dvd b"
   shows "a mod b mod c = a mod c"
 proof -
   from \<open>c dvd b\<close> obtain k where "b = c * k"
     by (rule dvdE)
   have "a mod b mod c = a mod (c * k) mod c"
     by (simp only: \<open>b = c * k\<close>)
   also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
     by (simp only: mod_mult_self1)
   also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
     by (simp only: ac_simps)
   also have "\<dots> = a mod c"
     by (simp only: div_mult_mod_eq)
   finally show ?thesis .
 qed
 
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   by (drule div_mult_mult1) (simp add: mult.commute)
 
 lemma div_mult_mult1_if [simp]:
   "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   by simp_all
 
 lemma mod_mult_mult1:
   "(c * a) mod (c * b) = c * (a mod b)"
 proof (cases "c = 0")
   case True then show ?thesis by simp
 next
   case False
   from div_mult_mod_eq
   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
     = c * a + c * (a mod b)" by (simp add: algebra_simps)
   with div_mult_mod_eq show ?thesis by simp
 qed
 
 lemma mod_mult_mult2:
   "(a * c) mod (b * c) = (a mod b) * c"
   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
 
 lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   by (fact mod_mult_mult2 [symmetric])
 
 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   by (fact mod_mult_mult1 [symmetric])
 
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
 lemma div_plus_div_distrib_dvd_left:
   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   by (cases "c = 0") (auto elim: dvdE)
 
 lemma div_plus_div_distrib_dvd_right:
   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   using div_plus_div_distrib_dvd_left [of c b a]
   by (simp add: ac_simps)
 
 named_theorems mod_simps
 
 text \<open>Addition respects modular equivalence.\<close>
 
 lemma mod_add_left_eq [mod_simps]:
   "(a mod c + b) mod c = (a + b) mod c"
 proof -
   have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
     by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a mod c + b + a div c * c) mod c"
     by (simp only: ac_simps)
   also have "\<dots> = (a mod c + b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis
     by (rule sym)
 qed
 
 lemma mod_add_right_eq [mod_simps]:
   "(a + b mod c) mod c = (a + b) mod c"
   using mod_add_left_eq [of b c a] by (simp add: ac_simps)
 
 lemma mod_add_eq:
   "(a mod c + b mod c) mod c = (a + b) mod c"
   by (simp add: mod_add_left_eq mod_add_right_eq)
 
 lemma mod_sum_eq [mod_simps]:
   "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
 proof (induct A rule: infinite_finite_induct)
   case (insert i A)
   then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
     = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
     by simp
   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
     by (simp add: mod_simps)
   also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
     by (simp add: insert.hyps)
   finally show ?case
     by (simp add: insert.hyps mod_simps)
 qed simp_all
 
 lemma mod_add_cong:
   assumes "a mod c = a' mod c"
   assumes "b mod c = b' mod c"
   shows "(a + b) mod c = (a' + b') mod c"
 proof -
   have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
     unfolding assms ..
   then show ?thesis
     by (simp add: mod_add_eq)
 qed
 
 text \<open>Multiplication respects modular equivalence.\<close>
 
 lemma mod_mult_left_eq [mod_simps]:
   "((a mod c) * b) mod c = (a * b) mod c"
 proof -
   have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
     by (simp only: div_mult_mod_eq)
   also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
     by (simp only: algebra_simps)
   also have "\<dots> = (a mod c * b) mod c"
     by (rule mod_mult_self1)
   finally show ?thesis
     by (rule sym)
 qed
 
 lemma mod_mult_right_eq [mod_simps]:
   "(a * (b mod c)) mod c = (a * b) mod c"
   using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
 
 lemma mod_mult_eq:
   "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   by (simp add: mod_mult_left_eq mod_mult_right_eq)
 
 lemma mod_prod_eq [mod_simps]:
   "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
 proof (induct A rule: infinite_finite_induct)
   case (insert i A)
   then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
     = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
     by simp
   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
     by (simp add: mod_simps)
   also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
     by (simp add: insert.hyps)
   finally show ?case
     by (simp add: insert.hyps mod_simps)
 qed simp_all
 
 lemma mod_mult_cong:
   assumes "a mod c = a' mod c"
   assumes "b mod c = b' mod c"
   shows "(a * b) mod c = (a' * b') mod c"
 proof -
   have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
     unfolding assms ..
   then show ?thesis
     by (simp add: mod_mult_eq)
 qed
 
 text \<open>Exponentiation respects modular equivalence.\<close>
 
 lemma power_mod [mod_simps]: 
   "((a mod b) ^ n) mod b = (a ^ n) mod b"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc n)
   have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
     by (simp add: mod_mult_right_eq)
   with Suc show ?case
     by (simp add: mod_mult_left_eq mod_mult_right_eq)
 qed
 
 end
 
 
 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
 begin
 
 subclass idom_divide ..
 
 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   using div_mult_mult1 [of "- 1" a b] by simp
 
 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   using mod_mult_mult1 [of "- 1" a b] by simp
 
 lemma div_minus_right: "a div (- b) = (- a) div b"
   using div_minus_minus [of "- a" b] by simp
 
 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   using mod_minus_minus [of "- a" b] by simp
 
 lemma div_minus1_right [simp]: "a div (- 1) = - a"
   using div_minus_right [of a 1] by simp
 
 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   using mod_minus_right [of a 1] by simp
 
 text \<open>Negation respects modular equivalence.\<close>
 
 lemma mod_minus_eq [mod_simps]:
   "(- (a mod b)) mod b = (- a) mod b"
 proof -
   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
     by (simp only: div_mult_mod_eq)
   also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
     by (simp add: ac_simps)
   also have "\<dots> = (- (a mod b)) mod b"
     by (rule mod_mult_self1)
   finally show ?thesis
     by (rule sym)
 qed
 
 lemma mod_minus_cong:
   assumes "a mod b = a' mod b"
   shows "(- a) mod b = (- a') mod b"
 proof -
   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
     unfolding assms ..
   then show ?thesis
     by (simp add: mod_minus_eq)
 qed
 
 text \<open>Subtraction respects modular equivalence.\<close>
 
 lemma mod_diff_left_eq [mod_simps]:
   "(a mod c - b) mod c = (a - b) mod c"
   using mod_add_cong [of a c "a mod c" "- b" "- b"]
   by simp
 
 lemma mod_diff_right_eq [mod_simps]:
   "(a - b mod c) mod c = (a - b) mod c"
   using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   by simp
 
 lemma mod_diff_eq:
   "(a mod c - b mod c) mod c = (a - b) mod c"
   using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   by simp
 
 lemma mod_diff_cong:
   assumes "a mod c = a' mod c"
   assumes "b mod c = b' mod c"
   shows "(a - b) mod c = (a' - b') mod c"
   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   by simp
 
 lemma minus_mod_self2 [simp]:
   "(a - b) mod b = a mod b"
   using mod_diff_right_eq [of a b b]
   by (simp add: mod_diff_right_eq)
 
 lemma minus_mod_self1 [simp]:
   "(b - a) mod b = - a mod b"
   using mod_add_self2 [of "- a" b] by simp
 
 lemma mod_eq_dvd_iff:
   "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   then have "(a mod c - b mod c) mod c = 0"
     by simp
   then show ?Q
     by (simp add: dvd_eq_mod_eq_0 mod_simps)
 next
   assume ?Q
   then obtain d where d: "a - b = c * d" ..
   then have "a = c * d + b"
     by (simp add: algebra_simps)
   then show ?P by simp
 qed
 
 lemma mod_eqE:
   assumes "a mod c = b mod c"
   obtains d where "b = a + c * d"
 proof -
   from assms have "c dvd a - b"
     by (simp add: mod_eq_dvd_iff)
   then obtain d where "a - b = c * d" ..
   then have "b = a + c * - d"
     by (simp add: algebra_simps)
   with that show thesis .
 qed
 
 lemma invertible_coprime:
   "coprime a c" if "a * b mod c = 1"
   by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
 
 end
 
   
 subsection \<open>Uniquely determined division\<close>
   
 class unique_euclidean_semiring = euclidean_semiring + 
   assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
   fixes division_segment :: "'a \<Rightarrow> 'a"
   assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
     and division_segment_mult:
     "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
     and division_segment_mod:
     "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
   assumes div_bounded:
     "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
     \<Longrightarrow> euclidean_size r < euclidean_size b
     \<Longrightarrow> (q * b + r) div b = q"
 begin
 
 lemma division_segment_not_0 [simp]:
   "division_segment a \<noteq> 0"
   using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
 
 lemma divmod_cases [case_names divides remainder by0]:
   obtains 
     (divides) q where "b \<noteq> 0"
       and "a div b = q"
       and "a mod b = 0"
       and "a = q * b"
   | (remainder) q r where "b \<noteq> 0"
       and "division_segment r = division_segment b"
       and "euclidean_size r < euclidean_size b"
       and "r \<noteq> 0"
       and "a div b = q"
       and "a mod b = r"
       and "a = q * b + r"
   | (by0) "b = 0"
 proof (cases "b = 0")
   case True
   then show thesis
   by (rule by0)
 next
   case False
   show thesis
   proof (cases "b dvd a")
     case True
     then obtain q where "a = b * q" ..
     with \<open>b \<noteq> 0\<close> divides
     show thesis
       by (simp add: ac_simps)
   next
     case False
     then have "a mod b \<noteq> 0"
       by (simp add: mod_eq_0_iff_dvd)
     moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
       by (rule division_segment_mod)
     moreover have "euclidean_size (a mod b) < euclidean_size b"
       using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
     moreover have "a = a div b * b + a mod b"
       by (simp add: div_mult_mod_eq)
     ultimately show thesis
       using \<open>b \<noteq> 0\<close> by (blast intro!: remainder)
   qed
 qed
 
 lemma div_eqI:
   "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
     "euclidean_size r < euclidean_size b" "q * b + r = a"
 proof -
   from that have "(q * b + r) div b = q"
     by (auto intro: div_bounded)
   with that show ?thesis
     by simp
 qed
 
 lemma mod_eqI:
   "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
     "euclidean_size r < euclidean_size b" "q * b + r = a" 
 proof -
   from that have "a div b = q"
     by (rule div_eqI)
   moreover have "a div b * b + a mod b = a"
     by (fact div_mult_mod_eq)
   ultimately have "a div b * b + a mod b = a div b * b + r"
     using \<open>q * b + r = a\<close> by simp
   then show ?thesis
     by simp
 qed
 
 subclass euclidean_semiring_cancel
 proof
   show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   proof (cases a b rule: divmod_cases)
     case by0
     with \<open>b \<noteq> 0\<close> show ?thesis
       by simp
   next
     case (divides q)
     then show ?thesis
       by (simp add: ac_simps)
   next
     case (remainder q r)
     then show ?thesis
       by (auto intro: div_eqI simp add: algebra_simps)
   qed
 next
   show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   proof (cases a b rule: divmod_cases)
     case by0
     then show ?thesis
       by simp
   next
     case (divides q)
     with \<open>c \<noteq> 0\<close> show ?thesis
       by (simp add: mult.left_commute [of c])
   next
     case (remainder q r)
     from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
       by simp
     from remainder \<open>c \<noteq> 0\<close>
     have "division_segment (r * c) = division_segment (b * c)"
       and "euclidean_size (r * c) < euclidean_size (b * c)"
       by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
     with remainder show ?thesis
       by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
         (use \<open>b * c \<noteq> 0\<close> in simp)
   qed
 qed
 
 lemma div_mult1_eq:
   "(a * b) div c = a * (b div c) + a * (b mod c) div c"
 proof (cases "a * (b mod c)" c rule: divmod_cases)
   case (divides q)
   have "a * b = a * (b div c * c + b mod c)"
     by (simp add: div_mult_mod_eq)
   also have "\<dots> = (a * (b div c) + q) * c"
     using divides by (simp add: algebra_simps)
   finally have "(a * b) div c = \<dots> div c"
     by simp
   with divides show ?thesis
     by simp
 next
   case (remainder q r)
   from remainder(1-3) show ?thesis
   proof (rule div_eqI)
     have "a * b = a * (b div c * c + b mod c)"
       by (simp add: div_mult_mod_eq)
     also have "\<dots> = a * c * (b div c) + q * c + r"
       using remainder by (simp add: algebra_simps)
     finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
       using remainder(5-7) by (simp add: algebra_simps)
   qed
 next
   case by0
   then show ?thesis
     by simp
 qed
 
 lemma div_add1_eq:
   "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
 proof (cases "a mod c + b mod c" c rule: divmod_cases)
   case (divides q)
   have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
     using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
   also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
     by (simp add: algebra_simps)
   also have "\<dots> = (a div c + b div c + q) * c"
     using divides by (simp add: algebra_simps)
   finally have "(a + b) div c = (a div c + b div c + q) * c div c"
     by simp
   with divides show ?thesis
     by simp
 next
   case (remainder q r)
   from remainder(1-3) show ?thesis
   proof (rule div_eqI)
     have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
         (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
       by (simp add: algebra_simps)
     also have "\<dots> = a + b + (a mod c + b mod c)"
       by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
     finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
       using remainder by simp
   qed
 next
   case by0
   then show ?thesis
     by simp
 qed
 
 lemma div_eq_0_iff:
   "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
   if "division_segment a = division_segment b"
 proof
   assume ?P
   with that show "a div b = 0"
     by (cases "b = 0") (auto intro: div_eqI)
 next
   assume "a div b = 0"
   then have "a mod b = a"
     using div_mult_mod_eq [of a b] by simp
   with mod_size_less [of b a] show ?P
     by auto
 qed
 
 end
 
 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
 begin
   
 subclass euclidean_ring_cancel ..
 
 end
 
 
 subsection \<open>Euclidean division on \<^typ>\<open>nat\<close>\<close>
 
 instantiation nat :: normalization_semidom
 begin
 
 definition normalize_nat :: "nat \<Rightarrow> nat"
   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
 
 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
 
 lemma unit_factor_simps [simp]:
   "unit_factor 0 = (0::nat)"
   "unit_factor (Suc n) = 1"
   by (simp_all add: unit_factor_nat_def)
 
 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
 
 instance
   by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
 
 end
 
 lemma coprime_Suc_0_left [simp]:
   "coprime (Suc 0) n"
   using coprime_1_left [of n] by simp
 
 lemma coprime_Suc_0_right [simp]:
   "coprime n (Suc 0)"
   using coprime_1_right [of n] by simp
 
 lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   for a b :: nat
   by (drule coprime_common_divisor [of _ _ x]) simp_all
 
 instantiation nat :: unique_euclidean_semiring
 begin
 
 definition euclidean_size_nat :: "nat \<Rightarrow> nat"
   where [simp]: "euclidean_size_nat = id"
 
 definition division_segment_nat :: "nat \<Rightarrow> nat"
   where [simp]: "division_segment_nat n = 1"
 
 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   where "m mod n = m - (m div n * (n::nat))"
 
 instance proof
   fix m n :: nat
   have ex: "\<exists>k. k * n \<le> l" for l :: nat
     by (rule exI [of _ 0]) simp
   have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
   proof -
     from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
       by (cases n) auto
     then show ?thesis
       by (rule finite_subset) simp
   qed
   have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
   proof (cases "n = 0")
     case True
     moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
       by auto
     ultimately show ?thesis
       by simp
   next
     case False
     with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
       by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
     also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
       by (auto simp add: ac_simps elim!: dvdE)
     finally show ?thesis
       using False by (simp add: divide_nat_def ac_simps)
   qed
   have less_eq: "m div n * n \<le> m"
     by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
   then show "m div n * n + m mod n = m"
     by (simp add: modulo_nat_def)
   assume "n \<noteq> 0" 
   show "euclidean_size (m mod n) < euclidean_size n"
   proof -
     have "m < Suc (m div n) * n"
     proof (rule ccontr)
       assume "\<not> m < Suc (m div n) * n"
       then have "Suc (m div n) * n \<le> m"
         by (simp add: not_less)
       moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
         by (simp add: divide_nat_def)
       with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
         by auto
       ultimately have "Suc (m div n) < Suc (m div n)"
         by blast
       then show False
         by simp
     qed
     with \<open>n \<noteq> 0\<close> show ?thesis
       by (simp add: modulo_nat_def)
   qed
   show "euclidean_size m \<le> euclidean_size (m * n)"
     using \<open>n \<noteq> 0\<close> by (cases n) simp_all
   fix q r :: nat
   show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
   proof -
     from that have "r < n"
       by simp
     have "k \<le> q" if "k * n \<le> q * n + r" for k
     proof (rule ccontr)
       assume "\<not> k \<le> q"
       then have "q < k"
         by simp
       then obtain l where "k = Suc (q + l)"
         by (auto simp add: less_iff_Suc_add)
       with \<open>r < n\<close> that show False
         by (simp add: algebra_simps)
     qed
     with \<open>n \<noteq> 0\<close> ex fin show ?thesis
       by (auto simp add: divide_nat_def Max_eq_iff)
   qed
 qed simp_all
 
 end
 
 text \<open>Tool support\<close>
 
 ML \<open>
 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
 (
   val div_name = \<^const_name>\<open>divide\<close>;
   val mod_name = \<^const_name>\<open>modulo\<close>;
   val mk_binop = HOLogic.mk_binop;
   val dest_plus = HOLogic.dest_bin \<^const_name>\<open>Groups.plus\<close> HOLogic.natT;
   val mk_sum = Arith_Data.mk_sum;
   fun dest_sum tm =
     if HOLogic.is_zero tm then []
     else
       (case try HOLogic.dest_Suc tm of
         SOME t => HOLogic.Suc_zero :: dest_sum t
       | NONE =>
           (case try dest_plus tm of
             SOME (t, u) => dest_sum t @ dest_sum u
           | NONE => [tm]));
 
   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
 
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
 )
 \<close>
 
 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   \<open>K Cancel_Div_Mod_Nat.proc\<close>
 
 lemma div_nat_eqI:
   "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
   by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
 
 lemma mod_nat_eqI:
   "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
   by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
 
 lemma div_mult_self_is_m [simp]:
   "m * n div n = m" if "n > 0" for m n :: nat
   using that by simp
 
 lemma div_mult_self1_is_m [simp]:
   "n * m div n = m" if "n > 0" for m n :: nat
   using that by simp
 
 lemma mod_less_divisor [simp]:
   "m mod n < n" if "n > 0" for m n :: nat
   using mod_size_less [of n m] that by simp
 
 lemma mod_le_divisor [simp]:
   "m mod n \<le> n" if "n > 0" for m n :: nat
   using that by (auto simp add: le_less)
 
 lemma div_times_less_eq_dividend [simp]:
   "m div n * n \<le> m" for m n :: nat
   by (simp add: minus_mod_eq_div_mult [symmetric])
 
 lemma times_div_less_eq_dividend [simp]:
   "n * (m div n) \<le> m" for m n :: nat
   using div_times_less_eq_dividend [of m n]
   by (simp add: ac_simps)
 
 lemma dividend_less_div_times:
   "m < n + (m div n) * n" if "0 < n" for m n :: nat
 proof -
   from that have "m mod n < n"
     by simp
   then show ?thesis
     by (simp add: minus_mod_eq_div_mult [symmetric])
 qed
 
 lemma dividend_less_times_div:
   "m < n + n * (m div n)" if "0 < n" for m n :: nat
   using dividend_less_div_times [of n m] that
   by (simp add: ac_simps)
 
 lemma mod_Suc_le_divisor [simp]:
   "m mod Suc n \<le> n"
   using mod_less_divisor [of "Suc n" m] by arith
 
 lemma mod_less_eq_dividend [simp]:
   "m mod n \<le> m" for m n :: nat
 proof (rule add_leD2)
   from div_mult_mod_eq have "m div n * n + m mod n = m" .
   then show "m div n * n + m mod n \<le> m" by auto
 qed
 
 lemma
   div_less [simp]: "m div n = 0"
   and mod_less [simp]: "m mod n = m"
   if "m < n" for m n :: nat
   using that by (auto intro: div_eqI mod_eqI) 
 
 lemma le_div_geq:
   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
 proof -
   from \<open>n \<le> m\<close> obtain q where "m = n + q"
     by (auto simp add: le_iff_add)
   with \<open>0 < n\<close> show ?thesis
     by (simp add: div_add_self1)
 qed
 
 lemma le_mod_geq:
   "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
 proof -
   from \<open>n \<le> m\<close> obtain q where "m = n + q"
     by (auto simp add: le_iff_add)
   then show ?thesis
     by simp
 qed
 
 lemma div_if:
   "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
   by (simp add: le_div_geq)
 
 lemma mod_if:
   "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
   by (simp add: le_mod_geq)
 
 lemma div_eq_0_iff:
   "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
   by (simp add: div_eq_0_iff)
 
 lemma div_greater_zero_iff:
   "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
   using div_eq_0_iff [of m n] by auto
 
 lemma mod_greater_zero_iff_not_dvd:
   "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
   by (simp add: dvd_eq_mod_eq_0)
 
 lemma div_by_Suc_0 [simp]:
   "m div Suc 0 = m"
   using div_by_1 [of m] by simp
 
 lemma mod_by_Suc_0 [simp]:
   "m mod Suc 0 = 0"
   using mod_by_1 [of m] by simp
 
 lemma div2_Suc_Suc [simp]:
   "Suc (Suc m) div 2 = Suc (m div 2)"
   by (simp add: numeral_2_eq_2 le_div_geq)
 
 lemma Suc_n_div_2_gt_zero [simp]:
   "0 < Suc n div 2" if "n > 0" for n :: nat
   using that by (cases n) simp_all
 
 lemma div_2_gt_zero [simp]:
   "0 < n div 2" if "Suc 0 < n" for n :: nat
   using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
 
 lemma mod2_Suc_Suc [simp]:
   "Suc (Suc m) mod 2 = m mod 2"
   by (simp add: numeral_2_eq_2 le_mod_geq)
 
 lemma add_self_div_2 [simp]:
   "(m + m) div 2 = m" for m :: nat
   by (simp add: mult_2 [symmetric])
 
 lemma add_self_mod_2 [simp]:
   "(m + m) mod 2 = 0" for m :: nat
   by (simp add: mult_2 [symmetric])
 
 lemma mod2_gr_0 [simp]:
   "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
 proof -
   have "m mod 2 < 2"
     by (rule mod_less_divisor) simp
   then have "m mod 2 = 0 \<or> m mod 2 = 1"
     by arith
   then show ?thesis
     by auto     
 qed
 
 lemma mod_Suc_eq [mod_simps]:
   "Suc (m mod n) mod n = Suc m mod n"
 proof -
   have "(m mod n + 1) mod n = (m + 1) mod n"
     by (simp only: mod_simps)
   then show ?thesis
     by simp
 qed
 
 lemma mod_Suc_Suc_eq [mod_simps]:
   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
 proof -
   have "(m mod n + 2) mod n = (m + 2) mod n"
     by (simp only: mod_simps)
   then show ?thesis
     by simp
 qed
 
 lemma
   Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
   and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
   and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
   and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
   by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
 
 lemma Suc_0_mod_eq [simp]:
   "Suc 0 mod n = of_bool (n \<noteq> Suc 0)"
   by (cases n) simp_all
 
 context
   fixes m n q :: nat
 begin
 
 private lemma eucl_rel_mult2:
   "m mod n + n * (m div n mod q) < n * q"
   if "n > 0" and "q > 0"
 proof -
   from \<open>n > 0\<close> have "m mod n < n"
     by (rule mod_less_divisor)
   from \<open>q > 0\<close> have "m div n mod q < q"
     by (rule mod_less_divisor)
   then obtain s where "q = Suc (m div n mod q + s)"
     by (blast dest: less_imp_Suc_add)
   moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
     using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
   ultimately show ?thesis
     by simp
 qed
 
 lemma div_mult2_eq:
   "m div (n * q) = (m div n) div q"
 proof (cases "n = 0 \<or> q = 0")
   case True
   then show ?thesis
     by auto
 next
   case False
   with eucl_rel_mult2 show ?thesis
     by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
       simp add: algebra_simps add_mult_distrib2 [symmetric])
 qed
 
 lemma mod_mult2_eq:
   "m mod (n * q) = n * (m div n mod q) + m mod n"
 proof (cases "n = 0 \<or> q = 0")
   case True
   then show ?thesis
     by auto
 next
   case False
   with eucl_rel_mult2 show ?thesis
     by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
       simp add: algebra_simps add_mult_distrib2 [symmetric])
 qed
 
 end
 
 lemma div_le_mono:
   "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
 proof -
   from that obtain q where "n = m + q"
     by (auto simp add: le_iff_add)
   then show ?thesis
     by (simp add: div_add1_eq [of m q k])
 qed
 
 text \<open>Antimonotonicity of \<^const>\<open>divide\<close> in second argument\<close>
 
 lemma div_le_mono2:
   "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
 using that proof (induct k arbitrary: m rule: less_induct)
   case (less k)
   show ?case
   proof (cases "n \<le> k")
     case False
     then show ?thesis
       by simp
   next
     case True
     have "(k - n) div n \<le> (k - m) div n"
       using less.prems
       by (blast intro: div_le_mono diff_le_mono2)
     also have "\<dots> \<le> (k - m) div m"
       using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
       by simp
     finally show ?thesis
       using \<open>n \<le> k\<close> less.prems
       by (simp add: le_div_geq)
   qed
 qed
 
 lemma div_le_dividend [simp]:
   "m div n \<le> m" for m n :: nat
   using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
 
 lemma div_less_dividend [simp]:
   "m div n < m" if "1 < n" and "0 < m" for m n :: nat
 using that proof (induct m rule: less_induct)
   case (less m)
   show ?case
   proof (cases "n < m")
     case False
     with less show ?thesis
       by (cases "n = m") simp_all
   next
     case True
     then show ?thesis
       using less.hyps [of "m - n"] less.prems
       by (simp add: le_div_geq)
   qed
 qed
 
 lemma div_eq_dividend_iff:
   "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
 proof
   assume "n = 1"
   then show "m div n = m"
     by simp
 next
   assume P: "m div n = m"
   show "n = 1"
   proof (rule ccontr)
     have "n \<noteq> 0"
       by (rule ccontr) (use that P in auto)
     moreover assume "n \<noteq> 1"
     ultimately have "n > 1"
       by simp
     with that have "m div n < m"
       by simp
     with P show False
       by simp
   qed
 qed
 
 lemma less_mult_imp_div_less:
   "m div n < i" if "m < i * n" for m n i :: nat
 proof -
   from that have "i * n > 0"
     by (cases "i * n = 0") simp_all
   then have "i > 0" and "n > 0"
     by simp_all
   have "m div n * n \<le> m"
     by simp
   then have "m div n * n < i * n"
     using that by (rule le_less_trans)
   with \<open>n > 0\<close> show ?thesis
     by simp
 qed
 
 text \<open>A fact for the mutilated chess board\<close>
 
 lemma mod_Suc:
   "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
 proof (cases "n = 0")
   case True
   then show ?thesis
     by simp
 next
   case False
   have "Suc m mod n = Suc (m mod n) mod n"
     by (simp add: mod_simps)
   also have "\<dots> = ?rhs"
     using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
   finally show ?thesis .
 qed
 
 lemma Suc_times_mod_eq:
   "Suc (m * n) mod m = 1" if "Suc 0 < m"
   using that by (simp add: mod_Suc)
 
 lemma Suc_times_numeral_mod_eq [simp]:
   "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
   by (rule Suc_times_mod_eq) (use that in simp)
 
 lemma Suc_div_le_mono [simp]:
   "m div n \<le> Suc m div n"
   by (simp add: div_le_mono)
 
 text \<open>These lemmas collapse some needless occurrences of Suc:
   at least three Sucs, since two and fewer are rewritten back to Suc again!
   We already have some rules to simplify operands smaller than 3.\<close>
 
 lemma div_Suc_eq_div_add3 [simp]:
   "m div Suc (Suc (Suc n)) = m div (3 + n)"
   by (simp add: Suc3_eq_add_3)
 
 lemma mod_Suc_eq_mod_add3 [simp]:
   "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
   by (simp add: Suc3_eq_add_3)
 
 lemma Suc_div_eq_add3_div:
   "Suc (Suc (Suc m)) div n = (3 + m) div n"
   by (simp add: Suc3_eq_add_3)
 
 lemma Suc_mod_eq_add3_mod:
   "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
   by (simp add: Suc3_eq_add_3)
 
 lemmas Suc_div_eq_add3_div_numeral [simp] =
   Suc_div_eq_add3_div [of _ "numeral v"] for v
 
 lemmas Suc_mod_eq_add3_mod_numeral [simp] =
   Suc_mod_eq_add3_mod [of _ "numeral v"] for v
 
 lemma (in field_char_0) of_nat_div:
   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
 proof -
   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
     unfolding of_nat_add by (cases "n = 0") simp_all
   then show ?thesis
     by simp
 qed
 
 text \<open>An ``induction'' law for modulus arithmetic.\<close>
 
 lemma mod_induct [consumes 3, case_names step]:
   "P m" if "P n" and "n < p" and "m < p"
     and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
 using \<open>m < p\<close> proof (induct m)
   case 0
   show ?case
   proof (rule ccontr)
     assume "\<not> P 0"
     from \<open>n < p\<close> have "0 < p"
       by simp
     from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
       by (blast dest: less_imp_add_positive)
     with \<open>P n\<close> have "P (p - m)"
       by simp
     moreover have "\<not> P (p - m)"
     using \<open>0 < m\<close> proof (induct m)
       case 0
       then show ?case
         by simp
     next
       case (Suc m)
       show ?case
       proof
         assume P: "P (p - Suc m)"
         with \<open>\<not> P 0\<close> have "Suc m < p"
           by (auto intro: ccontr) 
         then have "Suc (p - Suc m) = p - m"
           by arith
         moreover from \<open>0 < p\<close> have "p - Suc m < p"
           by arith
         with P step have "P ((Suc (p - Suc m)) mod p)"
           by blast
         ultimately show False
           using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
       qed
     qed
     ultimately show False
       by blast
   qed
 next
   case (Suc m)
   then have "m < p" and mod: "Suc m mod p = Suc m"
     by simp_all
   from \<open>m < p\<close> have "P m"
     by (rule Suc.hyps)
   with \<open>m < p\<close> have "P (Suc m mod p)"
     by (rule step)
   with mod show ?case
     by simp
 qed
 
 lemma split_div:
   "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
      (is "?P = ?Q") for m n :: nat
 proof (cases "n = 0")
   case True
   then show ?thesis
     by simp
 next
   case False
   show ?thesis
   proof
     assume ?P
     with False show ?Q
       by auto
   next
     assume ?Q
     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
       by simp
     with False show ?P
       by (auto intro: * [of "m mod n"])
   qed
 qed
 
 lemma split_div':
   "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
 proof (cases "n = 0")
   case True
   then show ?thesis
     by simp
 next
   case False
   then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
     by (auto intro: div_nat_eqI dividend_less_times_div)
   then show ?thesis
     by auto
 qed
 
 lemma split_mod:
   "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
      (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
      (is "?P \<longleftrightarrow> ?Q") for m n :: nat
 proof (cases "n = 0")
   case True
   then show ?thesis
     by simp
 next
   case False
   show ?thesis
   proof
     assume ?P
     with False show ?Q
       by auto
   next
     assume ?Q
     with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
       by simp
     with False show ?P
       by (auto intro: * [of _ "m div n"])
   qed
 qed
 
 
 subsection \<open>Euclidean division on \<^typ>\<open>int\<close>\<close>
 
 instantiation int :: normalization_semidom
 begin
 
 definition normalize_int :: "int \<Rightarrow> int"
   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
 
 definition unit_factor_int :: "int \<Rightarrow> int"
   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
 
 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
   where "k div l = (if l = 0 then 0
     else if sgn k = sgn l
       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
       else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
 
 lemma divide_int_unfold:
   "(sgn k * int m) div (sgn l * int n) =
    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
     else if sgn k = sgn l
       then int (m div n)
       else - int (m div n + of_bool (\<not> n dvd m)))"
   by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
     nat_mult_distrib)
 
 instance proof
   fix k :: int show "k div 0 = 0"
   by (simp add: divide_int_def)
 next
   fix k l :: int
   assume "l \<noteq> 0"
   obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   then have "k * l = sgn (s * t) * int (n * m)"
     by (simp add: ac_simps sgn_mult)
   with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
     by (simp only: divide_int_unfold)
       (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
 
 end
 
 lemma coprime_int_iff [simp]:
   "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   show ?Q
   proof (rule coprimeI)
     fix q
     assume "q dvd m" "q dvd n"
     then have "int q dvd int m" "int q dvd int n"
       by simp_all
     with \<open>?P\<close> have "is_unit (int q)"
       by (rule coprime_common_divisor)
     then show "is_unit q"
       by simp
   qed
 next
   assume ?Q
   show ?P
   proof (rule coprimeI)
     fix k
     assume "k dvd int m" "k dvd int n"
     then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
       by simp_all
     with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
       by (rule coprime_common_divisor)
     then show "is_unit k"
       by simp
   qed
 qed
 
 lemma coprime_abs_left_iff [simp]:
   "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
   using coprime_normalize_left_iff [of k l] by simp
 
 lemma coprime_abs_right_iff [simp]:
   "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
   using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
 
 lemma coprime_nat_abs_left_iff [simp]:
   "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
 proof -
   define m where "m = nat \<bar>k\<bar>"
   then have "\<bar>k\<bar> = int m"
     by simp
   moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
     by simp
   ultimately show ?thesis
     by simp
 qed
 
 lemma coprime_nat_abs_right_iff [simp]:
   "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
   using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
 
 lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   for a b :: int
   by (drule coprime_common_divisor [of _ _ x]) simp_all
 
 instantiation int :: idom_modulo
 begin
 
 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   where "k mod l = (if l = 0 then k
     else if sgn k = sgn l
       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
       else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
 
 lemma modulo_int_unfold:
   "(sgn k * int m) mod (sgn l * int n) =
    (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
     else if sgn k = sgn l
       then sgn l * int (m mod n)
       else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
   by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
     nat_mult_distrib)
 
 instance proof
   fix k l :: int
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   then show "k div l * l + k mod l = k"
     by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
        (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
          distrib_left [symmetric] minus_mult_right
          del: of_nat_mult minus_mult_right [symmetric])
 qed
 
 end
 
 instantiation int :: unique_euclidean_ring
 begin
 
 definition euclidean_size_int :: "int \<Rightarrow> nat"
   where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
 
 definition division_segment_int :: "int \<Rightarrow> int"
   where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)"
 
 lemma division_segment_eq_sgn:
   "division_segment k = sgn k" if "k \<noteq> 0" for k :: int
   using that by (simp add: division_segment_int_def)
 
 lemma abs_division_segment [simp]:
   "\<bar>division_segment k\<bar> = 1" for k :: int
   by (simp add: division_segment_int_def)
 
 lemma abs_mod_less:
   "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
 proof -
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
       abs_mult mod_greater_zero_iff_not_dvd)
 qed
 
 lemma sgn_mod:
   "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
 proof -
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
     by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
       sgn_mult mod_eq_0_iff_dvd)
 qed
 
 instance proof
   fix k l :: int
   show "division_segment (k mod l) = division_segment l" if
     "l \<noteq> 0" and "\<not> l dvd k"
     using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
 next
   fix l q r :: int
   obtain n m and s t
      where l: "l = sgn s * int n" and q: "q = sgn t * int m"
     by (blast intro: int_sgnE elim: that)
   assume \<open>l \<noteq> 0\<close>
   with l have "s \<noteq> 0" and "n > 0"
     by (simp_all add: sgn_0_0)
   assume "division_segment r = division_segment l"
   moreover have "r = sgn r * \<bar>r\<bar>"
     by (simp add: sgn_mult_abs)
   moreover define u where "u = nat \<bar>r\<bar>"
   ultimately have "r = sgn l * int u"
     using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all
   with l \<open>n > 0\<close> have r: "r = sgn s * int u"
     by (simp add: sgn_mult)
   assume "euclidean_size r < euclidean_size l"
   with l r \<open>s \<noteq> 0\<close> have "u < n"
     by (simp add: abs_mult)
   show "(q * l + r) div l = q"
   proof (cases "q = 0 \<or> r = 0")
     case True
     then show ?thesis
     proof
       assume "q = 0"
       then show ?thesis
         using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
     next
       assume "r = 0"
       from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
         using q l by (simp add: ac_simps sgn_mult)
       from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
         by (simp only: *, simp only: q l divide_int_unfold)
           (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
     qed
   next
     case False
     with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
       by (simp_all add: sgn_0_0)
     moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
       using mult_le_less_imp_less [of 1 m u n] by simp
     ultimately have *: "q * l + r = sgn (s * t)
       * int (if t < 0 then m * n - u else m * n + u)"
       using l q r
       by (simp add: sgn_mult algebra_simps of_nat_diff)
     have "(m * n - u) div n = m - 1" if "u > 0"
       using \<open>0 < m\<close> \<open>u < n\<close> that
       by (auto intro: div_nat_eqI simp add: algebra_simps)
     moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
       using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
       by auto
     ultimately show ?thesis
       using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
       by (simp only: *, simp only: l q divide_int_unfold)
         (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
   qed
 qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
 
 end
 
 lemma pos_mod_bound [simp]:
   "k mod l < l" if "l > 0" for k l :: int
 proof -
   obtain m and s where "k = sgn s * int m"
     by (rule int_sgnE)
   moreover from that obtain n where "l = sgn 1 * int n"
     by (cases l) simp_all
   moreover from this that have "n > 0"
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold)
       (simp add: mod_greater_zero_iff_not_dvd)
 qed
 
 lemma neg_mod_bound [simp]:
   "l < k mod l" if "l < 0" for k l :: int
 proof -
   obtain m and s where "k = sgn s * int m"
     by (rule int_sgnE)
   moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
     by (cases l) simp_all
   moreover define n where "n = Suc q"
   then have "Suc q = n"
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold)
       (simp add: mod_greater_zero_iff_not_dvd)
 qed
 
 lemma pos_mod_sign [simp]:
   "0 \<le> k mod l" if "l > 0" for k l :: int
 proof -
   obtain m and s where "k = sgn s * int m"
     by (rule int_sgnE)
   moreover from that obtain n where "l = sgn 1 * int n"
     by (cases l) auto
   moreover from this that have "n > 0"
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold) simp
 qed
 
 lemma neg_mod_sign [simp]:
   "k mod l \<le> 0" if "l < 0" for k l :: int
 proof -
   obtain m and s where "k = sgn s * int m"
     by (rule int_sgnE)
   moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
     by (cases l) simp_all
   moreover define n where "n = Suc q"
   then have "Suc q = n"
     by simp
   ultimately show ?thesis
     by (simp only: modulo_int_unfold) simp
 qed
 
 
 subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
 
 class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
   assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
     and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
     and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
 begin
 
 lemma division_segment_eq_iff:
   "a = b" if "division_segment a = division_segment b"
     and "euclidean_size a = euclidean_size b"
   using that division_segment_euclidean_size [of a] by simp
 
 lemma euclidean_size_of_nat [simp]:
   "euclidean_size (of_nat n) = n"
 proof -
   have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
     by (fact division_segment_euclidean_size)
   then show ?thesis by simp
 qed
 
 lemma of_nat_euclidean_size:
   "of_nat (euclidean_size a) = a div division_segment a"
 proof -
   have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
     by (subst nonzero_mult_div_cancel_left) simp_all
   also have "\<dots> = a div division_segment a"
     by simp
   finally show ?thesis .
 qed
 
 lemma division_segment_1 [simp]:
   "division_segment 1 = 1"
   using division_segment_of_nat [of 1] by simp
 
 lemma division_segment_numeral [simp]:
   "division_segment (numeral k) = 1"
   using division_segment_of_nat [of "numeral k"] by simp
 
 lemma euclidean_size_1 [simp]:
   "euclidean_size 1 = 1"
   using euclidean_size_of_nat [of 1] by simp
 
 lemma euclidean_size_numeral [simp]:
   "euclidean_size (numeral k) = numeral k"
   using euclidean_size_of_nat [of "numeral k"] by simp
 
 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
   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
 
 lemma one_mod_2_pow_eq [simp]:
   "1 mod (2 ^ n) = of_bool (n > 0)"
 proof -
   have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
     using of_nat_mod [of 1 "2 ^ n"] by simp
   also have "\<dots> = of_bool (n > 0)"
     by simp
   finally show ?thesis .
 qed
 
 lemma one_div_2_pow_eq [simp]:
   "1 div (2 ^ n) = of_bool (n = 0)"
   using div_mult_mod_eq [of 1 "2 ^ n"] by auto
 
 lemma div_mult2_eq':
   "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n"
 proof (cases a "of_nat m * of_nat n" rule: divmod_cases)
   case (divides q)
   then show ?thesis
     using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"]
     by (simp add: ac_simps)
 next
   case (remainder q r)
   then have "division_segment r = 1"
     using division_segment_of_nat [of "m * n"] by simp
   with division_segment_euclidean_size [of r]
   have "of_nat (euclidean_size r) = r"
     by simp
   have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
     by simp
   with remainder(6) have "r div (of_nat m * of_nat n) = 0"
     by simp
   with \<open>of_nat (euclidean_size r) = r\<close>
   have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
     by simp
   then have "of_nat (euclidean_size r div (m * n)) = 0"
     by (simp add: of_nat_div)
   then have "of_nat (euclidean_size r div m div n) = 0"
     by (simp add: div_mult2_eq)
   with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
     by (simp add: of_nat_div)
   with remainder(1)
   have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
     by simp
   with remainder(5) remainder(7) show ?thesis
     using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r]
     by (simp add: ac_simps)
 next
   case by0
   then show ?thesis
     by auto
 qed
 
 lemma mod_mult2_eq':
   "a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m"
 proof -
   have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)"
     by (simp add: combine_common_factor div_mult_mod_eq)
   moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)"
     by (simp add: ac_simps)
   ultimately show ?thesis
     by (simp add: div_mult2_eq' mult_commute)
 qed
 
 lemma div_mult2_numeral_eq:
   "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
 proof -
   have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
     by simp
   also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
     by (fact div_mult2_eq' [symmetric])
   also have "\<dots> = ?B"
     by simp
   finally show ?thesis .
 qed
 
 lemma numeral_Bit0_div_2:
   "numeral (num.Bit0 n) div 2 = numeral n"
 proof -
   have "numeral (num.Bit0 n) = numeral n + numeral n"
     by (simp only: numeral.simps)
   also have "\<dots> = numeral n * 2"
     by (simp add: mult_2_right)
   finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2"
     by simp
   also have "\<dots> = numeral n"
     by (rule nonzero_mult_div_cancel_right) simp
   finally show ?thesis .
 qed
 
 lemma numeral_Bit1_div_2:
   "numeral (num.Bit1 n) div 2 = numeral n"
 proof -
   have "numeral (num.Bit1 n) = numeral n + numeral n + 1"
     by (simp only: numeral.simps)
   also have "\<dots> = numeral n * 2 + 1"
     by (simp add: mult_2_right)
   finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2"
     by simp
   also have "\<dots> = numeral n * 2 div 2 + 1 div 2"
     using dvd_triv_right by (rule div_plus_div_distrib_dvd_left)
   also have "\<dots> = numeral n * 2 div 2"
     by simp
   also have "\<dots> = numeral n"
     by (rule nonzero_mult_div_cancel_right) simp
   finally show ?thesis .
 qed
 
 lemma exp_mod_exp:
   \<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close>
 proof -
   have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>)
     by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex)
   then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
     by simp
   then show ?thesis
     by (simp add: of_nat_mod)
 qed
 
-lemma range_mod_exp:
+lemma mask_mod_exp:
   \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close>
 proof -
   have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)
   proof (cases \<open>n \<le> m\<close>)
     case True
     then show ?thesis
       by (simp add: Suc_le_lessD min.absorb2)
   next
     case False
     then have \<open>m < n\<close>
       by simp
     then obtain q where n: \<open>n = Suc q + m\<close>
       by (auto dest: less_imp_Suc_add)
     then have \<open>min m n = m\<close>
       by simp
     moreover have \<open>(2::nat) ^ m \<le> 2 * 2 ^ q * 2 ^ m\<close>
       using mult_le_mono1 [of 1 \<open>2 * 2 ^ q\<close> \<open>2 ^ m\<close>] by simp
     with n have \<open>2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))\<close>
       by (simp add: monoid_mult_class.power_add algebra_simps)
     ultimately show ?thesis
       by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp
   qed
   then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
     by simp
   then show ?thesis
     by (simp add: of_nat_mod of_nat_diff)
 qed
 
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
 
 instance nat :: unique_euclidean_semiring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0)
 
 instance int :: unique_euclidean_ring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
 
 
 subsection \<open>Code generation\<close>
 
 code_identifier
   code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
diff --git a/src/HOL/Parity.thy b/src/HOL/Parity.thy
--- a/src/HOL/Parity.thy
+++ b/src/HOL/Parity.thy
@@ -1,1282 +1,1397 @@
 (*  Title:      HOL/Parity.thy
     Author:     Jeremy Avigad
     Author:     Jacques D. Fleuriot
 *)
 
 section \<open>Parity in rings and semirings\<close>
 
 theory Parity
   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 + semiring_modulo +
   assumes even_iff_mod_2_eq_zero: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
     and odd_iff_mod_2_eq_one: "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
     and odd_one [simp]: "\<not> 2 dvd 1"
 begin
 
 abbreviation even :: "'a \<Rightarrow> bool"
   where "even a \<equiv> 2 dvd a"
 
 abbreviation odd :: "'a \<Rightarrow> bool"
   where "odd a \<equiv> \<not> 2 dvd a"
 
 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: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric])
 
 lemma odd_of_bool_self [simp]:
   \<open>odd (of_bool p) \<longleftrightarrow> p\<close>
   by (cases p) 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 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 mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)"
   by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one)
 
 lemma evenE [elim?]:
   assumes "even a"
   obtains b where "a = 2 * b"
   using assms by (rule dvdE)
 
 lemma oddE [elim?]:
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
 proof -
   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 simp add: even_iff_mod_2_eq_zero)
 
 lemma of_bool_odd_eq_mod_2:
   "of_bool (odd a) = a mod 2"
   by (simp add: mod_2_eq_odd)
 
 lemma even_zero [simp]:
   "even 0"
   by (fact dvd_0_right)
 
 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_mult_iff by simp
   then have "even (numeral n + numeral n)"
     unfolding mult_2 .
   then show ?thesis
     unfolding numeral.simps .
 qed
 
 lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
 proof
   assume "even (numeral (num.Bit1 n))"
   then have "even (numeral n + numeral n + 1)"
     unfolding numeral.simps .
   then have "even (2 * numeral n + 1)"
     unfolding mult_2 .
   then have "2 dvd numeral n * 2 + 1"
     by (simp add: ac_simps)
   then have "2 dvd 1"
     using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
   then show False by simp
 qed
 
 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto
 
+lemma mask_eq_sum_exp:
+  \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
+proof -
+  have *: \<open>{q. q < Suc m} = insert m {q. q < m}\<close> for m
+    by auto
+  have \<open>2 ^ n = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1\<close>
+    by (induction n) (simp_all add: ac_simps mult_2 *)
+  then have \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1 - 1\<close>
+    by simp
+  then show ?thesis
+    by simp
+qed
+
 end
 
 class ring_parity = ring + semiring_parity
 begin
 
 subclass comm_ring_1 ..
 
 lemma even_minus:
   "even (- a) \<longleftrightarrow> even a"
   by (fact dvd_minus_iff)
 
 lemma even_diff [simp]:
   "even (a - b) \<longleftrightarrow> even (a + b)"
   using even_add [of a "- b"] by simp
 
 end
 
 
 subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
 
 context unique_euclidean_semiring_with_nat
 begin
 
 subclass semiring_parity
 proof
   show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a
     by (fact dvd_eq_mod_eq_0)
   show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a
   proof
     assume "a mod 2 = 1"
     then show "\<not> 2 dvd a"
       by auto
   next
     assume "\<not> 2 dvd a"
     have eucl: "euclidean_size (a mod 2) = 1"
     proof (rule order_antisym)
       show "euclidean_size (a mod 2) \<le> 1"
         using mod_size_less [of 2 a] by simp
       show "1 \<le> euclidean_size (a mod 2)"
         using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
     qed 
     from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
       by simp
     then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
       by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
     then have "\<not> 2 dvd euclidean_size a"
       using of_nat_dvd_iff [of 2] by simp
     then have "euclidean_size a mod 2 = 1"
       by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
     then have "of_nat (euclidean_size a mod 2) = of_nat 1"
       by simp
     then have "of_nat (euclidean_size a) mod 2 = 1"
       by (simp add: of_nat_mod)
     from \<open>\<not> 2 dvd a\<close> eucl
     show "a mod 2 = 1"
       by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
   qed
   show "\<not> is_unit 2"
   proof (rule notI)
     assume "is_unit 2"
     then have "of_nat 2 dvd of_nat 1"
       by simp
     then have "is_unit (2::nat)"
       by (simp only: of_nat_dvd_iff)
     then show False
       by simp
   qed
 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_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)
 
 lemma coprime_left_2_iff_odd [simp]:
   "coprime 2 a \<longleftrightarrow> odd a"
 proof
   assume "odd a"
   show "coprime 2 a"
   proof (rule coprimeI)
     fix b
     assume "b dvd 2" "b dvd a"
     then have "b dvd a mod 2"
       by (auto intro: dvd_mod)
     with \<open>odd a\<close> show "is_unit b"
       by (simp add: mod_2_eq_odd)
   qed
 next
   assume "coprime 2 a"
   show "odd a"
   proof (rule notI)
     assume "even a"
     then obtain b where "a = 2 * b" ..
     with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
       by simp
     moreover have "\<not> coprime 2 (2 * b)"
       by (rule not_coprimeI [of 2]) simp_all
     ultimately show False
       by blast
   qed
 qed
 
 lemma coprime_right_2_iff_odd [simp]:
   "coprime a 2 \<longleftrightarrow> odd a"
   using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
 
 end
 
 context unique_euclidean_ring_with_nat
 begin
 
 subclass ring_parity ..
 
 lemma minus_1_mod_2_eq [simp]:
   "- 1 mod 2 = 1"
   by (simp add: mod_2_eq_odd)
 
 lemma minus_1_div_2_eq [simp]:
   "- 1 div 2 = - 1"
 proof -
   from div_mult_mod_eq [of "- 1" 2]
   have "- 1 div 2 * 2 = - 1 * 2"
     using add_implies_diff by fastforce
   then show ?thesis
     using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
 qed
 
 end
 
 
 subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close>
 
 instance nat :: unique_euclidean_semiring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0)
 
 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]: "even (Suc n) \<longleftrightarrow> odd n"
   using even_plus_one_iff [of n] by simp
 
 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 "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
 
 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"
 proof
   assume "Suc (2 * m) = 2 * n"
   moreover have "odd (Suc (2 * m))" and "even (2 * n)"
     by simp_all
   ultimately show False by simp
 qed
 
 lemma double_not_eq_Suc_double:
   "2 * m \<noteq> Suc (2 * n)"
   using Suc_double_not_eq_double [of n m] by simp
 
 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 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
 
 lemma odd_card_imp_not_empty:
   \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
   using that by auto
 
 lemma nat_induct2 [case_names 0 1 step]:
   assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)"
   shows "P n"
 proof (induct n rule: less_induct)
   case (less n)
   show ?case
   proof (cases "n < Suc (Suc 0)")
     case True
     then show ?thesis
       using assms by (auto simp: less_Suc_eq)
   next
     case False
     then obtain k where k: "n = Suc (Suc k)"
       by (force simp: not_less nat_le_iff_add)
     then have "k<n"
       by simp
     with less assms have "P (k+2)"
       by blast
     then show ?thesis
       by (simp add: k)
   qed
 qed
 
+context semiring_parity
+begin
+
+lemma even_sum_iff:
+  \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close>
+using that proof (induction A)
+  case empty
+  then show ?case
+    by simp
+next
+  case (insert a A)
+  moreover have \<open>{b \<in> insert a A. odd (f b)} = (if odd (f a) then {a} else {}) \<union> {b \<in> A. odd (f b)}\<close>
+    by auto
+  ultimately show ?case
+    by simp
+qed
+
+lemma even_prod_iff:
+  \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
+  using that by (induction A) simp_all
+
+lemma even_mask_iff [simp]:
+  \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
+proof (cases \<open>n = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have \<open>{a. a = 0 \<and> a < n} = {0}\<close>
+    by auto
+  then show ?thesis
+    by (auto simp add: mask_eq_sum_exp even_sum_iff)
+qed
+
+end
+
 
 subsection \<open>Parity and powers\<close>
 
 context ring_1
 begin
 
 lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n"
   by (auto elim: evenE)
 
 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
 
 lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   by simp
 
 lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
   by (cases "even (n + k)") auto
 
 lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
   by (induct n) auto
 
 end
 
 context linordered_idom
 begin
 
 lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n"
   by (auto elim: evenE)
 
 lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
 
 lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   by (auto simp add: zero_le_even_power zero_le_odd_power)
 
 lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
 proof -
   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
     unfolding power_eq_0_iff [of a n, symmetric] by blast
   show ?thesis
     unfolding less_le zero_le_power_eq by auto
 qed
 
 lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
   unfolding not_le [symmetric] zero_le_power_eq by auto
 
 lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
   unfolding not_less [symmetric] zero_less_power_eq by auto
 
 lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n"
   using power_abs [of a n] by (simp add: zero_le_even_power)
 
 lemma power_mono_even:
   assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>"
   shows "a ^ n \<le> b ^ n"
 proof -
   have "0 \<le> \<bar>a\<bar>" by auto
   with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n"
     by (rule power_mono)
   with \<open>even n\<close> show ?thesis
     by (simp add: power_even_abs)
 qed
 
 lemma power_mono_odd:
   assumes "odd n" and "a \<le> b"
   shows "a ^ n \<le> b ^ n"
 proof (cases "b < 0")
   case True
   with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto
   then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono)
   with \<open>odd n\<close> show ?thesis by simp
 next
   case False
   then have "0 \<le> b" by auto
   show ?thesis
   proof (cases "a < 0")
     case True
     then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto
     then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto
     moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto
     ultimately show ?thesis by auto
   next
     case False
     then have "0 \<le> a" by auto
     with \<open>a \<le> b\<close> show ?thesis
       using power_mono by auto
   qed
 qed
 
 text \<open>Simplify, when the exponent is a numeral\<close>
 
 lemma zero_le_power_eq_numeral [simp]:
   "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a"
   by (fact zero_le_power_eq)
 
 lemma zero_less_power_eq_numeral [simp]:
   "0 < a ^ numeral w \<longleftrightarrow>
     numeral w = (0 :: nat) \<or>
     even (numeral w :: nat) \<and> a \<noteq> 0 \<or>
     odd (numeral w :: nat) \<and> 0 < a"
   by (fact zero_less_power_eq)
 
 lemma power_le_zero_eq_numeral [simp]:
   "a ^ numeral w \<le> 0 \<longleftrightarrow>
     (0 :: nat) < numeral w \<and>
     (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)"
   by (fact power_le_zero_eq)
 
 lemma power_less_zero_eq_numeral [simp]:
   "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
   by (fact power_less_zero_eq)
 
 lemma power_even_abs_numeral [simp]:
   "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
   by (fact power_even_abs)
 
 end
 
 
 subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
 
 lemma even_diff_iff:
   "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
   by (fact even_diff)
 
 lemma even_abs_add_iff:
   "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
   by simp
 
 lemma even_add_abs_iff:
   "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
   by simp
 
 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 zdiv_zmult2_eq:
   \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
 proof (cases \<open>b \<ge> 0\<close>)
   case True
   with that show ?thesis
     using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
 next
   case False
   with that show ?thesis
     using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
 lemma zmod_zmult2_eq:
   \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
 proof (cases \<open>b \<ge> 0\<close>)
   case True
   with that show ?thesis
     using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
 next
   case False
   with that show ?thesis
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
 
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
   assumes bits_induct [case_names stable rec]:
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
   assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
     and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
     and bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
     and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
     and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
     and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
     and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
     and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
     and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
 begin
 
 lemma bits_div_by_0 [simp]:
   \<open>a div 0 = 0\<close>
   by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
 
 lemma bits_1_div_2 [simp]:
   \<open>1 div 2 = 0\<close>
   using even_succ_div_2 [of 0] by simp
 
 lemma bits_1_div_exp [simp]:
   \<open>1 div 2 ^ n = of_bool (n = 0)\<close>
   using div_exp_eq [of 1 1] by (cases n) simp_all
 
 lemma even_succ_div_exp [simp]:
   \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
 proof (cases n)
   case 0
   with that show ?thesis
     by simp
 next
   case (Suc n)
   with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
   proof (induction n)
     case 0
     then show ?case
       by simp
   next
     case (Suc n)
     then show ?case
       using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
       by simp
   qed
   with Suc show ?thesis
     by simp
 qed
 
 lemma even_succ_mod_exp [simp]:
   \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
   using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that
   apply simp
   by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq)
 
 lemma bits_mod_by_1 [simp]:
   \<open>a mod 1 = 0\<close>
   using div_mult_mod_eq [of a 1] by simp
 
 lemma bits_mod_0 [simp]:
   \<open>0 mod a = 0\<close>
   using div_mult_mod_eq [of 0 a] by simp
 
 lemma bits_one_mod_two_eq_one [simp]:
   \<open>1 mod 2 = 1\<close>
   by (simp add: mod2_eq_if)
 
 definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
   where \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 
 lemma bit_0 [simp]:
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
   by (simp add: bit_def)
 
 lemma bit_Suc [simp]:
   \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
   using div_exp_eq [of a 1 n] by (simp add: bit_def)
 
 lemma bit_0_eq [simp]:
   \<open>bit 0 = bot\<close>
   by (simp add: fun_eq_iff bit_def)
 
 context
   fixes a
   assumes stable: \<open>a div 2 = a\<close>
 begin
 
 lemma bits_stable_imp_add_self:
   \<open>a + a mod 2 = 0\<close>
 proof -
   have \<open>a div 2 * 2 + a mod 2 = a\<close>
     by (fact div_mult_mod_eq)
   then have \<open>a * 2 + a mod 2 = a\<close>
     by (simp add: stable)
   then show ?thesis
     by (simp add: mult_2_right ac_simps)
 qed
 
 lemma stable_imp_bit_iff_odd:
   \<open>bit a n \<longleftrightarrow> odd a\<close>
   by (induction n) (simp_all add: stable)
 
 end
 
 lemma bit_iff_idd_imp_stable:
   \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
 using that proof (induction a rule: bits_induct)
   case (stable a)
   then show ?case
     by simp
 next
   case (rec a b)
   from rec.prems [of 1] have [simp]: \<open>b = odd a\<close>
     by (simp add: rec.hyps)
   from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close>
     by simp
   have \<open>bit a n \<longleftrightarrow> odd a\<close> for n
     using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp)
   then have \<open>a div 2 = a\<close>
     by (rule rec.IH)
   then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close>
     by (simp add: ac_simps)
   also have \<open>\<dots> = a\<close>
     using mult_div_mod_eq [of 2 a]
     by (simp add: of_bool_odd_eq_mod_2)
   finally show ?case
     using \<open>a div 2 = a\<close> by (simp add: hyp)
 qed
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> bit b n\<close>
 using that proof (induction a arbitrary: b rule: bits_induct)
   case (stable a)
   from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
     by simp
   have \<open>b div 2 = b\<close>
   proof (rule bit_iff_idd_imp_stable)
     fix n
     from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
       by simp
     also have \<open>bit a n \<longleftrightarrow> odd a\<close>
       using stable by (simp add: stable_imp_bit_iff_odd)
     finally show \<open>bit b n \<longleftrightarrow> odd b\<close>
       by (simp add: **)
   qed
   from ** have \<open>a mod 2 = b mod 2\<close>
     by (simp add: mod2_eq_if)
   then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close>
     by simp
   then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
     by (simp add: ac_simps)
   with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
     by (simp add: bits_stable_imp_add_self)
 next
   case (rec a p)
   from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
     by simp
   from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
     using rec.prems [of \<open>Suc n\<close>] by simp
   then have \<open>a = b div 2\<close>
     by (rule rec.IH)
   then have \<open>2 * a = 2 * (b div 2)\<close>
     by simp
   then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close>
     by simp
   also have \<open>\<dots> = b\<close>
     by (fact mod_mult_div_eq)
   finally show ?case
     by (auto simp add: mod2_eq_if)
 qed
 
 lemma bit_eq_iff:
   \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
   by (auto intro: bit_eqI)
 
 lemma bit_eq_rec:
   \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
   apply (simp add: bit_eq_iff)
   apply auto
   using bit_0 apply blast
   using bit_0 apply blast
   using bit_Suc apply blast
   using bit_Suc apply blast
      apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq)
     apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq)
    apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
   apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
   done
 
 lemma bit_exp_iff:
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
   by (auto simp add: bit_def exp_div_exp_eq)
 
 lemma bit_1_iff:
   \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
   using bit_exp_iff [of 0 n] by simp
 
 lemma bit_2_iff:
   \<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
   using bit_exp_iff [of 1 n] by auto
 
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
   "P n" if zero: "P 0"
     and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
     and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
 proof (induction 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
       then have "n \<noteq> 1"
         by auto
       with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
         by simp
       with \<open>even n\<close> 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
 
 instance nat :: semiring_bits
 proof
   show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
     and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
     for P and n :: nat
   proof (induction n rule: nat_bit_induct)
     case zero
     from stable [of 0] show ?case
       by simp
   next
     case (even n)
     with rec [of n False] show ?case
       by simp
   next
     case (odd n)
     with rec [of n True] show ?case
       by simp
   qed
   show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close>
     for q m n :: nat
     apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin)
     apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes)
     done
   show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close>
     for q m n :: nat
     using that
     apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
     apply (simp add: mult.commute)
     done
 qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
 
 lemma int_bit_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_bit_induct)
     case zero
     then show ?case
       by (simp add: zero_int)
   next
     case (even n)
     have "P (int n * 2)"
       by (rule even_int) (use even in simp_all)
     with even show ?case
       by (simp add: ac_simps)
   next
     case (odd n)
     have "P (1 + (int n * 2))"
       by (rule odd_int) (use odd in simp_all)
     with odd show ?case
       by (simp add: ac_simps)
   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_bit_induct)
     case zero
     then show ?case
       by (simp add: minus_int)
   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"
       by (simp add: algebra_simps)
     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"
       by (simp add: algebra_simps)
     finally show ?case
       using odd by simp
   qed
 qed
 
 instance int :: semiring_bits
 proof
   show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
     and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
     for P and k :: int
   proof (induction k rule: int_bit_induct)
     case zero
     from stable [of 0] show ?case
       by simp
   next
     case minus
     from stable [of \<open>- 1\<close>] show ?case
       by simp
   next
     case (even k)
     with rec [of k False] show ?case
       by (simp add: ac_simps)
   next
     case (odd k)
     with rec [of k True] show ?case
       by (simp add: ac_simps)
   qed
   show \<open>(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
     for m n :: nat
   proof (cases \<open>m < n\<close>)
     case True
     then have \<open>n = m + (n - m)\<close>
       by simp
     then have \<open>(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\<close>
       by simp
     also have \<open>\<dots> = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\<close>
       by (simp add: power_add)
     also have \<open>\<dots> = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\<close>
       by (simp add: zdiv_zmult2_eq)
     finally show ?thesis using \<open>m < n\<close> by simp
   next
     case False
     then show ?thesis
       by (simp add: power_diff)
   qed
   show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
     for m n :: nat and k :: int
     using mod_exp_eq [of \<open>nat k\<close> m n]
     apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
      apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add)
     apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>])
     apply (subst zmod_zmult2_eq) apply simp_all
     done
   show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close>
     if \<open>m \<le> n\<close> for m n :: nat and k :: int
     using that
     apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
     apply (simp add: ac_simps)
     done
 qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
 
 class semiring_bit_shifts = semiring_bits +
   fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
   fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
 begin
 
 definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
 
 text \<open>
   Logically, \<^const>\<open>push_bit\<close>,
   \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
   as separate operations makes proofs easier, otherwise proof automation
   would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
   algebraic relationships between those operations.
   Having
   \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations
   takes into account that specific instances of these can be implemented
   differently wrt. code generation.
 \<close>
 
 lemma bit_iff_odd_drop_bit:
   \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
   by (simp add: bit_def drop_bit_eq_div)
 
 lemma even_drop_bit_iff_not_bit:
   \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
   by (simp add: bit_iff_odd_drop_bit)
 
 lemma bits_ident:
   "push_bit n (drop_bit n a) + take_bit n a = a"
   using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
 
 lemma push_bit_push_bit [simp]:
   "push_bit m (push_bit n a) = push_bit (m + n) a"
   by (simp add: push_bit_eq_mult power_add ac_simps)
 
 lemma push_bit_0_id [simp]:
   "push_bit 0 = id"
   by (simp add: fun_eq_iff push_bit_eq_mult)
 
 lemma push_bit_of_0 [simp]:
   "push_bit n 0 = 0"
   by (simp add: push_bit_eq_mult)
 
 lemma push_bit_of_1:
   "push_bit n 1 = 2 ^ n"
   by (simp add: push_bit_eq_mult)
 
 lemma push_bit_Suc [simp]:
   "push_bit (Suc n) a = push_bit n (a * 2)"
   by (simp add: push_bit_eq_mult ac_simps)
 
 lemma push_bit_double:
   "push_bit n (a * 2) = push_bit n a * 2"
   by (simp add: push_bit_eq_mult ac_simps)
 
 lemma push_bit_add:
   "push_bit n (a + b) = push_bit n a + push_bit n b"
   by (simp add: push_bit_eq_mult algebra_simps)
 
 lemma take_bit_0 [simp]:
   "take_bit 0 a = 0"
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_Suc [simp]:
   \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
 proof -
   have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
     using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>]
       mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>]
     by (auto simp add: take_bit_eq_mod ac_simps)
   then show ?thesis
     using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
 qed
 
 lemma take_bit_of_0 [simp]:
   "take_bit n 0 = 0"
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_of_1 [simp]:
   "take_bit n 1 = of_bool (n > 0)"
   by (cases n) simp_all
 
 lemma drop_bit_of_0 [simp]:
   "drop_bit n 0 = 0"
   by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_of_1 [simp]:
   "drop_bit n 1 = of_bool (n = 0)"
   by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_0 [simp]:
   "drop_bit 0 = id"
   by (simp add: fun_eq_iff drop_bit_eq_div)
 
 lemma drop_bit_Suc [simp]:
   "drop_bit (Suc n) a = drop_bit n (a div 2)"
   using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_half:
   "drop_bit n (a div 2) = drop_bit n a div 2"
   by (induction n arbitrary: a) simp_all
 
 lemma drop_bit_of_bool [simp]:
   "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
   by (cases n) simp_all
 
 lemma take_bit_eq_0_imp_dvd:
   "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a"
   by (simp add: take_bit_eq_mod mod_0_imp_dvd)
 
 lemma even_take_bit_eq [simp]:
   \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
   by (cases n) simp_all
 
 lemma take_bit_take_bit [simp]:
   "take_bit m (take_bit n a) = take_bit (min m n) a"
   by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)
 
 lemma drop_bit_drop_bit [simp]:
   "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
   by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
 
 lemma push_bit_take_bit:
   "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
   apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps)
   using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add)
   done
 
 lemma take_bit_push_bit:
   "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
 proof (cases "m \<le> n")
   case True
   then show ?thesis
     apply (simp add:)
     apply (simp_all add: push_bit_eq_mult take_bit_eq_mod)
     apply (auto dest!: le_Suc_ex simp add: power_add ac_simps)
     using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n]
     apply (simp add: ac_simps)
     done
 next
   case False
   then show ?thesis
     using push_bit_take_bit [of n "m - n" a]
     by simp
 qed
 
 lemma take_bit_drop_bit:
   "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
   by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)
 
 lemma drop_bit_take_bit:
   "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
 proof (cases "m \<le> n")
   case True
   then show ?thesis
     using take_bit_drop_bit [of "n - m" m a] by simp
 next
   case False
   then obtain q where \<open>m = n + q\<close>
     by (auto simp add: not_le dest: less_imp_Suc_add)
   then have \<open>drop_bit m (take_bit n a) = 0\<close>
     using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q]
     by (simp add: take_bit_eq_mod drop_bit_eq_div)
   with False show ?thesis
     by simp
 qed
 
 lemma bit_drop_bit_eq:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
   by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div)
 
 lemma bit_take_bit_iff:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
   by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div)
 
 end
 
 instantiation nat :: semiring_bit_shifts
 begin
 
 definition push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
   where \<open>push_bit_nat n m = m * 2 ^ n\<close>
 
 definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
   where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
 
 instance proof
   show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat
     by (simp add: push_bit_nat_def)
   show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat
     by (simp add: drop_bit_nat_def)
 qed
 
 end
 
 instantiation int :: semiring_bit_shifts
 begin
 
 definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>push_bit_int n k = k * 2 ^ n\<close>
 
 definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>drop_bit_int n k = k div 2 ^ n\<close>
 
 instance proof
   show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int
     by (simp add: push_bit_int_def)
   show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int
     by (simp add: drop_bit_int_def)
 qed
 
 end
 
+lemma bit_push_bit_iff_nat:
+  \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  then obtain r where \<open>n = m + r\<close>
+    using le_Suc_ex by blast
+  with True show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+  case False
+  then obtain r where \<open>m = Suc (n + r)\<close>
+    using less_imp_Suc_add not_le by blast
+  with False show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
+lemma bit_push_bit_iff_int:
+  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  then obtain r where \<open>n = m + r\<close>
+    using le_Suc_ex by blast
+  with True show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+  case False
+  then obtain r where \<open>m = Suc (n + r)\<close>
+    using less_imp_Suc_add not_le by blast
+  with False show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
 class unique_euclidean_semiring_with_bit_shifts =
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
 begin
 
 lemma take_bit_of_exp [simp]:
   \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
   by (simp add: take_bit_eq_mod exp_mod_exp)
 
 lemma take_bit_of_2 [simp]:
   \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
   using take_bit_of_exp [of n 1] by simp
 
-lemma take_bit_of_range:
+lemma take_bit_of_mask:
   \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
-  by (simp add: take_bit_eq_mod range_mod_exp)
+  by (simp add: take_bit_eq_mod mask_mod_exp)
 
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
 
 lemma push_bit_numeral [simp]:
   "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
 
 lemma push_bit_of_nat:
   "push_bit n (of_nat m) = of_nat (push_bit n m)"
   by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
 
 lemma take_bit_add:
   "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
   by (simp add: take_bit_eq_mod mod_simps)
 
 lemma take_bit_eq_0_iff:
   "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a"
   by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd)
 
 lemma take_bit_of_1_eq_0_iff [simp]:
   "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_numeral_bit0 [simp]:
   "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc
     ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp
 
 lemma take_bit_numeral_bit1 [simp]:
   "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc
     ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps)
 
 lemma take_bit_of_nat:
   "take_bit n (of_nat m) = of_nat (take_bit n m)"
   by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
 
 lemma drop_bit_numeral_bit0 [simp]:
   "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc
     nonzero_mult_div_cancel_left [OF numeral_neq_zero])
 
 lemma drop_bit_numeral_bit1 [simp]:
   "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
     div_mult_self4 [OF numeral_neq_zero]) simp
 
 lemma drop_bit_of_nat:
   "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
   by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
 
+lemma bit_of_nat_iff_bit [simp]:
+  \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+proof -
+  have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
+    by simp
+  also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
+    by (simp add: of_nat_div)
+  finally show ?thesis
+    by (simp add: bit_def semiring_bits_class.bit_def)
+qed
+
+lemma of_nat_push_bit:
+  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_nat_drop_bit:
+  \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
+  by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
+
+lemma of_nat_take_bit:
+  \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close>
+  by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod)
+
+lemma bit_push_bit_iff_of_nat_iff:
+  \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+proof -
+  from bit_push_bit_iff_nat
+  have \<open>bit (of_nat (push_bit m r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_push_bit)
+qed
+
 end
 
 instance nat :: unique_euclidean_semiring_with_bit_shifts ..
 
 instance int :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma push_bit_of_Suc_0 [simp]:
   "push_bit n (Suc 0) = 2 ^ n"
   using push_bit_of_1 [where ?'a = nat] by simp
 
 lemma take_bit_of_Suc_0 [simp]:
   "take_bit n (Suc 0) = of_bool (0 < n)"
   using take_bit_of_1 [where ?'a = nat] by simp
 
 lemma drop_bit_of_Suc_0 [simp]:
   "drop_bit n (Suc 0) = of_bool (n = 0)"
   using drop_bit_of_1 [where ?'a = nat] by simp
 
 lemma take_bit_eq_self:
   \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat
   using that by (simp add: take_bit_eq_mod)
 
 lemma push_bit_minus_one:
   "push_bit n (- 1 :: int) = - (2 ^ n)"
   by (simp add: push_bit_eq_mult)
 
 lemma minus_1_div_exp_eq_int:
   \<open>- 1 div (2 :: int) ^ n = - 1\<close>
   by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
 
 lemma drop_bit_minus_one [simp]:
   \<open>drop_bit n (- 1 :: int) = - 1\<close>
   by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
 
 lemma take_bit_uminus:
   "take_bit n (- (take_bit n k)) = take_bit n (- k)"
     for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
 
 lemma take_bit_minus:
   "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
     for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
 
 lemma take_bit_nonnegative [simp]:
   "take_bit n k \<ge> 0"
     for k :: int
   by (simp add: take_bit_eq_mod)
 
 end
diff --git a/src/HOL/ex/Bit_Operations.thy b/src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy
+++ b/src/HOL/ex/Bit_Operations.thy
@@ -1,847 +1,775 @@
 (*  Author:  Florian Haftmann, TUM
 *)
 
 section \<open>Proof of concept for purely algebraically founded lists of bits\<close>
 
 theory Bit_Operations
   imports
     "HOL-Library.Boolean_Algebra"
     Main
 begin
 
-lemma bit_push_bit_eq_int:
-  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-proof (cases \<open>m \<le> n\<close>)
-  case True
-  then obtain q where \<open>n = m + q\<close>
-    using le_Suc_ex by blast
-  with True show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add)
-next
-  case False
-  then obtain q where \<open>m = Suc (n + q)\<close>
-    using less_imp_Suc_add not_le by blast
-  with False show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add)
-qed
-
 context semiring_bits
 begin
 
-(*lemma range_rec:
-  \<open>2 ^ Suc n - 1 = 1 + 2 * (2 ^ n - 1)\<close>
+(*lemma even_mask_div_iff:
+  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
   sorry
 
-lemma even_range_div_iff:
-  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
-  sorry*)
-
-(*lemma even_range_iff [simp]:
-  \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
-  by (induction n) (simp_all only: range_rec, simp_all)
-
-lemma bit_range_iff:
+lemma bit_mask_iff:
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
-  by (simp add: bit_def even_range_div_iff not_le)*)
+  by (simp add: bit_def even_mask_div_iff not_le)*)
 
 end
 
 context semiring_bit_shifts
 begin
 
 (*lemma bit_push_bit_iff:
   \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>*)
 
 end
 
 
 subsection \<open>Bit operations in suitable algebraic structures\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
   fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "AND" 64)
     and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "OR"  59)
     and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "XOR" 59)
   assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
     and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
     and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
 begin
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
   than \<open>+\<close> and \<open>-\<close>.
   For the sake of code generation
   the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
   are specified as definitional class operations.
 \<close>
 
 definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\<close>
 
 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>set_bit n = map_bit n top\<close>
 
 definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>unset_bit n = map_bit n bot\<close>
 
 definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>flip_bit n = map_bit n Not\<close>
 
 text \<open>
   Having 
   \<^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
   operations allows to implement them using bit masks later.
 \<close>
 
 lemma stable_imp_drop_eq:
   \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
   by (induction n) (simp_all add: that)
 
 lemma map_bit_0 [simp]:
   \<open>map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\<close>
   by (simp add: map_bit_def)
 
 lemma map_bit_Suc [simp]:
   \<open>map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\<close>
   by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2
     elim: evenE oddE)
 
 lemma set_bit_0 [simp]:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
   by (simp add: set_bit_def)
 
 lemma set_bit_Suc [simp]:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
   by (simp add: set_bit_def)
 
 lemma unset_bit_0 [simp]:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
   by (simp add: unset_bit_def)
 
 lemma unset_bit_Suc [simp]:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
   by (simp add: unset_bit_def)
 
 lemma flip_bit_0 [simp]:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
   by (simp add: flip_bit_def)
 
 lemma flip_bit_Suc [simp]:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
   by (simp add: flip_bit_def)
 
+lemma zero_and_eq [simp]:
+  "0 AND a = 0"
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma and_zero_eq [simp]:
+  "a AND 0 = 0"
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma zero_or_eq [simp]:
+  "0 OR a = a"
+  by (simp add: bit_eq_iff bit_or_iff)
+
+lemma or_zero_eq [simp]:
+  "a OR 0 = a"
+  by (simp add: bit_eq_iff bit_or_iff)
+
+lemma zero_xor_eq [simp]:
+  "0 XOR a = a"
+  by (simp add: bit_eq_iff bit_xor_iff)
+
+lemma xor_zero_eq [simp]:
+  "a XOR 0 = a"
+  by (simp add: bit_eq_iff bit_xor_iff)
+
 lemma take_bit_and [simp]:
   \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
 
 lemma take_bit_or [simp]:
   \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
 
 lemma take_bit_xor [simp]:
   \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
   assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
   assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
 begin
 
 text \<open>
   For the sake of code generation \<^const>\<open>not\<close> is specified as
   definitional class operation.  Note that \<^const>\<open>not\<close> has no
   sensible definition for unlimited but only positive bit strings
   (type \<^typ>\<open>nat\<close>).
 \<close>
 
 lemma bits_minus_1_mod_2_eq [simp]:
   \<open>(- 1) mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
 
 lemma not_eq_complement:
   \<open>NOT a = - a - 1\<close>
   using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
 
 lemma minus_eq_not_plus_1:
   \<open>- a = NOT a + 1\<close>
   using not_eq_complement [of a] by simp
 
 lemma bit_minus_iff:
   \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
   by (simp add: minus_eq_not_minus_1 bit_not_iff)
 
 lemma bit_not_exp_iff:
   \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
   by (auto simp add: bit_not_iff bit_exp_iff)
 
 lemma bit_minus_1_iff [simp]:
   \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
   by (simp add: bit_minus_iff)
 
 lemma bit_minus_exp_iff:
   \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
   oops
 
 lemma bit_minus_2_iff [simp]:
   \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
   by (simp add: bit_minus_iff bit_1_iff)
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
     apply standard
              apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
      apply (simp_all add: bit_exp_iff)
      apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
     done
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
     apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
          apply (simp add: bit_exp_iff, simp add: bit_def)
         apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
        apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
       apply (simp_all add: bit_exp_iff, simp_all add: bit_def)
     done
 qed
 
+lemma push_bit_minus:
+  \<open>push_bit n (- a) = - push_bit n a\<close>
+  by (simp add: push_bit_eq_mult)
+
 lemma take_bit_not_take_bit:
   \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
 
 end
 
 
 subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
 locale zip_nat = single: abel_semigroup f
     for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70) +
   assumes end_of_bits: "\<not> False \<^bold>* False"
 begin
 
 lemma False_P_imp:
   "False \<^bold>* True \<and> P" if "False \<^bold>* P"
   using that end_of_bits by (cases P) simp_all
 
 function F :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "\<^bold>\<times>" 70)
   where "m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
     else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2)"
   by auto
 
 termination
   by (relation "measure (case_prod (+))") auto
 
 lemma zero_left_eq:
   "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
   by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
 
 lemma zero_right_eq:
   "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
   by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits)
 
 lemma simps [simp]:
   "0 \<^bold>\<times> 0 = 0"
   "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
   "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
   "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
   by (simp_all only: zero_left_eq zero_right_eq) simp
 
 lemma rec:
   "m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
   by (cases "m = 0 \<and> n = 0") (auto simp add: end_of_bits)
 
 declare F.simps [simp del]
 
 sublocale abel_semigroup F
 proof
   show "m \<^bold>\<times> n \<^bold>\<times> q = m \<^bold>\<times> (n \<^bold>\<times> q)" for m n q :: nat
   proof (induction m arbitrary: n q rule: nat_bit_induct)
     case zero
     show ?case
       by simp
   next
     case (even m)
     with rec [of "2 * m"] rec [of _ q] show ?case
       by (cases "even n") (auto simp add: ac_simps dest: False_P_imp)
   next
     case (odd m)
     with rec [of "Suc (2 * m)"] rec [of _ q] show ?case
       by (cases "even n"; cases "even q")
         (auto dest: False_P_imp simp add: ac_simps)
   qed
   show "m \<^bold>\<times> n = n \<^bold>\<times> m" for m n :: nat
   proof (induction m arbitrary: n rule: nat_bit_induct)
     case zero
     show ?case
       by (simp add: ac_simps)
   next
     case (even m)
     with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
       by (simp add: ac_simps)
   next
     case (odd m)
     with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
       by (simp add: ac_simps)
   qed
 qed
 
 lemma self [simp]:
   "n \<^bold>\<times> n = of_bool (True \<^bold>* True) * n"
   by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
 
 lemma even_iff [simp]:
   "even (m \<^bold>\<times> n) \<longleftrightarrow> \<not> (odd m \<^bold>* odd n)"
 proof (induction m arbitrary: n rule: nat_bit_induct)
   case zero
   show ?case
     by (cases "even n") (simp_all add: end_of_bits)
 next
   case (even m)
   then show ?case
     by (simp add: rec [of "2 * m"])
 next
   case (odd m)
   then show ?case
     by (simp add: rec [of "Suc (2 * m)"])
 qed
 
 end
 
 instantiation nat :: semiring_bit_operations
 begin
 
 global_interpretation and_nat: zip_nat "(\<and>)"
   defines and_nat = and_nat.F
   by standard auto
 
 global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
 proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard)
   show "n AND n = n" for n :: nat
     by (simp add: and_nat.self)
 qed
 
 declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_and_eq [simp]:
-  "0 AND n = 0" for n :: nat
-  by simp
-
-lemma and_zero_nat_eq [simp]:
-  "n AND 0 = 0" for n :: nat
-  by simp
-
 global_interpretation or_nat: zip_nat "(\<or>)"
   defines or_nat = or_nat.F
   by standard auto
 
 global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
 proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard)
   show "n OR n = n" for n :: nat
     by (simp add: or_nat.self)
 qed
 
 declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_or_eq [simp]:
-  "0 OR n = n" for n :: nat
-  by simp
-
-lemma or_zero_nat_eq [simp]:
-  "n OR 0 = n" for n :: nat
-  by simp
-
 global_interpretation xor_nat: zip_nat "(\<noteq>)"
   defines xor_nat = xor_nat.F
   by standard auto
 
 declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_xor_eq [simp]:
-  "0 XOR n = n" for n :: nat
-  by simp
-
-lemma xor_zero_nat_eq [simp]:
-  "n XOR 0 = n" for n :: nat
-  by simp
-
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
   proof (rule sym, induction q arbitrary: m n)
     case 0
     then show ?case
       by (simp add: and_nat.even_iff)
   next
     case (Suc q)
     with and_nat.rec [of m n] show ?case
       by simp
   qed
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
   proof (rule sym, induction q arbitrary: m n)
     case 0
     then show ?case
       by (simp add: or_nat.even_iff)
   next
     case (Suc q)
     with or_nat.rec [of m n] show ?case
       by simp
   qed
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
   proof (rule sym, induction q arbitrary: m n)
     case 0
     then show ?case
       by (simp add: xor_nat.even_iff)
   next
     case (Suc q)
     with xor_nat.rec [of m n] show ?case
       by simp
   qed
 qed
 
 end
 
 global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat"
   by standard simp
 
 global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat"
   by standard simp
 
 lemma Suc_0_and_eq [simp]:
   "Suc 0 AND n = n mod 2"
   by (cases n) auto
 
 lemma and_Suc_0_eq [simp]:
   "n AND Suc 0 = n mod 2"
   using Suc_0_and_eq [of n] by (simp add: ac_simps)
 
 lemma Suc_0_or_eq [simp]:
   "Suc 0 OR n = n + of_bool (even n)"
   by (cases n) (simp_all add: ac_simps)
 
 lemma or_Suc_0_eq [simp]:
   "n OR Suc 0 = n + of_bool (even n)"
   using Suc_0_or_eq [of n] by (simp add: ac_simps)
 
 lemma Suc_0_xor_eq [simp]:
   "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)"
   by (cases n) (simp_all add: ac_simps)
 
 lemma xor_Suc_0_eq [simp]:
   "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)"
   using Suc_0_xor_eq [of n] by (simp add: ac_simps)
 
 
 subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
 abbreviation (input) complement :: "int \<Rightarrow> int"
   where "complement k \<equiv> - k - 1"
 
 lemma complement_half:
   "complement (k * 2) div 2 = complement k"
   by simp
 
 lemma complement_div_2:
   "complement (k div 2) = complement k div 2"
   by linarith
 
 locale zip_int = single: abel_semigroup f
   for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
 begin
  
 lemma False_False_imp_True_True:
   "True \<^bold>* True" if "False \<^bold>* False"
 proof (rule ccontr)
   assume "\<not> True \<^bold>* True"
   with that show False
     using single.assoc [of False True True]
     by (cases "False \<^bold>* True") simp_all
 qed
 
 function F :: "int \<Rightarrow> int \<Rightarrow> int"  (infixl "\<^bold>\<times>" 70)
   where "k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
     then - of_bool (odd k \<^bold>* odd l)
     else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2)"
   by auto
 
 termination
   by (relation "measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))") auto
 
 lemma zero_left_eq:
   "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> l
      | (True, False) \<Rightarrow> complement l
      | (True, True) \<Rightarrow> - 1)"
   by (induction l rule: int_bit_induct)
    (simp_all split: bool.split) 
 
 lemma minus_left_eq:
   "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> l
      | (True, False) \<Rightarrow> complement l
      | (True, True) \<Rightarrow> - 1)"
   by (induction l rule: int_bit_induct)
    (simp_all split: bool.split) 
 
 lemma zero_right_eq:
   "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> k
      | (True, False) \<Rightarrow> complement k
      | (True, True) \<Rightarrow> - 1)"
   by (induction k rule: int_bit_induct)
     (simp_all add: ac_simps split: bool.split)
 
 lemma minus_right_eq:
   "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> k
      | (True, False) \<Rightarrow> complement k
      | (True, True) \<Rightarrow> - 1)"
   by (induction k rule: int_bit_induct)
     (simp_all add: ac_simps split: bool.split)
 
 lemma simps [simp]:
   "0 \<^bold>\<times> 0 = - of_bool (False \<^bold>* False)"
   "- 1 \<^bold>\<times> 0 = - of_bool (True \<^bold>* False)"
   "0 \<^bold>\<times> - 1 = - of_bool (False \<^bold>* True)"
   "- 1 \<^bold>\<times> - 1 = - of_bool (True \<^bold>* True)"
   "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> l
      | (True, False) \<Rightarrow> complement l
      | (True, True) \<Rightarrow> - 1)"
   "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> l
      | (True, False) \<Rightarrow> complement l
      | (True, True) \<Rightarrow> - 1)"
   "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> k
      | (True, False) \<Rightarrow> complement k
      | (True, True) \<Rightarrow> - 1)"
   "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> k
      | (True, False) \<Rightarrow> complement k
      | (True, True) \<Rightarrow> - 1)"
   "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> l \<noteq> - 1
     \<Longrightarrow> k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
   by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp)
 
 declare F.simps [simp del]
 
 lemma rec:
   "k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
   by (cases "k \<in> {0, - 1} \<and> l \<in> {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split)
 
 sublocale abel_semigroup F
 proof
   show "k \<^bold>\<times> l \<^bold>\<times> r = k \<^bold>\<times> (l \<^bold>\<times> r)" for k l r :: int
   proof (induction k arbitrary: l r rule: int_bit_induct)
     case zero
     have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "False \<^bold>* False" "\<not> False \<^bold>* True"
     proof (induction l arbitrary: r rule: int_bit_induct)
       case zero
       from that show ?case
         by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     next
       case minus
       from that show ?case
         by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     next
       case (even l)
       with that rec [of _ r] show ?case
         by (cases "even r")
           (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
     next
       case (odd l)
       moreover have "- l - 1 = - 1 - l"
         by simp
       ultimately show ?case
         using that rec [of _ r]
         by (cases "even r")
           (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     qed
     then show ?case
       by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
   next
     case minus
     have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "\<not> True \<^bold>* True" "False \<^bold>* True"
     proof (induction l arbitrary: r rule: int_bit_induct)
       case zero
       from that show ?case
         by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     next
       case minus
       from that show ?case
         by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     next
       case (even l)
       with that rec [of _ r] show ?case
         by (cases "even r")
           (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
     next
       case (odd l)
       moreover have "- l - 1 = - 1 - l"
         by simp
       ultimately show ?case
         using that rec [of _ r]
         by (cases "even r")
           (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
     qed
     then show ?case
       by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
   next
     case (even k)
     with rec [of "k * 2"] rec [of _ r] show ?case
       by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
   next
     case (odd k)
     with rec [of "1 + k * 2"] rec [of _ r] show ?case
       by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
   qed
   show "k \<^bold>\<times> l = l \<^bold>\<times> k" for k l :: int
   proof (induction k arbitrary: l rule: int_bit_induct)
     case zero
     show ?case
       by simp
   next
     case minus
     show ?case
       by simp
   next
     case (even k)
     with rec [of "k * 2" l] rec [of l "k * 2"] show ?case
       by (simp add: ac_simps)
   next
     case (odd k)
     with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
       by (simp add: ac_simps)
   qed
 qed
 
 lemma self [simp]:
   "k \<^bold>\<times> k = (case (False \<^bold>* False, True \<^bold>* True)
     of (False, False) \<Rightarrow> 0
      | (False, True) \<Rightarrow> k
      | (True, True) \<Rightarrow> - 1)"
   by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split)
 
 lemma even_iff [simp]:
   "even (k \<^bold>\<times> l) \<longleftrightarrow> \<not> (odd k \<^bold>* odd l)"
 proof (induction k arbitrary: l rule: int_bit_induct)
   case zero
   show ?case
     by (cases "even l") (simp_all split: bool.splits)
 next
   case minus
   show ?case
     by (cases "even l") (simp_all split: bool.splits)
 next
   case (even k)
   then show ?case
     by (simp add: rec [of "k * 2"])
 next
   case (odd k)
   then show ?case
     by (simp add: rec [of "1 + k * 2"])
 qed
 
 end
 
 instantiation int :: ring_bit_operations
 begin
 
 definition not_int :: "int \<Rightarrow> int"
   where "not_int = complement"
 
 global_interpretation and_int: zip_int "(\<and>)"
   defines and_int = and_int.F
   by standard
 
 declare and_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
 global_interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
 proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
   show "k AND k = k" for k :: int
     by (simp add: and_int.self)
 qed
 
-lemma zero_int_and_eq [simp]:
-  "0 AND k = 0" for k :: int
-  by simp
-
-lemma and_zero_int_eq [simp]:
-  "k AND 0 = 0" for k :: int
-  by simp
-
-lemma minus_int_and_eq [simp]:
-  "- 1 AND k = k" for k :: int
-  by simp
-
-lemma and_minus_int_eq [simp]:
-  "k AND - 1 = k" for k :: int
-  by simp
-
 global_interpretation or_int: zip_int "(\<or>)"
   defines or_int = or_int.F
   by standard
 
 declare or_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
 global_interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
 proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
   show "k OR k = k" for k :: int
     by (simp add: or_int.self)
 qed
 
-lemma zero_int_or_eq [simp]:
-  "0 OR k = k" for k :: int
-  by simp
-
-lemma and_zero_or_eq [simp]:
-  "k OR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_or_eq [simp]:
-  "- 1 OR k = - 1" for k :: int
-  by simp
-
-lemma or_minus_int_eq [simp]:
-  "k OR - 1 = - 1" for k :: int
-  by simp
-
 global_interpretation xor_int: zip_int "(\<noteq>)"
   defines xor_int = xor_int.F
   by standard
 
 declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_int_xor_eq [simp]:
-  "0 XOR k = k" for k :: int
-  by simp
-
-lemma and_zero_xor_eq [simp]:
-  "k XOR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_xor_eq [simp]:
-  "- 1 XOR k = complement k" for k :: int
-  by simp
-
-lemma xor_minus_int_eq [simp]:
-  "k XOR - 1 = complement k" for k :: int
-  by simp
-
-lemma not_div_2:
-  "NOT k div 2 = NOT (k div 2)"
-  for k :: int
-  by (simp add: complement_div_2 not_int_def)
-
-lemma not_int_simps [simp]:
-  "NOT 0 = (- 1 :: int)"
-  "NOT (- 1) = (0 :: int)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
-  by (auto simp add: not_int_def elim: oddE)
-
-lemma not_one_int [simp]:
-  "NOT 1 = (- 2 :: int)"
-  by simp
-
-lemma even_not_iff [simp]:
-  "even (NOT k) \<longleftrightarrow> odd k"
-    for k :: int
-  by (simp add: not_int_def)
-
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
     by (induction n arbitrary: k)
       (simp_all add: not_int_def flip: complement_div_2)
 
 instance proof
   fix k l :: int and n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
   proof (rule sym, induction n arbitrary: k l)
     case 0
     then show ?case
       by (simp add: and_int.even_iff)
   next
     case (Suc n)
     with and_int.rec [of k l] show ?case
       by simp
   qed
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
   proof (rule sym, induction n arbitrary: k l)
     case 0
     then show ?case
       by (simp add: or_int.even_iff)
   next
     case (Suc n)
     with or_int.rec [of k l] show ?case
       by simp
   qed
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
   proof (rule sym, induction n arbitrary: k l)
     case 0
     then show ?case
       by (simp add: xor_int.even_iff)
   next
     case (Suc n)
     with xor_int.rec [of k l] show ?case
       by simp
   qed
 qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
 
 end
 
+lemma not_div_2:
+  "NOT k div 2 = NOT (k div 2)" for k :: int
+  by (simp add: complement_div_2 not_int_def)
+
+lemma not_int_rec [simp]:
+  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  by (auto simp add: not_int_def elim: oddE)
+
+lemma not_one_int [simp]:
+  "NOT 1 = (- 2 :: int)"
+  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+
+lemma even_not_int_iff [simp]:
+  "even (NOT k) \<longleftrightarrow> odd k" for k :: int
+  using bit_not_iff [of k 0] by auto
+
 lemma one_and_int_eq [simp]:
-  "1 AND k = k mod 2" for k :: int
-  by (simp add: bit_eq_iff bit_and_iff mod2_eq_if) (auto simp add: bit_1_iff)
+  "1 AND k = of_bool (odd k)" for k :: int
+  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
 lemma and_one_int_eq [simp]:
-  "k AND 1 = k mod 2" for k :: int
+  "k AND 1 = of_bool (odd k)" for k :: int
   using one_and_int_eq [of 1] by (simp add: ac_simps)
 
 lemma one_or_int_eq [simp]:
   "1 OR k = k + of_bool (even k)" for k :: int
   using or_int.rec [of 1] by (auto elim: oddE)
 
 lemma or_one_int_eq [simp]:
   "k OR 1 = k + of_bool (even k)" for k :: int
   using one_or_int_eq [of k] by (simp add: ac_simps)
 
 lemma one_xor_int_eq [simp]:
   "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int
   using xor_int.rec [of 1] by (auto elim: oddE)
 
 lemma xor_one_int_eq [simp]:
   "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int
   using one_xor_int_eq [of k] by (simp add: ac_simps)
 
 lemma take_bit_complement_iff:
   "take_bit n (complement k) = take_bit n (complement l) \<longleftrightarrow> take_bit n k = take_bit n l"
   for k l :: int
   by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
 
 lemma take_bit_not_iff_int:
   "take_bit n (NOT k) = take_bit n (NOT l) \<longleftrightarrow> take_bit n k = take_bit n l"
   for k l :: int
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
 
 end
diff --git a/src/HOL/ex/Word.thy b/src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy
+++ b/src/HOL/ex/Word.thy
@@ -1,708 +1,708 @@
 (*  Author:  Florian Haftmann, TUM
 *)
 
 section \<open>Proof of concept for algebraically founded bit word types\<close>
 
 theory Word
   imports
     Main
     "HOL-Library.Type_Length"
     "HOL-ex.Bit_Operations"
 begin
 
 subsection \<open>Preliminaries\<close>
 
 definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
   where signed_take_bit_eq_take_bit:
     "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
 
 lemma signed_take_bit_eq_take_bit':
   "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0"
   using that by (simp add: signed_take_bit_eq_take_bit)
 
 lemma signed_take_bit_0 [simp]:
   "signed_take_bit 0 k = - (k mod 2)"
 proof (cases "even k")
   case True
   then have "odd (k + 1)"
     by simp
   then have "(k + 1) mod 2 = 1"
     by (simp add: even_iff_mod_2_eq_zero)
   with True show ?thesis
     by (simp add: signed_take_bit_eq_take_bit)
 next
   case False
   then show ?thesis
     by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
 qed
 
 lemma signed_take_bit_Suc [simp]:
   "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
   by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
 
 lemma signed_take_bit_of_0 [simp]:
   "signed_take_bit n 0 = 0"
   by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod)
 
 lemma signed_take_bit_of_minus_1 [simp]:
   "signed_take_bit n (- 1) = - 1"
   by (induct n) simp_all
 
 lemma signed_take_bit_eq_iff_take_bit_eq:
   "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
   if "n > 0"
 proof -
   from that obtain m where m: "n = Suc m"
     by (cases n) auto
   show ?thesis
   proof
     assume ?Q
     have "take_bit (Suc m) (k + 2 ^ m) =
       take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
       by (simp only: take_bit_add)
     also have "\<dots> =
       take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
       by (simp only: \<open>?Q\<close> m [symmetric])
     also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
       by (simp only: take_bit_add)
     finally show ?P
       by (simp only: signed_take_bit_eq_take_bit m) simp
   next
     assume ?P
     with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
       by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod)
     then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
       by (metis mod_add_eq)
     then have "k mod 2 ^ n = l mod 2 ^ n"
       by (metis add_diff_cancel_right' uminus_add_conv_diff)
     then show ?Q
       by (simp add: take_bit_eq_mod)
   qed
 qed
 
 
 subsection \<open>Bit strings as quotient type\<close>
 
 subsubsection \<open>Basic properties\<close>
 
 quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l"
   by (auto intro!: equivpI reflpI sympI transpI)
 
 instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
 begin
 
 lift_definition zero_word :: "'a word"
   is 0
   .
 
 lift_definition one_word :: "'a word"
   is 1
   .
 
 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is plus
   by (subst take_bit_add [symmetric]) (simp add: take_bit_add)
 
 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   is uminus
   by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus)
 
 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is minus
   by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
 
 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is times
   by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
 
 instance
   by standard (transfer; simp add: algebra_simps)+
 
 end
 
 instance word :: (len) comm_ring_1
   by standard (transfer; simp)+
 
 quickcheck_generator word
   constructors:
     "zero_class.zero :: ('a::len0) word",
     "numeral :: num \<Rightarrow> ('a::len0) word",
     "uminus :: ('a::len0) word \<Rightarrow> ('a::len0) word"
 
 context
   includes lifting_syntax
   notes power_transfer [transfer_rule]
 begin
 
 lemma power_transfer_word [transfer_rule]:
   \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
   by transfer_prover
 
 end
 
 
 subsubsection \<open>Conversions\<close>
 
 context
   includes lifting_syntax
   notes 
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
     transfer_rule_of_nat [transfer_rule]
     transfer_rule_of_int [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_word) int of_nat"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_word) (\<lambda>k. k) of_int"
 proof -
   have "((=) ===> pcr_word) of_int of_int"
     by transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 end
 
 lemma abs_word_eq:
   "abs_word = of_int"
   by (rule ext) (transfer, rule)
 
 context semiring_1
 begin
 
 lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
   is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
   by simp
 
 lemma unsigned_0 [simp]:
   "unsigned 0 = 0"
   by transfer simp
 
 end
 
 context semiring_char_0
 begin
 
 lemma word_eq_iff_unsigned:
   "a = b \<longleftrightarrow> unsigned a = unsigned b"
   by safe (transfer; simp add: eq_nat_nat_iff)
 
 end
 
 instantiation word :: (len0) equal
 begin
 
 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
 
 instance proof
   fix a b :: "'a word"
   show "HOL.equal a b \<longleftrightarrow> a = b"
     using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def)
 qed
 
 end
 
 context ring_1
 begin
 
 lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
   by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
 
 lemma signed_0 [simp]:
   "signed 0 = 0"
   by transfer simp
 
 end
 
 lemma unsigned_of_nat [simp]:
   "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n"
   by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int)
 
 lemma of_nat_unsigned [simp]:
   "of_nat (unsigned a) = a"
   by transfer simp
 
 lemma of_int_unsigned [simp]:
   "of_int (unsigned a) = a"
   by transfer simp
 
 lemma unsigned_nat_less:
   \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len0 word\<close>
   by transfer (simp add: take_bit_eq_mod)
 
 lemma unsigned_int_less:
   \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len0 word\<close>
   by transfer (simp add: take_bit_eq_mod)
 
 context ring_char_0
 begin
 
 lemma word_eq_iff_signed:
   "a = b \<longleftrightarrow> signed a = signed b"
   by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq)
 
 end
 
 lemma signed_of_int [simp]:
   "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k"
   by transfer simp
 
 lemma of_int_signed [simp]:
   "of_int (signed a) = a"
   by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps)
 
 
 subsubsection \<open>Properties\<close>
 
 lemma exp_eq_zero_iff:
   \<open>(2 :: 'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a) \<le> n\<close>
   by transfer simp
 
 
 subsubsection \<open>Division\<close>
 
 instantiation word :: (len0) modulo
 begin
 
 lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
   by simp
 
 lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
   by simp
 
 instance ..
 
 end
 
 lemma zero_word_div_eq [simp]:
   \<open>0 div a = 0\<close> for a :: \<open>'a::len0 word\<close>
   by transfer simp
 
 lemma div_zero_word_eq [simp]:
   \<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
   by transfer simp
 
 context
   includes lifting_syntax
 begin
 
 lemma [transfer_rule]:
   "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
 proof -
   have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
     for k :: int
   proof
     assume ?P
     then show ?Q
       by auto
   next
     assume ?Q
     then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
     then have "even (take_bit LENGTH('a) k)"
       by simp
     then show ?P
       by simp
   qed
   show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
     transfer_prover
 qed
 
 end
 
 instance word :: (len) semiring_modulo
 proof
   show "a div b * b + a mod b = a" for a b :: "'a word"
   proof transfer
     fix k l :: int
     define r :: int where "r = 2 ^ LENGTH('a)"
     then have r: "take_bit LENGTH('a) k = k mod r" for k
       by (simp add: take_bit_eq_mod)
     have "k mod r = ((k mod r) div (l mod r) * (l mod r)
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: div_mult_mod_eq)
     also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: mod_add_left_eq)
     also have "... = (((k mod r) div (l mod r) * l) mod r
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: mod_mult_right_eq)
     finally have "k mod r = ((k mod r) div (l mod r) * l
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: mod_simps)
     with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
       + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
       by simp
   qed
 qed
 
 instance word :: (len) semiring_parity
 proof
   show "\<not> 2 dvd (1::'a word)"
     by transfer simp
   show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
     for a :: "'a word"
     by transfer (simp_all add: mod_2_eq_odd)
   show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
     for a :: "'a word"
     by transfer (simp_all add: mod_2_eq_odd)
 qed
 
 
 subsubsection \<open>Orderings\<close>
 
 instantiation word :: (len0) linorder
 begin
 
 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
   by simp
 
 lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
   by simp
 
 instance
   by standard (transfer; auto)+
 
 end
 
 context linordered_semidom
 begin
 
 lemma word_less_eq_iff_unsigned:
   "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
   by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
 
 lemma word_less_iff_unsigned:
   "a < b \<longleftrightarrow> unsigned a < unsigned b"
   by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
 
 end
 
 lemma word_greater_zero_iff:
   \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len0 word\<close>
   by transfer (simp add: less_le)
 
 lemma of_nat_word_eq_iff:
   \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)
 
 lemma of_nat_word_less_eq_iff:
   \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)
 
 lemma of_nat_word_less_iff:
   \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)
 
 lemma of_nat_word_eq_0_iff:
   \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
   using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
 
 lemma of_int_word_eq_iff:
   \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
   by transfer rule
 
 lemma of_int_word_less_eq_iff:
   \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
   by transfer rule
 
 lemma of_int_word_less_iff:
   \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
   by transfer rule
 
 lemma of_int_word_eq_0_iff:
   \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
   using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
 
 
 subsection \<open>Bit structure on \<^typ>\<open>'a word\<close>\<close>
 
 lemma word_bit_induct [case_names zero even odd]:
   \<open>P a\<close> if word_zero: \<open>P 0\<close>
     and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close>
     and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close>
   for P and a :: \<open>'a::len word\<close>
 proof -
   define m :: nat where \<open>m = LENGTH('a) - 1\<close>
   then have l: \<open>LENGTH('a) = Suc m\<close>
     by simp
   define n :: nat where \<open>n = unsigned a\<close>
   then have \<open>n < 2 ^ LENGTH('a)\<close>
     by (simp add: unsigned_nat_less)
   then have \<open>n < 2 * 2 ^ m\<close>
     by (simp add: l)
   then have \<open>P (of_nat n)\<close>
   proof (induction n rule: nat_bit_induct)
     case zero
     show ?case
       by simp (rule word_zero)
   next
     case (even n)
     then have \<open>n < 2 ^ m\<close>
       by simp
     with even.IH have \<open>P (of_nat n)\<close>
       by simp
     moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
       by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
     moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
       by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
     ultimately have \<open>P (2 * of_nat n)\<close>
       by (rule word_even)
     then show ?case
       by simp
   next
     case (odd n)
     then have \<open>Suc n \<le> 2 ^ m\<close>
       by simp
     with odd.IH have \<open>P (of_nat n)\<close>
       by simp
     moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
       by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
     ultimately have \<open>P (1 + 2 * of_nat n)\<close>
       by (rule word_odd)
     then show ?case
       by simp
   qed
   then show ?thesis
     by (simp add: n_def)
 qed
 
 lemma bit_word_half_eq:
   \<open>(of_bool b + a * 2) div 2 = a\<close>
     if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close>
     for a :: \<open>'a::len word\<close>
 proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
   case False
   have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
     by auto
   with False that show ?thesis
     by (auto; transfer) simp_all
 next
   case True
   obtain n where length: \<open>LENGTH('a) = Suc n\<close>
     by (cases \<open>LENGTH('a)\<close>) simp_all
   show ?thesis proof (cases b)
     case False
     moreover have \<open>a * 2 div 2 = a\<close>
     using that proof transfer
       fix k :: int
       from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close>
         by simp
       moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
       with \<open>LENGTH('a) = Suc n\<close>
       have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
         by (simp add: take_bit_eq_mod divmod_digit_0)
       ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
       with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
         by simp
     qed
     ultimately show ?thesis
       by simp
   next
     case True
     moreover have \<open>(1 + a * 2) div 2 = a\<close>
     using that proof transfer
       fix k :: int
       from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close>
         using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
       moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
       with \<open>LENGTH('a) = Suc n\<close>
       have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
         by (simp add: take_bit_eq_mod divmod_digit_0)
       ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
       with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
         by auto
     qed
     ultimately show ?thesis
       by simp
   qed
 qed
 
 lemma even_mult_exp_div_word_iff:
   \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> (
     m \<le> n \<and>
     n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
   by transfer
     (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
-      simp_all flip: push_bit_eq_mult add: bit_push_bit_eq_int)
+      simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
 
-(*lemma even_range_div_iff_word:
+(*lemma even_mask_div_iff_word:
   \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
-  by transfer (auto simp add: take_bit_of_range even_range_div_iff)*)
+  by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
 
 instance word :: (len) semiring_bits
 proof
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
   for P and a :: \<open>'a word\<close>
   proof (induction a rule: word_bit_induct)
     case zero
     from stable [of 0] show ?case
       by simp
   next
     case (even a)
     with rec [of a False] show ?case
       using bit_word_half_eq [of a False] by (simp add: ac_simps)
   next
     case (odd a)
     with rec [of a True] show ?case
       using bit_word_half_eq [of a True] by (simp add: ac_simps)
   qed
   show \<open>0 div a = 0\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
   show \<open>a div 1 = a\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
   show \<open>a mod b div b = 0\<close>
     for a b :: \<open>'a word\<close>
     apply transfer
     apply (simp add: take_bit_eq_mod)
     apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>])
       apply simp_all
      apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power)
     using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp
   proof -
     fix aa :: int and ba :: int
     have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n"
       by (metis le_less take_bit_eq_mod take_bit_nonnegative)
     have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
       by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power)
     then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
       using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound)
   qed
   show \<open>(1 + a) div 2 = a div 2\<close>
     if \<open>even a\<close>
     for a :: \<open>'a word\<close>
     using that by transfer (auto dest: le_Suc_ex)
   show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
     for m n :: nat
     by transfer (simp, simp add: exp_div_exp_eq)
   show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
     for a :: "'a word" and m n :: nat
     apply transfer
     apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div)
     apply (simp add: drop_bit_take_bit)
     done
   show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
     for a :: "'a word" and m n :: nat
     by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
   show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
     if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
     using that apply transfer
     apply (auto simp flip: take_bit_eq_mod)
            apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin)
     done
   show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
     for a :: "'a word" and m n :: nat
     by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
 qed
 
 context
   includes lifting_syntax
 begin
 
 lemma transfer_rule_bit_word [transfer_rule]:
   \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
 proof -
   let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
   have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
     by (unfold bit_def) transfer_prover
   also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
     by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
   finally show ?thesis .
 qed
 
 end
 
 instantiation word :: (len) semiring_bit_shifts
 begin
 
 lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is push_bit
 proof -
   show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
     if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
   proof -
     from that
     have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
       = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
       by simp
     moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
       by simp
     ultimately show ?thesis
       by (simp add: take_bit_push_bit)
   qed
 qed
 
 lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
   by (simp add: take_bit_eq_mod)
 
 instance proof
   show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
     by transfer (simp add: push_bit_eq_mult)
   show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
     by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
 qed
 
 end
 
 instantiation word :: (len) ring_bit_operations
 begin
 
 lift_definition not_word :: "'a word \<Rightarrow> 'a word"
   is not
   by (simp add: take_bit_not_iff_int)
 
 lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is \<open>and\<close>
   by simp
 
 lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is or
   by simp
 
 lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is xor
   by simp
 
 instance proof
   fix a b :: \<open>'a word\<close> and n :: nat
   show \<open>- a = NOT (a - 1)\<close>
     by transfer (simp add: minus_eq_not_minus_1)
   show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
     by transfer (simp add: bit_not_iff)
   show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
     by transfer (auto simp add: bit_and_iff)
   show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
     by transfer (auto simp add: bit_or_iff)
   show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
     by transfer (auto simp add: bit_xor_iff)
 qed
 
 end
 
 end