# HG changeset patch
# User haftmann
# Date 1681214346 0
# Node ID fb3d81bd9803b04e6bde98c839b52ef67d69c293
# Parent  ae9e6218443dda4b7da49e5c842d9fd8254f803d
some remarks on division

diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/Euclidean_Rings.thy
--- 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}"
diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/Library/Rounded_Division.thy
--- 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)
diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/Library/Signed_Division.thy
--- 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
 
diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/Library/Word.thy
--- 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
 
diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/Library/document/root.bib
--- 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}},
diff -r ae9e6218443d -r fb3d81bd9803 src/HOL/document/root.bib
--- 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}}