--- 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