diff --git a/src/HOL/Code_Numeral.thy b/src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy
+++ b/src/HOL/Code_Numeral.thy
@@ -1,1176 +1,1180 @@
 (*  Title:      HOL/Code_Numeral.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 section \<open>Numeric types for code generation onto target language numerals only\<close>
 
 theory Code_Numeral
 imports Divides Lifting
 begin
 
 subsection \<open>Type of target language integers\<close>
 
 typedef integer = "UNIV :: int set"
   morphisms int_of_integer integer_of_int ..
 
 setup_lifting type_definition_integer
 
 lemma integer_eq_iff:
   "k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
   by transfer rule
 
 lemma integer_eqI:
   "int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
   using integer_eq_iff [of k l] by simp
 
 lemma int_of_integer_integer_of_int [simp]:
   "int_of_integer (integer_of_int k) = k"
   by transfer rule
 
 lemma integer_of_int_int_of_integer [simp]:
   "integer_of_int (int_of_integer k) = k"
   by transfer rule
 
 instantiation integer :: ring_1
 begin
 
 lift_definition zero_integer :: integer
   is "0 :: int"
   .
 
 declare zero_integer.rep_eq [simp]
 
 lift_definition one_integer :: integer
   is "1 :: int"
   .
 
 declare one_integer.rep_eq [simp]
 
 lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "plus :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare plus_integer.rep_eq [simp]
 
 lift_definition uminus_integer :: "integer \<Rightarrow> integer"
   is "uminus :: int \<Rightarrow> int"
   .
 
 declare uminus_integer.rep_eq [simp]
 
 lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "minus :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare minus_integer.rep_eq [simp]
 
 lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "times :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare times_integer.rep_eq [simp]
 
 instance proof
 qed (transfer, simp add: algebra_simps)+
 
 end
 
 instance integer :: Rings.dvd ..
 
 context
   includes lifting_syntax
   notes transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "(pcr_integer ===> pcr_integer ===> (\<longleftrightarrow>)) (dvd) (dvd)"
   by (unfold dvd_def) transfer_prover
 
 lemma [transfer_rule]:
   "((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
   by (unfold of_bool_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_integer) int of_nat"
   by (rule transfer_rule_of_nat) transfer_prover+
 
 lemma [transfer_rule]:
   "((=) ===> pcr_integer) (\<lambda>k. k) of_int"
 proof -
   have "((=) ===> pcr_integer) of_int of_int"
     by (rule transfer_rule_of_int) transfer_prover+
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
   "((=) ===> pcr_integer) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
   "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
   by (unfold power_def [abs_def]) transfer_prover
 
 end
 
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"
   by transfer rule
 
 lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
   is "of_nat :: nat \<Rightarrow> int"
   .
 
 lemma integer_of_nat_eq_of_nat [code]:
   "integer_of_nat = of_nat"
   by transfer rule
 
 lemma int_of_integer_integer_of_nat [simp]:
   "int_of_integer (integer_of_nat n) = of_nat n"
   by transfer rule
 
 lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
   is Int.nat
   .
 
 lemma nat_of_integer_of_nat [simp]:
   "nat_of_integer (of_nat n) = n"
   by transfer simp
 
 lemma int_of_integer_of_int [simp]:
   "int_of_integer (of_int k) = k"
   by transfer simp
 
 lemma nat_of_integer_integer_of_nat [simp]:
   "nat_of_integer (integer_of_nat n) = n"
   by transfer simp
 
 lemma integer_of_int_eq_of_int [simp, code_abbrev]:
   "integer_of_int = of_int"
   by transfer (simp add: fun_eq_iff)
 
 lemma of_int_integer_of [simp]:
   "of_int (int_of_integer k) = (k :: integer)"
   by transfer rule
 
 lemma int_of_integer_numeral [simp]:
   "int_of_integer (numeral k) = numeral k"
   by transfer rule
 
 lemma int_of_integer_sub [simp]:
   "int_of_integer (Num.sub k l) = Num.sub k l"
   by transfer rule
 
 definition integer_of_num :: "num \<Rightarrow> integer"
   where [simp]: "integer_of_num = numeral"
 
 lemma integer_of_num [code]:
   "integer_of_num Num.One = 1"
   "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
   "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
   by (simp_all only: integer_of_num_def numeral.simps Let_def)
 
 lemma integer_of_num_triv:
   "integer_of_num Num.One = 1"
   "integer_of_num (Num.Bit0 Num.One) = 2"
   by simp_all
 
 instantiation integer :: "{linordered_idom, equal}"
 begin
 
 lift_definition abs_integer :: "integer \<Rightarrow> integer"
   is "abs :: int \<Rightarrow> int"
   .
 
 declare abs_integer.rep_eq [simp]
 
 lift_definition sgn_integer :: "integer \<Rightarrow> integer"
   is "sgn :: int \<Rightarrow> int"
   .
 
 declare sgn_integer.rep_eq [simp]
 
 lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
   .
 
 lemma integer_less_eq_iff:
   "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
   by (fact less_eq_integer.rep_eq)
 
 lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   is "less :: int \<Rightarrow> int \<Rightarrow> bool"
   .
 
 lemma integer_less_iff:
   "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
   by (fact less_integer.rep_eq)
 
 lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
   .
 
 instance
   by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
 
 end
 
 lemma [transfer_rule]:
   "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
   "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma int_of_integer_min [simp]:
   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
   by transfer rule
 
 lemma int_of_integer_max [simp]:
   "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
   by transfer rule
 
 lemma nat_of_integer_non_positive [simp]:
   "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
   by transfer simp
 
 lemma of_nat_of_integer [simp]:
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
 instantiation integer :: unique_euclidean_ring
 begin
 
 lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "divide :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare divide_integer.rep_eq [simp]
 
 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare modulo_integer.rep_eq [simp]
 
 lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
   is "euclidean_size :: int \<Rightarrow> nat"
   .
 
 declare euclidean_size_integer.rep_eq [simp]
 
 lift_definition division_segment_integer :: "integer \<Rightarrow> integer"
   is "division_segment :: int \<Rightarrow> int"
   .
 
 declare division_segment_integer.rep_eq [simp]
 
 instance
   by (standard; transfer)
     (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib
      division_segment_mult division_segment_mod intro: div_eqI\<close>)
 
 end
 
 lemma [code]:
   "euclidean_size = nat_of_integer \<circ> abs"
   by (simp add: fun_eq_iff nat_of_integer.rep_eq)
 
 lemma [code]:
   "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
   by transfer (simp add: division_segment_int_def)
 
 instance integer :: unique_euclidean_ring_with_nat
   by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
 
 instantiation integer :: semiring_bit_shifts
 begin
 
 lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
   is \<open>push_bit\<close> .
 
 lift_definition drop_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
   is \<open>drop_bit\<close> .
 
 instance by (standard; transfer)
-  (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+  (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+    div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
 
 lemma [transfer_rule]:
   "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold take_bit_eq_mod [abs_def]) transfer_prover
 
 instance integer :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
   \<open>push_bit n k = k * 2 ^ n\<close>
   \<open>drop_bit n k = k div 2 ^ n\<close> for k :: integer
   by (fact push_bit_eq_mult drop_bit_eq_div)+
 
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
 where
   divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
 
 definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_step_integer l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
 
 instance proof
   show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
     for m n by (fact divmod_integer'_def)
   show "divmod_step l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))" for l and qr :: "integer \<times> integer"
     by (fact divmod_step_integer_def)
 qed (transfer,
   fact le_add_diff_inverse2
   unique_euclidean_semiring_numeral_class.div_less
   unique_euclidean_semiring_numeral_class.mod_less
   unique_euclidean_semiring_numeral_class.div_positive
   unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
   unique_euclidean_semiring_numeral_class.pos_mod_bound
   unique_euclidean_semiring_numeral_class.pos_mod_sign
   unique_euclidean_semiring_numeral_class.mod_mult2_eq
   unique_euclidean_semiring_numeral_class.div_mult2_eq
   unique_euclidean_semiring_numeral_class.discrete)+
 
 end
 
 declare divmod_algorithm_code [where ?'a = integer,
   folded integer_of_num_def, unfolded integer_of_num_triv,
   code]
 
 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
 by transfer simp
 
 lemma integer_of_nat_1: "integer_of_nat 1 = 1"
 by transfer simp
 
 lemma integer_of_nat_numeral:
   "integer_of_nat (numeral n) = numeral n"
 by transfer simp
 
 
 subsection \<open>Code theorems for target language integers\<close>
 
 text \<open>Constructors\<close>
 
 definition Pos :: "num \<Rightarrow> integer"
 where
   [simp, code_post]: "Pos = numeral"
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer numeral Pos"
   by simp transfer_prover
 
 lemma Pos_fold [code_unfold]:
   "numeral Num.One = Pos Num.One"
   "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
   "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"
   by simp_all
 
 definition Neg :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Neg n = - Pos n"
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
   by (simp add: Neg_def [abs_def]) transfer_prover
 
 code_datatype "0::integer" Pos Neg
 
   
 text \<open>A further pair of constructors for generated computations\<close>
 
 context
 begin  
 
 qualified definition positive :: "num \<Rightarrow> integer"
   where [simp]: "positive = numeral"
 
 qualified definition negative :: "num \<Rightarrow> integer"
   where [simp]: "negative = uminus \<circ> numeral"
 
 lemma [code_computation_unfold]:
   "numeral = positive"
   "Pos = positive"
   "Neg = negative"
   by (simp_all add: fun_eq_iff)
 
 end
 
 
 text \<open>Auxiliary operations\<close>
 
 lift_definition dup :: "integer \<Rightarrow> integer"
   is "\<lambda>k::int. k + k"
   .
 
 lemma dup_code [code]:
   "dup 0 = 0"
   "dup (Pos n) = Pos (Num.Bit0 n)"
   "dup (Neg n) = Neg (Num.Bit0 n)"
   by (transfer, simp only: numeral_Bit0 minus_add_distrib)+
 
 lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
   is "\<lambda>m n. numeral m - numeral n :: int"
   .
 
 lemma sub_code [code]:
   "sub Num.One Num.One = 0"
   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
 
 
 text \<open>Implementations\<close>
 
 lemma one_integer_code [code, code_unfold]:
   "1 = Pos Num.One"
   by simp
 
 lemma plus_integer_code [code]:
   "k + 0 = (k::integer)"
   "0 + l = (l::integer)"
   "Pos m + Pos n = Pos (m + n)"
   "Pos m + Neg n = sub m n"
   "Neg m + Pos n = sub n m"
   "Neg m + Neg n = Neg (m + n)"
   by (transfer, simp)+
 
 lemma uminus_integer_code [code]:
   "uminus 0 = (0::integer)"
   "uminus (Pos m) = Neg m"
   "uminus (Neg m) = Pos m"
   by simp_all
 
 lemma minus_integer_code [code]:
   "k - 0 = (k::integer)"
   "0 - l = uminus (l::integer)"
   "Pos m - Pos n = sub m n"
   "Pos m - Neg n = Pos (m + n)"
   "Neg m - Pos n = Neg (m + n)"
   "Neg m - Neg n = sub n m"
   by (transfer, simp)+
 
 lemma abs_integer_code [code]:
   "\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
   by simp
 
 lemma sgn_integer_code [code]:
   "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)"
   by simp
 
 lemma times_integer_code [code]:
   "k * 0 = (0::integer)"
   "0 * l = (0::integer)"
   "Pos m * Pos n = Pos (m * n)"
   "Pos m * Neg n = Neg (m * n)"
   "Neg m * Pos n = Neg (m * n)"
   "Neg m * Neg n = Pos (m * n)"
   by simp_all
 
 definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_integer k l = (k div l, k mod l)"
 
 lemma fst_divmod_integer [simp]:
   "fst (divmod_integer k l) = k div l"
   by (simp add: divmod_integer_def)
 
 lemma snd_divmod_integer [simp]:
   "snd (divmod_integer k l) = k mod l"
   by (simp add: divmod_integer_def)
 
 definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
 
 lemma fst_divmod_abs [simp]:
   "fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>"
   by (simp add: divmod_abs_def)
 
 lemma snd_divmod_abs [simp]:
   "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
   by (simp add: divmod_abs_def)
 
 lemma divmod_abs_code [code]:
   "divmod_abs (Pos k) (Pos l) = divmod k l"
   "divmod_abs (Neg k) (Neg l) = divmod k l"
   "divmod_abs (Neg k) (Pos l) = divmod k l"
   "divmod_abs (Pos k) (Neg l) = divmod k l"
   "divmod_abs j 0 = (0, \<bar>j\<bar>)"
   "divmod_abs 0 j = (0, 0)"
   by (simp_all add: prod_eq_iff)
 
 lemma divmod_integer_eq_cases:
   "divmod_integer k l =
     (if k = 0 then (0, 0) else if l = 0 then (0, k) else
     (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
       then divmod_abs k l
       else (let (r, s) = divmod_abs k l in
         if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
 proof -
   have *: "sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" for k l :: int
     by (auto simp add: sgn_if)
   have **: "- k = l * q \<longleftrightarrow> k = - (l * q)" for k l q :: int
     by auto
   show ?thesis
     by (simp add: divmod_integer_def divmod_abs_def)
       (transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right)
 qed
 
 lemma divmod_integer_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
   "divmod_integer k l =
    (if k = 0 then (0, 0)
     else if l > 0 then
             (if k > 0 then Code_Numeral.divmod_abs k l
              else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
                   if s = 0 then (- r, 0) else (- r - 1, l - s))
     else if l = 0 then (0, k)
     else apsnd uminus
             (if k < 0 then Code_Numeral.divmod_abs k l
              else case Code_Numeral.divmod_abs k l of (r, s) \<Rightarrow>
                   if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
   by (cases l "0 :: integer" rule: linorder_cases)
     (auto split: prod.splits simp add: divmod_integer_eq_cases)
 
 lemma div_integer_code [code]:
   "k div l = fst (divmod_integer k l)"
   by simp
 
 lemma mod_integer_code [code]:
   "k mod l = snd (divmod_integer k l)"
   by simp
 
 definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool"
   where "bit_cut_integer k = (k div 2, odd k)"
 
 lemma bit_cut_integer_code [code]:
   "bit_cut_integer k = (if k = 0 then (0, False)
      else let (r, s) = Code_Numeral.divmod_abs k 2
        in (if k > 0 then r else - r - s, s = 1))"
 proof -
   have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))"
     by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one)
   then show ?thesis
     by (simp add: divmod_integer_code) (auto simp add: split_def)
 qed
 
 lemma equal_integer_code [code]:
   "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
   by (simp_all add: equal)
 
 lemma equal_integer_refl [code nbe]:
   "HOL.equal (k::integer) k \<longleftrightarrow> True"
   by (fact equal_refl)
 
 lemma less_eq_integer_code [code]:
   "0 \<le> (0::integer) \<longleftrightarrow> True"
   "0 \<le> Pos l \<longleftrightarrow> True"
   "0 \<le> Neg l \<longleftrightarrow> False"
   "Pos k \<le> 0 \<longleftrightarrow> False"
   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
   "Pos k \<le> Neg l \<longleftrightarrow> False"
   "Neg k \<le> 0 \<longleftrightarrow> True"
   "Neg k \<le> Pos l \<longleftrightarrow> True"
   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
   by simp_all
 
 lemma less_integer_code [code]:
   "0 < (0::integer) \<longleftrightarrow> False"
   "0 < Pos l \<longleftrightarrow> True"
   "0 < Neg l \<longleftrightarrow> False"
   "Pos k < 0 \<longleftrightarrow> False"
   "Pos k < Pos l \<longleftrightarrow> k < l"
   "Pos k < Neg l \<longleftrightarrow> False"
   "Neg k < 0 \<longleftrightarrow> True"
   "Neg k < Pos l \<longleftrightarrow> True"
   "Neg k < Neg l \<longleftrightarrow> l < k"
   by simp_all
 
 lift_definition num_of_integer :: "integer \<Rightarrow> num"
   is "num_of_nat \<circ> nat"
   .
 
 lemma num_of_integer_code [code]:
   "num_of_integer k = (if k \<le> 1 then Num.One
      else let
        (l, j) = divmod_integer k 2;
        l' = num_of_integer l;
        l'' = l' + l'
      in if j = 0 then l'' else l'' + Num.One)"
 proof -
   {
     assume "int_of_integer k mod 2 = 1"
     then have "nat (int_of_integer k mod 2) = nat 1" by simp
     moreover assume *: "1 < int_of_integer k"
     ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib)
     have "num_of_nat (nat (int_of_integer k)) =
       num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)"
       by simp
     then have "num_of_nat (nat (int_of_integer k)) =
       num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)"
       by (simp add: mult_2)
     with ** have "num_of_nat (nat (int_of_integer k)) =
       num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)"
       by simp
   }
   note aux = this
   show ?thesis
     by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
       not_le integer_eq_iff less_eq_integer_def
       nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
        mult_2 [where 'a=nat] aux add_One)
 qed
 
 lemma nat_of_integer_code [code]:
   "nat_of_integer k = (if k \<le> 0 then 0
      else let
        (l, j) = divmod_integer k 2;
        l' = nat_of_integer l;
        l'' = l' + l'
      in if j = 0 then l'' else l'' + 1)"
 proof -
   obtain j where k: "k = integer_of_int j"
   proof
     show "k = integer_of_int (int_of_integer k)" by simp
   qed
   have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \<ge> 0"
     using that by transfer (simp add: nat_mod_distrib)
   from k show ?thesis
     by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
       minus_mod_eq_mult_div [symmetric] *)
 qed
 
 lemma int_of_integer_code [code]:
   "int_of_integer k = (if k < 0 then - (int_of_integer (- k))
      else if k = 0 then 0
      else let
        (l, j) = divmod_integer k 2;
        l' = 2 * int_of_integer l
      in if j = 0 then l' else l' + 1)"
   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
 lemma integer_of_int_code [code]:
   "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
      else if k = 0 then 0
      else let
        l = 2 * integer_of_int (k div 2);
        j = k mod 2
      in if j = 0 then l else l + 1)"
   by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
 hide_const (open) Pos Neg sub dup divmod_abs
 
 
 subsection \<open>Serializer setup for target language integers\<close>
 
 code_reserved Eval int Integer abs
 
 code_printing
   type_constructor integer \<rightharpoonup>
     (SML) "IntInf.int"
     and (OCaml) "Z.t"
     and (Haskell) "Integer"
     and (Scala) "BigInt"
     and (Eval) "int"
 | class_instance integer :: equal \<rightharpoonup>
     (Haskell) -
 
 code_printing
   constant "0::integer" \<rightharpoonup>
     (SML) "!(0/ :/ IntInf.int)"
     and (OCaml) "Z.zero"
     and (Haskell) "!(0/ ::/ Integer)"
     and (Scala) "BigInt(0)"
 
 setup \<open>
   fold (fn target =>
     Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I Code_Printer.literal_numeral target
     #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) Code_Printer.literal_numeral target)
     ["SML", "OCaml", "Haskell", "Scala"]
 \<close>
 
 code_printing
   constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.+ ((_), (_))"
     and (OCaml) "Z.add"
     and (Haskell) infixl 6 "+"
     and (Scala) infixl 7 "+"
     and (Eval) infixl 8 "+"
 | constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.~"
     and (OCaml) "Z.neg"
     and (Haskell) "negate"
     and (Scala) "!(- _)"
     and (Eval) "~/ _"
 | constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.- ((_), (_))"
     and (OCaml) "Z.sub"
     and (Haskell) infixl 6 "-"
     and (Scala) infixl 7 "-"
     and (Eval) infixl 8 "-"
 | constant Code_Numeral.dup \<rightharpoonup>
     (SML) "IntInf.*/ (2,/ (_))"
     and (OCaml) "Z.shift'_left/ _/ 1"
     and (Haskell) "!(2 * _)"
     and (Scala) "!(2 * _)"
     and (Eval) "!(2 * _)"
 | constant Code_Numeral.sub \<rightharpoonup>
     (SML) "!(raise/ Fail/ \"sub\")"
     and (OCaml) "failwith/ \"sub\""
     and (Haskell) "error/ \"sub\""
     and (Scala) "!sys.error(\"sub\")"
 | constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.* ((_), (_))"
     and (OCaml) "Z.mul"
     and (Haskell) infixl 7 "*"
     and (Scala) infixl 8 "*"
     and (Eval) infixl 9 "*"
 | constant Code_Numeral.divmod_abs \<rightharpoonup>
     (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
     and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))"
     and (Haskell) "divMod/ (abs _)/ (abs _)"
     and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
     and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
 | constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : IntInf.int) = _)"
     and (OCaml) "Z.equal"
     and (Haskell) infix 4 "=="
     and (Scala) infixl 5 "=="
     and (Eval) infixl 6 "="
 | constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
     (SML) "IntInf.<= ((_), (_))"
     and (OCaml) "Z.leq"
     and (Haskell) infix 4 "<="
     and (Scala) infixl 4 "<="
     and (Eval) infixl 6 "<="
 | constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
     (SML) "IntInf.< ((_), (_))"
     and (OCaml) "Z.lt"
     and (Haskell) infix 4 "<"
     and (Scala) infixl 4 "<"
     and (Eval) infixl 6 "<"
 | constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.abs"
     and (OCaml) "Z.abs"
     and (Haskell) "Prelude.abs"
     and (Scala) "_.abs"
     and (Eval) "abs"
 
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 
 subsection \<open>Type of target language naturals\<close>
 
 typedef natural = "UNIV :: nat set"
   morphisms nat_of_natural natural_of_nat ..
 
 setup_lifting type_definition_natural
 
 lemma natural_eq_iff [termination_simp]:
   "m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
   by transfer rule
 
 lemma natural_eqI:
   "nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
   using natural_eq_iff [of m n] by simp
 
 lemma nat_of_natural_of_nat_inverse [simp]:
   "nat_of_natural (natural_of_nat n) = n"
   by transfer rule
 
 lemma natural_of_nat_of_natural_inverse [simp]:
   "natural_of_nat (nat_of_natural n) = n"
   by transfer rule
 
 instantiation natural :: "{comm_monoid_diff, semiring_1}"
 begin
 
 lift_definition zero_natural :: natural
   is "0 :: nat"
   .
 
 declare zero_natural.rep_eq [simp]
 
 lift_definition one_natural :: natural
   is "1 :: nat"
   .
 
 declare one_natural.rep_eq [simp]
 
 lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
 declare plus_natural.rep_eq [simp]
 
 lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
 declare minus_natural.rep_eq [simp]
 
 lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
 declare times_natural.rep_eq [simp]
 
 instance proof
 qed (transfer, simp add: algebra_simps)+
 
 end
 
 instance natural :: Rings.dvd ..
 
 lemma [transfer_rule]:
   "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
   unfolding dvd_def by transfer_prover
 
 lemma [transfer_rule]:
   "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)"
   by (unfold of_bool_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
 proof -
   have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
     by (unfold of_nat_def [abs_def]) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
 proof -
   have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
     by transfer_prover
   then show ?thesis by simp
 qed
 
 lemma [transfer_rule]:
   "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold power_def [abs_def]) transfer_prover
 
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
   by transfer rule
 
 lemma natural_of_nat_of_nat [simp, code_abbrev]:
   "natural_of_nat = of_nat"
   by transfer rule
 
 lemma of_nat_of_natural [simp]:
   "of_nat (nat_of_natural n) = n"
   by transfer rule
 
 lemma nat_of_natural_numeral [simp]:
   "nat_of_natural (numeral k) = numeral k"
   by transfer rule
 
 instantiation natural :: "{linordered_semiring, equal}"
 begin
 
 lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   .
 
 declare less_eq_natural.rep_eq [termination_simp]
 
 lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
   .
 
 declare less_natural.rep_eq [termination_simp]
 
 lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
   .
 
 instance proof
 qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
 
 end
 
 lemma [transfer_rule]:
   "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold min_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
   "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold max_def [abs_def]) transfer_prover
 
 lemma nat_of_natural_min [simp]:
   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
   by transfer rule
 
 lemma nat_of_natural_max [simp]:
   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   by transfer rule
 
 instantiation natural :: unique_euclidean_semiring
 begin
 
 lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
 declare divide_natural.rep_eq [simp]
 
 lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
 
 declare modulo_natural.rep_eq [simp]
 
 lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
   is "euclidean_size :: nat \<Rightarrow> nat"
   .
 
 declare euclidean_size_natural.rep_eq [simp]
 
 lift_definition division_segment_natural :: "natural \<Rightarrow> natural"
   is "division_segment :: nat \<Rightarrow> nat"
   .
 
 declare division_segment_natural.rep_eq [simp]
 
 instance
   by (standard; transfer)
     (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
 
 end
 
 lemma [code]:
   "euclidean_size = nat_of_natural"
   by (simp add: fun_eq_iff)
 
 lemma [code]:
   "division_segment (n::natural) = 1"
   by (simp add: natural_eq_iff)
 
 instance natural :: linordered_semidom
   by (standard; transfer) simp_all
 
 instance natural :: unique_euclidean_semiring_with_nat
   by (standard; transfer) simp_all
 
 instantiation natural :: semiring_bit_shifts
 begin
 
 lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
   is \<open>push_bit\<close> .
 
 lift_definition drop_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
   is \<open>drop_bit\<close> .
 
 instance by (standard; transfer)
-  (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+
+  (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
+    div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
 
 lemma [transfer_rule]:
   "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
   by (unfold take_bit_eq_mod [abs_def]) transfer_prover
 
 instance natural :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
   \<open>push_bit n m = m * 2 ^ n\<close>
   \<open>drop_bit n m = m div 2 ^ n\<close> for m :: natural
   by (fact push_bit_eq_mult drop_bit_eq_div)+
 
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .
 
 lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
   is "of_nat :: nat \<Rightarrow> int"
   .
 
 lemma natural_of_integer_of_natural [simp]:
   "natural_of_integer (integer_of_natural n) = n"
   by transfer simp
 
 lemma integer_of_natural_of_integer [simp]:
   "integer_of_natural (natural_of_integer k) = max 0 k"
   by transfer auto
 
 lemma int_of_integer_of_natural [simp]:
   "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
   by transfer rule
 
 lemma integer_of_natural_of_nat [simp]:
   "integer_of_natural (of_nat n) = of_nat n"
   by transfer rule
 
 lemma [measure_function]:
   "is_measure nat_of_natural"
   by (rule is_measure_trivial)
 
 
 subsection \<open>Inductive representation of target language naturals\<close>
 
 lift_definition Suc :: "natural \<Rightarrow> natural"
   is Nat.Suc
   .
 
 declare Suc.rep_eq [simp]
 
 old_rep_datatype "0::natural" Suc
   by (transfer, fact nat.induct nat.inject nat.distinct)+
 
 lemma natural_cases [case_names nat, cases type: natural]:
   fixes m :: natural
   assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
   shows P
   using assms by transfer blast
 
 instantiation natural :: size
 begin
 
 definition size_nat where [simp, code]: "size_nat = nat_of_natural"
 
 instance ..
 
 end
 
 lemma natural_decr [termination_simp]:
   "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
   by transfer simp
 
 lemma natural_zero_minus_one: "(0::natural) - 1 = 0"
   by (rule zero_diff)
 
 lemma Suc_natural_minus_one: "Suc n - 1 = n"
   by transfer simp
 
 hide_const (open) Suc
 
 
 subsection \<open>Code refinement for target language naturals\<close>
 
 lift_definition Nat :: "integer \<Rightarrow> natural"
   is nat
   .
 
 lemma [code_post]:
   "Nat 0 = 0"
   "Nat 1 = 1"
   "Nat (numeral k) = numeral k"
   by (transfer, simp)+
 
 lemma [code abstype]:
   "Nat (integer_of_natural n) = n"
   by transfer simp
 
 lemma [code]:
   "natural_of_nat n = natural_of_integer (integer_of_nat n)"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (natural_of_integer k) = max 0 k"
   by simp
 
 lemma [code_abbrev]:
   "natural_of_integer (Code_Numeral.Pos k) = numeral k"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 0 = 0"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural 1 = 1"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1"
   by transfer simp
 
 lemma [code]:
   "nat_of_natural = nat_of_integer \<circ> integer_of_natural"
   by transfer (simp add: fun_eq_iff)
 
 lemma [code, code_unfold]:
   "case_natural f g n = (if n = 0 then f else g (n - 1))"
   by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
 
 declare natural.rec [code del]
 
 lemma [code abstract]:
   "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
   by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
   by transfer (simp add: zdiv_int)
 
 lemma [code abstract]:
   "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
   by transfer (simp add: zmod_int)
 
 lemma [code]:
   "HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
   by transfer (simp add: equal)
 
 lemma [code nbe]: "HOL.equal n (n::natural) \<longleftrightarrow> True"
   by (rule equal_class.equal_refl)
 
 lemma [code]: "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
   by transfer simp
 
 lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
   by transfer simp
 
 hide_const (open) Nat
 
 lifting_update integer.lifting
 lifting_forget integer.lifting
 
 lifting_update natural.lifting
 lifting_forget natural.lifting
 
 code_reflect Code_Numeral
   datatypes natural
   functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
     "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
     "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
     "modulo :: natural \<Rightarrow> _"
     integer_of_natural natural_of_integer
 
 end
diff --git a/src/HOL/Divides.thy b/src/HOL/Divides.thy
--- a/src/HOL/Divides.thy
+++ b/src/HOL/Divides.thy
@@ -1,1349 +1,1329 @@
 (*  Title:      HOL/Divides.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 *)
 
 section \<open>More on quotient and remainder\<close>
 
 theory Divides
 imports Parity
 begin
 
 subsection \<open>More on division\<close>
 
 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
 
 lemma eucl_rel_int_iff:    
   "eucl_rel_int k l (q, r) \<longleftrightarrow> 
     k = l * q + r \<and>
      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
   by (cases "r = 0")
     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
     simp add: ac_simps sgn_1_pos sgn_1_neg)
 
 lemma unique_quotient_lemma:
   assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)"
 proof -
   have "r' + b * (q'-q) \<le> r"
     using assms by (simp add: right_diff_distrib)
   moreover have "0 < b * (1 + q - q') "
     using assms by (simp add: right_diff_distrib distrib_left)
   moreover have "b * q' < b * (1 + q)"
     using assms by (simp add: right_diff_distrib distrib_left)
   ultimately show ?thesis
     using assms by (simp add: mult_less_cancel_left)
 qed
 
 lemma unique_quotient_lemma_neg:
   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
 
 lemma unique_quotient:
   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
   apply (rule order_antisym)
    apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
      apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   done
 
 lemma unique_remainder:
   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
 apply (subgoal_tac "q = q'")
  apply (simp add: eucl_rel_int_iff)
 apply (blast intro: unique_quotient)
 done
 
 lemma eucl_rel_int:
   "eucl_rel_int k l (k div l, k mod l)"
 proof (cases k rule: int_cases3)
   case zero
   then show ?thesis
     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
 next
   case (pos n)
   then show ?thesis
     using div_mult_mod_eq [of n]
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
         eucl_rel_int_iff divide_int_def modulo_int_def)
 next
   case (neg n)
   then show ?thesis
     using div_mult_mod_eq [of n]
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
         eucl_rel_int_iff divide_int_def modulo_int_def)
 qed
 
 lemma divmod_int_unique:
   assumes "eucl_rel_int k l (q, r)"
   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   using assms eucl_rel_int [of k l]
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
 
 lemma div_abs_eq_div_nat:
   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
   by (simp add: divide_int_def)
 
 lemma mod_abs_eq_div_nat:
   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
   by (simp add: modulo_int_def)
 
 lemma zdiv_int:
   "int (a div b) = int a div int b"
   by (simp add: divide_int_def)
 
 lemma zmod_int:
   "int (a mod b) = int a mod int b"
   by (simp add: modulo_int_def)
 
 lemma div_sgn_abs_cancel:
   fixes k l v :: int
   assumes "v \<noteq> 0"
   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
 proof -
   from assms have "sgn v = - 1 \<or> sgn v = 1"
     by (cases "v \<ge> 0") auto
   then show ?thesis
     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
     by (fastforce simp add: not_less div_abs_eq_div_nat)
 qed
 
 lemma div_eq_sgn_abs:
   fixes k l v :: int
   assumes "sgn k = sgn l"
   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
 proof (cases "l = 0")
   case True
   then show ?thesis
     by simp
 next
   case False
   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
     using div_sgn_abs_cancel [of l k l] by simp
   then show ?thesis
     by (simp add: sgn_mult_abs)
 qed
 
 lemma div_dvd_sgn_abs:
   fixes k l :: int
   assumes "l dvd k"
   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
 proof (cases "k = 0 \<or> l = 0")
   case True
   then show ?thesis
     by auto
 next
   case False
   then have "k \<noteq> 0" and "l \<noteq> 0"
     by auto
   show ?thesis
   proof (cases "sgn l = sgn k")
     case True
     then show ?thesis
       by (simp add: div_eq_sgn_abs)
   next
     case False
     with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
     have "sgn l * sgn k = - 1"
       by (simp add: sgn_if split: if_splits)
     with assms show ?thesis
       unfolding divide_int_def [of k l]
       by (auto simp add: zdiv_int ac_simps)
   qed
 qed
 
 lemma div_noneq_sgn_abs:
   fixes k l :: int
   assumes "l \<noteq> 0"
   assumes "sgn k \<noteq> sgn l"
   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
   using assms
   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   
 
 subsubsection \<open>General Properties of div and mod\<close>
 
 lemma div_pos_pos_trivial [simp]:
   "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
   using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
 
 lemma mod_pos_pos_trivial [simp]:
   "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
   using that by (simp add: mod_eq_self_iff_div_eq_0)
 
 lemma div_neg_neg_trivial [simp]:
   "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
   using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
 
 lemma mod_neg_neg_trivial [simp]:
   "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
   using that by (simp add: mod_eq_self_iff_div_eq_0)
 
 lemma div_pos_neg_trivial:
   "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
   apply (rule div_int_unique [of _ _ _ "k + l"])
   apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
   done
 
 lemma mod_pos_neg_trivial:
   "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
   apply (rule mod_int_unique [of _ _ "- 1"])
   apply (use that in \<open>auto simp add: eucl_rel_int_iff\<close>)
   done
 
 text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
   because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
 
 
 
 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
 
 lemma zminus1_lemma:
      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
                           if r=0 then 0 else b-r)"
 by (force simp add: eucl_rel_int_iff right_diff_distrib)
 
 
 lemma zdiv_zminus1_eq_if:
      "b \<noteq> (0::int)
       \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
 
 lemma zmod_zminus1_eq_if:
      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
 proof (cases "b = 0")
   case False
   then show ?thesis
     by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
 qed auto
 
 lemma zmod_zminus1_not_zero:
   fixes k l :: int
   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   by (simp add: mod_eq_0_iff_dvd)
 
 lemma zmod_zminus2_not_zero:
   fixes k l :: int
   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   by (simp add: mod_eq_0_iff_dvd)
 
 lemma zdiv_zminus2_eq_if:
   "b \<noteq> (0::int)
       ==> a div (-b) =
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
 
 lemma zmod_zminus2_eq_if:
   "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
 
 
 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
 
 lemma zdiv_mono1:
   fixes b::int
   assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
 proof (rule unique_quotient_lemma)
   show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
     using assms(1) by auto
 qed (use assms in auto)
 
 lemma zdiv_mono1_neg:
   fixes b::int
   assumes "a \<le> a'" "b < 0" shows "a' div b \<le> a div b"
 proof (rule unique_quotient_lemma_neg)
   show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
     using assms(1) by auto
 qed (use assms in auto)
 
 
 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
 
 lemma q_pos_lemma:
   fixes q'::int
   assumes "0 \<le> b'*q' + r'" "r' < b'" "0 < b'"
   shows "0 \<le> q'"
 proof -
   have "0 < b'* (q' + 1)"
     using assms by (simp add: distrib_left)
   with assms show ?thesis
     by (simp add: zero_less_mult_iff)
 qed
 
 lemma zdiv_mono2_lemma:
   fixes q'::int
   assumes eq: "b*q + r = b'*q' + r'" and le: "0 \<le> b'*q' + r'" and "r' < b'" "0 \<le> r" "0 < b'" "b' \<le> b"
   shows "q \<le> q'"
 proof -
   have "0 \<le> q'"
     using q_pos_lemma le \<open>r' < b'\<close> \<open>0 < b'\<close> by blast
   moreover have "b*q = r' - r + b'*q'"
     using eq by linarith
   ultimately have "b*q < b* (q' + 1)"
     using mult_right_mono assms unfolding distrib_left by fastforce
   with assms show ?thesis
     by (simp add: mult_less_cancel_left_pos)
 qed
 
 lemma zdiv_mono2:
   fixes a::int
   assumes "0 \<le> a" "0 < b'" "b' \<le> b" shows "a div b \<le> a div b'"
 proof (rule zdiv_mono2_lemma)
   have "b \<noteq> 0"
     using assms by linarith
   show "b * (a div b) + a mod b = b' * (a div b') + a mod b'"
     by simp
 qed (use assms in auto)
 
 lemma zdiv_mono2_neg_lemma:
     fixes q'::int
     assumes "b*q + r = b'*q' + r'" "b'*q' + r' < 0" "r < b" "0 \<le> r'" "0 < b'" "b' \<le> b"
     shows "q' \<le> q"
 proof -
   have "b'*q' < 0"
     using assms by linarith
   with assms have "q' \<le> 0"
     by (simp add: mult_less_0_iff)
   have "b*q' \<le> b'*q'"
     by (simp add: \<open>q' \<le> 0\<close> assms(6) mult_right_mono_neg)
   then have "b*q' < b* (q + 1)"
     using assms by (simp add: distrib_left)
   then show ?thesis
     using assms by (simp add: mult_less_cancel_left)
 qed
 
 lemma zdiv_mono2_neg:
   fixes a::int
   assumes "a < 0" "0 < b'" "b' \<le> b" shows "a div b' \<le> a div b"
 proof (rule zdiv_mono2_neg_lemma)
   have "b \<noteq> 0"
     using assms by linarith
   show "b * (a div b) + a mod b = b' * (a div b') + a mod b'"
     by simp
 qed (use assms in auto)
 
 
 subsubsection \<open>Proving  \<^term>\<open>a div (b * c) = (a div b) div c\<close>\<close>
 
 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   to cause particular problems.*)
 
 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
 
 lemma zmult2_lemma_aux1: 
   fixes c::int
   assumes "0 < c" "b < r" "r \<le> 0"
   shows "b * c < b * (q mod c) + r"
 proof -
   have "b * (c - q mod c) \<le> b * 1"
     by (rule mult_left_mono_neg) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
   also have "... < r * 1"
     by (simp add: \<open>b < r\<close>)
   finally show ?thesis
     by (simp add: algebra_simps)
 qed
 
 lemma zmult2_lemma_aux2:
   fixes c::int
   assumes "0 < c" "b < r" "r \<le> 0"
   shows "b * (q mod c) + r \<le> 0"
 proof -
   have "b * (q mod c) \<le> 0"
     using assms by (simp add: mult_le_0_iff)
   with assms show ?thesis
     by arith
 qed
 
 lemma zmult2_lemma_aux3:
   fixes c::int
   assumes "0 < c" "0 \<le> r" "r < b"
   shows "0 \<le> b * (q mod c) + r"
 proof -
   have "0 \<le> b * (q mod c)"
     using assms by (simp add: mult_le_0_iff)
   with assms show ?thesis
     by arith
 qed
 
 lemma zmult2_lemma_aux4: 
   fixes c::int
   assumes "0 < c" "0 \<le> r" "r < b"
   shows "b * (q mod c) + r < b * c"
 proof -
   have "r * 1 < b * 1"
     by (simp add: \<open>r < b\<close>)
   also have "\<dots> \<le> b * (c - q mod c) "
     by (rule mult_left_mono) (use assms in \<open>auto simp: int_one_le_iff_zero_less\<close>)
   finally show ?thesis
     by (simp add: algebra_simps)
 qed
 
 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
                    zero_less_mult_iff distrib_left [symmetric]
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
 
-lemma zdiv_zmult2_eq:
-  fixes a b c :: int
-  assumes "0 \<le> c"
-  shows "a div (b * c) = (a div b) div c"
-proof (cases "b = 0")
-  case False
-  with assms show ?thesis
-    by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
-qed auto
-
-lemma zmod_zmult2_eq:
-  fixes a b c :: int
-  assumes "0 \<le> c"
-  shows "a mod (b * c) = b * (a div b mod c) + a mod b"
-proof (cases "b = 0")
-  case False
-  with assms show ?thesis
-    by (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
-qed auto
-
 lemma div_pos_geq:
   fixes k l :: int
   assumes "0 < l" and "l \<le> k"
   shows "k div l = (k - l) div l + 1"
 proof -
   have "k = (k - l) + l" by simp
   then obtain j where k: "k = j + l" ..
   with assms show ?thesis by (simp add: div_add_self2)
 qed
 
 lemma mod_pos_geq:
   fixes k l :: int
   assumes "0 < l" and "l \<le> k"
   shows "k mod l = (k - l) mod l"
 proof -
   have "k = (k - l) + l" by simp
   then obtain j where k: "k = j + l" ..
   with assms show ?thesis by simp
 qed
 
 
 subsubsection \<open>Splitting Rules for div and mod\<close>
 
 text\<open>The proofs of the two lemmas below are essentially identical\<close>
 
 lemma split_pos_lemma:
  "0<k \<Longrightarrow>
     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i j)"
   by auto
 
 lemma split_neg_lemma:
  "k<0 \<Longrightarrow>
     P(n div k :: int)(n mod k) = (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i j)"
   by auto
 
 lemma split_zdiv:
  "P(n div k :: int) =
   ((k = 0 \<longrightarrow> P 0) \<and>
    (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i)) \<and>
    (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i)))"
 proof (cases "k = 0")
   case False
   then show ?thesis
     unfolding linorder_neq_iff
     by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P x"] split_neg_lemma [of concl: "\<lambda>x y. P x"])
 qed auto
 
 lemma split_zmod:
  "P(n mod k :: int) =
   ((k = 0 \<longrightarrow> P n) \<and>
    (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P j)) \<and>
    (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P j)))"
 proof (cases "k = 0")
   case False
   then show ?thesis
     unfolding linorder_neq_iff
     by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P y"] split_neg_lemma [of concl: "\<lambda>x y. P y"])
 qed auto
 
 text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
   when these are applied to some constant that is of the form
   \<^term>\<open>numeral k\<close>:\<close>
 declare split_zdiv [of _ _ "numeral k", arith_split] for k
 declare split_zmod [of _ _ "numeral k", arith_split] for k
 
 
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
 lemma pos_eucl_rel_int_mult_2:
   assumes "0 \<le> b"
   assumes "eucl_rel_int a b (q, r)"
   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
   using assms unfolding eucl_rel_int_iff by auto
 
 lemma neg_eucl_rel_int_mult_2:
   assumes "b \<le> 0"
   assumes "eucl_rel_int (a + 1) b (q, r)"
   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
   using assms unfolding eucl_rel_int_iff by auto
 
 text\<open>computing div by shifting\<close>
 
 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
   by (rule div_int_unique)
 
 lemma neg_zdiv_mult_2:
   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
   by (rule div_int_unique)
 
 lemma zdiv_numeral_Bit0 [simp]:
   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
     numeral v div (numeral w :: int)"
   unfolding numeral.simps unfolding mult_2 [symmetric]
   by (rule div_mult_mult1, simp)
 
 lemma zdiv_numeral_Bit1 [simp]:
   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
     (numeral v div (numeral w :: int))"
   unfolding numeral.simps
   unfolding mult_2 [symmetric] add.commute [of _ 1]
   by (rule pos_zdiv_mult_2, simp)
 
 lemma pos_zmod_mult_2:
   fixes a b :: int
   assumes "0 \<le> a"
   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   by (rule mod_int_unique)
 
 lemma neg_zmod_mult_2:
   fixes a b :: int
   assumes "a \<le> 0"
   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   by (rule mod_int_unique)
 
 lemma zmod_numeral_Bit0 [simp]:
   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
     (2::int) * (numeral v mod numeral w)"
   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
 
 lemma zmod_numeral_Bit1 [simp]:
   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
     2 * (numeral v mod numeral w) + (1::int)"
   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
   unfolding mult_2 [symmetric] add.commute [of _ 1]
   by (rule pos_zmod_mult_2, simp)
 
 lemma zdiv_eq_0_iff:
   "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
   for i k :: int
 proof
   assume ?L
   moreover have "?L \<longrightarrow> ?R"
     by (rule split_zdiv [THEN iffD2]) simp
   ultimately show ?R
     by blast
 next
   assume ?R then show ?L
     by auto
 qed
 
 lemma zmod_trival_iff:
   fixes i k :: int
   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
 proof -
   have "i mod k = i \<longleftrightarrow> i div k = 0"
     by safe (insert div_mult_mod_eq [of i k], auto)
   with zdiv_eq_0_iff
   show ?thesis
     by simp
 qed
 
   
 subsubsection \<open>Quotients of Signs\<close>
 
 lemma div_eq_minus1: "0 < b \<Longrightarrow> - 1 div b = - 1" for b :: int
   by (simp add: divide_int_def)
 
 lemma zmod_minus1: "0 < b \<Longrightarrow> - 1 mod b = b - 1" for b :: int
   by (auto simp add: modulo_int_def)
 
 lemma div_neg_pos_less0:
   fixes a::int
   assumes "a < 0" "0 < b" 
   shows "a div b < 0"
 proof -
   have "a div b \<le> - 1 div b"
     using zdiv_mono1 assms by auto
   also have "... \<le> -1"
     by (simp add: assms(2) div_eq_minus1)
   finally show ?thesis 
     by force
 qed
 
 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
   by (drule zdiv_mono1_neg, auto)
 
 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
   by (drule zdiv_mono1, auto)
 
 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
 They should all be simp rules unless that causes too much search.\<close>
 
 lemma pos_imp_zdiv_nonneg_iff:
       fixes a::int
       assumes "0 < b" 
       shows "(0 \<le> a div b) = (0 \<le> a)"
 proof
   show "0 \<le> a div b \<Longrightarrow> 0 \<le> a"
     using assms
     by (simp add: linorder_not_less [symmetric]) (blast intro: div_neg_pos_less0)
 next
   assume "0 \<le> a"
   then have "0 div b \<le> a div b"
     using zdiv_mono1 assms by blast
   then show "0 \<le> a div b"
     by auto
 qed
 
 lemma pos_imp_zdiv_pos_iff:
   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith
 
 
 lemma neg_imp_zdiv_nonneg_iff:
   fixes a::int
   assumes "b < 0" 
   shows "(0 \<le> a div b) = (a \<le> 0)"
   using assms by (simp add: div_minus_minus [of a, symmetric] pos_imp_zdiv_nonneg_iff del: div_minus_minus)
 
 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
   by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
 
 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
   by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
 
 lemma nonneg1_imp_zdiv_pos_iff:
   fixes a::int
   assumes "0 \<le> a" 
   shows "a div b > 0 \<longleftrightarrow> a \<ge> b \<and> b>0"
 proof -
   have "0 < a div b \<Longrightarrow> b \<le> a"
     using div_pos_pos_trivial[of a b] assms by arith
   moreover have "0 < a div b \<Longrightarrow> b > 0"
     using assms div_nonneg_neg_le0[of a b]  by(cases "b=0"; force)
   moreover have "b \<le> a \<and> 0 < b \<Longrightarrow> 0 < a div b"
     using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b] by simp
   ultimately show ?thesis
     by blast
 qed
 
 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 \<Longrightarrow> m mod k \<le> m"
   by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le)
 
 
 subsubsection \<open>Further properties\<close>
 
 lemma div_int_pos_iff:
   "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
     \<or> k < 0 \<and> l < 0"
   for k l :: int
 proof (cases "k = 0 \<or> l = 0")
   case False
   then show ?thesis
    apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
     by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq)
 qed auto
 
 lemma mod_int_pos_iff:
   "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
   for k l :: int
 proof (cases "l > 0")
   case False
   then show ?thesis 
     by (simp add: dvd_eq_mod_eq_0) (use neg_mod_sign [of l k] in \<open>auto simp add: le_less not_less\<close>)
 qed auto
 
 text \<open>Simplify expressions in which div and mod combine numerical constants\<close>
 
 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
 
 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   by (rule div_int_unique [of a b q r],
     simp add: eucl_rel_int_iff)
 
 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   by (rule mod_int_unique [of a b q r],
     simp add: eucl_rel_int_iff)
 
 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   by (rule mod_int_unique [of a b q r],
     simp add: eucl_rel_int_iff)
 
 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
   unfolding dvd_def by (cases "y=0") (auto simp add: abs_mult)
 
 text\<open>Suggested by Matthias Daum\<close>
 lemma int_power_div_base:
   fixes k :: int
   assumes "0 < m" "0 < k"
   shows "k ^ m div k = (k::int) ^ (m - Suc 0)"
 proof -
   have eq: "k ^ m = k ^ ((m - Suc 0) + Suc 0)"
     by (simp add: assms)
   show ?thesis
     using assms by (simp only: power_add eq) auto
 qed
 
 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
 
 lemma nat_div_distrib:
   assumes "0 \<le> x"
   shows "nat (x div y) = nat x div nat y"
 proof (cases y "0::int" rule: linorder_cases)
   case less
   with assms show ?thesis
     using div_nonneg_neg_le0 by auto
 next
   case greater
   then show ?thesis
     by (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
 qed auto
 
 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
 lemma nat_mod_distrib:
   assumes "0 \<le> x" "0 \<le> y"
   shows "nat (x mod y) = nat x mod nat y"
 proof (cases "y = 0")
   case False
   with assms show ?thesis
     by (simp add: nat_eq_iff zmod_int)
 qed auto
 
 text\<open>Suggested by Matthias Daum\<close>
 lemma int_div_less_self:
   fixes x::int
   assumes "0 < x" "1 < k"
   shows  "x div k < x"
 proof -
   have "nat x div nat k < nat x"
     by (simp add: assms)
   with assms show ?thesis
     by (simp add: nat_div_distrib [symmetric])
 qed
 
 lemma mod_eq_dvd_iff_nat:
   "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
 proof -
   have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n"
     by (simp add: mod_eq_dvd_iff)
   with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
     by (simp only: of_nat_mod of_nat_diff)
   then show ?thesis
     by simp
 qed
 
 lemma mod_eq_nat1E:
   fixes m n q :: nat
   assumes "m mod q = n mod q" and "m \<ge> n"
   obtains s where "m = n + q * s"
 proof -
   from assms have "q dvd m - n"
     by (simp add: mod_eq_dvd_iff_nat)
   then obtain s where "m - n = q * s" ..
   with \<open>m \<ge> n\<close> have "m = n + q * s"
     by simp
   with that show thesis .
 qed
 
 lemma mod_eq_nat2E:
   fixes m n q :: nat
   assumes "m mod q = n mod q" and "n \<ge> m"
   obtains s where "n = m + q * s"
   using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)
 
 lemma nat_mod_eq_lemma:
   assumes "(x::nat) mod n = y mod n" and "y \<le> x"
   shows "\<exists>q. x = y + n * q"
   using assms by (rule mod_eq_nat1E) rule
 
 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
   (is "?lhs = ?rhs")
 proof
   assume H: "x mod n = y mod n"
   {assume xy: "x \<le> y"
     from H have th: "y mod n = x mod n" by simp
     from nat_mod_eq_lemma[OF th xy] have ?rhs
       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
   moreover
   {assume xy: "y \<le> x"
     from nat_mod_eq_lemma[OF H xy] have ?rhs
       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
   ultimately  show ?rhs using linear[of x y] by blast
 next
   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
   thus  ?lhs by simp
 qed
 
 
 subsection \<open>Numeral division with a pragmatic type class\<close>
 
 text \<open>
   The following type class contains everything necessary to formulate
   a division algorithm in ring structures with numerals, restricted
   to its positive segments.  This is its primary motivation, and it
   could surely be formulated using a more fine-grained, more algebraic
   and less technical class hierarchy.
 \<close>
 
 class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
     \<comment> \<open>These are conceptually definitions but force generated code
     to be monomorphic wrt. particular instances of this class which
     yields a significant speedup.\<close>
 begin
 
 lemma divmod_digit_1:
   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
     and "a mod (2 * b) - b = a mod b" (is "?Q")
 proof -
   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
     by (auto intro: trans)
   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
   define w where "w = a div b mod 2"
   then have w_exhaust: "w = 0 \<or> w = 1" by auto
   have mod_w: "a mod (2 * b) = a mod b + b * w"
     by (simp add: w_def mod_mult2_eq ac_simps)
   from assms w_exhaust have "w = 1"
     by (auto simp add: mod_w) (insert mod_less, auto)
   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   then show ?P and ?Q
     by (simp_all add: div mod add_implies_diff [symmetric])
 qed
 
 lemma divmod_digit_0:
   assumes "0 < b" and "a mod (2 * b) < b"
   shows "2 * (a div (2 * b)) = a div b" (is "?P")
     and "a mod (2 * b) = a mod b" (is "?Q")
 proof -
   define w where "w = a div b mod 2"
   then have w_exhaust: "w = 0 \<or> w = 1" by auto
   have mod_w: "a mod (2 * b) = a mod b + b * w"
     by (simp add: w_def mod_mult2_eq ac_simps)
   moreover have "b \<le> a mod b + b"
   proof -
     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
     then show ?thesis by simp
   qed
   moreover note assms w_exhaust
   ultimately have "w = 0" by auto
   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
   then show ?P and ?Q
     by (simp_all add: div mod)
 qed
 
 lemma mod_double_modulus:
   assumes "m > 0" "x \<ge> 0"
   shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
 proof (cases "x mod (2 * m) < m")
   case True
   thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
 next
   case False
   hence *: "x mod (2 * m) - m = x mod m"
     using assms by (intro divmod_digit_1) auto
   hence "x mod (2 * m) = x mod m + m"
     by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
   thus ?thesis by simp
 qed
 
 lemma fst_divmod:
   "fst (divmod m n) = numeral m div numeral n"
   by (simp add: divmod_def)
 
 lemma snd_divmod:
   "snd (divmod m n) = numeral m mod numeral n"
   by (simp add: divmod_def)
 
 text \<open>
   This is a formulation of one step (referring to one digit position)
   in school-method division: compare the dividend at the current
   digit position with the remainder from previous division steps
   and evaluate accordingly.
 \<close>
 
 lemma divmod_step_eq [simp]:
   "divmod_step l (q, r) = (if numeral l \<le> r
     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   by (simp add: divmod_step_def)
 
 text \<open>
   This is a formulation of school-method division.
   If the divisor is smaller than the dividend, terminate.
   If not, shift the dividend to the right until termination
   occurs and then reiterate single division steps in the
   opposite direction.
 \<close>
 
 lemma divmod_divmod_step:
   "divmod m n = (if m < n then (0, numeral m)
     else divmod_step n (divmod m (Num.Bit0 n)))"
 proof (cases "m < n")
   case True then have "numeral m < numeral n" by simp
   then show ?thesis
     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
 next
   case False
   have "divmod m n =
     divmod_step n (numeral m div (2 * numeral n),
       numeral m mod (2 * numeral n))"
   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
     case True
     with divmod_step_eq
       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
         by simp
     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
       by simp_all
     ultimately show ?thesis by (simp only: divmod_def)
   next
     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
       by (simp add: not_le)
     with divmod_step_eq
       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
         by auto
     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
       by (simp_all only: zero_less_numeral)
     ultimately show ?thesis by (simp only: divmod_def)
   qed
   then have "divmod m n =
     divmod_step n (numeral m div numeral (Num.Bit0 n),
       numeral m mod numeral (Num.Bit0 n))"
     by (simp only: numeral.simps distrib mult_1)
   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
     by (simp add: divmod_def)
   with False show ?thesis by simp
 qed
 
 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
 
 lemma divmod_trivial [simp]:
   "divmod Num.One Num.One = (numeral Num.One, 0)"
   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
 
 text \<open>Division by an even number is a right-shift\<close>
 
 lemma divmod_cancel [simp]:
   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
 proof -
   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   then show ?P and ?Q
     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
       add.commute del: numeral_times_numeral)
 qed
 
 text \<open>The really hard work\<close>
 
 lemma divmod_steps [simp]:
   "divmod (num.Bit0 m) (num.Bit1 n) =
       (if m \<le> n then (0, numeral (num.Bit0 m))
        else divmod_step (num.Bit1 n)
              (divmod (num.Bit0 m)
                (num.Bit0 (num.Bit1 n))))"
   "divmod (num.Bit1 m) (num.Bit1 n) =
       (if m < n then (0, numeral (num.Bit1 m))
        else divmod_step (num.Bit1 n)
              (divmod (num.Bit1 m)
                (num.Bit0 (num.Bit1 n))))"
   by (simp_all add: divmod_divmod_step)
 
 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
 
 text \<open>Special case: divisibility\<close>
 
 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
 where
   "divides_aux qr \<longleftrightarrow> snd qr = 0"
 
 lemma divides_aux_eq [simp]:
   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   by (simp add: divides_aux_def)
 
 lemma dvd_numeral_simp [simp]:
   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   by (simp add: divmod_def mod_eq_0_iff_dvd)
 
 text \<open>Generic computation of quotient and remainder\<close>  
 
 lemma numeral_div_numeral [simp]: 
   "numeral k div numeral l = fst (divmod k l)"
   by (simp add: fst_divmod)
 
 lemma numeral_mod_numeral [simp]: 
   "numeral k mod numeral l = snd (divmod k l)"
   by (simp add: snd_divmod)
 
 lemma one_div_numeral [simp]:
   "1 div numeral n = fst (divmod num.One n)"
   by (simp add: fst_divmod)
 
 lemma one_mod_numeral [simp]:
   "1 mod numeral n = snd (divmod num.One n)"
   by (simp add: snd_divmod)
 
 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
 
 lemma cong_exp_iff_simps:
   "numeral n mod numeral Num.One = 0
     \<longleftrightarrow> True"
   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
     \<longleftrightarrow> numeral n mod numeral q = 0"
   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
     \<longleftrightarrow> False"
   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
     \<longleftrightarrow> True"
   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
     \<longleftrightarrow> True"
   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> False"
   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> (numeral n mod numeral q) = 0"
   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
     \<longleftrightarrow> False"
   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> False"
   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
     \<longleftrightarrow> (numeral m mod numeral q) = 0"
   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> False"
   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
 
 end
 
 hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
 
 instantiation nat :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
 where
   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
 
 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
 where
   "divmod_step_nat l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
 
 instance by standard
   (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
 
 end
 
 declare divmod_algorithm_code [where ?'a = nat, code]
 
 lemma Suc_0_div_numeral [simp]:
   fixes k l :: num
   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   by (simp_all add: fst_divmod)
 
 lemma Suc_0_mod_numeral [simp]:
   fixes k l :: num
   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   by (simp_all add: snd_divmod)
 
 instantiation int :: unique_euclidean_semiring_numeral
 begin
 
 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
 where
   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
 
 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
 where
   "divmod_step_int l qr = (let (q, r) = qr
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
 
 instance
   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
     pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
 
 end
 
 declare divmod_algorithm_code [where ?'a = int, code]
 
 context
 begin
   
 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
 where
   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
 
 qualified lemma adjust_div_eq [simp, code]:
   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
   by (simp add: adjust_div_def)
 
 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
 where
   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
 
 lemma minus_numeral_div_numeral [simp]:
   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
 proof -
   have "int (fst (divmod m n)) = fst (divmod m n)"
     by (simp only: fst_divmod divide_int_def) auto
   then show ?thesis
     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
 qed
 
 lemma minus_numeral_mod_numeral [simp]:
   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
 next
   case False
   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
     by (simp only: snd_divmod modulo_int_def) auto
   then show ?thesis
     by (simp add: divides_aux_def adjust_div_def)
       (simp add: divides_aux_def modulo_int_def)
 qed
 
 lemma numeral_div_minus_numeral [simp]:
   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
 proof -
   have "int (fst (divmod m n)) = fst (divmod m n)"
     by (simp only: fst_divmod divide_int_def) auto
   then show ?thesis
     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
 qed
   
 lemma numeral_mod_minus_numeral [simp]:
   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
 next
   case False
   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
     by (simp only: snd_divmod modulo_int_def) auto
   then show ?thesis
     by (simp add: divides_aux_def adjust_div_def)
       (simp add: divides_aux_def modulo_int_def)
 qed
 
 lemma minus_one_div_numeral [simp]:
   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
   using minus_numeral_div_numeral [of Num.One n] by simp  
 
 lemma minus_one_mod_numeral [simp]:
   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
   using minus_numeral_mod_numeral [of Num.One n] by simp
 
 lemma one_div_minus_numeral [simp]:
   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
   using numeral_div_minus_numeral [of Num.One n] by simp
   
 lemma one_mod_minus_numeral [simp]:
   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
   using numeral_mod_minus_numeral [of Num.One n] by simp
 
 end
 
 lemma div_positive_int:
   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   using that div_positive [of l k] by blast
 
 
 subsubsection \<open>Dedicated simproc for calculation\<close>
 
 text \<open>
   There is space for improvement here: the calculation itself
   could be carried out outside the logic, and a generic simproc
   (simplifier setup) for generic calculation would be helpful. 
 \<close>
 
 simproc_setup numeral_divmod
   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "0 div - 1 :: int" | "0 mod - 1 :: int" |
    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "1 div - 1 :: int" | "1 mod - 1 :: int" |
    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
 \<open> let
     val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>);
     fun successful_rewrite ctxt ct =
       let
         val thm = Simplifier.rewrite ctxt ct
       in if Thm.is_reflexive thm then NONE else SOME thm end;
   in fn phi =>
     let
       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
         one_div_minus_numeral one_mod_minus_numeral
         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
         numeral_div_minus_numeral numeral_mod_minus_numeral
         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
   end
 \<close>
 
 
 subsubsection \<open>Code generation\<close>
 
 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
   where "divmod_nat m n = (m div n, m mod n)"
 
 lemma fst_divmod_nat [simp]:
   "fst (divmod_nat m n) = m div n"
   by (simp add: divmod_nat_def)
 
 lemma snd_divmod_nat [simp]:
   "snd (divmod_nat m n) = m mod n"
   by (simp add: divmod_nat_def)
 
 lemma divmod_nat_if [code]:
   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
 lemma [code]:
   "m div n = fst (divmod_nat m n)"
   "m mod n = snd (divmod_nat m n)"
   by simp_all
 
 lemma [code]:
   fixes k :: int
   shows 
     "k div 0 = 0"
     "k mod 0 = k"
     "0 div k = 0"
     "0 mod k = 0"
     "k div Int.Pos Num.One = k"
     "k mod Int.Pos Num.One = 0"
     "k div Int.Neg Num.One = - k"
     "k mod Int.Neg Num.One = 0"
     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
   by simp_all
 
 code_identifier
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 
 subsection \<open>Lemmas of doubtful value\<close>
 
 lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
 
 lemma mod_geq: "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
 
 lemma mod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: nat
   using that by (auto simp add: mod_eq_0_iff_dvd)
 
 lemma pos_mod_conj: "0 < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b" for a b :: int
   by simp
 
 lemma neg_mod_conj: "b < 0 \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b" for a b :: int
   by simp
 
 lemma zmod_eq_0_iff: "m mod d = 0 \<longleftrightarrow> (\<exists>q. m = d * q)" for m d :: int
   by (auto simp add: mod_eq_0_iff_dvd)
 
 (* REVISIT: should this be generalized to all semiring_div types? *)
 lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
   using that by auto
 
 end
diff --git a/src/HOL/Lattices.thy b/src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy
+++ b/src/HOL/Lattices.thy
@@ -1,969 +1,977 @@
 (*  Title:      HOL/Lattices.thy
     Author:     Tobias Nipkow
 *)
 
 section \<open>Abstract lattices\<close>
 
 theory Lattices
 imports Groups
 begin
 
 subsection \<open>Abstract semilattice\<close>
 
 text \<open>
   These locales provide a basic structure for interpretation into
   bigger structures;  extensions require careful thinking, otherwise
   undesired effects may occur due to interpretation.
 \<close>
 
 locale semilattice = abel_semigroup +
   assumes idem [simp]: "a \<^bold>* a = a"
 begin
 
 lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
   by (simp add: assoc [symmetric])
 
 lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
   by (simp add: assoc)
 
 end
 
 locale semilattice_neutr = semilattice + comm_monoid
 
 locale semilattice_order = semilattice +
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold>\<le>" 50)
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold><" 50)
   assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
     and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
 begin
 
 lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
   by (simp add: order_iff)
 
 lemma orderE:
   assumes "a \<^bold>\<le> b"
   obtains "a = a \<^bold>* b"
   using assms by (unfold order_iff)
 
 sublocale ordering less_eq less
 proof
   show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b
     by (simp add: order_iff strict_order_iff)
 next
   show "a \<^bold>\<le> a" for a
     by (simp add: order_iff)
 next
   fix a b
   assume "a \<^bold>\<le> b" "b \<^bold>\<le> a"
   then have "a = a \<^bold>* b" "a \<^bold>* b = b"
     by (simp_all add: order_iff commute)
   then show "a = b" by simp
 next
   fix a b c
   assume "a \<^bold>\<le> b" "b \<^bold>\<le> c"
   then have "a = a \<^bold>* b" "b = b \<^bold>* c"
     by (simp_all add: order_iff commute)
   then have "a = a \<^bold>* (b \<^bold>* c)"
     by simp
   then have "a = (a \<^bold>* b) \<^bold>* c"
     by (simp add: assoc)
   with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp
   then show "a \<^bold>\<le> c" by (rule orderI)
 qed
 
 lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\<le> a"
   by (simp add: order_iff commute)
 
 lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\<le> b"
   by (simp add: order_iff)
 
 lemma boundedI:
   assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
   shows "a \<^bold>\<le> b \<^bold>* c"
 proof (rule orderI)
   from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a"
     by (auto elim!: orderE)
   then show "a = a \<^bold>* (b \<^bold>* c)"
     by (simp add: assoc [symmetric])
 qed
 
 lemma boundedE:
   assumes "a \<^bold>\<le> b \<^bold>* c"
   obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
   using assms by (blast intro: trans cobounded1 cobounded2)
 
 lemma bounded_iff [simp]: "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
   by (blast intro: boundedI elim: boundedE)
 
 lemma strict_boundedE:
   assumes "a \<^bold>< b \<^bold>* c"
   obtains "a \<^bold>< b" and "a \<^bold>< c"
   using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
 
 lemma coboundedI1: "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   by (rule trans) auto
 
 lemma coboundedI2: "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   by (rule trans) auto
 
 lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   using irrefl
   by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order
       elim: strict_boundedE)
 
 lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   using strict_coboundedI1 [of b c a] by (simp add: commute)
 
 lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
   by (blast intro: boundedI coboundedI1 coboundedI2)
 
 lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a"
   by (rule antisym) (auto simp: refl)
 
 lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
   by (rule antisym) (auto simp: refl)
 
 lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
   using order_iff by auto
 
 lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b"
   using order_iff by (auto simp add: commute)
 
 end
 
 locale semilattice_neutr_order = semilattice_neutr + semilattice_order
 begin
 
 sublocale ordering_top less_eq less "\<^bold>1"
   by standard (simp add: order_iff)
 
 end
 
 text \<open>Passive interpretations for boolean operators\<close>
 
 lemma semilattice_neutr_and:
   "semilattice_neutr HOL.conj True"
   by standard auto
 
 lemma semilattice_neutr_or:
   "semilattice_neutr HOL.disj False"
   by standard auto
 
 
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class inf =
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
 
 class sup =
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
 
 
 subsection \<open>Concrete lattices\<close>
 
 class semilattice_inf = order + inf +
   assumes inf_le1 [simp]: "x \<sqinter> y \<le> x"
   and inf_le2 [simp]: "x \<sqinter> y \<le> y"
   and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
 
 class semilattice_sup = order + sup +
   assumes sup_ge1 [simp]: "x \<le> x \<squnion> y"
   and sup_ge2 [simp]: "y \<le> x \<squnion> y"
   and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
 begin
 
 text \<open>Dual lattice.\<close>
 lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
   by (rule class.semilattice_inf.intro, rule dual_order)
     (unfold_locales, simp_all add: sup_least)
 
 end
 
 class lattice = semilattice_inf + semilattice_sup
 
 
 subsubsection \<open>Intro and elim rules\<close>
 
 context semilattice_inf
 begin
 
 lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
   by (rule order_trans) auto
 
 lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
   by (rule order_trans) auto
 
 lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b"
   by (fact inf_greatest) (* FIXME: duplicate lemma *)
 
 lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans inf_le1 inf_le2)
 
 lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z"
   by (blast intro: le_infI elim: le_infE)
 
 lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
 
 lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
   by (fast intro: inf_greatest le_infI1 le_infI2)
 
 lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
   by (auto simp add: mono_def intro: Lattices.inf_greatest)
 
 end
 
 context semilattice_sup
 begin
 
 lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"
   by (rule order_trans) auto
 
 lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b"
   by (rule order_trans) auto
 
 lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x"
   by (fact sup_least) (* FIXME: duplicate lemma *)
 
 lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans sup_ge1 sup_ge2)
 
 lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
   by (blast intro: le_supI elim: le_supE)
 
 lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
 
 lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
   by (fast intro: sup_least le_supI1 le_supI2)
 
 lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
 end
 
 
 subsubsection \<open>Equational laws\<close>
 
 context semilattice_inf
 begin
 
 sublocale inf: semilattice inf
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
     by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
   show "a \<sqinter> b = b \<sqinter> a"
     by (rule antisym) (auto simp add: le_inf_iff)
   show "a \<sqinter> a = a"
     by (rule antisym) (auto simp add: le_inf_iff)
 qed
 
 sublocale inf: semilattice_order inf less_eq less
   by standard (auto simp add: le_iff_inf less_le)
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   by (fact inf.assoc)
 
 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   by (fact inf.commute)
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   by (fact inf.left_commute)
 
 lemma inf_idem: "x \<sqinter> x = x"
   by (fact inf.idem) (* already simp *)
 
 lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (fact inf.left_idem) (* already simp *)
 
 lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
   by (fact inf.right_idem) (* already simp *)
 
 lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
 lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
 
 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
 end
 
 context semilattice_sup
 begin
 
 sublocale sup: semilattice sup
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
     by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
   show "a \<squnion> b = b \<squnion> a"
     by (rule antisym) (auto simp add: le_sup_iff)
   show "a \<squnion> a = a"
     by (rule antisym) (auto simp add: le_sup_iff)
 qed
 
 sublocale sup: semilattice_order sup greater_eq greater
   by standard (auto simp add: le_iff_sup sup.commute less_le)
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   by (fact sup.assoc)
 
 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   by (fact sup.commute)
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   by (fact sup.left_commute)
 
 lemma sup_idem: "x \<squnion> x = x"
   by (fact sup.idem) (* already simp *)
 
 lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (fact sup.left_idem)
 
 lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
 
 lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
 
 end
 
 context lattice
 begin
 
 lemma dual_lattice: "class.lattice sup (\<ge>) (>) inf"
   by (rule class.lattice.intro,
       rule dual_semilattice,
       rule class.semilattice_sup.intro,
       rule dual_order)
     (unfold_locales, auto)
 
 lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
 
 lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
   by (blast intro: antisym sup_ge1 sup_least inf_le1)
 
 lemmas inf_sup_aci = inf_aci sup_aci
 
 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
 
 text \<open>Towards distributivity.\<close>
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 text \<open>If you have one of them, you have them all.\<close>
 
 lemma distrib_imp1:
   assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 proof-
   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)"
     by simp
   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
     by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb)
   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
     by (simp add: inf_commute)
   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib)
   finally show ?thesis .
 qed
 
 lemma distrib_imp2:
   assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
 proof-
   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)"
     by simp
   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
     by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb)
   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
     by (simp add: sup_commute)
   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib)
   finally show ?thesis .
 qed
 
 end
 
 
 subsubsection \<open>Strict order\<close>
 
 context semilattice_inf
 begin
 
 lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < x"
   by (auto simp add: less_le inf_absorb1 intro: le_infI1)
 
 lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < x"
   by (auto simp add: less_le inf_absorb2 intro: le_infI2)
 
 end
 
 context semilattice_sup
 begin
 
 lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b"
   using dual_semilattice
   by (rule semilattice_inf.less_infI1)
 
 lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b"
   using dual_semilattice
   by (rule semilattice_inf.less_infI2)
 
 end
 
 
 subsection \<open>Distributive lattices\<close>
 
 class distrib_lattice = lattice +
   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 
 context distrib_lattice
 begin
 
 lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   by (simp add: sup_commute sup_inf_distrib1)
 
 lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   by (rule distrib_imp2 [OF sup_inf_distrib1])
 
 lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   by (simp add: inf_commute inf_sup_distrib1)
 
 lemma dual_distrib_lattice: "class.distrib_lattice sup (\<ge>) (>) inf"
   by (rule class.distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
 lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2
 
 lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2
 
 lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
 
 end
 
 
 subsection \<open>Bounded lattices and boolean algebras\<close>
 
 class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
 
 sublocale inf_top: semilattice_neutr inf top
   + inf_top: semilattice_neutr_order inf top less_eq less
 proof
   show "x \<sqinter> \<top> = x" for x
     by (rule inf_absorb1) simp
 qed
 
 end
 
 class bounded_semilattice_sup_bot = semilattice_sup + order_bot
 begin
 
 sublocale sup_bot: semilattice_neutr sup bot
   + sup_bot: semilattice_neutr_order sup bot greater_eq greater
 proof
   show "x \<squnion> \<bottom> = x" for x
     by (rule sup_absorb1) simp
 qed
 
 end
 
 class bounded_lattice_bot = lattice + order_bot
 begin
 
 subclass bounded_semilattice_sup_bot ..
 
 lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>"
   by (rule inf_absorb1) simp
 
 lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>"
   by (rule inf_absorb2) simp
 
 lemma sup_bot_left: "\<bottom> \<squnion> x = x"
   by (fact sup_bot.left_neutral)
 
 lemma sup_bot_right: "x \<squnion> \<bottom> = x"
   by (fact sup_bot.right_neutral)
 
 lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   by (simp add: eq_iff)
 
 lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   by (simp add: eq_iff)
 
 end
 
 class bounded_lattice_top = lattice + order_top
 begin
 
 subclass bounded_semilattice_inf_top ..
 
 lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>"
   by (rule sup_absorb1) simp
 
 lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>"
   by (rule sup_absorb2) simp
 
 lemma inf_top_left: "\<top> \<sqinter> x = x"
   by (fact inf_top.left_neutral)
 
 lemma inf_top_right: "x \<sqinter> \<top> = x"
   by (fact inf_top.right_neutral)
 
 lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   by (simp add: eq_iff)
 
 end
 
 class bounded_lattice = lattice + order_bot + order_top
 begin
 
 subclass bounded_lattice_bot ..
 subclass bounded_lattice_top ..
 
 lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
 
 end
 
 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
   assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
     and sup_compl_top: "x \<squnion> - x = \<top>"
   assumes diff_eq: "x - y = x \<sqinter> - y"
 begin
 
 lemma dual_boolean_algebra:
   "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
   by (rule class.boolean_algebra.intro,
       rule dual_bounded_lattice,
       rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
 lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>"
   by (simp add: inf_commute inf_compl_bot)
 
 lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>"
   by (simp add: sup_commute sup_compl_top)
 
 lemma compl_unique:
   assumes "x \<sqinter> y = \<bottom>"
     and "x \<squnion> y = \<top>"
   shows "- x = y"
 proof -
   have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
     using inf_compl_bot assms(1) by simp
   then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
     by (simp add: inf_commute)
   then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
     by (simp add: inf_sup_distrib1)
   then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
     using sup_compl_top assms(2) by simp
   then show "- x = y" by simp
 qed
 
 lemma double_compl [simp]: "- (- x) = x"
   using compl_inf_bot compl_sup_top by (rule compl_unique)
 
 lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y"
 proof
   assume "- x = - y"
   then have "- (- x) = - (- y)" by (rule arg_cong)
   then show "x = y" by simp
 next
   assume "x = y"
   then show "- x = - y" by simp
 qed
 
 lemma compl_bot_eq [simp]: "- \<bottom> = \<top>"
 proof -
   from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   then show ?thesis by simp
 qed
 
 lemma compl_top_eq [simp]: "- \<top> = \<bottom>"
 proof -
   from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   then show ?thesis by simp
 qed
 
 lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y"
 proof (rule compl_unique)
   have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
     by (simp only: inf_sup_distrib inf_aci)
   then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
     by (simp add: inf_compl_bot)
 next
   have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
     by (simp only: sup_inf_distrib sup_aci)
   then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
     by (simp add: sup_compl_top)
 qed
 
 lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y"
   using dual_boolean_algebra
   by (rule boolean_algebra.compl_inf)
 
 lemma compl_mono:
   assumes "x \<le> y"
   shows "- y \<le> - x"
 proof -
   from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
   then have "- (x \<squnion> y) = - y" by simp
   then have "- x \<sqinter> - y = - y" by simp
   then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   then show ?thesis by (simp only: le_iff_inf)
 qed
 
 lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
   by (auto dest: compl_mono)
 
 lemma compl_le_swap1:
   assumes "y \<le> - x"
   shows "x \<le> -y"
 proof -
   from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma compl_le_swap2:
   assumes "- y \<le> x"
   shows "- x \<le> y"
 proof -
   from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x"  (* TODO: declare [simp] ? *)
   by (auto simp add: less_le)
 
 lemma compl_less_swap1:
   assumes "y < - x"
   shows "x < - y"
 proof -
   from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma compl_less_swap2:
   assumes "- y < x"
   shows "- x < y"
 proof -
   from assms have "- x < - (- y)"
     by (simp only: compl_less_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
   by (simp add: inf_sup_aci sup_compl_top)
 
 lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
   by (simp add: inf_sup_aci sup_compl_top)
 
 lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
   by (simp add: inf_sup_aci inf_compl_bot)
 
 lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
   by (simp add: inf_sup_aci inf_compl_bot)
 
 declare inf_compl_bot [simp]
   and sup_compl_top [simp]
 
 lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
   by (simp add: sup_assoc[symmetric])
 
 lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
   using sup_compl_top_left1[of "- x" y] by simp
 
 lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
   by (simp add: inf_assoc[symmetric])
 
 lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
   using inf_compl_bot_left1[of "- x" y] by simp
 
 lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
   by (subst inf_left_commute) simp
 
 end
 
 locale boolean_algebra_cancel
 begin
 
 lemma sup1: "(A::'a::semilattice_sup) \<equiv> sup k a \<Longrightarrow> sup A b \<equiv> sup k (sup a b)"
   by (simp only: ac_simps)
 
 lemma sup2: "(B::'a::semilattice_sup) \<equiv> sup k b \<Longrightarrow> sup a B \<equiv> sup k (sup a b)"
   by (simp only: ac_simps)
 
 lemma sup0: "(a::'a::bounded_semilattice_sup_bot) \<equiv> sup a bot"
   by simp
 
 lemma inf1: "(A::'a::semilattice_inf) \<equiv> inf k a \<Longrightarrow> inf A b \<equiv> inf k (inf a b)"
   by (simp only: ac_simps)
 
 lemma inf2: "(B::'a::semilattice_inf) \<equiv> inf k b \<Longrightarrow> inf a B \<equiv> inf k (inf a b)"
   by (simp only: ac_simps)
 
 lemma inf0: "(a::'a::bounded_semilattice_inf_top) \<equiv> inf a top"
   by simp
 
 end
 
 ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
 
 simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
   \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
 
 simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
   \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
 
 
 subsection \<open>\<open>min/max\<close> as special case of lattice\<close>
 
 context linorder
 begin
 
 sublocale min: semilattice_order min less_eq less
   + max: semilattice_order max greater_eq greater
   by standard (auto simp add: min_def max_def)
 
 lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   unfolding min_def using linear by (auto intro: order_trans)
 
 lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   unfolding max_def using linear by (auto intro: order_trans)
 
 lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   unfolding min_def le_less using less_linear by (auto intro: less_trans)
 
 lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
 lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   unfolding min_def le_less using less_linear by (auto intro: less_trans)
 
 lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
 lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)"
   by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
 
 lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)"
   by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
 
 lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)"
   by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
 
 lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)"
   by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
 
 lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2
 
 lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   by (simp add: min_def)
 
 lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   by (simp add: max_def)
 
+lemma split_min_lin [no_atp]:
+  \<open>P (min a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P a) \<and> (b < a \<longrightarrow> P b)\<close>
+  by (cases a b rule: linorder_cases) (auto simp add: min.absorb1 min.absorb2)
+
+lemma split_max_lin [no_atp]:
+  \<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
+  by (cases a b rule: linorder_cases) (auto simp add: max.absorb1 max.absorb2)
+
 lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
 
 lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
 
 end
 
 lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)"
   and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)"
   for f::"'a::linorder \<Rightarrow> 'b::linorder"
   by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym)
 
 lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (auto intro: antisym simp add: min_def fun_eq_iff)
 
 lemma sup_max: "sup = (max :: 'a::{semilattice_sup,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (auto intro: antisym simp add: max_def fun_eq_iff)
 
 
 subsection \<open>Uniqueness of inf and sup\<close>
 
 lemma (in semilattice_inf) inf_unique:
   fixes f  (infixl "\<triangle>" 70)
   assumes le1: "\<And>x y. x \<triangle> y \<le> x"
     and le2: "\<And>x y. x \<triangle> y \<le> y"
     and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
   show "x \<triangle> y \<le> x \<sqinter> y"
     by (rule le_infI) (rule le1, rule le2)
   have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
     by (blast intro: greatest)
   show "x \<sqinter> y \<le> x \<triangle> y"
     by (rule leI) simp_all
 qed
 
 lemma (in semilattice_sup) sup_unique:
   fixes f  (infixl "\<nabla>" 70)
   assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y"
     and ge2: "\<And>x y. y \<le> x \<nabla> y"
     and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
   show "x \<squnion> y \<le> x \<nabla> y"
     by (rule le_supI) (rule ge1, rule ge2)
   have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z"
     by (blast intro: least)
   show "x \<nabla> y \<le> x \<squnion> y"
     by (rule leI) simp_all
 qed
 
 
 subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close>
 
 instantiation bool :: boolean_algebra
 begin
 
 definition bool_Compl_def [simp]: "uminus = Not"
 
 definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
 
 definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
 
 definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
 
 instance by standard auto
 
 end
 
 lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q"
   by simp
 
 lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q"
   by simp
 
 lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
 
 subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>
 
 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
 begin
 
 definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
 lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x"
   by (simp add: sup_fun_def)
 
 instance
   by standard (simp_all add: le_fun_def)
 
 end
 
 instantiation "fun" :: (type, semilattice_inf) semilattice_inf
 begin
 
 definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
 lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x"
   by (simp add: inf_fun_def)
 
 instance by standard (simp_all add: le_fun_def)
 
 end
 
 instance "fun" :: (type, lattice) lattice ..
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice
   by standard (rule ext, simp add: sup_inf_distrib1)
 
 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
 
 instantiation "fun" :: (type, uminus) uminus
 begin
 
 definition fun_Compl_def: "- A = (\<lambda>x. - A x)"
 
 lemma uminus_apply [simp, code]: "(- A) x = - (A x)"
   by (simp add: fun_Compl_def)
 
 instance ..
 
 end
 
 instantiation "fun" :: (type, minus) minus
 begin
 
 definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
 
 lemma minus_apply [simp, code]: "(A - B) x = A x - B x"
   by (simp add: fun_diff_def)
 
 instance ..
 
 end
 
 instance "fun" :: (type, boolean_algebra) boolean_algebra
   by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
 
 
 subsection \<open>Lattice on unary and binary predicates\<close>
 
 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   by (simp add: inf_fun_def)
 
 lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
   by (simp add: inf_fun_def)
 
 lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: inf_fun_def)
 
 lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: inf_fun_def)
 
 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
   by (rule inf1E)
 
 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
   by (rule inf2E)
 
 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   by (rule inf1E)
 
 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   by (rule inf2E)
 
 lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
 lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
 lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
 lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
 lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
 text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close>
 
 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   by (auto simp add: sup_fun_def)
 
 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   by (auto simp add: sup_fun_def)
 
 end
diff --git a/src/HOL/Parity.thy b/src/HOL/Parity.thy
--- a/src/HOL/Parity.thy
+++ b/src/HOL/Parity.thy
@@ -1,1216 +1,1305 @@
 (*  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 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
 
 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>
 
 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
 
 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 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 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)
 
 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
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_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
 
+
 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>
 
 instance int :: unique_euclidean_ring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
 
 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 shifts\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bit_split_eq: \<open>\<And>a. of_bool (odd a) + 2 * (a div 2) = a\<close>
-    and bit_eq_rec: \<open>\<And>a b. a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
+  assumes bit_eq_rec: \<open>a = b \<longleftrightarrow> (even a = even b) \<and> a div 2 = b div 2\<close>
     and bit_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 bit_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 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_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 one_mod_two_eq_one [simp]:
+  \<open>1 mod 2 = 1\<close>
+  by (simp add: mod2_eq_if)
+
+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>of_bool (odd n) + 2 * (n div 2) = n\<close>
-    for n :: nat
-    by simp
   show \<open>m = n \<longleftrightarrow> (even m \<longleftrightarrow> even n) \<and> m div 2 = n div 2\<close>
     for m n :: nat
     by (auto dest: odd_two_times_div_two_succ)
   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
-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)
 
 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>of_bool (odd k) + 2 * (k div 2) = k\<close>
-    for k :: int
-    by (auto elim: oddE)
   show \<open>k = l \<longleftrightarrow> (even k \<longleftrightarrow> even l) \<and> k div 2 = l div 2\<close>
     for k l :: int
     by (auto dest: odd_two_times_div_two_succ)
   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
-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)
 
 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_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
+
 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
 
 class unique_euclidean_semiring_with_bit_shifts =
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
 begin
 
-lemma bit_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 take_bit_take_bit [simp]:
-  "take_bit m (take_bit n a) = take_bit (min m n) a"
-proof (cases "m \<le> n")
-  case True
-  then show ?thesis
-    by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd)
-next
-  case False
-  then have "n < m" and "min m n = n"
-    by simp_all
-  then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))"
-    by (simp add: power_add [symmetric])
-  then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
-    by simp
-  also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)"
-    by (simp only: mod_mult2_eq')
-  finally show ?thesis
-    using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod)
-qed
-
-lemma drop_bit_drop_bit [simp]:
-  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
-proof -
-  have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))"
-    by (simp add: ac_simps)
-  also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)"
-    by (simp only: div_mult2_eq')
-  finally show ?thesis
-    by (simp add: drop_bit_eq_div power_add)
-qed
-
-lemma push_bit_take_bit:
-  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
-  by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps)
+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_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
-    by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le)
-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)"
-  using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"]
-  by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps)
-
-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 have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))"
-    by simp
-  also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))"
-    by (simp add: power_add)
-  also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))"
-    by simp
-  also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))"
-    by (simp only: div_mult2_eq')
-  finally show ?thesis
-    using False by (simp add: take_bit_eq_mod drop_bit_eq_div)
-qed
-
-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 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 push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
 
-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 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_0 [simp]:
-  "take_bit 0 a = 0"
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_Suc [simp]:
-  "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
-proof -
-  have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
-    if "odd a"
-    using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"]
-    by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right)
-  also have "\<dots> = a mod (2 * 2 ^ n)"
-    by (simp only: div_mult_mod_eq)
-  finally show ?thesis
-    by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
-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 (simp add: take_bit_eq_mod)
-
 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 even_take_bit_eq [simp]:
-  "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
-  by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
-
 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_0 [simp]:
-  "drop_bit 0 = id"
-  by (simp add: fun_eq_iff drop_bit_eq_div)
-
-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_Suc [simp]:
-  "drop_bit (Suc n) a = drop_bit n (a div 2)"
-proof (cases "even a")
-  case True
-  then obtain b where "a = 2 * b" ..
-  moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
-    by (simp add: drop_bit_eq_div)
-  ultimately show ?thesis
-    by simp
-next
-  case False
-  then obtain b where "a = 2 * b + 1" ..
-  moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
-    using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
-    by (auto simp add: drop_bit_eq_div ac_simps)
-  ultimately show ?thesis
-    by simp
-qed
-
-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 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"])
 
 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)
 
 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,691 +1,737 @@
 (*  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>
 
+lemma length_not_greater_eq_2_iff [simp]:
+  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+  by (auto simp add: not_le dest: less_2_cases)
+
 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)
 
 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_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)) 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 length_cases:
   obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
     | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
 proof (cases "LENGTH('a) \<ge> 2")
   case False
   then have "LENGTH('a) = 1"
     by (auto simp add: not_le dest: less_2_cases)
   then have "take_bit LENGTH('a) 2 = (0 :: int)"
     by simp
   with \<open>LENGTH('a) = 1\<close> triv show ?thesis
     by simp
 next
   case True
   then obtain n where "LENGTH('a) = Suc (Suc n)"
     by (auto dest: le_Suc_ex)
   then have "take_bit LENGTH('a) 2 = (2 :: int)"
     by simp
   with take_bit_2 show ?thesis
     by simp
 qed
 
 
 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; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
   show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
     for a :: "'a word"
     by (transfer; cases rule: length_cases [where ?'a = 'a]) (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 rule: length_cases [where ?'a = 'a])
   case triv
   have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
     by auto
   with triv that show ?thesis
     by (auto; transfer) simp_all
 next
   case take_bit_2
   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 take_bit_2 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 take_bit_2 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 simp
     qed
     ultimately show ?thesis
       by simp
   qed
 qed
 
 instance word :: (len) semiring_bits
 proof
-  show \<open>of_bool (odd a) + 2 * (a div 2) = a\<close>
-    for a :: \<open>'a word\<close>
-    apply (cases \<open>even a\<close>; simp, transfer; cases rule: length_cases [where ?'a = 'a])
-      apply auto
-    apply (auto simp add: take_bit_eq_mod)
-    apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod)
-    done
   show \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
     for a b :: \<open>'a word\<close>
     apply transfer
-    apply (cases rule: length_cases [where ?'a = 'a])
-     apply auto
-       apply (metis even_take_bit_eq len_not_eq_0)
+    apply auto
+       apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
       apply (metis even_take_bit_eq len_not_eq_0)
-    apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus)
-    apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod)
+     apply (metis even_take_bit_eq len_not_eq_0)
+    apply (metis (no_types, hide_lams) div_0 drop_bit_eq_div drop_bit_half dvd_mult_div_cancel even_take_bit_eq mod_div_trivial mod_eq_self_iff_div_eq_0 take_bit_eq_mod)
     done
   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 "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
+    apply transfer
+    apply (auto simp flip: take_bit_eq_mod)
+    apply (simp add: ac_simps)
+    done
+  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
+    apply transfer
+    apply (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)
+    done
 qed
 
 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>Parity.take_bit LENGTH('a) (push_bit n k) = Parity.take_bit LENGTH('a) (push_bit n l)\<close>
     if \<open>Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
   proof -
     from that
     have \<open>Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k)
       = Parity.take_bit (LENGTH('a) - n) (Parity.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"
   proof (cases \<open>n < LENGTH('a)\<close>)
     case True
     then show ?thesis
       by transfer
         (simp add: take_bit_eq_mod drop_bit_eq_div)
   next
     case False
     then obtain m where n: \<open>n = LENGTH('a) + m\<close>
       by (auto simp add: not_less dest: le_Suc_ex)
     then show ?thesis
       by transfer
         (simp add: take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
   qed
 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)
 
 lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is "and"
   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
   interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
   proof
     show "a AND (b OR c) = a AND b OR a AND c"
       for a b c :: "'a word"
       by transfer (simp add: bit.conj_disj_distrib)
     show "a OR b AND c = (a OR b) AND (a OR c)"
       for a b c :: "'a word"
       by transfer (simp add: bit.disj_conj_distrib)
   qed (transfer; simp add: ac_simps)+
   show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
     by (fact bit_word.boolean_algebra_axioms)
   show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
   proof (rule ext)+
     fix a b :: "'a word"
     have "a XOR b = a AND NOT b OR NOT a AND b"
       by transfer (simp add: bit.xor_def)
     then show "bit_word.xor a b = a XOR b"
       by (simp add: bit_word.xor_def)
   qed
 qed
 
 end
 
 end