src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
 changeset 66817 0b12755ccbb2 parent 65435 378175f44328 child 67167 88d1c9d86f48
```     1.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -9,10 +9,26 @@
1.4  begin
1.5
1.6  subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
1.7 -
1.8 -context euclidean_semiring
1.9 +
1.10 +class normalization_euclidean_semiring = euclidean_semiring + normalization_semidom
1.11  begin
1.12
1.13 +lemma euclidean_size_normalize [simp]:
1.14 +  "euclidean_size (normalize a) = euclidean_size a"
1.15 +proof (cases "a = 0")
1.16 +  case True
1.17 +  then show ?thesis
1.18 +    by simp
1.19 +next
1.20 +  case [simp]: False
1.21 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
1.22 +    by (rule size_mult_mono) simp
1.23 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
1.24 +    by (rule size_mult_mono) simp
1.25 +  ultimately show ?thesis
1.26 +    by simp
1.27 +qed
1.28 +
1.29  context
1.30  begin
1.31
1.32 @@ -282,7 +298,7 @@
1.33
1.34  subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
1.35
1.36 -class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
1.37 +class euclidean_semiring_gcd = normalization_euclidean_semiring + gcd + Gcd +
1.38    assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
1.39      and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
1.40    assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
1.41 @@ -400,7 +416,7 @@
1.42  end
1.43
1.44  lemma factorial_euclidean_semiring_gcdI:
1.45 -  "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
1.46 +  "OFCLASS('a::{factorial_semiring_gcd, normalization_euclidean_semiring}, euclidean_semiring_gcd_class)"
1.47  proof
1.48    interpret semiring_Gcd 1 0 times
1.49      Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
1.50 @@ -502,7 +518,7 @@
1.51          also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
1.53          finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
1.54 -      qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
1.55 +      qed (auto simp: algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
1.56        finally show ?thesis .
1.57      qed
1.58    qed
1.59 @@ -552,6 +568,8 @@
1.60
1.61  subsection \<open>Typical instances\<close>
1.62
1.63 +instance nat :: normalization_euclidean_semiring ..
1.64 +
1.65  instance nat :: euclidean_semiring_gcd
1.66  proof
1.67    interpret semiring_Gcd 1 0 times
1.68 @@ -584,6 +602,8 @@
1.69      by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
1.70  qed
1.71
1.72 +instance int :: normalization_euclidean_semiring ..
1.73 +
1.74  instance int :: euclidean_ring_gcd
1.75  proof
1.76    interpret semiring_Gcd 1 0 times
```