--- a/src/HOL/Euclidean_Rings.thy Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Euclidean_Rings.thy Tue Apr 11 11:59:06 2023 +0000
@@ -1654,6 +1654,13 @@
subsection \<open>Division on \<^typ>\<open>int\<close>\<close>
+text \<open>
+ The following specification of integer division rounds towards minus infinity
+ and is advocated by Donald Knuth. See \cite{leijen01} for an overview and
+ terminology of different possibilities to specify integer division;
+ there division rounding towards minus infinitiy is named ``F-division''.
+\<close>
+
subsubsection \<open>Basic instantiation\<close>
instantiation int :: "{normalization_semidom, idom_modulo}"
--- a/src/HOL/Library/Rounded_Division.thy Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Library/Rounded_Division.thy Tue Apr 11 11:59:06 2023 +0000
@@ -11,12 +11,34 @@
\<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 -
@@ -118,11 +140,6 @@
by (simp add: rounded_modulo_def algebra_simps)
qed
-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)
-
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)
--- a/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:06 2023 +0000
@@ -47,6 +47,13 @@
end
+text \<open>
+ \noindent The following specification of division is named ``T-division'' in \cite{leijen01}.
+ It is motivated by ISO C99, which in turn adopted the typical behavior of
+ hardware modern in the beginning of the 1990ies; but note ISO C99 describes
+ the instance on machine words, not mathematical integers.
+\<close>
+
instantiation int :: signed_division
begin
--- a/src/HOL/Library/Word.thy Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Library/Word.thy Tue Apr 11 11:59:06 2023 +0000
@@ -624,6 +624,11 @@
subsection \<open>Bit-wise operations\<close>
+text \<open>
+ The following specification of word division just lifts the pre-existing
+ division on integers named ``F-Division'' in \cite{leijen01}.
+\<close>
+
instantiation word :: (len) semiring_modulo
begin
--- a/src/HOL/Library/document/root.bib Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Library/document/root.bib Tue Apr 11 11:59:06 2023 +0000
@@ -43,6 +43,12 @@
publisher = {Springer},
series = {LNCS 664}}
+@article{leijen01,
+ author = {Leijen, Daan},
+ title = {Division and Modulus for Computer Scientists},
+ year = 2001,
+ url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}}
+
@InProceedings{LochbihlerStoop2018,
author = {Andreas Lochbihler and Pascal Stoop},
title = {Lazy Algebraic Types in {Isabelle/HOL}},
--- a/src/HOL/document/root.bib Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/document/root.bib Tue Apr 11 11:59:06 2023 +0000
@@ -60,3 +60,9 @@
year = 1993,
publisher = {Springer},
series = {LNCS 664}}
+
+@article{leijen01,
+ author = {Leijen, Daan},
+ title = {Division and Modulus for Computer Scientists},
+ year = 2001,
+ url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}}