# HG changeset patch
# User haftmann
# Date 1708532376 0
# Node ID c172eecba85d49b637f124fe9869d142ee948d61
# Parent  76720aeab21e86199772f58b61bd1a96b8a1db64
simplified specification of type class semiring_bits

diff -r 76720aeab21e -r c172eecba85d src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Bit_Operations.thy	Wed Feb 21 16:19:36 2024 +0000
@@ -14,9 +14,9 @@
     \<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 half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
+  assumes bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+    and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
     and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
-    and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
   fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
   assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 begin
@@ -382,24 +382,6 @@
     with rec [of n True] show ?case
       by simp
   qed
-  show \<open>even (q mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (q div 2 ^ n)\<close> for q m n :: nat
-  proof (cases \<open>m \<le> n\<close>)
-    case True
-    moreover define r where \<open>r = n - m\<close>
-    ultimately have \<open>n = m + r\<close>
-      by simp
-    with True show ?thesis
-      by (simp add: power_add div_mult2_eq)
-  next
-    case False
-    moreover define r where \<open>r = m - Suc n\<close>
-    ultimately have \<open>m = n + Suc r\<close>
-      by simp
-    moreover have \<open>even (q mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (q div 2 ^ n)\<close>
-      by (simp only: power_add) (simp add: mod_mult2_eq dvd_mod_iff)
-    ultimately show ?thesis
-      by simp
-  qed
 qed (auto simp add: div_mult2_eq bit_nat_def)
 
 end
@@ -539,24 +521,6 @@
     with rec [of k True] show ?case
       by (simp add: ac_simps)
   qed
-  show \<open>even (k mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (k div 2 ^ n)\<close> for k :: int and m n :: nat
-  proof (cases \<open>m \<le> n\<close>)
-    case True
-    moreover define r where \<open>r = n - m\<close>
-    ultimately have \<open>n = m + r\<close>
-      by simp
-    with True show ?thesis
-      by (simp add: power_add zdiv_zmult2_eq)
-  next
-    case False
-    moreover define r where \<open>r = m - Suc n\<close>
-    ultimately have \<open>m = n + Suc r\<close>
-      by simp
-    moreover have \<open>even (k mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (k div 2 ^ n)\<close>
-      by (simp only: power_add) (simp add: zmod_zmult2_eq dvd_mod_iff)
-    ultimately show ?thesis
-      by simp
-  qed
 qed (auto simp add: zdiv_zmult2_eq bit_int_def)
 
 end
@@ -879,13 +843,96 @@
   \<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
   by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
 
+lemma bit_drop_bit_eq [bit_simps]:
+  \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
+  by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
+
+lemma disjunctive_xor_eq_or:
+  \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
+  using that by (auto simp add: bit_eq_iff bit_simps)
+
+lemma disjunctive_add_eq_or:
+  \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
+proof (rule bit_eqI)
+  fix n
+  assume \<open>possible_bit TYPE('a) n\<close>
+  moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
+    by simp
+  then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+    by (simp add: bit_simps)
+  ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
+  proof (induction n arbitrary: a b)
+    case 0
+    from "0"(2)[of 0] show ?case
+      by (auto simp add: even_or_iff bit_0)
+  next
+    case (Suc n)
+    from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
+      by (auto simp add: bit_0)
+    have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+      using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+    from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
+      using possible_bit_less_imp by force
+    with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
+    have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+      by (simp add: bit_Suc)
+    have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+      using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+    also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+      using even by (auto simp add: algebra_simps mod2_eq_if)
+    finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+      using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+    also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+      by (rule IH)
+    finally show ?case
+      by (simp add: bit_simps flip: bit_Suc)
+  qed
+qed
+
+lemma disjunctive_add_eq_xor:
+  \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
+  using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
+
 lemma take_bit_0 [simp]:
   "take_bit 0 a = 0"
   by (simp add: take_bit_eq_mod)
 
 lemma bit_take_bit_iff [bit_simps]:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
-  by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le)
+proof -
+  have \<open>push_bit m (drop_bit m a) AND take_bit m a = 0\<close> (is \<open>?lhs = _\<close>)
+  proof (rule bit_eqI)
+    fix n
+    show \<open>bit ?lhs n \<longleftrightarrow> bit 0 n\<close>
+    proof (cases \<open>m \<le> n\<close>)
+      case False
+      then show ?thesis
+        by (simp add: bit_simps)
+    next
+      case True
+      moreover define q where \<open>q = n - m\<close>
+      ultimately have \<open>n = m + q\<close> by simp
+      moreover have \<open>\<not> bit (take_bit m a) (m + q)\<close>
+        by (simp add: take_bit_eq_mod bit_iff_odd flip: div_exp_eq)
+      ultimately show ?thesis
+        by (simp add: bit_simps)
+    qed
+  qed
+  then have \<open>push_bit m (drop_bit m a) XOR take_bit m a = push_bit m (drop_bit m a) + take_bit m a\<close>
+    by (simp add: disjunctive_add_eq_xor)
+  also have \<open>\<dots> = a\<close>
+    by (simp add: bits_ident)
+  finally have \<open>bit (push_bit m (drop_bit m a) XOR take_bit m a) n \<longleftrightarrow> bit a n\<close>
+    by simp
+  also have \<open>\<dots> \<longleftrightarrow> (m \<le> n \<or> n < m) \<and> bit a n\<close>
+    by auto
+  also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
+    by auto
+  also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
+    by (auto simp add: bit_simps bit_imp_possible_bit)
+  finally show ?thesis
+    by (auto simp add: bit_simps)
+qed
 
 lemma take_bit_Suc:
   \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
@@ -915,10 +962,6 @@
   \<open>take_bit n 1 = of_bool (n > 0)\<close>
   by (cases n) (simp_all add: take_bit_Suc)
 
-lemma bit_drop_bit_eq [bit_simps]:
-  \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
-  by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
-
 lemma drop_bit_of_0 [simp]:
   \<open>drop_bit n 0 = 0\<close>
   by (rule bit_eqI) (simp add: bit_simps)
@@ -1245,52 +1288,6 @@
   \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
   by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
 
-lemma disjunctive_xor_eq_or:
-  \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
-  using that by (auto simp add: bit_eq_iff bit_simps)
-
-lemma disjunctive_add_eq_or:
-  \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
-proof (rule bit_eqI)
-  fix n
-  assume \<open>possible_bit TYPE('a) n\<close>
-  moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
-    by simp
-  then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
-    by (simp add: bit_simps)
-  ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
-  proof (induction n arbitrary: a b)
-    case 0
-    from "0"(2)[of 0] show ?case
-      by (auto simp add: even_or_iff bit_0)
-  next
-    case (Suc n)
-    from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
-      by (auto simp add: bit_0)
-    have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
-      using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
-    from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
-      using possible_bit_less_imp by force
-    with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
-    have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
-      by (simp add: bit_Suc)
-    have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
-      using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
-    also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
-      using even by (auto simp add: algebra_simps mod2_eq_if)
-    finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
-      using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
-    also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
-      by (rule IH)
-    finally show ?case
-      by (simp add: bit_simps flip: bit_Suc)
-  qed
-qed
-
-lemma disjunctive_add_eq_xor:
-  \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
-  using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
-
 lemma set_bit_eq:
   \<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
 proof -
@@ -3921,6 +3918,10 @@
   \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
   by (rule disjunctive_add_eq_or) (use that in \<open>simp add: bit_eq_iff bit_simps\<close>)
 
+lemma even_mod_exp_div_exp_iff [no_atp]:
+  \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
+  by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
+
 end
 
 context ring_bit_operations
diff -r 76720aeab21e -r c172eecba85d src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Code_Numeral.thy	Wed Feb 21 16:19:36 2024 +0000
@@ -349,7 +349,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+    half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
@@ -1109,7 +1109,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+    half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
diff -r 76720aeab21e -r c172eecba85d src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Library/Word.thy	Wed Feb 21 16:19:36 2024 +0000
@@ -667,6 +667,32 @@
 
 end
 
+lemma unat_div_distrib:
+  \<open>unat (v div w) = unat v div unat w\<close>
+proof transfer
+  fix k l
+  have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+    by (rule div_le_dividend)
+  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+    by (simp add: nat_less_iff)
+  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
+    (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
+    by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
+qed
+
+lemma unat_mod_distrib:
+  \<open>unat (v mod w) = unat v mod unat w\<close>
+proof transfer
+  fix k l
+  have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+    by (rule mod_less_eq_dividend)
+  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+    by (simp add: nat_less_iff)
+  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
+    (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
+    by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
+qed
+
 instance word :: (len) semiring_parity
   by (standard; transfer)
     (auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
@@ -838,6 +864,9 @@
   show \<open>0 div a = 0\<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>
+    by (simp add: word_eq_iff_unsigned [where ?'a = nat] unat_div_distrib unat_mod_distrib)
   show \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
     for a :: \<open>'a word\<close> and m n :: nat
     apply transfer
@@ -849,10 +878,6 @@
     for a :: \<open>'a word\<close> and n :: nat
     using that by transfer
       (simp add: even_drop_bit_iff_not_bit bit_simps flip: drop_bit_eq_div del: power.simps)
-  show \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
-    for a :: \<open>'a word\<close> and m n :: nat
-    by transfer
-      (auto simp flip: take_bit_eq_mod drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_simps)
 qed
 
 end
@@ -1301,32 +1326,6 @@
   by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
     (simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)
 
-lemma unat_div_distrib:
-  \<open>unat (v div w) = unat v div unat w\<close>
-proof transfer
-  fix k l
-  have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
-    by (rule div_le_dividend)
-  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
-    by (simp add: nat_less_iff)
-  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
-    (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
-    by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
-qed
-
-lemma unat_mod_distrib:
-  \<open>unat (v mod w) = unat v mod unat w\<close>
-proof transfer
-  fix k l
-  have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
-    by (rule mod_less_eq_dividend)
-  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
-    by (simp add: nat_less_iff)
-  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
-    (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
-    by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
-qed
-
 lemma uint_div_distrib:
   \<open>uint (v div w) = uint v div uint w\<close>
 proof -