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.52            by (simp add: algebra_simps)
    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