--- a/src/HOL/Bit_Operations.thy Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Bit_Operations.thy Mon Jan 29 19:35:07 2024 +0000
@@ -9,15 +9,12 @@
subsection \<open>Abstract bit structures\<close>
-class semiring_bits = semiring_parity +
+class semiring_bits = semiring_parity + semiring_modulo_trivial +
assumes 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_by_0 [simp]: \<open>a div 0 = 0\<close>
- and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
- and bits_0_div [simp]: \<open>0 div a = 0\<close>
- and even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ assumes even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<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_decr_exp_div_exp_iff: \<open>2 ^ n \<noteq> 0 \<Longrightarrow> even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
@@ -36,18 +33,6 @@
\<open>1 div 2 = 0\<close>
using even_half_succ_eq [of 0] by simp
-lemma bits_mod_by_0 [simp]:
- \<open>a mod 0 = a\<close>
- using div_mult_mod_eq [of a 0] by simp
-
-lemma bits_mod_by_1 [simp]:
- \<open>a mod 1 = 0\<close>
- using div_mult_mod_eq [of a 1] by simp
-
-lemma bits_0_mod [simp]:
- \<open>0 mod a = 0\<close>
- using div_mult_mod_eq [of 0 a] by simp
-
lemma div_exp_eq_funpow_half:
\<open>a div 2 ^ n = ((\<lambda>a. a div 2) ^^ n) a\<close>
proof -
@@ -3716,10 +3701,6 @@
\<open>1 div 2 ^ n = of_bool (n = 0)\<close>
using div_exp_eq [of 1 1] by (cases n) simp_all
-lemmas bits_div_0 = bits_0_div
-
-lemmas bits_mod_0 = bits_0_mod
-
lemma exp_add_not_zero_imp [no_atp]:
\<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
proof -
--- a/src/HOL/Code_Numeral.thy Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Code_Numeral.thy Mon Jan 29 19:35:07 2024 +0000
@@ -348,7 +348,7 @@
is take_bit .
instance by (standard; transfer)
- (fact bit_induct bits_div_by_0 bits_div_by_1 bits_0_div even_half_succ_eq
+ (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_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
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
@@ -1108,7 +1108,7 @@
is take_bit .
instance by (standard; transfer)
- (fact bit_induct bits_div_by_0 bits_div_by_1 bits_0_div even_half_succ_eq
+ (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_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
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
--- a/src/HOL/Fields.thy Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Fields.thy Mon Jan 29 19:35:07 2024 +0000
@@ -136,7 +136,10 @@
qed
lemma inverse_1 [simp]: "inverse 1 = 1"
-by (rule inverse_unique) simp
+ by (rule inverse_unique) simp
+
+subclass divide_trivial
+ by standard (simp_all add: divide_inverse)
lemma nonzero_inverse_mult_distrib:
assumes "a \<noteq> 0" and "b \<noteq> 0"
@@ -250,9 +253,9 @@
"z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
by (simp add: divide_diff_eq_iff[symmetric])
-lemma division_ring_divide_zero [simp]:
+lemma division_ring_divide_zero:
"a / 0 = 0"
- by (simp add: divide_inverse)
+ by (fact div_by_0)
lemma divide_self_if [simp]:
"a / a = (if a = 0 then 0 else 1)"
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Mon Jan 29 19:35:07 2024 +0000
@@ -768,6 +768,9 @@
instance star :: (idom) idom ..
instance star :: (idom_divide) idom_divide ..
+instance star :: (divide_trivial) divide_trivial
+ by (intro_classes; transfer) simp_all
+
instance star :: (division_ring) division_ring
by (intro_classes; transfer) (simp_all add: divide_inverse)
--- a/src/HOL/Rings.thy Mon Jan 29 11:54:44 2024 +0100
+++ b/src/HOL/Rings.thy Mon Jan 29 19:35:07 2024 +0000
@@ -706,16 +706,32 @@
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
+class divide_trivial = zero + one + divide +
+ assumes div_by_0 [simp]: \<open>a div 0 = 0\<close>
+ and div_by_1 [simp]: \<open>a div 1 = a\<close>
+ and div_0 [simp]: \<open>0 div a = 0\<close>
+
+
text \<open>Algebraic classes with division\<close>
class semidom_divide = semidom + divide +
- assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
- assumes div_by_0 [simp]: "a div 0 = 0"
+ assumes nonzero_mult_div_cancel_right [simp]: \<open>b \<noteq> 0 \<Longrightarrow> (a * b) div b = a\<close>
+ assumes semidom_div_by_0: \<open>a div 0 = 0\<close>
begin
-lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
+lemma nonzero_mult_div_cancel_left [simp]: \<open>a \<noteq> 0 \<Longrightarrow> (a * b) div a = b\<close>
using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
+subclass divide_trivial
+proof
+ show [simp]: \<open>a div 0 = 0\<close> for a
+ by (fact semidom_div_by_0)
+ show \<open>a div 1 = a\<close> for a
+ using nonzero_mult_div_cancel_right [of 1 a] by simp
+ show \<open>0 div a = 0\<close> for a
+ using nonzero_mult_div_cancel_right [of a 0] by (cases \<open>a = 0\<close>) simp_all
+qed
+
subclass semiring_no_zero_divisors_cancel
proof
show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c
@@ -740,20 +756,6 @@
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
using nonzero_mult_div_cancel_left [of a 1] by simp
-lemma div_0 [simp]: "0 div a = 0"
-proof (cases "a = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have "a * 0 div a = 0"
- by (rule nonzero_mult_div_cancel_left)
- then show ?thesis by simp
-qed
-
-lemma div_by_1 [simp]: "a div 1 = a"
- using nonzero_mult_div_cancel_left [of 1 a] by simp
-
lemma dvd_div_eq_0_iff:
assumes "b dvd a"
shows "a div b = 0 \<longleftrightarrow> a = 0"
@@ -1725,7 +1727,7 @@
text \<open>Arbitrary quotient and remainder partitions\<close>
class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
- assumes div_mult_mod_eq: "a div b * b + a mod b = a"
+ assumes div_mult_mod_eq: \<open>a div b * b + a mod b = a\<close>
begin
lemma mod_div_decomp:
@@ -1775,25 +1777,37 @@
end
+class semiring_modulo_trivial = semiring_modulo + divide_trivial
+begin
+
+lemma mod_0 [simp]:
+ \<open>0 mod a = 0\<close>
+ using div_mult_mod_eq [of 0 a] by simp
+
+lemma mod_by_0 [simp]:
+ \<open>a mod 0 = a\<close>
+ using div_mult_mod_eq [of a 0] by simp
+
+lemma mod_by_1 [simp]:
+ \<open>a mod 1 = 0\<close>
+proof -
+ have \<open>a + a mod 1 = a\<close>
+ using div_mult_mod_eq [of a 1] by simp
+ then have \<open>a + a mod 1 = a + 0\<close>
+ by simp
+ then show ?thesis
+ by (rule add_left_imp_eq)
+qed
+
+end
+
subsection \<open>Quotient and remainder in integral domains\<close>
class semidom_modulo = algebraic_semidom + semiring_modulo
begin
-lemma mod_0 [simp]: "0 mod a = 0"
- using div_mult_mod_eq [of 0 a] by simp
-
-lemma mod_by_0 [simp]: "a mod 0 = a"
- using div_mult_mod_eq [of a 0] by simp
-
-lemma mod_by_1 [simp]:
- "a mod 1 = 0"
-proof -
- from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
- then have "a + a mod 1 = a + 0" by simp
- then show ?thesis by (rule add_left_imp_eq)
-qed
+subclass semiring_modulo_trivial ..
lemma mod_self [simp]:
"a mod a = 0"