# HG changeset patch
# User wenzelm
# Date 1701727967 -3600
# Node ID e475d6ac8eb1c7d06b0c8bcbd964c4db1977d34f
# Parent  486a32079c60061d47be85d7892cd60ed68f0eb6# Parent  89d4a8f52738eddf6a8c9fae0a499fd67aed982e
merged

diff -r 89d4a8f52738 -r e475d6ac8eb1 NEWS
--- a/NEWS	Mon Dec 04 23:07:06 2023 +0100
+++ b/NEWS	Mon Dec 04 23:12:47 2023 +0100
@@ -29,6 +29,9 @@
   unique_euclidean_semiring_with_bit_operations is renamed
   to linordered_euclidean_semiring_bit_operations.  Minor INCOMPATIBILITY.
 
+* Streamlined specification of type class (semi)ring_parity.  Minor
+  INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r 89d4a8f52738 -r e475d6ac8eb1 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Mon Dec 04 23:07:06 2023 +0100
+++ b/src/HOL/Bit_Operations.thy	Mon Dec 04 23:12:47 2023 +0100
@@ -5,7 +5,7 @@
 
 theory Bit_Operations
   imports Presburger Groups_List
-begin
+begin                 
 
 subsection \<open>Abstract bit structures\<close>
 
@@ -83,10 +83,6 @@
   \<open>0 mod a = 0\<close>
   using div_mult_mod_eq [of 0 a] by simp
 
-lemma bits_one_mod_two_eq_one [simp]:
-  \<open>1 mod 2 = 1\<close>
-  by (simp add: mod2_eq_if)
-
 lemma bit_0:
   \<open>bit a 0 \<longleftrightarrow> odd a\<close>
   by (simp add: bit_iff_odd)
@@ -3761,68 +3757,75 @@
 
 subsection \<open>Lemma duplicates and other\<close>
 
-lemmas set_bit_def = set_bit_eq_or
-
-lemmas unset_bit_def = unset_bit_eq_and_not
-
-lemmas flip_bit_def = flip_bit_eq_xor
-
-lemma and_nat_rec:
+context semiring_bit_operations
+begin
+
+lemmas bits_one_mod_two_eq_one [no_atp] = one_mod_two_eq_one
+
+lemmas set_bit_def [no_atp] = set_bit_eq_or
+
+lemmas unset_bit_def [no_atp] = unset_bit_eq_and_not
+
+lemmas flip_bit_def [no_atp] = flip_bit_eq_xor
+
+end
+
+lemma and_nat_rec [no_atp]:
   \<open>m AND n = of_bool (odd m \<and> odd n) + 2 * ((m div 2) AND (n div 2))\<close> for m n :: nat
   by (fact and_rec)
 
-lemma or_nat_rec:
+lemma or_nat_rec [no_atp]:
   \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat
   by (fact or_rec)
 
-lemma xor_nat_rec:
+lemma xor_nat_rec [no_atp]:
   \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat
   by (fact xor_rec)
 
-lemma bit_push_bit_iff_nat:
+lemma bit_push_bit_iff_nat [no_atp]:
   \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
   by (fact bit_push_bit_iff')
 
-lemmas and_int_rec = and_int.rec
-
-lemmas bit_and_int_iff = and_int.bit_iff
-
-lemmas or_int_rec = or_int.rec
-
-lemmas bit_or_int_iff = or_int.bit_iff
-
-lemmas xor_int_rec = xor_int.rec
-
-lemmas bit_xor_int_iff = xor_int.bit_iff
-
-lemma not_int_rec:
+lemma mask_half_int [no_atp]:
+  \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
+  by (fact mask_half)
+
+lemma not_int_rec [no_atp]:
   \<open>NOT k = of_bool (even k) + 2 * NOT (k div 2)\<close> for k :: int
   by (fact not_rec)
 
-lemma mask_half_int:
-  \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
-  by (fact mask_half)
-
-lemma drop_bit_push_bit_int:
-  \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
-  by (fact drop_bit_push_bit)
-
-lemma even_not_iff_int:
+lemma even_not_iff_int [no_atp]:
   \<open>even (NOT k) \<longleftrightarrow> odd k\<close> for k :: int
   by (fact even_not_iff)
 
-lemma even_and_iff_int:
-  \<open>even (k AND l) \<longleftrightarrow> even k \<or> even l\<close> for k l :: int
-  by (fact even_and_iff)
-
-lemma bit_push_bit_iff_int:
-  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-  by (fact bit_push_bit_iff')
-
 lemma bit_not_int_iff':
   \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
   by (simp flip: not_eq_complement add: bit_simps)
 
+lemmas and_int_rec [no_atp] = and_int.rec
+
+lemma even_and_iff_int [no_atp]:
+  \<open>even (k AND l) \<longleftrightarrow> even k \<or> even l\<close> for k l :: int
+  by (fact even_and_iff)
+
+lemmas bit_and_int_iff [no_atp] = and_int.bit_iff
+
+lemmas or_int_rec [no_atp] = or_int.rec
+
+lemmas bit_or_int_iff [no_atp] = or_int.bit_iff
+
+lemmas xor_int_rec [no_atp] = xor_int.rec
+
+lemmas bit_xor_int_iff [no_atp] = xor_int.bit_iff
+
+lemma drop_bit_push_bit_int [no_atp]:
+  \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
+  by (fact drop_bit_push_bit)
+
+lemma bit_push_bit_iff_int [no_atp] :
+  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+  by (fact bit_push_bit_iff')
+
 no_notation
   not  (\<open>NOT\<close>)
     and "and"  (infixr \<open>AND\<close> 64)
diff -r 89d4a8f52738 -r e475d6ac8eb1 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Mon Dec 04 23:07:06 2023 +0100
+++ b/src/HOL/Library/Word.thy	Mon Dec 04 23:12:47 2023 +0100
@@ -668,16 +668,7 @@
 end
 
 instance word :: (len) semiring_parity
-proof
-  show "\<not> 2 dvd (1::'a word)"
-    by transfer simp
-  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
-    for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
-  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
-    for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
-qed
+  by (standard; transfer) (simp_all add: mod_2_eq_odd)
 
 lemma word_bit_induct [case_names zero even odd]:
   \<open>P a\<close> if word_zero: \<open>P 0\<close>
diff -r 89d4a8f52738 -r e475d6ac8eb1 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Dec 04 23:07:06 2023 +0100
+++ b/src/HOL/Parity.thy	Mon Dec 04 23:12:47 2023 +0100
@@ -12,16 +12,15 @@
 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"
+  assumes mod_2_eq_odd: \<open>a mod 2 = of_bool (\<not> 2 dvd a)\<close>
+    and odd_one [simp]: \<open>\<not> 2 dvd 1\<close>
 begin
 
 abbreviation even :: "'a \<Rightarrow> bool"
-  where "even a \<equiv> 2 dvd a"
+  where \<open>even a \<equiv> 2 dvd a\<close>
 
 abbreviation odd :: "'a \<Rightarrow> bool"
-  where "odd a \<equiv> \<not> 2 dvd a"
+  where \<open>odd a \<equiv> \<not> 2 dvd a\<close>
 
 end
 
@@ -41,47 +40,44 @@
 context semiring_parity
 begin
 
-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 evenE [elim?]:
+  assumes \<open>even a\<close>
+  obtains b where \<open>a = 2 * b\<close>
+  using assms by (rule dvdE)
+
+lemma oddE [elim?]:
+  assumes \<open>odd a\<close>
+  obtains b where \<open>a = 2 * b + 1\<close>
+proof -
+  have \<open>a = 2 * (a div 2) + a mod 2\<close>
+    by (simp add: mult_div_mod_eq)
+  with assms have \<open>a = 2 * (a div 2) + 1\<close>
+    by (simp add: mod_2_eq_odd)
+  then show thesis ..
+qed
+
+lemma of_bool_odd_eq_mod_2:
+  \<open>of_bool (odd a) = a mod 2\<close>
+  by (simp add: mod_2_eq_odd)
 
 lemma odd_of_bool_self [simp]:
   \<open>odd (of_bool p) \<longleftrightarrow> p\<close>
   by (cases p) simp_all
 
 lemma not_mod_2_eq_0_eq_1 [simp]:
-  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
-  by (cases a rule: parity_cases) simp_all
+  \<open>a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1\<close>
+  by (simp add: mod_2_eq_odd)
 
 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 evenE [elim?]:
-  assumes "even a"
-  obtains b where "a = 2 * b"
-  using assms by (rule dvdE)
+  \<open>a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0\<close>
+  by (simp add: mod_2_eq_odd)
 
-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 even_iff_mod_2_eq_zero:
+  \<open>2 dvd a \<longleftrightarrow> a mod 2 = 0\<close>
+  by (simp add: mod_2_eq_odd)
 
-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"
+lemma odd_iff_mod_2_eq_one:
+  \<open>\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
 
 lemma even_mod_2_iff [simp]:
@@ -92,8 +88,22 @@
   "a mod 2 = (if even a then 0 else 1)"
   by (simp add: mod_2_eq_odd)
 
+lemma zero_mod_two_eq_zero [simp]:
+  \<open>0 mod 2 = 0\<close>
+  by (simp add: mod_2_eq_odd)
+
+lemma one_mod_two_eq_one [simp]:
+  \<open>1 mod 2 = 1\<close>
+  by (simp add: mod_2_eq_odd)
+
+lemma parity_cases [case_names even odd]:
+  assumes \<open>even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P\<close>
+  assumes \<open>odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P\<close>
+  shows P
+  using assms by (auto simp add: mod_2_eq_odd)
+
 lemma even_zero [simp]:
-  "even 0"
+  \<open>even 0\<close>
   by (fact dvd_0_right)
 
 lemma odd_even_add:
@@ -622,15 +632,6 @@
     by simp
 qed
 
-lemma one_mod_two_eq_one [simp]:
-  "1 mod 2 = 1"
-proof -
-  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
-    by (simp only:) simp
-  then show ?thesis
-    by simp
-qed
-
 lemma one_mod_2_pow_eq [simp]:
   "1 mod (2 ^ n) = of_bool (n > 0)"
 proof -
@@ -812,15 +813,13 @@
 
 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
+  show \<open>a mod 2 = of_bool (\<not> 2 dvd a)\<close> for a
+  proof (cases \<open>2 dvd a\<close>)
+    case True
+    then show ?thesis
+      by (simp add: dvd_eq_mod_eq_0)
   next
-    assume "\<not> 2 dvd a"
+    case False
     have eucl: "euclidean_size (a mod 2) = 1"
     proof (rule Orderings.order_antisym)
       show "euclidean_size (a mod 2) \<le> 1"
@@ -841,15 +840,17 @@
     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"
+    have "a mod 2 = 1"
       by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
+    with \<open>\<not> 2 dvd a\<close> show ?thesis
+      by simp
   qed
-  show "\<not> is_unit 2"
-  proof (rule notI)
-    assume "is_unit 2"
-    then have "of_nat 2 dvd of_nat 1"
+  show \<open>\<not> is_unit 2\<close>
+  proof
+    assume \<open>is_unit 2\<close>
+    then have \<open>of_nat 2 dvd of_nat 1\<close>
       by simp
-    then have "is_unit (2::nat)"
+    then have \<open>is_unit (2::nat)\<close>
       by (simp only: of_nat_dvd_iff)
     then show False
       by simp