--- a/src/HOL/Examples/Gauss_Numbers.thy Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/Examples/Gauss_Numbers.thy Wed Apr 19 18:21:30 2023 +0000
@@ -4,7 +4,7 @@
section \<open>Gauss Numbers: integral gauss numbers\<close>
theory Gauss_Numbers
- imports "HOL-Library.Rounded_Division"
+ imports "HOL-Library.Centered_Division"
begin
codatatype gauss = Gauss (Re: int) (Im: int)
@@ -308,17 +308,17 @@
primcorec divide_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
where
- \<open>Re (x div y) = (Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
- | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
+ \<open>Re (x div y) = (Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
+ | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
primcorec modulo_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
where
\<open>Re (x mod y) = Re x -
- ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y -
- (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y)\<close>
+ ((Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y -
+ (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y)\<close>
| \<open>Im (x mod y) = Im x -
- ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y +
- (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y)\<close>
+ ((Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y +
+ (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y)\<close>
instance proof
fix x y :: gauss
@@ -334,7 +334,7 @@
\<open>(Im y)\<^sup>2 + (Re y)\<^sup>2 = Y\<close>
by (simp_all add: power2_eq_square algebra_simps Y_def)
from \<open>Y > 0\<close> show ?thesis
- by (simp add: gauss_eq_iff algebra_simps) (simp add: * nonzero_mult_rdiv_cancel_right)
+ by (simp add: gauss_eq_iff algebra_simps) (simp add: * nonzero_mult_cdiv_cancel_right)
qed
show \<open>x div y * y + x mod y = x\<close>
by (simp add: gauss_eq_iff)
@@ -360,22 +360,22 @@
by (simp_all add: gauss_neq_0 euclidean_size_gauss_def)
have \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>
by (simp add: R_def I_def X_def Y_def power2_eq_square algebra_simps)
- let ?lhs = \<open>X - I * (I rdiv Y) - R * (R rdiv Y)
- - I rdiv Y * (I rmod Y) - R rdiv Y * (R rmod Y)\<close>
- have \<open>?lhs = X + Y * (R rdiv Y) * (R rdiv Y) + Y * (I rdiv Y) * (I rdiv Y)
- - 2 * (R rdiv Y * R + I rdiv Y * I)\<close>
- by (simp flip: minus_rmod_eq_mult_rdiv add: algebra_simps)
+ let ?lhs = \<open>X - I * (I cdiv Y) - R * (R cdiv Y)
+ - I cdiv Y * (I cmod Y) - R cdiv Y * (R cmod Y)\<close>
+ have \<open>?lhs = X + Y * (R cdiv Y) * (R cdiv Y) + Y * (I cdiv Y) * (I cdiv Y)
+ - 2 * (R cdiv Y * R + I cdiv Y * I)\<close>
+ by (simp flip: minus_cmod_eq_mult_cdiv add: algebra_simps)
also have \<open>\<dots> = (Re (x mod y))\<^sup>2 + (Im (x mod y))\<^sup>2\<close>
by (simp add: X_def Y_def R_def I_def algebra_simps power2_eq_square)
finally have lhs: \<open>int (euclidean_size (x mod y)) = ?lhs\<close>
by (simp add: euclidean_size_gauss_def)
- have \<open>?lhs * Y = (I rmod Y)\<^sup>2 + (R rmod Y)\<^sup>2\<close>
+ have \<open>?lhs * Y = (I cmod Y)\<^sup>2 + (R cmod Y)\<^sup>2\<close>
apply (simp add: algebra_simps power2_eq_square \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>)
- apply (simp flip: mult.assoc add.assoc minus_rmod_eq_mult_rdiv)
+ apply (simp flip: mult.assoc add.assoc minus_cmod_eq_mult_cdiv)
apply (simp add: algebra_simps)
done
also have \<open>\<dots> \<le> (Y div 2)\<^sup>2 + (Y div 2)\<^sup>2\<close>
- by (rule add_mono) (use \<open>Y > 0\<close> abs_rmod_less_equal [of Y] in \<open>simp_all add: power2_le_iff_abs_le\<close>)
+ by (rule add_mono) (use \<open>Y > 0\<close> abs_cmod_less_equal [of Y] in \<open>simp_all add: power2_le_iff_abs_le\<close>)
also have \<open>\<dots> < Y\<^sup>2\<close>
using \<open>Y > 0\<close> by (cases \<open>Y = 1\<close>) (simp_all add: power2_eq_square mult_le_less_imp_less flip: mult.assoc)
finally have \<open>?lhs * Y < Y\<^sup>2\<close> .
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Centered_Division.thy Wed Apr 19 18:21:30 2023 +0000
@@ -0,0 +1,178 @@
+(* Author: Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Division with modulus centered towards zero.\<close>
+
+theory Centered_Division
+ imports Main
+begin
+
+lemma off_iff_abs_mod_2_eq_one:
+ \<open>odd l \<longleftrightarrow> \<bar>l\<bar> mod 2 = 1\<close> for l :: int
+ by (simp flip: odd_iff_mod_2_eq_one)
+
+text \<open>
+ \noindent The following specification of division on integers centers
+ the modulus around zero. This is useful e.g.~to define division
+ on Gauss numbers.
+ N.b.: This is not mentioned \cite{leijen01}.
+\<close>
+
+definition centered_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>cdiv\<close> 70)
+ where \<open>k cdiv l = sgn l * ((k + \<bar>l\<bar> div 2) div \<bar>l\<bar>)\<close>
+
+definition centered_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>cmod\<close> 70)
+ where \<open>k cmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+
+text \<open>
+ \noindent Example: @{lemma \<open>k cmod 5 \<in> {-2, -1, 0, 1, 2}\<close> by (auto simp add: centered_modulo_def)}
+\<close>
+
+lemma signed_take_bit_eq_cmod:
+ \<open>signed_take_bit n k = k cmod (2 ^ Suc n)\<close>
+ by (simp only: centered_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)
+ (simp add: signed_take_bit_eq_take_bit_shift)
+
+text \<open>
+ \noindent Property @{thm signed_take_bit_eq_cmod [no_vars]} is the key to generalize
+ centered division to arbitrary structures satisfying \<^class>\<open>ring_bit_operations\<close>,
+ but so far it is not clear what practical relevance that would have.
+\<close>
+
+lemma cdiv_mult_cmod_eq:
+ \<open>k cdiv l * l + k cmod l = k\<close>
+proof -
+ have *: \<open>l * (sgn l * j) = \<bar>l\<bar> * j\<close> for j
+ by (simp add: ac_simps abs_sgn)
+ show ?thesis
+ by (simp add: centered_divide_def centered_modulo_def algebra_simps *)
+qed
+
+lemma mult_cdiv_cmod_eq:
+ \<open>l * (k cdiv l) + k cmod l = k\<close>
+ using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma cmod_cdiv_mult_eq:
+ \<open>k cmod l + k cdiv l * l = k\<close>
+ using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma cmod_mult_cdiv_eq:
+ \<open>k cmod l + l * (k cdiv l) = k\<close>
+ using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma minus_cdiv_mult_eq_cmod:
+ \<open>k - k cdiv l * l = k cmod l\<close>
+ by (rule add_implies_diff [symmetric]) (fact cmod_cdiv_mult_eq)
+
+lemma minus_mult_cdiv_eq_cmod:
+ \<open>k - l * (k cdiv l) = k cmod l\<close>
+ by (rule add_implies_diff [symmetric]) (fact cmod_mult_cdiv_eq)
+
+lemma minus_cmod_eq_cdiv_mult:
+ \<open>k - k cmod l = k cdiv l * l\<close>
+ by (rule add_implies_diff [symmetric]) (fact cdiv_mult_cmod_eq)
+
+lemma minus_cmod_eq_mult_cdiv:
+ \<open>k - k cmod l = l * (k cdiv l)\<close>
+ by (rule add_implies_diff [symmetric]) (fact mult_cdiv_cmod_eq)
+
+lemma cdiv_0_eq [simp]:
+ \<open>k cdiv 0 = 0\<close>
+ by (simp add: centered_divide_def)
+
+lemma cmod_0_eq [simp]:
+ \<open>k cmod 0 = k\<close>
+ by (simp add: centered_modulo_def)
+
+lemma cdiv_1_eq [simp]:
+ \<open>k cdiv 1 = k\<close>
+ by (simp add: centered_divide_def)
+
+lemma cmod_1_eq [simp]:
+ \<open>k cmod 1 = 0\<close>
+ by (simp add: centered_modulo_def)
+
+lemma zero_cdiv_eq [simp]:
+ \<open>0 cdiv k = 0\<close>
+ by (auto simp add: centered_divide_def not_less zdiv_eq_0_iff)
+
+lemma zero_cmod_eq [simp]:
+ \<open>0 cmod k = 0\<close>
+ by (auto simp add: centered_modulo_def not_less zmod_trivial_iff)
+
+lemma cdiv_minus_eq:
+ \<open>k cdiv - l = - (k cdiv l)\<close>
+ by (simp add: centered_divide_def)
+
+lemma cmod_minus_eq [simp]:
+ \<open>k cmod - l = k cmod l\<close>
+ by (simp add: centered_modulo_def)
+
+lemma cdiv_abs_eq:
+ \<open>k cdiv \<bar>l\<bar> = sgn l * (k cdiv l)\<close>
+ by (simp add: centered_divide_def)
+
+lemma cmod_abs_eq [simp]:
+ \<open>k cmod \<bar>l\<bar> = k cmod l\<close>
+ by (simp add: centered_modulo_def)
+
+lemma nonzero_mult_cdiv_cancel_right:
+ \<open>k * l cdiv l = k\<close> if \<open>l \<noteq> 0\<close>
+proof -
+ have \<open>sgn l * k * \<bar>l\<bar> cdiv l = k\<close>
+ using that by (simp add: centered_divide_def)
+ with that show ?thesis
+ by (simp add: ac_simps abs_sgn)
+qed
+
+lemma cdiv_self_eq [simp]:
+ \<open>k cdiv k = 1\<close> if \<open>k \<noteq> 0\<close>
+ using that nonzero_mult_cdiv_cancel_right [of k 1] by simp
+
+lemma cmod_self_eq [simp]:
+ \<open>k cmod k = 0\<close>
+proof -
+ have \<open>(sgn k * \<bar>k\<bar> + \<bar>k\<bar> div 2) mod \<bar>k\<bar> = \<bar>k\<bar> div 2\<close>
+ by (auto simp add: zmod_trivial_iff)
+ also have \<open>sgn k * \<bar>k\<bar> = k\<close>
+ by (simp add: abs_sgn)
+ finally show ?thesis
+ by (simp add: centered_modulo_def algebra_simps)
+qed
+
+lemma cmod_less_divisor:
+ \<open>k cmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+ using that pos_mod_bound [of \<open>\<bar>l\<bar>\<close>] by (simp add: centered_modulo_def)
+
+lemma cmod_less_equal_divisor:
+ \<open>k cmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+proof -
+ from that cmod_less_divisor [of l k]
+ have \<open>k cmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+ by simp
+ also have \<open>\<bar>l\<bar> - \<bar>l\<bar> div 2 = \<bar>l\<bar> div 2 + of_bool (odd l)\<close>
+ by auto
+ finally show ?thesis
+ by (cases \<open>even l\<close>) simp_all
+qed
+
+lemma divisor_less_equal_cmod':
+ \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k cmod l\<close> if \<open>l \<noteq> 0\<close>
+proof -
+ have \<open>0 \<le> (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar>\<close>
+ using that pos_mod_sign [of \<open>\<bar>l\<bar>\<close>] by simp
+ then show ?thesis
+ by (simp_all add: centered_modulo_def)
+qed
+
+lemma divisor_less_equal_cmod:
+ \<open>- (\<bar>l\<bar> div 2) \<le> k cmod l\<close> if \<open>l \<noteq> 0\<close>
+ using that divisor_less_equal_cmod' [of l k]
+ by (simp add: centered_modulo_def)
+
+lemma abs_cmod_less_equal:
+ \<open>\<bar>k cmod l\<bar> \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+ using that divisor_less_equal_cmod [of l k]
+ by (simp add: abs_le_iff cmod_less_equal_divisor)
+
+end
--- a/src/HOL/Library/Library.thy Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/Library/Library.thy Wed Apr 19 18:21:30 2023 +0000
@@ -6,6 +6,7 @@
BNF_Axiomatization
BNF_Corec
Bourbaki_Witt_Fixpoint
+ Centered_Division
Char_ord
Code_Cardinality
Code_Lazy
@@ -78,7 +79,6 @@
Ramsey
Reflection
Rewrite
- Rounded_Division
Saturated
Set_Algebras
Set_Idioms
--- a/src/HOL/Library/Rounded_Division.thy Wed Apr 19 14:48:43 2023 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen
-*)
-
-section \<open>Rounded division: modulus centered towards zero.\<close>
-
-theory Rounded_Division
- imports Main
-begin
-
-lemma off_iff_abs_mod_2_eq_one:
- \<open>odd l \<longleftrightarrow> \<bar>l\<bar> mod 2 = 1\<close> for l :: int
- by (simp flip: odd_iff_mod_2_eq_one)
-
-text \<open>
- \noindent The following specification of division on integers centers
- the modulus around zero. This is useful e.g.~to define division
- on Gauss numbers.
- N.b.: This is not mentioned \cite{leijen01}.
-\<close>
-
-definition rounded_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>rdiv\<close> 70)
- where \<open>k rdiv l = sgn l * ((k + \<bar>l\<bar> div 2) div \<bar>l\<bar>)\<close>
-
-definition rounded_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> (infixl \<open>rmod\<close> 70)
- where \<open>k rmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
-
-text \<open>
- \noindent Example: @{lemma \<open>k rmod 5 \<in> {-2, -1, 0, 1, 2}\<close> by (auto simp add: rounded_modulo_def)}
-\<close>
-
-lemma signed_take_bit_eq_rmod:
- \<open>signed_take_bit n k = k rmod (2 ^ Suc n)\<close>
- by (simp only: rounded_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)
- (simp add: signed_take_bit_eq_take_bit_shift)
-
-text \<open>
- \noindent Property @{thm signed_take_bit_eq_rmod [no_vars]} is the key to generalize
- rounded division to arbitrary structures satisfying \<^class>\<open>ring_bit_operations\<close>,
- but so far it is not clear what practical relevance that would have.
-\<close>
-
-lemma rdiv_mult_rmod_eq:
- \<open>k rdiv l * l + k rmod l = k\<close>
-proof -
- have *: \<open>l * (sgn l * j) = \<bar>l\<bar> * j\<close> for j
- by (simp add: ac_simps abs_sgn)
- show ?thesis
- by (simp add: rounded_divide_def rounded_modulo_def algebra_simps *)
-qed
-
-lemma mult_rdiv_rmod_eq:
- \<open>l * (k rdiv l) + k rmod l = k\<close>
- using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma rmod_rdiv_mult_eq:
- \<open>k rmod l + k rdiv l * l = k\<close>
- using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma rmod_mult_rdiv_eq:
- \<open>k rmod l + l * (k rdiv l) = k\<close>
- using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma minus_rdiv_mult_eq_rmod:
- \<open>k - k rdiv l * l = k rmod l\<close>
- by (rule add_implies_diff [symmetric]) (fact rmod_rdiv_mult_eq)
-
-lemma minus_mult_rdiv_eq_rmod:
- \<open>k - l * (k rdiv l) = k rmod l\<close>
- by (rule add_implies_diff [symmetric]) (fact rmod_mult_rdiv_eq)
-
-lemma minus_rmod_eq_rdiv_mult:
- \<open>k - k rmod l = k rdiv l * l\<close>
- by (rule add_implies_diff [symmetric]) (fact rdiv_mult_rmod_eq)
-
-lemma minus_rmod_eq_mult_rdiv:
- \<open>k - k rmod l = l * (k rdiv l)\<close>
- by (rule add_implies_diff [symmetric]) (fact mult_rdiv_rmod_eq)
-
-lemma rdiv_0_eq [simp]:
- \<open>k rdiv 0 = 0\<close>
- by (simp add: rounded_divide_def)
-
-lemma rmod_0_eq [simp]:
- \<open>k rmod 0 = k\<close>
- by (simp add: rounded_modulo_def)
-
-lemma rdiv_1_eq [simp]:
- \<open>k rdiv 1 = k\<close>
- by (simp add: rounded_divide_def)
-
-lemma rmod_1_eq [simp]:
- \<open>k rmod 1 = 0\<close>
- by (simp add: rounded_modulo_def)
-
-lemma zero_rdiv_eq [simp]:
- \<open>0 rdiv k = 0\<close>
- by (auto simp add: rounded_divide_def not_less zdiv_eq_0_iff)
-
-lemma zero_rmod_eq [simp]:
- \<open>0 rmod k = 0\<close>
- by (auto simp add: rounded_modulo_def not_less zmod_trivial_iff)
-
-lemma rdiv_minus_eq:
- \<open>k rdiv - l = - (k rdiv l)\<close>
- by (simp add: rounded_divide_def)
-
-lemma rmod_minus_eq [simp]:
- \<open>k rmod - l = k rmod l\<close>
- by (simp add: rounded_modulo_def)
-
-lemma rdiv_abs_eq:
- \<open>k rdiv \<bar>l\<bar> = sgn l * (k rdiv l)\<close>
- by (simp add: rounded_divide_def)
-
-lemma rmod_abs_eq [simp]:
- \<open>k rmod \<bar>l\<bar> = k rmod l\<close>
- by (simp add: rounded_modulo_def)
-
-lemma nonzero_mult_rdiv_cancel_right:
- \<open>k * l rdiv l = k\<close> if \<open>l \<noteq> 0\<close>
-proof -
- have \<open>sgn l * k * \<bar>l\<bar> rdiv l = k\<close>
- using that by (simp add: rounded_divide_def)
- with that show ?thesis
- by (simp add: ac_simps abs_sgn)
-qed
-
-lemma rdiv_self_eq [simp]:
- \<open>k rdiv k = 1\<close> if \<open>k \<noteq> 0\<close>
- using that nonzero_mult_rdiv_cancel_right [of k 1] by simp
-
-lemma rmod_self_eq [simp]:
- \<open>k rmod k = 0\<close>
-proof -
- have \<open>(sgn k * \<bar>k\<bar> + \<bar>k\<bar> div 2) mod \<bar>k\<bar> = \<bar>k\<bar> div 2\<close>
- by (auto simp add: zmod_trivial_iff)
- also have \<open>sgn k * \<bar>k\<bar> = k\<close>
- by (simp add: abs_sgn)
- finally show ?thesis
- by (simp add: rounded_modulo_def algebra_simps)
-qed
-
-lemma rmod_less_divisor:
- \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
- using that pos_mod_bound [of \<open>\<bar>l\<bar>\<close>] by (simp add: rounded_modulo_def)
-
-lemma rmod_less_equal_divisor:
- \<open>k rmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
-proof -
- from that rmod_less_divisor [of l k]
- have \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
- by simp
- also have \<open>\<bar>l\<bar> - \<bar>l\<bar> div 2 = \<bar>l\<bar> div 2 + of_bool (odd l)\<close>
- by auto
- finally show ?thesis
- by (cases \<open>even l\<close>) simp_all
-qed
-
-lemma divisor_less_equal_rmod':
- \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
-proof -
- have \<open>0 \<le> (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar>\<close>
- using that pos_mod_sign [of \<open>\<bar>l\<bar>\<close>] by simp
- then show ?thesis
- by (simp_all add: rounded_modulo_def)
-qed
-
-lemma divisor_less_equal_rmod:
- \<open>- (\<bar>l\<bar> div 2) \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
- using that divisor_less_equal_rmod' [of l k]
- by (simp add: rounded_modulo_def)
-
-lemma abs_rmod_less_equal:
- \<open>\<bar>k rmod l\<bar> \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
- using that divisor_less_equal_rmod [of l k]
- by (simp add: abs_le_iff rmod_less_equal_divisor)
-
-end
--- a/src/HOL/ex/Note_on_signed_division_on_words.thy Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy Wed Apr 19 18:21:30 2023 +0000
@@ -1,5 +1,5 @@
theory Note_on_signed_division_on_words
- imports "HOL-Library.Word" "HOL-Library.Rounded_Division"
+ imports "HOL-Library.Word" "HOL-Library.Centered_Division"
begin
unbundle bit_operations_syntax
@@ -24,26 +24,26 @@
end
lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> (infixl \<open>wdiv\<close> 70)
- is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+ is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
by (simp flip: signed_take_bit_decr_length_iff)
lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> (infixl \<open>wmod\<close> 70)
- is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+ is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
by (simp flip: signed_take_bit_decr_length_iff)
lemma signed_take_bit_eq_wmod:
\<open>signed_take_bit n w = w wmod (2 ^ Suc n)\<close>
proof (transfer fixing: n)
show \<open>take_bit LENGTH('a) (signed_take_bit n (take_bit LENGTH('a) k)) =
- take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k rmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
+ take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k cmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
proof (cases \<open>LENGTH('a) = Suc (Suc n)\<close>)
case True
then show ?thesis
- by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit rmod_minus_eq flip: power_Suc signed_take_bit_eq_rmod)
+ by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit cmod_minus_eq flip: power_Suc signed_take_bit_eq_cmod)
next
case False
then show ?thesis
- by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_rmod)
+ by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_cmod)
qed
qed