author  Manuel Eberl <eberlm@in.tum.de> 
Fri, 26 Feb 2016 18:33:01 +0100  
changeset 62428  4d5fbec92bb1 
parent 62425  d0936b500bf5 
child 62429  25271ff79171 
permissions  rwrr 
58023  1 
(* Author: Manuel Eberl *) 
2 

60526  3 
section \<open>Abstract euclidean algorithm\<close> 
58023  4 

5 
theory Euclidean_Algorithm 

60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60634
diff
changeset

6 
imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial" 
58023  7 
begin 
60634  8 

60526  9 
text \<open> 
58023  10 
A Euclidean semiring is a semiring upon which the Euclidean algorithm can be 
11 
implemented. It must provide: 

12 
\begin{itemize} 

13 
\item division with remainder 

14 
\item a size function such that @{term "size (a mod b) < size b"} 

15 
for any @{term "b \<noteq> 0"} 

16 
\end{itemize} 

17 
The existence of these functions makes it possible to derive gcd and lcm functions 

18 
for any Euclidean semiring. 

60526  19 
\<close> 
60634  20 
class euclidean_semiring = semiring_div + normalization_semidom + 
58023  21 
fixes euclidean_size :: "'a \<Rightarrow> nat" 
62422  22 
assumes size_0 [simp]: "euclidean_size 0 = 0" 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

23 
assumes mod_size_less: 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

24 
"b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b" 
58023  25 
assumes size_mult_mono: 
60634  26 
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)" 
58023  27 
begin 
28 

29 
lemma euclidean_division: 

30 
fixes a :: 'a and b :: 'a 

60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

31 
assumes "b \<noteq> 0" 
58023  32 
obtains s and t where "a = s * b + t" 
33 
and "euclidean_size t < euclidean_size b" 

34 
proof  

60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

35 
from div_mod_equality [of a b 0] 
58023  36 
have "a = a div b * b + a mod b" by simp 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

37 
with that and assms show ?thesis by (auto simp add: mod_size_less) 
58023  38 
qed 
39 

40 
lemma dvd_euclidean_size_eq_imp_dvd: 

41 
assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b" 

42 
shows "a dvd b" 

60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

43 
proof (rule ccontr) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

44 
assume "\<not> a dvd b" 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

45 
then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd) 
58023  46 
from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff) 
47 
from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast 

60526  48 
with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto 
49 
with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b" 

58023  50 
using size_mult_mono by force 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

51 
moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close> 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

52 
have "euclidean_size (b mod a) < euclidean_size a" 
58023  53 
using mod_size_less by blast 
54 
ultimately show False using size_eq by simp 

55 
qed 

56 

57 
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

58 
where 

60634  59 
"gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))" 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

60 
by pat_completeness simp 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

61 
termination 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

62 
by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less) 
58023  63 

64 
declare gcd_eucl.simps [simp del] 

65 

60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

66 
lemma gcd_eucl_induct [case_names zero mod]: 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

67 
assumes H1: "\<And>b. P b 0" 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

68 
and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b" 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

69 
shows "P a b" 
58023  70 
proof (induct a b rule: gcd_eucl.induct) 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

71 
case ("1" a b) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

72 
show ?case 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

73 
proof (cases "b = 0") 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

74 
case True then show "P a b" by simp (rule H1) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

75 
next 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

76 
case False 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

77 
then have "P b (a mod b)" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

78 
by (rule "1.hyps") 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

79 
with \<open>b \<noteq> 0\<close> show "P a b" 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

80 
by (blast intro: H2) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

81 
qed 
58023  82 
qed 
83 

84 
definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

85 
where 

60634  86 
"lcm_eucl a b = normalize (a * b) div gcd_eucl a b" 
58023  87 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

88 
definition Lcm_eucl :: "'a set \<Rightarrow> 'a"  \<open> 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

89 
Somewhat complicated definition of Lcm that has the advantage of working 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

90 
for infinite sets as well\<close> 
58023  91 
where 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

92 
"Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

93 
let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

94 
(LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n) 
60634  95 
in normalize l 
58023  96 
else 0)" 
97 

98 
definition Gcd_eucl :: "'a set \<Rightarrow> 'a" 

99 
where 

100 
"Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}" 

101 

62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

102 
declare Lcm_eucl_def Gcd_eucl_def [code del] 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

103 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

104 
lemma gcd_eucl_0: 
60634  105 
"gcd_eucl a 0 = normalize a" 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

106 
by (simp add: gcd_eucl.simps [of a 0]) 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

107 

718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

108 
lemma gcd_eucl_0_left: 
60634  109 
"gcd_eucl 0 a = normalize a" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

110 
by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a]) 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

111 

718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

112 
lemma gcd_eucl_non_0: 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

113 
"b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

114 
by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0]) 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

115 

62422  116 
lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a" 
117 
and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b" 

118 
by (induct a b rule: gcd_eucl_induct) 

119 
(simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff) 

120 

121 
lemma normalize_gcd_eucl [simp]: 

122 
"normalize (gcd_eucl a b) = gcd_eucl a b" 

123 
by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0) 

124 

125 
lemma gcd_eucl_greatest: 

126 
fixes k a b :: 'a 

127 
shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b" 

128 
proof (induct a b rule: gcd_eucl_induct) 

129 
case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0) 

130 
next 

131 
case (mod a b) 

132 
then show ?case 

133 
by (simp add: gcd_eucl_non_0 dvd_mod_iff) 

134 
qed 

135 

136 
lemma eq_gcd_euclI: 

137 
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

138 
assumes "\<And>a b. gcd a b dvd a" "\<And>a b. gcd a b dvd b" "\<And>a b. normalize (gcd a b) = gcd a b" 

139 
"\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b" 

140 
shows "gcd = gcd_eucl" 

141 
by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) 

142 

143 
lemma gcd_eucl_zero [simp]: 

144 
"gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" 

145 
by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+ 

146 

147 

148 
lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A" 

149 
and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b" 

150 
and unit_factor_Lcm_eucl [simp]: 

151 
"unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" 

152 
proof  

153 
have "(\<forall>a\<in>A. a dvd Lcm_eucl A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm_eucl A dvd l') \<and> 

154 
unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis) 

155 
proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)") 

156 
case False 

157 
hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) 

158 
with False show ?thesis by auto 

159 
next 

160 
case True 

161 
then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast 

162 
def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 

163 
def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 

164 
have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 

165 
apply (subst n_def) 

166 
apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) 

167 
apply (rule exI[of _ l\<^sub>0]) 

168 
apply (simp add: l\<^sub>0_props) 

169 
done 

170 
from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 

171 
unfolding l_def by simp_all 

172 
{ 

173 
fix l' assume "\<forall>a\<in>A. a dvd l'" 

174 
with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd_eucl l l'" by (auto intro: gcd_eucl_greatest) 

175 
moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp 

176 
ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 

177 
euclidean_size b = euclidean_size (gcd_eucl l l')" 

178 
by (intro exI[of _ "gcd_eucl l l'"], auto) 

179 
hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le) 

180 
moreover have "euclidean_size (gcd_eucl l l') \<le> n" 

181 
proof  

182 
have "gcd_eucl l l' dvd l" by simp 

183 
then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast 

184 
with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto 

185 
hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)" 

186 
by (rule size_mult_mono) 

187 
also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> .. 

188 
also note \<open>euclidean_size l = n\<close> 

189 
finally show "euclidean_size (gcd_eucl l l') \<le> n" . 

190 
qed 

191 
ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" 

192 
by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>) 

193 
from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'" 

194 
by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) 

195 
hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2]) 

196 
} 

197 

198 
with \<open>(\<forall>a\<in>A. a dvd l)\<close> and unit_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close> 

199 
have "(\<forall>a\<in>A. a dvd normalize l) \<and> 

200 
(\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and> 

201 
unit_factor (normalize l) = 

202 
(if normalize l = 0 then 0 else 1)" 

203 
by (auto simp: unit_simps) 

204 
also from True have "normalize l = Lcm_eucl A" 

205 
by (simp add: Lcm_eucl_def Let_def n_def l_def) 

206 
finally show ?thesis . 

207 
qed 

208 
note A = this 

209 

210 
{fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast} 

211 
{fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast} 

212 
from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast 

213 
qed 

214 

215 
lemma normalize_Lcm_eucl [simp]: 

216 
"normalize (Lcm_eucl A) = Lcm_eucl A" 

217 
proof (cases "Lcm_eucl A = 0") 

218 
case True then show ?thesis by simp 

219 
next 

220 
case False 

221 
have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A" 

222 
by (fact unit_factor_mult_normalize) 

223 
with False show ?thesis by simp 

224 
qed 

225 

226 
lemma eq_Lcm_euclI: 

227 
fixes lcm :: "'a set \<Rightarrow> 'a" 

228 
assumes "\<And>A a. a \<in> A \<Longrightarrow> a dvd lcm A" and "\<And>A c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> lcm A dvd c" 

229 
"\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl" 

230 
by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least) 

231 

58023  232 
end 
233 

60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

234 
class euclidean_ring = euclidean_semiring + idom 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

235 
begin 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

236 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

237 
function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

238 
"euclid_ext a b = 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

239 
(if b = 0 then 
60634  240 
(1 div unit_factor a, 0, normalize a) 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

241 
else 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

242 
case euclid_ext b (a mod b) of 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

243 
(s, t, c) \<Rightarrow> (t, s  t * (a div b), c))" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

244 
by pat_completeness simp 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

245 
termination 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

246 
by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

247 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

248 
declare euclid_ext.simps [simp del] 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

249 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

250 
lemma euclid_ext_0: 
60634  251 
"euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)" 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

252 
by (simp add: euclid_ext.simps [of a 0]) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

253 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

254 
lemma euclid_ext_left_0: 
60634  255 
"euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

256 
by (simp add: euclid_ext_0 euclid_ext.simps [of 0 a]) 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

257 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

258 
lemma euclid_ext_non_0: 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

259 
"b \<noteq> 0 \<Longrightarrow> euclid_ext a b = (case euclid_ext b (a mod b) of 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

260 
(s, t, c) \<Rightarrow> (t, s  t * (a div b), c))" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

261 
by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

262 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

263 
lemma euclid_ext_code [code]: 
60634  264 
"euclid_ext a b = (if b = 0 then (1 div unit_factor a, 0, normalize a) 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

265 
else let (s, t, c) = euclid_ext b (a mod b) in (t, s  t * (a div b), c))" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

266 
by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0]) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

267 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

268 
lemma euclid_ext_correct: 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

269 
"case euclid_ext a b of (s, t, c) \<Rightarrow> s * a + t * b = c" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

270 
proof (induct a b rule: gcd_eucl_induct) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

271 
case (zero a) then show ?case 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

272 
by (simp add: euclid_ext_0 ac_simps) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

273 
next 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

274 
case (mod a b) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

275 
obtain s t c where stc: "euclid_ext b (a mod b) = (s,t,c)" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

276 
by (cases "euclid_ext b (a mod b)") blast 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

277 
with mod have "c = s * b + t * (a mod b)" by simp 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

278 
also have "... = t * ((a div b) * b + a mod b) + (s  t * (a div b)) * b" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

279 
by (simp add: algebra_simps) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

280 
also have "(a div b) * b + a mod b = a" using mod_div_equality . 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

281 
finally show ?case 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

282 
by (subst euclid_ext.simps) (simp add: stc mod ac_simps) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

283 
qed 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

284 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

285 
definition euclid_ext' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

286 
where 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

287 
"euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

288 

60634  289 
lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)" 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

290 
by (simp add: euclid_ext'_def euclid_ext_0) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

291 

60634  292 
lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div unit_factor a)" 
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

293 
by (simp add: euclid_ext'_def euclid_ext_left_0) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

294 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

295 
lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)), 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

296 
fst (euclid_ext' b (a mod b))  snd (euclid_ext' b (a mod b)) * (a div b))" 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

297 
by (simp add: euclid_ext'_def euclid_ext_non_0 split_def) 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

298 

78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

299 
end 
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset

300 

58023  301 
class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + 
302 
assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl" 

303 
assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl" 

304 
begin 

305 

62422  306 
subclass semiring_gcd 
307 
by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def) 

58023  308 

62422  309 
subclass semiring_Gcd 
310 
by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least) 

311 

58023  312 

313 
lemma gcd_non_0: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

314 
"b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)" 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

315 
unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) 
58023  316 

62422  317 
lemmas gcd_0 = gcd_0_right 
318 
lemmas dvd_gcd_iff = gcd_greatest_iff 

58023  319 

320 
lemmas gcd_greatest_iff = dvd_gcd_iff 

321 

322 
lemma gcdI: 

60634  323 
assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

324 
and "normalize c = c" 
60634  325 
shows "c = gcd a b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

326 
by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) 
58023  327 

328 
lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

329 
normalize d = d \<and> 
58023  330 
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

331 
by rule (auto intro: gcdI simp: gcd_greatest) 
58023  332 

333 
lemma gcd_dvd_prod: "gcd a b dvd k * b" 

334 
using mult_dvd_mono [of 1] by auto 

335 

336 
lemma gcd_proj2_if_dvd: 

60634  337 
"b dvd a \<Longrightarrow> gcd a b = normalize b" 
62422  338 
by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0) 
58023  339 

340 
lemma gcd_proj1_if_dvd: 

60634  341 
"a dvd b \<Longrightarrow> gcd a b = normalize a" 
58023  342 
by (subst gcd.commute, simp add: gcd_proj2_if_dvd) 
343 

60634  344 
lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n" 
58023  345 
proof 
60634  346 
assume A: "gcd m n = normalize m" 
58023  347 
show "m dvd n" 
348 
proof (cases "m = 0") 

349 
assume [simp]: "m \<noteq> 0" 

60634  350 
from A have B: "m = gcd m n * unit_factor m" 
58023  351 
by (simp add: unit_eq_div2) 
352 
show ?thesis by (subst B, simp add: mult_unit_dvd_iff) 

353 
qed (insert A, simp) 

354 
next 

355 
assume "m dvd n" 

60634  356 
then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd) 
58023  357 
qed 
358 

60634  359 
lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m" 
360 
using gcd_proj1_iff [of n m] by (simp add: ac_simps) 

58023  361 

362 
lemma gcd_mod1 [simp]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

363 
"gcd (a mod b) b = gcd a b" 
58023  364 
by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) 
365 

366 
lemma gcd_mod2 [simp]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

367 
"gcd a (b mod a) = gcd a b" 
58023  368 
by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) 
369 

370 
lemma gcd_mult_distrib': 

60634  371 
"normalize c * gcd a b = gcd (c * a) (c * b)" 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

372 
proof (cases "c = 0") 
62422  373 
case True then show ?thesis by simp_all 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

374 
next 
60634  375 
case False then have [simp]: "is_unit (unit_factor c)" by simp 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

376 
show ?thesis 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

377 
proof (induct a b rule: gcd_eucl_induct) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

378 
case (zero a) show ?case 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

379 
proof (cases "a = 0") 
62422  380 
case True then show ?thesis by simp 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

381 
next 
60634  382 
case False 
62422  383 
then show ?thesis by (simp add: normalize_mult) 
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

384 
qed 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

385 
case (mod a b) 
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset

386 
then show ?case by (simp add: mult_mod_right gcd.commute) 
58023  387 
qed 
388 
qed 

389 

390 
lemma gcd_mult_distrib: 

60634  391 
"k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 
58023  392 
proof 
60634  393 
have "normalize k * gcd a b = gcd (k * a) (k * b)" 
394 
by (simp add: gcd_mult_distrib') 

395 
then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k" 

396 
by simp 

397 
then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 

398 
by (simp only: ac_simps) 

399 
then show ?thesis 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

400 
by simp 
58023  401 
qed 
402 

403 
lemma euclidean_size_gcd_le1 [simp]: 

404 
assumes "a \<noteq> 0" 

405 
shows "euclidean_size (gcd a b) \<le> euclidean_size a" 

406 
proof  

407 
have "gcd a b dvd a" by (rule gcd_dvd1) 

408 
then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast 

60526  409 
with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto 
58023  410 
qed 
411 

412 
lemma euclidean_size_gcd_le2 [simp]: 

413 
"b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b" 

414 
by (subst gcd.commute, rule euclidean_size_gcd_le1) 

415 

416 
lemma euclidean_size_gcd_less1: 

417 
assumes "a \<noteq> 0" and "\<not>a dvd b" 

418 
shows "euclidean_size (gcd a b) < euclidean_size a" 

419 
proof (rule ccontr) 

420 
assume "\<not>euclidean_size (gcd a b) < euclidean_size a" 

62422  421 
with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a" 
58023  422 
by (intro le_antisym, simp_all) 
62422  423 
have "a dvd gcd a b" 
424 
by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A) 

425 
hence "a dvd b" using dvd_gcdD2 by blast 

60526  426 
with \<open>\<not>a dvd b\<close> show False by contradiction 
58023  427 
qed 
428 

429 
lemma euclidean_size_gcd_less2: 

430 
assumes "b \<noteq> 0" and "\<not>b dvd a" 

431 
shows "euclidean_size (gcd a b) < euclidean_size b" 

432 
using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) 

433 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

434 
lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c" 
58023  435 
apply (rule gcdI) 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

436 
apply simp_all 
58023  437 
apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) 
438 
done 

439 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

440 
lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c" 
58023  441 
by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute) 
442 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

443 
lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c" 
60433  444 
by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) 
58023  445 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

446 
lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c" 
60433  447 
by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) 
58023  448 

60634  449 
lemma normalize_gcd_left [simp]: 
450 
"gcd (normalize a) b = gcd a b" 

451 
proof (cases "a = 0") 

452 
case True then show ?thesis 

453 
by simp 

454 
next 

455 
case False then have "is_unit (unit_factor a)" 

456 
by simp 

457 
moreover have "normalize a = a div unit_factor a" 

458 
by simp 

459 
ultimately show ?thesis 

460 
by (simp only: gcd_div_unit1) 

461 
qed 

462 

463 
lemma normalize_gcd_right [simp]: 

464 
"gcd a (normalize b) = gcd a b" 

465 
using normalize_gcd_left [of b a] by (simp add: ac_simps) 

466 

467 
lemma gcd_idem: "gcd a a = normalize a" 

62422  468 
by (cases "a = 0") (simp, rule sym, rule gcdI, simp_all) 
58023  469 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

470 
lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b" 
58023  471 
apply (rule gcdI) 
472 
apply (simp add: ac_simps) 

473 
apply (rule gcd_dvd2) 

474 
apply (rule gcd_greatest, erule (1) gcd_greatest, assumption) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

475 
apply simp 
58023  476 
done 
477 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

478 
lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b" 
58023  479 
apply (rule gcdI) 
480 
apply simp 

481 
apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2) 

482 
apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

483 
apply simp 
58023  484 
done 
485 

486 
lemma comp_fun_idem_gcd: "comp_fun_idem gcd" 

487 
proof 

488 
fix a b show "gcd a \<circ> gcd b = gcd b \<circ> gcd a" 

489 
by (simp add: fun_eq_iff ac_simps) 

490 
next 

491 
fix a show "gcd a \<circ> gcd a = gcd a" 

492 
by (simp add: fun_eq_iff gcd_left_idem) 

493 
qed 

494 

495 
lemma gcd_dvd_antisym: 

496 
"gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d" 

497 
proof (rule gcdI) 

498 
assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b" 

499 
have "gcd c d dvd c" by simp 

500 
with A show "gcd a b dvd c" by (rule dvd_trans) 

501 
have "gcd c d dvd d" by simp 

502 
with A show "gcd a b dvd d" by (rule dvd_trans) 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

503 
show "normalize (gcd a b) = gcd a b" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

504 
by simp 
58023  505 
fix l assume "l dvd c" and "l dvd d" 
506 
hence "l dvd gcd c d" by (rule gcd_greatest) 

507 
from this and B show "l dvd gcd a b" by (rule dvd_trans) 

508 
qed 

509 

510 
lemma coprime_crossproduct: 

511 
assumes [simp]: "gcd a d = 1" "gcd b c = 1" 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

512 
shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

513 
(is "?lhs \<longleftrightarrow> ?rhs") 
58023  514 
proof 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

515 
assume ?rhs 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

516 
then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

517 
then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+ 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

518 
then show ?lhs by (simp add: associated_iff_dvd) 
58023  519 
next 
520 
assume ?lhs 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

521 
then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

522 
then have "a dvd b * d" by (metis dvd_mult_left) 
58023  523 
hence "a dvd b" by (simp add: coprime_dvd_mult_iff) 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

524 
moreover from dvd have "b dvd a * c" by (metis dvd_mult_left) 
58023  525 
hence "b dvd a" by (simp add: coprime_dvd_mult_iff) 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

526 
moreover from dvd have "c dvd d * b" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

527 
by (auto dest: dvd_mult_right simp add: ac_simps) 
58023  528 
hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute) 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

529 
moreover from dvd have "d dvd c * a" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

530 
by (auto dest: dvd_mult_right simp add: ac_simps) 
58023  531 
hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute) 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

532 
ultimately show ?rhs by (simp add: associated_iff_dvd) 
58023  533 
qed 
534 

535 
lemma gcd_add1 [simp]: 

536 
"gcd (m + n) n = gcd m n" 

537 
by (cases "n = 0", simp_all add: gcd_non_0) 

538 

539 
lemma gcd_add2 [simp]: 

540 
"gcd m (m + n) = gcd m n" 

541 
using gcd_add1 [of n m] by (simp add: ac_simps) 

542 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

543 
lemma gcd_add_mult: 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

544 
"gcd m (k * m + n) = gcd m n" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

545 
proof  
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

546 
have "gcd m ((k * m + n) mod m) = gcd m (k * m + n)" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

547 
by (fact gcd_mod2) 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

548 
then show ?thesis by simp 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

549 
qed 
58023  550 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

551 
lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1" 
58023  552 
by (rule sym, rule gcdI, simp_all) 
553 

554 
lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" 

62422  555 
by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2) 
58023  556 

557 
lemma div_gcd_coprime: 

558 
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0" 

559 
defines [simp]: "d \<equiv> gcd a b" 

560 
defines [simp]: "a' \<equiv> a div d" and [simp]: "b' \<equiv> b div d" 

561 
shows "gcd a' b' = 1" 

562 
proof (rule coprimeI) 

563 
fix l assume "l dvd a'" "l dvd b'" 

564 
then obtain s t where "a' = l * s" "b' = l * t" unfolding dvd_def by blast 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

565 
moreover have "a = a' * d" "b = b' * d" by simp_all 
58023  566 
ultimately have "a = (l * d) * s" "b = (l * d) * t" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

567 
by (simp_all only: ac_simps) 
58023  568 
hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left) 
569 
hence "l*d dvd d" by (simp add: gcd_greatest) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

570 
then obtain u where "d = l * d * u" .. 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

571 
then have "d * (l * u) = d" by (simp add: ac_simps) 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

572 
moreover from nz have "d \<noteq> 0" by simp 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

573 
with div_mult_self1_is_id have "d * (l * u) div d = l * u" . 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

574 
ultimately have "1 = l * u" 
60526  575 
using \<open>d \<noteq> 0\<close> by simp 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

576 
then show "l dvd 1" .. 
58023  577 
qed 
578 

579 
lemma coprime_lmult: 

580 
assumes dab: "gcd d (a * b) = 1" 

581 
shows "gcd d a = 1" 

582 
proof (rule coprimeI) 

583 
fix l assume "l dvd d" and "l dvd a" 

584 
hence "l dvd a * b" by simp 

60526  585 
with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest) 
58023  586 
qed 
587 

588 
lemma coprime_rmult: 

589 
assumes dab: "gcd d (a * b) = 1" 

590 
shows "gcd d b = 1" 

591 
proof (rule coprimeI) 

592 
fix l assume "l dvd d" and "l dvd b" 

593 
hence "l dvd a * b" by simp 

60526  594 
with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest) 
58023  595 
qed 
596 

597 
lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1" 

598 
using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast 

599 

600 
lemma gcd_coprime: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

601 
assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" 
58023  602 
shows "gcd a' b' = 1" 
603 
proof  

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

604 
from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp 
58023  605 
with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" . 
606 
also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+ 

607 
also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+ 

608 
finally show ?thesis . 

609 
qed 

610 

611 
lemma coprime_power: 

612 
assumes "0 < n" 

613 
shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1" 

614 
using assms proof (induct n) 

615 
case (Suc n) then show ?case 

616 
by (cases n) (simp_all add: coprime_mul_eq) 

617 
qed simp 

618 

619 
lemma gcd_coprime_exists: 

620 
assumes nz: "gcd a b \<noteq> 0" 

621 
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1" 

622 
apply (rule_tac x = "a div gcd a b" in exI) 

623 
apply (rule_tac x = "b div gcd a b" in exI) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

624 
apply (insert nz, auto intro: div_gcd_coprime) 
58023  625 
done 
626 

627 
lemma coprime_exp: 

628 
"gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1" 

629 
by (induct n, simp_all add: coprime_mult) 

630 

631 
lemma gcd_exp: 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

632 
"gcd (a ^ n) (b ^ n) = gcd a b ^ n" 
58023  633 
proof (cases "a = 0 \<and> b = 0") 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

634 
case True 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

635 
then show ?thesis by (cases n) simp_all 
58023  636 
next 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

637 
case False 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

638 
then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 
62422  639 
using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

640 
then have "gcd a b ^ n = gcd a b ^ n * ..." by simp 
58023  641 
also note gcd_mult_distrib 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

642 
also have "unit_factor (gcd a b ^ n) = 1" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

643 
using False by (auto simp add: unit_factor_power unit_factor_gcd) 
58023  644 
also have "(gcd a b)^n * (a div gcd a b)^n = a^n" 
645 
by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) 

646 
also have "(gcd a b)^n * (b div gcd a b)^n = b^n" 

647 
by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) 

648 
finally show ?thesis by simp 

649 
qed 

650 

651 
lemma coprime_common_divisor: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

652 
"gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

653 
apply (subgoal_tac "a dvd gcd a b") 
59061  654 
apply simp 
58023  655 
apply (erule (1) gcd_greatest) 
656 
done 

657 

658 
lemma division_decomp: 

659 
assumes dc: "a dvd b * c" 

660 
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 

661 
proof (cases "gcd a b = 0") 

662 
assume "gcd a b = 0" 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

663 
hence "a = 0 \<and> b = 0" by simp 
58023  664 
hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp 
665 
then show ?thesis by blast 

666 
next 

667 
let ?d = "gcd a b" 

668 
assume "?d \<noteq> 0" 

669 
from gcd_coprime_exists[OF this] 

670 
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" 

671 
by blast 

672 
from ab'(1) have "a' dvd a" unfolding dvd_def by blast 

673 
with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp 

674 
from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp 

675 
hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac) 

60526  676 
with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp 
58023  677 
with coprime_dvd_mult[OF ab'(3)] 
678 
have "a' dvd c" by (subst (asm) ac_simps, blast) 

679 
with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac) 

680 
then show ?thesis by blast 

681 
qed 

682 

60433  683 
lemma pow_divs_pow: 
58023  684 
assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0" 
685 
shows "a dvd b" 

686 
proof (cases "gcd a b = 0") 

687 
assume "gcd a b = 0" 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

688 
then show ?thesis by simp 
58023  689 
next 
690 
let ?d = "gcd a b" 

691 
assume "?d \<noteq> 0" 

692 
from n obtain m where m: "n = Suc m" by (cases n, simp_all) 

60526  693 
from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero) 
694 
from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>] 

58023  695 
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" 
696 
by blast 

697 
from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n" 

698 
by (simp add: ab'(1,2)[symmetric]) 

699 
hence "?d^n * a'^n dvd ?d^n * b'^n" 

700 
by (simp only: power_mult_distrib ac_simps) 

59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

701 
with zn have "a'^n dvd b'^n" by simp 
58023  702 
hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m) 
703 
hence "a' dvd b'^m * b'" by (simp add: m ac_simps) 

704 
with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]] 

705 
have "a' dvd b'" by (subst (asm) ac_simps, blast) 

706 
hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp) 

707 
with ab'(1,2) show ?thesis by simp 

708 
qed 

709 

60433  710 
lemma pow_divs_eq [simp]: 
58023  711 
"n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" 
60433  712 
by (auto intro: pow_divs_pow dvd_power_same) 
58023  713 

62422  714 
lemmas divs_mult = divides_mult 
58023  715 

716 
lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1" 

717 
by (subst add_commute, simp) 

718 

719 
lemma setprod_coprime [rule_format]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

720 
"(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1" 
58023  721 
apply (cases "finite A") 
722 
apply (induct set: finite) 

723 
apply (auto simp add: gcd_mult_cancel) 

724 
done 

62422  725 

726 
lemma listprod_coprime: 

727 
"(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 

728 
by (induction xs) (simp_all add: gcd_mult_cancel) 

58023  729 

730 
lemma coprime_divisors: 

731 
assumes "d dvd a" "e dvd b" "gcd a b = 1" 

732 
shows "gcd d e = 1" 

733 
proof  

734 
from assms obtain k l where "a = d * k" "b = e * l" 

735 
unfolding dvd_def by blast 

736 
with assms have "gcd (d * k) (e * l) = 1" by simp 

737 
hence "gcd (d * k) e = 1" by (rule coprime_lmult) 

738 
also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps) 

739 
finally have "gcd e d = 1" by (rule coprime_lmult) 

740 
then show ?thesis by (simp add: ac_simps) 

741 
qed 

742 

743 
lemma invertible_coprime: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

744 
assumes "a * b mod m = 1" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

745 
shows "coprime a m" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

746 
proof  
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

747 
from assms have "coprime m (a * b mod m)" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

748 
by simp 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

749 
then have "coprime m (a * b)" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

750 
by simp 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

751 
then have "coprime m a" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

752 
by (rule coprime_lmult) 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

753 
then show ?thesis 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

754 
by (simp add: ac_simps) 
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

755 
qed 
58023  756 

757 
lemma lcm_gcd_prod: 

60634  758 
"lcm a b * gcd a b = normalize (a * b)" 
759 
by (simp add: lcm_gcd) 

58023  760 

761 
lemma lcm_zero: 

762 
"lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 

60687  763 
by (fact lcm_eq_0_iff) 
58023  764 

765 
lemmas lcm_0_iff = lcm_zero 

766 

767 
lemma gcd_lcm: 

768 
assumes "lcm a b \<noteq> 0" 

60634  769 
shows "gcd a b = normalize (a * b) div lcm a b" 
770 
proof  

771 
have "lcm a b * gcd a b = normalize (a * b)" 

772 
by (fact lcm_gcd_prod) 

773 
with assms show ?thesis 

774 
by (metis nonzero_mult_divide_cancel_left) 

58023  775 
qed 
776 

60687  777 
declare unit_factor_lcm [simp] 
58023  778 

779 
lemma lcmI: 

60634  780 
assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

781 
and "normalize c = c" 
60634  782 
shows "c = lcm a b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

783 
by (rule associated_eqI) (auto simp: assms intro: lcm_least) 
58023  784 

785 
lemma gcd_dvd_lcm [simp]: 

786 
"gcd a b dvd lcm a b" 

60690  787 
using gcd_dvd2 by (rule dvd_lcmI2) 
58023  788 

62422  789 
lemmas lcm_0 = lcm_0_right 
58023  790 

791 
lemma lcm_unique: 

792 
"a dvd d \<and> b dvd d \<and> 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

793 
normalize d = d \<and> 
58023  794 
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

795 
by rule (auto intro: lcmI simp: lcm_least lcm_zero) 
58023  796 

797 
lemma lcm_coprime: 

60634  798 
"gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)" 
58023  799 
by (subst lcm_gcd) simp 
800 

801 
lemma lcm_proj1_if_dvd: 

60634  802 
"b dvd a \<Longrightarrow> lcm a b = normalize a" 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

803 
by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) 
58023  804 

805 
lemma lcm_proj2_if_dvd: 

60634  806 
"a dvd b \<Longrightarrow> lcm a b = normalize b" 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

807 
using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) 
58023  808 

809 
lemma lcm_proj1_iff: 

60634  810 
"lcm m n = normalize m \<longleftrightarrow> n dvd m" 
58023  811 
proof 
60634  812 
assume A: "lcm m n = normalize m" 
58023  813 
show "n dvd m" 
814 
proof (cases "m = 0") 

815 
assume [simp]: "m \<noteq> 0" 

60634  816 
from A have B: "m = lcm m n * unit_factor m" 
58023  817 
by (simp add: unit_eq_div2) 
818 
show ?thesis by (subst B, simp) 

819 
qed simp 

820 
next 

821 
assume "n dvd m" 

60634  822 
then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd) 
58023  823 
qed 
824 

825 
lemma lcm_proj2_iff: 

60634  826 
"lcm m n = normalize n \<longleftrightarrow> m dvd n" 
58023  827 
using lcm_proj1_iff [of n m] by (simp add: ac_simps) 
828 

829 
lemma euclidean_size_lcm_le1: 

830 
assumes "a \<noteq> 0" and "b \<noteq> 0" 

831 
shows "euclidean_size a \<le> euclidean_size (lcm a b)" 

832 
proof  

60690  833 
have "a dvd lcm a b" by (rule dvd_lcm1) 
834 
then obtain c where A: "lcm a b = a * c" .. 

60526  835 
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero) 
58023  836 
then show ?thesis by (subst A, intro size_mult_mono) 
837 
qed 

838 

839 
lemma euclidean_size_lcm_le2: 

840 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)" 

841 
using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps) 

842 

843 
lemma euclidean_size_lcm_less1: 

844 
assumes "b \<noteq> 0" and "\<not>b dvd a" 

845 
shows "euclidean_size a < euclidean_size (lcm a b)" 

846 
proof (rule ccontr) 

847 
from assms have "a \<noteq> 0" by auto 

848 
assume "\<not>euclidean_size a < euclidean_size (lcm a b)" 

60526  849 
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a" 
58023  850 
by (intro le_antisym, simp, intro euclidean_size_lcm_le1) 
851 
with assms have "lcm a b dvd a" 

852 
by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero) 

62422  853 
hence "b dvd a" by (rule lcm_dvdD2) 
60526  854 
with \<open>\<not>b dvd a\<close> show False by contradiction 
58023  855 
qed 
856 

857 
lemma euclidean_size_lcm_less2: 

858 
assumes "a \<noteq> 0" and "\<not>a dvd b" 

859 
shows "euclidean_size b < euclidean_size (lcm a b)" 

860 
using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) 

861 

862 
lemma lcm_mult_unit1: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

863 
"is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c" 
60690  864 
by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1) 
58023  865 

866 
lemma lcm_mult_unit2: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

867 
"is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

868 
using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) 
58023  869 

870 
lemma lcm_div_unit1: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

871 
"is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c" 
60433  872 
by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
58023  873 

874 
lemma lcm_div_unit2: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

875 
"is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c" 
60433  876 
by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) 
58023  877 

60634  878 
lemma normalize_lcm_left [simp]: 
879 
"lcm (normalize a) b = lcm a b" 

880 
proof (cases "a = 0") 

881 
case True then show ?thesis 

882 
by simp 

883 
next 

884 
case False then have "is_unit (unit_factor a)" 

885 
by simp 

886 
moreover have "normalize a = a div unit_factor a" 

887 
by simp 

888 
ultimately show ?thesis 

889 
by (simp only: lcm_div_unit1) 

890 
qed 

891 

892 
lemma normalize_lcm_right [simp]: 

893 
"lcm a (normalize b) = lcm a b" 

894 
using normalize_lcm_left [of b a] by (simp add: ac_simps) 

895 

58023  896 
lemma LcmI: 
60634  897 
assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

898 
and "normalize b = b" shows "b = Lcm A" 
62422  899 
by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least) 
58023  900 

901 
lemma Lcm_subset: 

902 
"A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B" 

60634  903 
by (blast intro: Lcm_least dvd_Lcm) 
58023  904 

905 
lemma Lcm_Un: 

906 
"Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)" 

907 
apply (rule lcmI) 

908 
apply (blast intro: Lcm_subset) 

909 
apply (blast intro: Lcm_subset) 

60634  910 
apply (intro Lcm_least ballI, elim UnE) 
58023  911 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 
912 
apply (rule dvd_trans, erule dvd_Lcm, assumption) 

913 
apply simp 

914 
done 

915 

916 
lemma Lcm_no_units: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

917 
"Lcm A = Lcm (A  {a. is_unit a})" 
58023  918 
proof  
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

919 
have "(A  {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

920 
hence "Lcm A = lcm (Lcm (A  {a. is_unit a})) (Lcm {a\<in>A. is_unit a})" 
60634  921 
by (simp add: Lcm_Un [symmetric]) 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

922 
also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff) 
58023  923 
finally show ?thesis by simp 
924 
qed 

925 

62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62348
diff
changeset

926 
lemma Lcm_0_iff': 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

927 
"Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" 
58023  928 
proof 
929 
assume "Lcm A = 0" 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

930 
show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" 
58023  931 
proof 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

932 
assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

933 
then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

934 
def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

935 
def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

936 
have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" 
58023  937 
apply (subst n_def) 
938 
apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) 

939 
apply (rule exI[of _ l\<^sub>0]) 

940 
apply (simp add: l\<^sub>0_props) 

941 
done 

942 
from someI_ex[OF this] have "l \<noteq> 0" unfolding l_def by simp_all 

60634  943 
hence "normalize l \<noteq> 0" by simp 
944 
also from ex have "normalize l = Lcm A" 

58023  945 
by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def) 
60526  946 
finally show False using \<open>Lcm A = 0\<close> by contradiction 
58023  947 
qed 
948 
qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) 

949 

950 
lemma Lcm_no_multiple: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

951 
"(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0" 
58023  952 
proof  
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

953 
assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)" 
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

954 
hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" by blast 
58023  955 
then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) 
956 
qed 

957 

958 
lemma Lcm_finite: 

959 
assumes "finite A" 

960 
shows "Lcm A = Finite_Set.fold lcm 1 A" 

60526  961 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
58023  962 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) 
963 

62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

964 
lemma Lcm_set: 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

965 
"Lcm (set xs) = foldl lcm 1 xs" 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

966 
using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

967 
by (simp add: foldl_conv_fold lcm.commute) 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

968 

4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

969 
lemma Lcm_eucl_set [code]: 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

970 
"Lcm_eucl (set xs) = foldl lcm_eucl 1 xs" 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

971 
by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set) 
58023  972 

973 
lemma Lcm_singleton [simp]: 

60634  974 
"Lcm {a} = normalize a" 
58023  975 
by simp 
976 

977 
lemma Lcm_2 [simp]: 

978 
"Lcm {a,b} = lcm a b" 

60634  979 
by simp 
58023  980 

981 
lemma Lcm_coprime: 

982 
assumes "finite A" and "A \<noteq> {}" 

983 
assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1" 

60634  984 
shows "Lcm A = normalize (\<Prod>A)" 
58023  985 
using assms proof (induct rule: finite_ne_induct) 
986 
case (insert a A) 

987 
have "Lcm (insert a A) = lcm a (Lcm A)" by simp 

60634  988 
also from insert have "Lcm A = normalize (\<Prod>A)" by blast 
58023  989 
also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2) 
990 
also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto 

60634  991 
with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))" 
58023  992 
by (simp add: lcm_coprime) 
993 
finally show ?case . 

994 
qed simp 

995 

996 
lemma Lcm_coprime': 

997 
"card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) 

60634  998 
\<Longrightarrow> Lcm A = normalize (\<Prod>A)" 
58023  999 
by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) 
1000 

62422  1001 
lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
58023  1002 
proof  
60634  1003 
show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
62422  1004 
by (simp add: Gcd_Lcm unit_factor_Lcm) 
58023  1005 
qed 
1006 

1007 
lemma GcdI: 

60634  1008 
assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b" 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60687
diff
changeset

1009 
and "normalize b = b" 
60634  1010 
shows "b = Gcd A" 
62422  1011 
by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) 
58023  1012 

1013 
lemma Gcd_1: 

1014 
"1 \<in> A \<Longrightarrow> Gcd A = 1" 

60687  1015 
by (auto intro!: Gcd_eq_1_I) 
58023  1016 

1017 
lemma Gcd_finite: 

1018 
assumes "finite A" 

1019 
shows "Gcd A = Finite_Set.fold gcd 0 A" 

60526  1020 
by (induct rule: finite.induct[OF \<open>finite A\<close>]) 
58023  1021 
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) 
1022 

62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1023 
lemma Gcd_set: 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1024 
"Gcd (set xs) = foldl gcd 0 xs" 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1025 
using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1026 
by (simp add: foldl_conv_fold gcd.commute) 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1027 

4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1028 
lemma Gcd_eucl_set [code]: 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1029 
"Gcd_eucl (set xs) = foldl gcd_eucl 0 xs" 
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset

1030 
by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set) 
58023  1031 

60634  1032 
lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" 
60687  1033 
by simp 
58023  1034 

1035 
lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" 

60687  1036 
by simp 
60686  1037 

62422  1038 

1039 
definition pairwise_coprime where 

1040 
"pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)" 

1041 

1042 
lemma pairwise_coprimeI [intro?]: 

1043 
"(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A" 

1044 
by (simp add: pairwise_coprime_def) 

1045 

1046 
lemma pairwise_coprimeD: 

1047 
"pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y" 

1048 
by (simp add: pairwise_coprime_def) 

1049 

1050 
lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B" 

1051 
by (force simp: pairwise_coprime_def) 

1052 

58023  1053 
end 
1054 

60526  1055 
text \<open> 
58023  1056 
A Euclidean ring is a Euclidean semiring with additive inverses. It provides a 
1057 
few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring. 

60526  1058 
\<close> 
58023  1059 

1060 
class euclidean_ring_gcd = euclidean_semiring_gcd + idom 

1061 
begin 

1062 

1063 
subclass euclidean_ring .. 

60439
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset

1064 
subclass ring_gcd .. 
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset

1065 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1066 
lemma euclid_ext_gcd [simp]: 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1067 
"(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1068 
by (induct a b rule: gcd_eucl_induct) 
60686  1069 
(simp_all add: euclid_ext_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm) 
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1070 

718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1071 
lemma euclid_ext_gcd' [simp]: 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1072 
"euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1073 
by (insert euclid_ext_gcd[of a b], drule (1) subst, simp) 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1074 

718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1075 
lemma euclid_ext'_correct: 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1076 
"fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1077 
proof 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1078 
obtain s t c where "euclid_ext a b = (s,t,c)" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1079 
by (cases "euclid_ext a b", blast) 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1080 
with euclid_ext_correct[of a b] euclid_ext_gcd[of a b] 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1081 
show ?thesis unfolding euclid_ext'_def by simp 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1082 
qed 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1083 

718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1084 
lemma bezout: "\<exists>s t. s * a + t * b = gcd a b" 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1085 
using euclid_ext'_correct by blast 
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1086 

58023  1087 
lemma gcd_neg1 [simp]: 
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1088 
"gcd (a) b = gcd a b" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

1089 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
58023  1090 

1091 
lemma gcd_neg2 [simp]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1092 
"gcd a (b) = gcd a b" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

1093 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
58023  1094 

1095 
lemma gcd_neg_numeral_1 [simp]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1096 
"gcd ( numeral n) a = gcd (numeral n) a" 
58023  1097 
by (fact gcd_neg1) 
1098 

1099 
lemma gcd_neg_numeral_2 [simp]: 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1100 
"gcd a ( numeral n) = gcd a (numeral n)" 
58023  1101 
by (fact gcd_neg2) 
1102 

1103 
lemma gcd_diff1: "gcd (m  n) n = gcd m n" 

1104 
by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) 

1105 

1106 
lemma gcd_diff2: "gcd (n  m) n = gcd m n" 

1107 
by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1) 

1108 

1109 
lemma coprime_minus_one [simp]: "gcd (n  1) n = 1" 

1110 
proof  

1111 
have "gcd (n  1) n = gcd n (n  1)" by (fact gcd.commute) 

1112 
also have "\<dots> = gcd ((n  1) + 1) (n  1)" by simp 

1113 
also have "\<dots> = 1" by (rule coprime_plus_one) 

1114 
finally show ?thesis . 

1115 
qed 

1116 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1117 
lemma lcm_neg1 [simp]: "lcm (a) b = lcm a b" 
58023  1118 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) 
1119 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1120 
lemma lcm_neg2 [simp]: "lcm a (b) = lcm a b" 
58023  1121 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) 
1122 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1123 
lemma lcm_neg_numeral_1 [simp]: "lcm ( numeral n) a = lcm (numeral n) a" 
58023  1124 
by (fact lcm_neg1) 
1125 

60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset

1126 
lemma lcm_neg_numeral_2 [simp]: "lcm a ( numeral n) = lcm a (numeral n)" 
58023  1127 
by (fact lcm_neg2) 
1128 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1129 
end 
58023  1130 

1131 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1132 
subsection \<open>Typical instances\<close> 
58023  1133 

1134 
instantiation nat :: euclidean_semiring 

1135 
begin 

1136 

1137 
definition [simp]: 

1138 
"euclidean_size_nat = (id :: nat \<Rightarrow> nat)" 

1139 

1140 
instance proof 

59061  1141 
qed simp_all 
58023  1142 

1143 
end 

1144 

62422  1145 

58023  1146 
instantiation int :: euclidean_ring 
1147 
begin 

1148 

1149 
definition [simp]: 

1150 
"euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)" 

1151 

60580  1152 
instance 
60686  1153 
by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split) 
58023  1154 

1155 
end 

1156 

62422  1157 

60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset

1158 
instantiation poly :: (field) euclidean_ring 
60571  1159 
begin 
1160 

1161 
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" 

62422  1162 
where "euclidean_size p = (if p = 0 then 0 else 2 ^ degree p)" 
60571  1163 

60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1164 
lemma euclidean_size_poly_0 [simp]: 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1165 
"euclidean_size (0::'a poly) = 0" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1166 
by (simp add: euclidean_size_poly_def) 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1167 

87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1168 
lemma euclidean_size_poly_not_0 [simp]: 
62422  1169 
"p \<noteq> 0 \<Longrightarrow> euclidean_size p = 2 ^ degree p" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1170 
by (simp add: euclidean_size_poly_def) 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1171 

60571  1172 
instance 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1173 
proof 
60571  1174 
fix p q :: "'a poly" 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1175 
assume "q \<noteq> 0" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1176 
then have "p mod q = 0 \<or> degree (p mod q) < degree q" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1177 
by (rule degree_mod_less [of q p]) 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1178 
with \<open>q \<noteq> 0\<close> show "euclidean_size (p mod q) < euclidean_size q" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1179 
by (cases "p mod q = 0") simp_all 
60571  1180 
next 
1181 
fix p q :: "'a poly" 

1182 
assume "q \<noteq> 0" 

60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1183 
from \<open>q \<noteq> 0\<close> have "degree p \<le> degree (p * q)" 
60571  1184 
by (rule degree_mult_right_le) 
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1185 
with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)" 
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset

1186 
by (cases "p = 0") simp_all 
62422  1187 
qed simp 
60571  1188 

58023  1189 
end 
60571  1190 

62422  1191 

1192 
instance nat :: euclidean_semiring_gcd 

1193 
proof 

1194 
show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)" 

1195 
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) 

1196 
show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)" 

1197 
by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+ 

1198 
qed 

1199 

1200 
instance int :: euclidean_ring_gcd 

1201 
proof 

1202 
show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)" 

1203 
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) 

1204 
show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)" 

1205 
by (intro ext, simp add: lcm_eucl_def lcm_altdef_int 

1206 
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+ 

1207 
qed 

1208 

1209 

1210 
instantiation poly :: (field) euclidean_ring_gcd 

1211 
begin 

1212 

1213 
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

1214 
"gcd_poly = gcd_eucl" 

1215 

1216 
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where 

1217 
"lcm_poly = lcm_eucl" 

1218 

1219 
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where 

1220 
"Gcd_poly = Gcd_eucl" 

1221 

1222 
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where 

1223 
"Lcm_poly = Lcm_eucl" 

1224 

1225 
instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) 

1226 
end 

60687  1227 

62425  1228 
lemma poly_gcd_monic: 
1229 
"lead_coeff (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)" 

1230 
using unit_factor_gcd[of x y] 

< 