--- 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 \<circ> 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 \<Rightarrow> 'a"
+definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open>
+ Somewhat complicated definition of Lcm that has the advantage of working
+ for infinite sets as well\<close>
where
"Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
@@ -224,6 +223,23 @@
where
"Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>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 \<noteq> 0 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> 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: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
by (rule sym, rule gcdI, simp_all)
@@ -1401,6 +1417,74 @@
\<close>
class euclidean_ring = euclidean_semiring + idom
+begin
+
+function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> '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) \<Rightarrow> (t, s - t * (a div b), c))"
+ by pat_completeness simp
+termination
+ by (relation "measure (euclidean_size \<circ> 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 \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
+ (s, t, c) \<Rightarrow> (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) \<Rightarrow> 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 \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
+where
+ "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (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 \<noteq> 0 \<Longrightarrow> 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) \<Rightarrow> 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) \<Longrightarrow> 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: "\<exists>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 \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> '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) \<Rightarrow> (t, s - t * (a div b), c))"
- by (pat_completeness, simp)
- termination by (relation "measure (euclidean_size \<circ> 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 \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of
- (s, t, c) \<Rightarrow> (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 \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
-where
- "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
-
-lemma euclid_ext_gcd [simp]:
- "(case euclid_ext a b of (_, _ , t) \<Rightarrow> 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) \<Longrightarrow> 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) \<Rightarrow> 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: "\<exists>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 \<noteq> 0 \<Longrightarrow> 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 \<open>Typical instances\<close>
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 \<Rightarrow> nat"