author  eberlm 
Fri, 26 Feb 2016 14:58:07 +0100  
changeset 62425  d0936b500bf5 
parent 62422  4aa35fd6c152 
child 62428  4d5fbec92bb1 
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 

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

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

104 
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

105 

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

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

108 
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

109 

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

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

111 
"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

112 
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

113 

62422  114 
lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a" 
115 
and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b" 

116 
by (induct a b rule: gcd_eucl_induct) 

117 
(simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff) 

118 

119 
lemma normalize_gcd_eucl [simp]: 

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

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

122 

123 
lemma gcd_eucl_greatest: 

124 
fixes k a b :: 'a 

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

126 
proof (induct a b rule: gcd_eucl_induct) 

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

128 
next 

129 
case (mod a b) 

130 
then show ?case 

131 
by (simp add: gcd_eucl_non_0 dvd_mod_iff) 

132 
qed 

133 

134 
lemma eq_gcd_euclI: 

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

136 
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" 

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

138 
shows "gcd = gcd_eucl" 

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

140 

141 
lemma gcd_eucl_zero [simp]: 

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

143 
by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+ 

144 

145 

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

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

148 
and unit_factor_Lcm_eucl [simp]: 

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

150 
proof  

151 
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> 

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

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

154 
case False 

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

156 
with False show ?thesis by auto 

157 
next 

158 
case True 

159 
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 

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

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

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

163 
apply (subst n_def) 

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

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

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

167 
done 

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

169 
unfolding l_def by simp_all 

170 
{ 

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

172 
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) 

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

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

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

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

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

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

179 
proof  

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

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

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

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

184 
by (rule size_mult_mono) 

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

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

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

188 
qed 

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

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

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

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

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

194 
} 

195 

196 
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> 

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

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

199 
unit_factor (normalize l) = 

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

201 
by (auto simp: unit_simps) 

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

203 
by (simp add: Lcm_eucl_def Let_def n_def l_def) 

204 
finally show ?thesis . 

205 
qed 

206 
note A = this 

207 

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

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

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

211 
qed 

212 

213 
lemma normalize_Lcm_eucl [simp]: 

214 
"normalize (Lcm_eucl A) = Lcm_eucl A" 

215 
proof (cases "Lcm_eucl A = 0") 

216 
case True then show ?thesis by simp 

217 
next 

218 
case False 

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

220 
by (fact unit_factor_mult_normalize) 

221 
with False show ?thesis by simp 

222 
qed 

223 

224 
lemma eq_Lcm_euclI: 

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

226 
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" 

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

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

229 

58023  230 
end 
231 

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

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

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

234 

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

235 
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

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

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

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

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

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

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

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

244 
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

245 

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

246 
declare euclid_ext.simps [simp del] 
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 
lemma euclid_ext_0: 
60634  249 
"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

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

251 

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

252 
lemma euclid_ext_left_0: 
60634  253 
"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

254 
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

255 

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

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

257 
"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

258 
(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

259 
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

260 

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

261 
lemma euclid_ext_code [code]: 
60634  262 
"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

263 
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

264 
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

265 

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

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

267 
"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

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

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

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

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

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

273 
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

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

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

276 
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

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

278 
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

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

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

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

282 

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

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

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

285 
"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

286 

60634  287 
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

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

289 

60634  290 
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

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

292 

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

293 
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

294 
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

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

296 

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

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

298 

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

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

302 
begin 

303 

62422  304 
subclass semiring_gcd 
305 
by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def) 

58023  306 

62422  307 
subclass semiring_Gcd 
308 
by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least) 

309 

58023  310 

311 
lemma gcd_non_0: 

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

312 
"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

313 
unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) 
58023  314 

62422  315 
lemmas gcd_0 = gcd_0_right 
316 
lemmas dvd_gcd_iff = gcd_greatest_iff 

58023  317 

318 
lemmas gcd_greatest_iff = dvd_gcd_iff 

319 

320 
lemma gcdI: 

60634  321 
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

322 
and "normalize c = c" 
60634  323 
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

324 
by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) 
58023  325 

326 
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

327 
normalize d = d \<and> 
58023  328 
(\<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

329 
by rule (auto intro: gcdI simp: gcd_greatest) 
58023  330 

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

332 
using mult_dvd_mono [of 1] by auto 

333 

334 
lemma gcd_proj2_if_dvd: 

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

338 
lemma gcd_proj1_if_dvd: 

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

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

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

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

351 
qed (insert A, simp) 

352 
next 

353 
assume "m dvd n" 

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

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

58023  359 

360 
lemma gcd_mod1 [simp]: 

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

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

364 
lemma gcd_mod2 [simp]: 

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

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

368 
lemma gcd_mult_distrib': 

60634  369 
"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

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

372 
next 
60634  373 
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

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

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

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

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

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

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

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

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

387 

388 
lemma gcd_mult_distrib: 

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

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

394 
by simp 

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

396 
by (simp only: ac_simps) 

397 
then show ?thesis 

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

398 
by simp 
58023  399 
qed 
400 

401 
lemma euclidean_size_gcd_le1 [simp]: 

402 
assumes "a \<noteq> 0" 

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

404 
proof  

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

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

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

410 
lemma euclidean_size_gcd_le2 [simp]: 

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

412 
by (subst gcd.commute, rule euclidean_size_gcd_le1) 

413 

414 
lemma euclidean_size_gcd_less1: 

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

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

417 
proof (rule ccontr) 

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

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

423 
hence "a dvd b" using dvd_gcdD2 by blast 

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

427 
lemma euclidean_size_gcd_less2: 

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

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

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

431 

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

432 
lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c" 
58023  433 
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

434 
apply simp_all 
58023  435 
apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) 
436 
done 

437 

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

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

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

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

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

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

60634  447 
lemma normalize_gcd_left [simp]: 
448 
"gcd (normalize a) b = gcd a b" 

449 
proof (cases "a = 0") 

450 
case True then show ?thesis 

451 
by simp 

452 
next 

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

454 
by simp 

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

456 
by simp 

457 
ultimately show ?thesis 

458 
by (simp only: gcd_div_unit1) 

459 
qed 

460 

461 
lemma normalize_gcd_right [simp]: 

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

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

464 

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

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

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

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

471 
apply (rule gcd_dvd2) 

472 
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

473 
apply simp 
58023  474 
done 
475 

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

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

479 
apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2) 

480 
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

481 
apply simp 
58023  482 
done 
483 

484 
lemma comp_fun_idem_gcd: "comp_fun_idem gcd" 

485 
proof 

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

487 
by (simp add: fun_eq_iff ac_simps) 

488 
next 

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

490 
by (simp add: fun_eq_iff gcd_left_idem) 

491 
qed 

492 

493 
lemma gcd_dvd_antisym: 

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

495 
proof (rule gcdI) 

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

497 
have "gcd c d dvd c" by simp 

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

499 
have "gcd c d dvd d" by simp 

500 
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

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

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

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

506 
qed 

507 

508 
lemma coprime_crossproduct: 

509 
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

510 
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

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

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

514 
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

515 
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

516 
then show ?lhs by (simp add: associated_iff_dvd) 
58023  517 
next 
518 
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

519 
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

520 
then have "a dvd b * d" by (metis dvd_mult_left) 
58023  521 
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

522 
moreover from dvd have "b dvd a * c" by (metis dvd_mult_left) 
58023  523 
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

524 
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

525 
by (auto dest: dvd_mult_right simp add: ac_simps) 
58023  526 
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

527 
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

528 
by (auto dest: dvd_mult_right simp add: ac_simps) 
58023  529 
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

530 
ultimately show ?rhs by (simp add: associated_iff_dvd) 
58023  531 
qed 
532 

533 
lemma gcd_add1 [simp]: 

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

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

536 

537 
lemma gcd_add2 [simp]: 

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

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

540 

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

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

542 
"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

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

544 
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

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

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

547 
qed 
58023  548 

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

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

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

62422  553 
by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2) 
58023  554 

555 
lemma div_gcd_coprime: 

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

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

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

559 
shows "gcd a' b' = 1" 

560 
proof (rule coprimeI) 

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

562 
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

563 
moreover have "a = a' * d" "b = b' * d" by simp_all 
58023  564 
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

565 
by (simp_all only: ac_simps) 
58023  566 
hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left) 
567 
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

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

569 
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

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

571 
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

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

574 
then show "l dvd 1" .. 
58023  575 
qed 
576 

577 
lemma coprime_lmult: 

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

579 
shows "gcd d a = 1" 

580 
proof (rule coprimeI) 

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

582 
hence "l dvd a * b" by simp 

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

586 
lemma coprime_rmult: 

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

588 
shows "gcd d b = 1" 

589 
proof (rule coprimeI) 

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

591 
hence "l dvd a * b" by simp 

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

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

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

597 

598 
lemma gcd_coprime: 

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

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

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

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

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

606 
finally show ?thesis . 

607 
qed 

608 

609 
lemma coprime_power: 

610 
assumes "0 < n" 

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

612 
using assms proof (induct n) 

613 
case (Suc n) then show ?case 

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

615 
qed simp 

616 

617 
lemma gcd_coprime_exists: 

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

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

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

621 
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

622 
apply (insert nz, auto intro: div_gcd_coprime) 
58023  623 
done 
624 

625 
lemma coprime_exp: 

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

627 
by (induct n, simp_all add: coprime_mult) 

628 

629 
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

630 
"gcd (a ^ n) (b ^ n) = gcd a b ^ n" 
58023  631 
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

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

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

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

636 
then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 
62422  637 
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

638 
then have "gcd a b ^ n = gcd a b ^ n * ..." by simp 
58023  639 
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

640 
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

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

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

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

646 
finally show ?thesis by simp 

647 
qed 

648 

649 
lemma coprime_common_divisor: 

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

650 
"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

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

655 

656 
lemma division_decomp: 

657 
assumes dc: "a dvd b * c" 

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

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

660 
assume "gcd a b = 0" 

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

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

664 
next 

665 
let ?d = "gcd a b" 

666 
assume "?d \<noteq> 0" 

667 
from gcd_coprime_exists[OF this] 

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

669 
by blast 

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

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

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

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

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

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

678 
then show ?thesis by blast 

679 
qed 

680 

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

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

685 
assume "gcd a b = 0" 

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

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

689 
assume "?d \<noteq> 0" 

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

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

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

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

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

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

698 
by (simp only: power_mult_distrib ac_simps) 

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

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

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

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

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

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

706 
qed 

707 

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

62422  712 
lemmas divs_mult = divides_mult 
58023  713 

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

715 
by (subst add_commute, simp) 

716 

717 
lemma setprod_coprime [rule_format]: 

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

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

721 
apply (auto simp add: gcd_mult_cancel) 

722 
done 

62422  723 

724 
lemma listprod_coprime: 

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

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

58023  727 

728 
lemma coprime_divisors: 

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

730 
shows "gcd d e = 1" 

731 
proof  

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

733 
unfolding dvd_def by blast 

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

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

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

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

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

739 
qed 

740 

741 
lemma invertible_coprime: 

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

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

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

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

745 
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

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

747 
then have "coprime m (a * b)" 
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" 
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58953
diff
changeset

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

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

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

753 
qed 
58023  754 

755 
lemma lcm_gcd_prod: 

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

58023  758 

759 
lemma lcm_zero: 

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

60687  761 
by (fact lcm_eq_0_iff) 
58023  762 

763 
lemmas lcm_0_iff = lcm_zero 

764 

765 
lemma gcd_lcm: 

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

60634  767 
shows "gcd a b = normalize (a * b) div lcm a b" 
768 
proof  

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

770 
by (fact lcm_gcd_prod) 

771 
with assms show ?thesis 

772 
by (metis nonzero_mult_divide_cancel_left) 

58023  773 
qed 
774 

60687  775 
declare unit_factor_lcm [simp] 
58023  776 

777 
lemma lcmI: 

60634  778 
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

779 
and "normalize c = c" 
60634  780 
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

781 
by (rule associated_eqI) (auto simp: assms intro: lcm_least) 
58023  782 

783 
lemma gcd_dvd_lcm [simp]: 

784 
"gcd a b dvd lcm a b" 

60690  785 
using gcd_dvd2 by (rule dvd_lcmI2) 
58023  786 

62422  787 
lemmas lcm_0 = lcm_0_right 
58023  788 

789 
lemma lcm_unique: 

790 
"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

791 
normalize d = d \<and> 
58023  792 
(\<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

793 
by rule (auto intro: lcmI simp: lcm_least lcm_zero) 
58023  794 

795 
lemma lcm_coprime: 

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

799 
lemma lcm_proj1_if_dvd: 

60634  800 
"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

801 
by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) 
58023  802 

803 
lemma lcm_proj2_if_dvd: 

60634  804 
"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

805 
using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) 
58023  806 

807 
lemma lcm_proj1_iff: 

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

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

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

817 
qed simp 

818 
next 

819 
assume "n dvd m" 

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

823 
lemma lcm_proj2_iff: 

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

827 
lemma euclidean_size_lcm_le1: 

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

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

830 
proof  

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

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

836 

837 
lemma euclidean_size_lcm_le2: 

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

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

840 

841 
lemma euclidean_size_lcm_less1: 

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

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

844 
proof (rule ccontr) 

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

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

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

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

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

855 
lemma euclidean_size_lcm_less2: 

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

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

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

859 

860 
lemma lcm_mult_unit1: 

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

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

864 
lemma lcm_mult_unit2: 

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

865 
"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

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

868 
lemma lcm_div_unit1: 

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

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

872 
lemma lcm_div_unit2: 

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

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

60634  876 
lemma normalize_lcm_left [simp]: 
877 
"lcm (normalize a) b = lcm a b" 

878 
proof (cases "a = 0") 

879 
case True then show ?thesis 

880 
by simp 

881 
next 

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

883 
by simp 

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

885 
by simp 

886 
ultimately show ?thesis 

887 
by (simp only: lcm_div_unit1) 

888 
qed 

889 

890 
lemma normalize_lcm_right [simp]: 

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

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

893 

58023  894 
lemma LcmI: 
60634  895 
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

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

899 
lemma Lcm_subset: 

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

60634  901 
by (blast intro: Lcm_least dvd_Lcm) 
58023  902 

903 
lemma Lcm_Un: 

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

905 
apply (rule lcmI) 

906 
apply (blast intro: Lcm_subset) 

907 
apply (blast intro: Lcm_subset) 

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

911 
apply simp 

912 
done 

913 

914 
lemma Lcm_no_units: 

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

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

917 
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

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

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

923 

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

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

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

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

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

930 
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

931 
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

932 
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

933 
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

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

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

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

939 
done 

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

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

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

947 

948 
lemma Lcm_no_multiple: 

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

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

951 
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

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

955 

956 
lemma Lcm_finite: 

957 
assumes "finite A" 

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

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

60431
db9c67b760f1
dropped warnings by dropping ineffective code declarations
haftmann
parents:
60430
diff
changeset

962 
lemma Lcm_set [code_unfold]: 
58023  963 
"Lcm (set xs) = fold lcm xs 1" 
964 
using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps) 

965 

966 
lemma Lcm_singleton [simp]: 

60634  967 
"Lcm {a} = normalize a" 
58023  968 
by simp 
969 

970 
lemma Lcm_2 [simp]: 

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

60634  972 
by simp 
58023  973 

974 
lemma Lcm_coprime: 

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

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

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

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

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

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

987 
qed simp 

988 

989 
lemma Lcm_coprime': 

990 
"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  991 
\<Longrightarrow> Lcm A = normalize (\<Prod>A)" 
58023  992 
by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) 
993 

62422  994 
lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
58023  995 
proof  
60634  996 
show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 
62422  997 
by (simp add: Gcd_Lcm unit_factor_Lcm) 
58023  998 
qed 
999 

1000 
lemma GcdI: 

60634  1001 
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

1002 
and "normalize b = b" 
60634  1003 
shows "b = Gcd A" 
62422  1004 
by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) 
58023  1005 

1006 
lemma Gcd_1: 

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

60687  1008 
by (auto intro!: Gcd_eq_1_I) 
58023  1009 

1010 
lemma Gcd_finite: 

1011 
assumes "finite A" 

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

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

60431
db9c67b760f1
dropped warnings by dropping ineffective code declarations
haftmann
parents:
60430
diff
changeset

1016 
lemma Gcd_set [code_unfold]: 
58023  1017 
"Gcd (set xs) = fold gcd xs 0" 
1018 
using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps) 

1019 

60634  1020 
lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" 
60687  1021 
by simp 
58023  1022 

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

60687  1024 
by simp 
60686  1025 

62422  1026 

1027 
definition pairwise_coprime where 

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

1029 

1030 
lemma pairwise_coprimeI [intro?]: 

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

1032 
by (simp add: pairwise_coprime_def) 

1033 

1034 
lemma pairwise_coprimeD: 

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

1036 
by (simp add: pairwise_coprime_def) 

1037 

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

1039 
by (force simp: pairwise_coprime_def) 

1040 

58023  1041 
end 
1042 

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

60526  1046 
\<close> 
58023  1047 

1048 
class euclidean_ring_gcd = euclidean_semiring_gcd + idom 

1049 
begin 

1050 

1051 
subclass euclidean_ring .. 

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

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

1053 

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

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

1055 
"(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

1056 
by (induct a b rule: gcd_eucl_induct) 
60686  1057 
(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

1058 

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

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

1060 
"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

1061 
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

1062 

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

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

1064 
"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

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

1066 
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

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

1068 
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

1069 
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

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

1071 

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

1072 
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

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

1074 

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

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

1077 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
58023  1078 

1079 
lemma gcd_neg2 [simp]: 

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

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

1081 
by (rule sym, rule gcdI, simp_all add: gcd_greatest) 
58023  1082 

1083 
lemma gcd_neg_numeral_1 [simp]: 

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

1084 
"gcd ( numeral n) a = gcd (numeral n) a" 
58023  1085 
by (fact gcd_neg1) 
1086 

1087 
lemma gcd_neg_numeral_2 [simp]: 

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

1088 
"gcd a ( numeral n) = gcd a (numeral n)" 
58023  1089 
by (fact gcd_neg2) 
1090 

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

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

1093 

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

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

1096 

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

1098 
proof  

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

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

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

1102 
finally show ?thesis . 

1103 
qed 

1104 

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

1105 
lemma lcm_neg1 [simp]: "lcm (a) b = lcm a b" 
58023  1106 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) 
1107 

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

1108 
lemma lcm_neg2 [simp]: "lcm a (b) = lcm a b" 
58023  1109 
by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) 
1110 

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

1111 
lemma lcm_neg_numeral_1 [simp]: "lcm ( numeral n) a = lcm (numeral n) a" 
58023  1112 
by (fact lcm_neg1) 
1113 

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

1114 
lemma lcm_neg_numeral_2 [simp]: "lcm a ( numeral n) = lcm a (numeral n)" 
58023  1115 
by (fact lcm_neg2) 
1116 

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

1117 
end 
58023  1118 

1119 

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

1120 
subsection \<open>Typical instances\<close> 
58023  1121 

1122 
instantiation nat :: euclidean_semiring 

1123 
begin 

1124 

1125 
definition [simp]: 

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

1127 

1128 
instance proof 

59061  1129 
qed simp_all 
58023  1130 

1131 
end 

1132 

62422  1133 

58023  1134 
instantiation int :: euclidean_ring 
1135 
begin 

1136 

1137 
definition [simp]: 

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

1139 

60580  1140 
instance 
60686  1141 
by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split) 
58023  1142 

1143 
end 

1144 

62422  1145 

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

1146 
instantiation poly :: (field) euclidean_ring 
60571  1147 
begin 
1148 

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

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

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

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

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

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

1155 

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

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

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

1159 

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

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

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

1164 
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

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

1166 
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

1167 
by (cases "p mod q = 0") simp_all 
60571  1168 
next 
1169 
fix p q :: "'a poly" 

1170 
assume "q \<noteq> 0" 

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

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

1173 
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

1174 
by (cases "p = 0") simp_all 
62422  1175 
qed simp 
60571  1176 

58023  1177 
end 
60571  1178 

62422  1179 

1180 
instance nat :: euclidean_semiring_gcd 

1181 
proof 

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

1183 
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) 

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

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

1186 
qed 

1187 

1188 
instance int :: euclidean_ring_gcd 

1189 
proof 

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

1191 
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) 

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

1193 
by (intro ext, simp add: lcm_eucl_def lcm_altdef_int 

1194 
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+ 

1195 
qed 

1196 

1197 

1198 
instantiation poly :: (field) euclidean_ring_gcd 

1199 
begin 

1200 

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

1202 
"gcd_poly = gcd_eucl" 

1203 

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

1205 
"lcm_poly = lcm_eucl" 

1206 

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

1208 
"Gcd_poly = Gcd_eucl" 

1209 

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

1211 
"Lcm_poly = Lcm_eucl" 

1212 

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

1214 
end 

60687  1215 

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

1218 
using unit_factor_gcd[of x y] 

1219 
by (simp add: unit_factor_poly_def monom_0 one_poly_def lead_coeff_def split: if_split_asm) 

1220 

1221 
lemma poly_dvd_antisym: 

1222 
fixes p q :: "'a::idom poly" 

1223 
assumes coeff: "coeff p (degree p) = coeff q (degree q)" 

1224 
assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" 

1225 
proof (cases "p = 0") 

1226 
case True with coeff show "p = q" by simp 

1227 
next 

1228 
case False with coeff have "q \<noteq> 0" by auto 

1229 
have degree: "degree p = degree q" 

1230 
using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> 

1231 
by (intro order_antisym dvd_imp_degree_le) 

1232 

1233 
from \<open>p dvd q\<close> obtain a where a: "q = p * a" .. 
