# HG changeset patch # User haftmann # Date 1435429234 -7200 # Node ID 78ca5674c66a9666a58818ed33ea20cec8fa9130 # Parent 2da9b632069b43b176b5d0939dd6f569d5b53675 rings follow immediately their corresponding semirings diff -r 2da9b632069b -r 78ca5674c66a src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Jun 27 20:20:33 2015 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Jun 27 20:20:34 2015 +0200 @@ -242,6 +242,76 @@ end +class euclidean_ring = euclidean_semiring + idom +begin + +function euclid_ext :: "'a \ 'a \ 'a \ 'a \ 'a" where + "euclid_ext a b = + (if b = 0 then + let c = 1 div normalization_factor a in (c, 0, a * c) + else if b dvd a then + let c = 1 div normalization_factor b in (0, c, b * c) + else + case euclid_ext b (a mod b) of + (s, t, c) \ (t, s - t * (a div b), c))" + by pat_completeness simp +termination + by (relation "measure (euclidean_size \ snd)") (simp_all add: mod_size_less) + +declare euclid_ext.simps [simp del] + +lemma euclid_ext_0: + "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)" + by (simp add: euclid_ext.simps [of a 0]) + +lemma euclid_ext_left_0: + "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)" + by (simp add: euclid_ext.simps [of 0 a]) + +lemma euclid_ext_non_0: + "b \ 0 \ euclid_ext a b = (case euclid_ext b (a mod b) of + (s, t, c) \ (t, s - t * (a div b), c))" + by (cases "b dvd a") + (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) + +lemma euclid_ext_code [code]: + "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a) + else let (s, t, c) = euclid_ext b (a mod b) in (t, s - t * (a div b), c))" + by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) + +lemma euclid_ext_correct: + "case euclid_ext a b of (s, t, c) \ s * a + t * b = c" +proof (induct a b rule: gcd_eucl_induct) + case (zero a) then show ?case + by (simp add: euclid_ext_0 ac_simps) +next + case (mod a b) + obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)" + by (cases "euclid_ext b (a mod b)") blast + with mod have "c = s * b + t * (a mod b)" by simp + also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b" + by (simp add: algebra_simps) + also have "(a div b) * b + a mod b = a" using mod_div_equality . + finally show ?case + by (subst euclid_ext.simps) (simp add: stc mod ac_simps) +qed + +definition euclid_ext' :: "'a \ 'a \ 'a \ 'a" +where + "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \ (s, t))" + +lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" + by (simp add: euclid_ext'_def euclid_ext_0) + +lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)" + by (simp add: euclid_ext'_def euclid_ext_left_0) + +lemma euclid_ext'_non_0: "b \ 0 \ euclid_ext' a b = (snd (euclid_ext' b (a mod b)), + fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))" + by (simp add: euclid_ext'_def euclid_ext_non_0 split_def) + +end + class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl" assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl" @@ -1416,76 +1486,6 @@ few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring. \ -class euclidean_ring = euclidean_semiring + idom -begin - -function euclid_ext :: "'a \ 'a \ 'a \ 'a \ 'a" where - "euclid_ext a b = - (if b = 0 then - let c = 1 div normalization_factor a in (c, 0, a * c) - else if b dvd a then - let c = 1 div normalization_factor b in (0, c, b * c) - else - case euclid_ext b (a mod b) of - (s, t, c) \ (t, s - t * (a div b), c))" - by pat_completeness simp -termination - by (relation "measure (euclidean_size \ snd)") (simp_all add: mod_size_less) - -declare euclid_ext.simps [simp del] - -lemma euclid_ext_0: - "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)" - by (simp add: euclid_ext.simps [of a 0]) - -lemma euclid_ext_left_0: - "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)" - by (simp add: euclid_ext.simps [of 0 a]) - -lemma euclid_ext_non_0: - "b \ 0 \ euclid_ext a b = (case euclid_ext b (a mod b) of - (s, t, c) \ (t, s - t * (a div b), c))" - by (cases "b dvd a") - (simp_all add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) - -lemma euclid_ext_code [code]: - "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a) - else let (s, t, c) = euclid_ext b (a mod b) in (t, s - t * (a div b), c))" - by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) - -lemma euclid_ext_correct: - "case euclid_ext a b of (s, t, c) \ s * a + t * b = c" -proof (induct a b rule: gcd_eucl_induct) - case (zero a) then show ?case - by (simp add: euclid_ext_0 ac_simps) -next - case (mod a b) - obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)" - by (cases "euclid_ext b (a mod b)") blast - with mod have "c = s * b + t * (a mod b)" by simp - also have "... = t * ((a div b) * b + a mod b) + (s - t * (a div b)) * b" - by (simp add: algebra_simps) - also have "(a div b) * b + a mod b = a" using mod_div_equality . - finally show ?case - by (subst euclid_ext.simps) (simp add: stc mod ac_simps) -qed - -definition euclid_ext' :: "'a \ 'a \ 'a \ 'a" -where - "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \ (s, t))" - -lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" - by (simp add: euclid_ext'_def euclid_ext_0) - -lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)" - by (simp add: euclid_ext'_def euclid_ext_left_0) - -lemma euclid_ext'_non_0: "b \ 0 \ euclid_ext' a b = (snd (euclid_ext' b (a mod b)), - fst (euclid_ext' b (a mod b)) - snd (euclid_ext' b (a mod b)) * (a div b))" - by (simp add: euclid_ext'_def euclid_ext_non_0 split_def) - -end - class euclidean_ring_gcd = euclidean_semiring_gcd + idom begin