euclidean division on gaussian numbers

--- a/src/HOL/Examples/Gauss_Numbers.thy	Thu Oct 06 13:41:59 2022 +0000
+++ b/src/HOL/Examples/Gauss_Numbers.thy	Thu Oct 06 14:16:39 2022 +0000
@@ -325,16 +325,81 @@
   show \<open>x div 0 = 0\<close>
     by (simp add: gauss_eq_iff)
   show \<open>x * y div y = x\<close> if \<open>y \<noteq> 0\<close>
-    using that
-    apply (auto simp add: gauss_eq_iff algebra_simps power2_eq_square)
-       apply (simp_all only: flip: mult.assoc distrib_right)
-    apply (simp_all add: mult.assoc [of _ \<open>Re y\<close> \<open>Re y\<close>] mult.assoc [of _ \<open>Im y\<close> \<open>Im y\<close>] mult.commute [of _ \<open>Re x\<close>] flip: distrib_left)
-       apply (simp_all add: sum_squares_eq_zero_iff mult.commute nonzero_mult_rdiv_cancel_right flip: distrib_left)
-    done
+  proof -
+    define Y where \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
+    moreover have \<open>Y > 0\<close>
+      using that by (simp add: gauss_eq_0 less_le Y_def)
+    have *: \<open>Im y * (Im y * Re x) + Re x * (Re y * Re y) = Re x * Y\<close>
+      \<open>Im x * (Im y * Im y) + Im x * (Re y * Re y) = Im x * Y\<close>
+      \<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)
+  qed
   show \<open>x div y * y + x mod y = x\<close>
     by (simp add: gauss_eq_iff)
 qed
 
 end
 
+instantiation gauss :: euclidean_ring
+begin
+
+definition euclidean_size_gauss :: \<open>gauss \<Rightarrow> nat\<close>
+  where \<open>euclidean_size x = nat ((Re x)\<^sup>2 + (Im x)\<^sup>2)\<close>
+
+instance proof
+  show \<open>euclidean_size (0::gauss) = 0\<close>
+    by (simp add: euclidean_size_gauss_def)
+  show \<open>euclidean_size (x mod y) < euclidean_size y\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
+  proof-
+    define X and Y and R and I
+      where \<open>X = (Re x)\<^sup>2 + (Im x)\<^sup>2\<close> and \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
+        and \<open>R = Re x * Re y + Im x * Im y\<close> and \<open>I = Im x * Re y - Re x * Im y\<close>
+    with that have \<open>0 < Y\<close> and rhs: \<open>int (euclidean_size y) = Y\<close>
+      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)
+    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>
+      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 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>)
+    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> .
+    with \<open>Y > 0\<close> have \<open>?lhs < Y\<close>
+      by (simp add: power2_eq_square)
+    then have \<open>int (euclidean_size (x mod y)) < int (euclidean_size y)\<close>
+      by (simp only: lhs rhs)
+    then show ?thesis
+      by simp
+  qed
+  show \<open>euclidean_size x \<le> euclidean_size (x * y)\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
+  proof -
+    from that have \<open>euclidean_size y > 0\<close>
+      by (simp add: euclidean_size_gauss_def gauss_neq_0)
+    then have \<open>euclidean_size x \<le> euclidean_size x * euclidean_size y\<close>
+      by simp
+    also have \<open>\<dots> = nat (((Re x)\<^sup>2 + (Im x)\<^sup>2) * ((Re y)\<^sup>2 + (Im y)\<^sup>2))\<close>
+      by (simp add: euclidean_size_gauss_def nat_mult_distrib)
+    also have \<open>\<dots> = euclidean_size (x * y)\<close>
+      by (simp add: euclidean_size_gauss_def eq_nat_nat_iff) (simp add: algebra_simps power2_eq_square)
+    finally show ?thesis .
+  qed
+qed
+
 end
+
+end

--- a/src/HOL/Library/Rounded_Division.thy	Thu Oct 06 13:41:59 2022 +0000
+++ b/src/HOL/Library/Rounded_Division.thy	Thu Oct 06 14:16:39 2022 +0000
@@ -7,6 +7,10 @@
   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)
+
 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>
 
@@ -119,4 +123,39 @@
   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)
+
+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