# HG changeset patch # User haftmann # Date 1435237303 -7200 # Node ID 718b1ba06429bb3b7522a234d5f2988a68f0bcbd # Parent c9fdf20804476cbda9f6b2cd70e8850b0f3ec4e4 streamlined definitions and primitive lemma of euclidean algorithm, including code generation diff -r c9fdf2080447 -r 718b1ba06429 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Jun 25 15:01:42 2015 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Jun 25 15:01:43 2015 +0200 @@ -174,7 +174,7 @@ "gcd_eucl a b = (if b = 0 then a div normalization_factor a else if b dvd a then b div normalization_factor b else gcd_eucl b (a mod b))" - by (pat_completeness, simp) + by pat_completeness simp termination by (relation "measure (euclidean_size \ snd)") (simp_all add: mod_size_less) @@ -209,10 +209,9 @@ where "lcm_eucl a b = a * b div (gcd_eucl a b * normalization_factor (a * b))" - (* Somewhat complicated definition of Lcm that has the advantage of working - for infinite sets as well *) - -definition Lcm_eucl :: "'a set \ 'a" +definition Lcm_eucl :: "'a set \ 'a" -- \ + Somewhat complicated definition of Lcm that has the advantage of working + for infinite sets as well\ where "Lcm_eucl A = (if \l. l \ 0 \ (\a\A. a dvd l) then let l = SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = @@ -224,6 +223,23 @@ where "Gcd_eucl A = Lcm_eucl {d. \a\A. d dvd a}" +lemma gcd_eucl_0: + "gcd_eucl a 0 = a div normalization_factor a" + by (simp add: gcd_eucl.simps [of a 0]) + +lemma gcd_eucl_0_left: + "gcd_eucl 0 a = a div normalization_factor a" + by (simp add: gcd_eucl.simps [of 0 a]) + +lemma gcd_eucl_non_0: + "b \ 0 \ gcd_eucl a b = gcd_eucl b (a mod b)" + by (cases "b dvd a") + (simp_all add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0]) + +lemma gcd_eucl_code [code]: + "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))" + by (auto simp add: gcd_eucl_non_0 gcd_eucl_0 gcd_eucl_0_left) + end class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + @@ -231,22 +247,17 @@ assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl" begin -lemma gcd_red: - "gcd a b = gcd b (a mod b)" - by (cases "b dvd a") - (auto simp add: gcd_gcd_eucl gcd_eucl.simps [of a b] gcd_eucl.simps [of 0 a] gcd_eucl.simps [of b 0]) +lemma gcd_0_left: + "gcd 0 a = a div normalization_factor a" + unfolding gcd_gcd_eucl by (fact gcd_eucl_0_left) + +lemma gcd_0: + "gcd a 0 = a div normalization_factor a" + unfolding gcd_gcd_eucl by (fact gcd_eucl_0) lemma gcd_non_0: "b \ 0 \ gcd a b = gcd b (a mod b)" - by (rule gcd_red) - -lemma gcd_0_left: - "gcd 0 a = a div normalization_factor a" - by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, subst gcd_eucl.simps, simp add: Let_def) - -lemma gcd_0: - "gcd a 0 = a div normalization_factor a" - by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, simp add: Let_def) + unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) lemma gcd_dvd1 [iff]: "gcd a b dvd a" and gcd_dvd2 [iff]: "gcd a b dvd b" @@ -543,8 +554,13 @@ "gcd m (m + n) = gcd m n" using gcd_add1 [of n m] by (simp add: ac_simps) -lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n" - by (subst gcd.commute, subst gcd_red, simp) +lemma gcd_add_mult: + "gcd m (k * m + n) = gcd m n" +proof - + have "gcd m ((k * m + n) mod m) = gcd m (k * m + n)" + by (fact gcd_mod2) + then show ?thesis by simp +qed lemma coprimeI: "(\l. \l dvd a; l dvd b\ \ l dvd 1) \ gcd a b = 1" by (rule sym, rule gcdI, simp_all) @@ -1401,6 +1417,74 @@ \ 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 @@ -1409,6 +1493,27 @@ subclass ring_gcd .. +lemma euclid_ext_gcd [simp]: + "(case euclid_ext a b of (_, _ , t) \ t) = gcd a b" + by (induct a b rule: gcd_eucl_induct) + (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm) + +lemma euclid_ext_gcd' [simp]: + "euclid_ext a b = (r, s, t) \ t = gcd a b" + by (insert euclid_ext_gcd[of a b], drule (1) subst, simp) + +lemma euclid_ext'_correct: + "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b" +proof- + obtain s t c where "euclid_ext a b = (s,t,c)" + by (cases "euclid_ext a b", blast) + with euclid_ext_correct[of a b] euclid_ext_gcd[of a b] + show ?thesis unfolding euclid_ext'_def by simp +qed + +lemma bezout: "\s t. s * a + t * b = gcd a b" + using euclid_ext'_correct by blast + lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b" by (rule sym, rule gcdI, simp_all add: gcd_greatest) @@ -1451,85 +1556,10 @@ lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)" by (fact lcm_neg2) -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 (subst euclid_ext.simps) (simp add: Let_def) - -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))" - apply (subst euclid_ext.simps) - apply (auto simp add: split: if_splits) - apply (subst euclid_ext.simps) - apply (auto simp add: split: if_splits) - done - -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_gcd [simp]: - "(case euclid_ext a b of (_, _ , t) \ t) = gcd a b" - by (induct a b rule: gcd_eucl_induct) - (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm) +end -lemma euclid_ext_gcd' [simp]: - "euclid_ext a b = (r, s, t) \ t = gcd a b" - by (insert euclid_ext_gcd[of a b], drule (1) subst, simp) -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 - -lemma euclid_ext'_correct: - "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b" -proof- - obtain s t c where "euclid_ext a b = (s,t,c)" - by (cases "euclid_ext a b", blast) - with euclid_ext_correct[of a b] euclid_ext_gcd[of a b] - show ?thesis unfolding euclid_ext'_def by simp -qed - -lemma bezout: "\s t. s * a + t * b = gcd a b" - using euclid_ext'_correct by blast - -lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" - by (simp add: bezw_def euclid_ext'_def euclid_ext_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 (cases "euclid_ext b (a mod b)") - (simp add: euclid_ext'_def euclid_ext_non_0) - -end +subsection \Typical instances\ instantiation nat :: euclidean_semiring begin @@ -1566,7 +1596,7 @@ end -instantiation poly :: (field) euclidean_semiring +instantiation poly :: (field) euclidean_ring begin definition euclidean_size_poly :: "'a poly \ nat"