--- 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 ***
--- 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)
--- 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>
--- 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