# HG changeset patch
# User haftmann
# Date 1663146900 0
# Node ID e278bf6430cf0d1596eb371b8dd7c42151b554f1
# Parent  e8d4013c49d1b9f924de52aab4f4887db3cb3e8f
More on division concerning gauss numbers.

diff -r e8d4013c49d1 -r e278bf6430cf src/HOL/Examples/Gauss_Numbers.thy
--- a/src/HOL/Examples/Gauss_Numbers.thy	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/HOL/Examples/Gauss_Numbers.thy	Wed Sep 14 09:15:00 2022 +0000
@@ -1,10 +1,10 @@
-(*   Author:      Florian Haftmann, TU Muenchen; based on existing material on gauss numbers\<close>
+(*   Author:      Florian Haftmann, TU Muenchen; based on existing material on complex numbers\<close>
 *)
 
 section \<open>Gauss Numbers: integral gauss numbers\<close>
 
 theory Gauss_Numbers
-imports Main
+  imports "HOL-Library.Rounded_Division"
 begin
 
 codatatype gauss = Gauss (Re: int) (Im: int)
@@ -308,8 +308,8 @@
 
 primcorec divide_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
-    \<open>Re (x div y) = (Re x * Re y + Im x * Im y) div ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
-  | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) div ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
+    \<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>
 
 definition modulo_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
@@ -321,7 +321,7 @@
   apply (auto simp add: gauss_eq_iff algebra_simps power2_eq_square)
            apply (simp_all only: flip: mult.assoc distrib_right)
        apply (simp_all only: mult.assoc [of \<open>Im k\<close> \<open>Re l\<close> \<open>Re r\<close> for k l r])
-      apply (simp_all add: sum_squares_eq_zero_iff mult.commute flip: distrib_left)
+     apply (simp_all add: sum_squares_eq_zero_iff mult.commute nonzero_mult_rdiv_cancel_right flip: distrib_left)
   done
 
 end
diff -r e8d4013c49d1 -r e278bf6430cf src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/HOL/Library/Library.thy	Wed Sep 14 09:15:00 2022 +0000
@@ -79,6 +79,7 @@
   Ramsey
   Reflection
   Rewrite
+  Rounded_Division
   Saturated
   Set_Algebras
   Set_Idioms
diff -r e8d4013c49d1 -r e278bf6430cf src/HOL/Library/Rounded_Division.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Rounded_Division.thy	Wed Sep 14 09:15:00 2022 +0000
@@ -0,0 +1,84 @@
+(*  Author:  Florian Haftmann, TU Muenchen
+*)
+
+subsection \<open>Rounded division: modulus centered towars zero.\<close>
+
+theory Rounded_Division
+  imports Main
+begin
+
+definition rounded_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rdiv\<close> 70)
+  where \<open>k rdiv l = (k + l div 2 + of_bool (l < 0)) div l\<close>
+
+definition rounded_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rmod\<close> 70)
+  where \<open>k rmod l = k - k rdiv l * l\<close>
+
+lemma rdiv_mult_rmod_eq:
+  \<open>k rdiv l * l + k rmod l = k\<close>
+  by (simp add: rounded_divide_def rounded_modulo_def)
+
+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 (simp add: rounded_modulo_def)
+
+lemma nonzero_mult_rdiv_cancel_right:
+  \<open>k * l rdiv l = k\<close> if \<open>l \<noteq> 0\<close>
+  using that by (auto simp add: rounded_divide_def ac_simps)
+
+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>
+  by (cases \<open>k = 0\<close>) (simp_all add: rounded_modulo_def)
+
+end