diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Computational_Algebra/Euclidean_Algorithm.thy --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Sun Oct 08 22:28:22 2017 +0200 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Sun Oct 08 22:28:22 2017 +0200 @@ -9,10 +9,26 @@ begin subsection \Generic construction of the (simple) euclidean algorithm\ - -context euclidean_semiring + +class normalization_euclidean_semiring = euclidean_semiring + normalization_semidom begin +lemma euclidean_size_normalize [simp]: + "euclidean_size (normalize a) = euclidean_size a" +proof (cases "a = 0") + case True + then show ?thesis + by simp +next + case [simp]: False + have "euclidean_size (normalize a) \ euclidean_size (normalize a * unit_factor a)" + by (rule size_mult_mono) simp + moreover have "euclidean_size a \ euclidean_size (a * (1 div unit_factor a))" + by (rule size_mult_mono) simp + ultimately show ?thesis + by simp +qed + context begin @@ -282,7 +298,7 @@ subsection \The (simple) euclidean algorithm as gcd computation\ -class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + +class euclidean_semiring_gcd = normalization_euclidean_semiring + gcd + Gcd + assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd" and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm" assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd" @@ -400,7 +416,7 @@ end lemma factorial_euclidean_semiring_gcdI: - "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)" + "OFCLASS('a::{factorial_semiring_gcd, normalization_euclidean_semiring}, euclidean_semiring_gcd_class)" proof interpret semiring_Gcd 1 0 times Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm @@ -502,7 +518,7 @@ also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r] by (simp add: algebra_simps) finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" . - qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute) + qed (auto simp: algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute) finally show ?thesis . qed qed @@ -552,6 +568,8 @@ subsection \Typical instances\ +instance nat :: normalization_euclidean_semiring .. + instance nat :: euclidean_semiring_gcd proof interpret semiring_Gcd 1 0 times @@ -584,6 +602,8 @@ by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm) qed +instance int :: normalization_euclidean_semiring .. + instance int :: euclidean_ring_gcd proof interpret semiring_Gcd 1 0 times