--- a/src/HOL/Euclidean_Rings.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Euclidean_Rings.thy Wed Apr 12 09:18:36 2023 +0200
@@ -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/Cancellation.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Cancellation.thy Wed Apr 12 09:18:36 2023 +0200
@@ -74,7 +74,7 @@
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))
-subsection \<open>Simproc Set-Up\<close>
+text \<open>Simproc Set-Up\<close>
ML_file \<open>Cancellation/cancel.ML\<close>
ML_file \<open>Cancellation/cancel_data.ML\<close>
--- a/src/HOL/Library/Case_Converter.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Case_Converter.thy Wed Apr 12 09:18:36 2023 +0200
@@ -1,12 +1,12 @@
(* Author: Pascal Stoop, ETH Zurich
Author: Andreas Lochbihler, Digital Asset *)
+section \<open>Eliminating pattern matches\<close>
+
theory Case_Converter
imports Main
begin
-subsection \<open>Eliminating pattern matches\<close>
-
definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
[code del]: "missing_pattern_match m f = f ()"
--- a/src/HOL/Library/Code_Cardinality.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Code_Cardinality.thy Wed Apr 12 09:18:36 2023 +0200
@@ -1,4 +1,4 @@
-subsection \<open>Code setup for sets with cardinality type information\<close>
+section \<open>Code setup for sets with cardinality type information\<close>
theory Code_Cardinality imports Cardinality begin
--- a/src/HOL/Library/Code_Test.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Code_Test.thy Wed Apr 12 09:18:36 2023 +0200
@@ -4,6 +4,8 @@
Test infrastructure for the code generator.
*)
+section \<open>Test infrastructure for the code generator\<close>
+
theory Code_Test
imports Main
keywords "test_code" :: diag
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Apr 12 09:18:36 2023 +0200
@@ -2,7 +2,7 @@
Author: Johannes Hölzl
*)
-subsection \<open>The type of non-negative extended real numbers\<close>
+section \<open>The type of non-negative extended real numbers\<close>
theory Extended_Nonnegative_Real
imports Extended_Real Indicator_Function
--- a/src/HOL/Library/Finite_Lattice.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Wed Apr 12 09:18:36 2023 +0200
@@ -2,10 +2,14 @@
Author: Alessandro Coglio
*)
+section \<open>Finite Lattices\<close>
+
theory Finite_Lattice
imports Product_Order
begin
+subsection \<open>Finite Complete Lattices\<close>
+
text \<open>A non-empty finite lattice is a complete lattice.
Since types are never empty in Isabelle/HOL,
a type of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>
--- a/src/HOL/Library/Lattice_Constructions.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Wed Apr 12 09:18:36 2023 +0200
@@ -3,12 +3,12 @@
Copyright 2010 TU Muenchen
*)
+section \<open>Values extended by a bottom element\<close>
+
theory Lattice_Constructions
imports Main
begin
-subsection \<open>Values extended by a bottom element\<close>
-
datatype 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
--- a/src/HOL/Library/Rounded_Division.thy Tue Apr 11 21:42:45 2023 +0200
+++ b/src/HOL/Library/Rounded_Division.thy Wed Apr 12 09:18:36 2023 +0200
@@ -1,7 +1,7 @@
(* Author: Florian Haftmann, TU Muenchen
*)
-subsection \<open>Rounded division: modulus centered towards zero.\<close>
+section \<open>Rounded division: modulus centered towards zero.\<close>
theory Rounded_Division
imports Main
@@ -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 21:42:45 2023 +0200
+++ b/src/HOL/Library/Signed_Division.thy Wed Apr 12 09:18:36 2023 +0200
@@ -1,7 +1,7 @@
(* Author: Stefan Berghofer et al.
*)
-subsection \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
+section \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close>
theory Signed_Division
imports Main
@@ -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 21:42:45 2023 +0200
+++ b/src/HOL/Library/Word.thy Wed Apr 12 09:18:36 2023 +0200
@@ -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 21:42:45 2023 +0200
+++ b/src/HOL/Library/document/root.bib Wed Apr 12 09:18:36 2023 +0200
@@ -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 21:42:45 2023 +0200
+++ b/src/HOL/document/root.bib Wed Apr 12 09:18:36 2023 +0200
@@ -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}}