author  ballarin 
Fri, 01 Aug 2008 18:10:52 +0200  
changeset 27717  21bbd410ba04 
parent 27713  95b36bfe7fc4 
child 28599  12d914277b8d 
permissions  rwrr 
27701  1 
(* 
2 
Title: Divisibility in monoids and rings 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 18 July 2008 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

5 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

6 
Based on work by Stephan Hohe. 
27701  7 
*) 
8 

9 
theory Divisibility 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

10 
imports Permutation Coset Group 
27701  11 
begin 
12 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

13 
section {* Factorial Monoids *} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

14 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

15 
subsection {* Monoids with Cancellation Law *} 
27701  16 

17 
locale monoid_cancel = monoid + 

18 
assumes l_cancel: 

19 
"\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" 

20 
and r_cancel: 

21 
"\<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" 

22 

23 
lemma (in monoid) monoid_cancelI: 

24 
assumes l_cancel: 

25 
"\<And>a b c. \<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" 

26 
and r_cancel: 

27 
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" 

28 
shows "monoid_cancel G" 

29 
by unfold_locales fact+ 

30 

31 
lemma (in monoid_cancel) is_monoid_cancel: 

32 
"monoid_cancel G" 

33 
by intro_locales 

34 

35 
interpretation group \<subseteq> monoid_cancel 

36 
by unfold_locales simp+ 

37 

38 

39 
locale comm_monoid_cancel = monoid_cancel + comm_monoid 

40 

41 
lemma comm_monoid_cancelI: 

42 
includes comm_monoid 

43 
assumes cancel: 

44 
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b" 

45 
shows "comm_monoid_cancel G" 

46 
apply unfold_locales 

47 
apply (subgoal_tac "a \<otimes> c = b \<otimes> c") 

48 
apply (iprover intro: cancel) 

49 
apply (simp add: m_comm) 

50 
apply (iprover intro: cancel) 

51 
done 

52 

53 
lemma (in comm_monoid_cancel) is_comm_monoid_cancel: 

54 
"comm_monoid_cancel G" 

55 
by intro_locales 

56 

57 
interpretation comm_group \<subseteq> comm_monoid_cancel 

58 
by unfold_locales 

59 

60 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

61 
subsection {* Products of Units in Monoids *} 
27701  62 

63 
lemma (in monoid) Units_m_closed[simp, intro]: 

64 
assumes h1unit: "h1 \<in> Units G" and h2unit: "h2 \<in> Units G" 

65 
shows "h1 \<otimes> h2 \<in> Units G" 

66 
unfolding Units_def 

67 
using assms 

68 
apply safe 

69 
apply fast 

70 
apply (intro bexI[of _ "inv h2 \<otimes> inv h1"], safe) 

71 
apply (simp add: m_assoc Units_closed) 

72 
apply (simp add: m_assoc[symmetric] Units_closed Units_l_inv) 

73 
apply (simp add: m_assoc Units_closed) 

74 
apply (simp add: m_assoc[symmetric] Units_closed Units_r_inv) 

75 
apply fast 

76 
done 

77 

78 
lemma (in monoid) prod_unit_l: 

79 
assumes abunit[simp]: "a \<otimes> b \<in> Units G" and aunit[simp]: "a \<in> Units G" 

80 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" 

81 
shows "b \<in> Units G" 

82 
proof  

83 
have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp 

84 

85 
have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc) 

86 
also have "\<dots> = \<one>" by (simp add: Units_l_inv) 

87 
finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" . 

88 

89 
have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric]) 

90 
also have "\<dots> = inv a \<otimes> \<one> \<otimes> a" by simp 

91 
also have "\<dots> = inv a \<otimes> ((a \<otimes> b) \<otimes> inv (a \<otimes> b)) \<otimes> a" 

92 
by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv) 

93 
also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a" 

94 
by (simp add: m_assoc del: Units_l_inv) 

95 
also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv) 

96 
also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc) 

97 
finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp 

98 

99 
from c li ri 

100 
show "b \<in> Units G" by (simp add: Units_def, fast) 

101 
qed 

102 

103 
lemma (in monoid) prod_unit_r: 

104 
assumes abunit[simp]: "a \<otimes> b \<in> Units G" and bunit[simp]: "b \<in> Units G" 

105 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" 

106 
shows "a \<in> Units G" 

107 
proof  

108 
have c: "b \<otimes> inv (a \<otimes> b) \<in> carrier G" by simp 

109 

110 
have "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = (a \<otimes> b) \<otimes> inv (a \<otimes> b)" 

111 
by (simp add: m_assoc del: Units_r_inv) 

112 
also have "\<dots> = \<one>" by simp 

113 
finally have li: "a \<otimes> (b \<otimes> inv (a \<otimes> b)) = \<one>" . 

114 

115 
have "\<one> = b \<otimes> inv b" by (simp add: Units_r_inv[symmetric]) 

116 
also have "\<dots> = b \<otimes> \<one> \<otimes> inv b" by simp 

117 
also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> (a \<otimes> b)) \<otimes> inv b" 

118 
by (simp add: Units_l_inv[OF abunit, symmetric] del: Units_l_inv) 

119 
also have "\<dots> = (b \<otimes> inv (a \<otimes> b) \<otimes> a) \<otimes> (b \<otimes> inv b)" 

120 
by (simp add: m_assoc del: Units_l_inv) 

121 
also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp 

122 
finally have ri: "(b \<otimes> inv (a \<otimes> b)) \<otimes> a = \<one> " by simp 

123 

124 
from c li ri 

125 
show "a \<in> Units G" by (simp add: Units_def, fast) 

126 
qed 

127 

128 
lemma (in comm_monoid) unit_factor: 

129 
assumes abunit: "a \<otimes> b \<in> Units G" 

130 
and [simp]: "a \<in> carrier G" "b \<in> carrier G" 

131 
shows "a \<in> Units G" 

132 
using abunit[simplified Units_def] 

133 
proof clarsimp 

134 
fix i 

135 
assume [simp]: "i \<in> carrier G" 

136 
and li: "i \<otimes> (a \<otimes> b) = \<one>" 

137 
and ri: "a \<otimes> b \<otimes> i = \<one>" 

138 

139 
have carr': "b \<otimes> i \<in> carrier G" by simp 

140 

141 
have "(b \<otimes> i) \<otimes> a = (i \<otimes> b) \<otimes> a" by (simp add: m_comm) 

142 
also have "\<dots> = i \<otimes> (b \<otimes> a)" by (simp add: m_assoc) 

143 
also have "\<dots> = i \<otimes> (a \<otimes> b)" by (simp add: m_comm) 

144 
also note li 

145 
finally have li': "(b \<otimes> i) \<otimes> a = \<one>" . 

146 

147 
have "a \<otimes> (b \<otimes> i) = a \<otimes> b \<otimes> i" by (simp add: m_assoc) 

148 
also note ri 

149 
finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" . 

150 

151 
from carr' li' ri' 

152 
show "a \<in> Units G" by (simp add: Units_def, fast) 

153 
qed 

154 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

155 
subsection {* Divisibility and Association *} 
27701  156 

157 
subsubsection {* Function definitions *} 

158 

159 
constdefs (structure G) 

160 
factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65) 

161 
"a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c" 

162 

163 
constdefs (structure G) 

164 
associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55) 

165 
"a \<sim> b == a divides b \<and> b divides a" 

166 

167 
abbreviation 

168 
"division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>" 

169 

170 
constdefs (structure G) 

171 
properfactor :: "[_, 'a, 'a] \<Rightarrow> bool" 

172 
"properfactor G a b == a divides b \<and> \<not>(b divides a)" 

173 

174 
constdefs (structure G) 

175 
irreducible :: "[_, 'a] \<Rightarrow> bool" 

176 
"irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)" 

177 

178 
constdefs (structure G) 

179 
prime :: "[_, 'a] \<Rightarrow> bool" 

180 
"prime G p == p \<notin> Units G \<and> 

181 
(\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)" 

182 

183 

184 

185 
subsubsection {* Divisibility *} 

186 

187 
lemma dividesI: 

188 
fixes G (structure) 

189 
assumes carr: "c \<in> carrier G" 

190 
and p: "b = a \<otimes> c" 

191 
shows "a divides b" 

192 
unfolding factor_def 

193 
using assms by fast 

194 

195 
lemma dividesI' [intro]: 

196 
fixes G (structure) 

197 
assumes p: "b = a \<otimes> c" 

198 
and carr: "c \<in> carrier G" 

199 
shows "a divides b" 

200 
using assms 

201 
by (fast intro: dividesI) 

202 

203 
lemma dividesD: 

204 
fixes G (structure) 

205 
assumes "a divides b" 

206 
shows "\<exists>c\<in>carrier G. b = a \<otimes> c" 

207 
using assms 

208 
unfolding factor_def 

209 
by fast 

210 

211 
lemma dividesE [elim]: 

212 
fixes G (structure) 

213 
assumes d: "a divides b" 

214 
and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P" 

215 
shows "P" 

216 
proof  

217 
from dividesD[OF d] 

218 
obtain c 

219 
where "c\<in>carrier G" 

220 
and "b = a \<otimes> c" 

221 
by auto 

222 
thus "P" by (elim elim) 

223 
qed 

224 

225 
lemma (in monoid) divides_refl[simp, intro!]: 

226 
assumes carr: "a \<in> carrier G" 

227 
shows "a divides a" 

228 
apply (intro dividesI[of "\<one>"]) 

229 
apply (simp, simp add: carr) 

230 
done 

231 

232 
lemma (in monoid) divides_trans [trans]: 

233 
assumes dvds: "a divides b" "b divides c" 

234 
and acarr: "a \<in> carrier G" 

235 
shows "a divides c" 

236 
using dvds[THEN dividesD] 

237 
by (blast intro: dividesI m_assoc acarr) 

238 

239 
lemma (in monoid) divides_mult_lI [intro]: 

240 
assumes ab: "a divides b" 

241 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

242 
shows "(c \<otimes> a) divides (c \<otimes> b)" 

243 
using ab 

244 
apply (elim dividesE, simp add: m_assoc[symmetric] carr) 

245 
apply (fast intro: dividesI) 

246 
done 

247 

248 
lemma (in monoid_cancel) divides_mult_l [simp]: 

249 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

250 
shows "(c \<otimes> a) divides (c \<otimes> b) = a divides b" 

251 
apply safe 

252 
apply (elim dividesE, intro dividesI, assumption) 

253 
apply (rule l_cancel[of c]) 

254 
apply (simp add: m_assoc carr)+ 

255 
apply (fast intro: divides_mult_lI carr) 

256 
done 

257 

258 
lemma (in comm_monoid) divides_mult_rI [intro]: 

259 
assumes ab: "a divides b" 

260 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

261 
shows "(a \<otimes> c) divides (b \<otimes> c)" 

262 
using carr ab 

263 
apply (simp add: m_comm[of a c] m_comm[of b c]) 

264 
apply (rule divides_mult_lI, assumption+) 

265 
done 

266 

267 
lemma (in comm_monoid_cancel) divides_mult_r [simp]: 

268 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

269 
shows "(a \<otimes> c) divides (b \<otimes> c) = a divides b" 

270 
using carr 

271 
by (simp add: m_comm[of a c] m_comm[of b c]) 

272 

273 
lemma (in monoid) divides_prod_r: 

274 
assumes ab: "a divides b" 

275 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

276 
shows "a divides (b \<otimes> c)" 

277 
using ab carr 

278 
by (fast intro: m_assoc) 

279 

280 
lemma (in comm_monoid) divides_prod_l: 

281 
assumes carr[intro]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

282 
and ab: "a divides b" 

283 
shows "a divides (c \<otimes> b)" 

284 
using ab carr 

285 
apply (simp add: m_comm[of c b]) 

286 
apply (fast intro: divides_prod_r) 

287 
done 

288 

289 
lemma (in monoid) unit_divides: 

290 
assumes uunit: "u \<in> Units G" 

291 
and acarr: "a \<in> carrier G" 

292 
shows "u divides a" 

293 
proof (intro dividesI[of "(inv u) \<otimes> a"], fast intro: uunit acarr) 

294 
from uunit acarr 

295 
have xcarr: "inv u \<otimes> a \<in> carrier G" by fast 

296 

297 
from uunit acarr 

298 
have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a" by (fast intro: m_assoc[symmetric]) 

299 
also have "\<dots> = \<one> \<otimes> a" by (simp add: Units_r_inv[OF uunit]) 

300 
also from acarr 

301 
have "\<dots> = a" by simp 

302 
finally 

303 
show "a = u \<otimes> (inv u \<otimes> a)" .. 

304 
qed 

305 

306 
lemma (in comm_monoid) divides_unit: 

307 
assumes udvd: "a divides u" 

308 
and carr: "a \<in> carrier G" "u \<in> Units G" 

309 
shows "a \<in> Units G" 

310 
using udvd carr 

311 
by (blast intro: unit_factor) 

312 

313 
lemma (in comm_monoid) Unit_eq_dividesone: 

314 
assumes ucarr: "u \<in> carrier G" 

315 
shows "u \<in> Units G = u divides \<one>" 

316 
using ucarr 

317 
by (fast dest: divides_unit intro: unit_divides) 

318 

319 

320 
subsubsection {* Association *} 

321 

322 
lemma associatedI: 

323 
fixes G (structure) 

324 
assumes "a divides b" "b divides a" 

325 
shows "a \<sim> b" 

326 
using assms 

327 
by (simp add: associated_def) 

328 

329 
lemma (in monoid) associatedI2: 

330 
assumes uunit[simp]: "u \<in> Units G" 

331 
and a: "a = b \<otimes> u" 

332 
and bcarr[simp]: "b \<in> carrier G" 

333 
shows "a \<sim> b" 

334 
using uunit bcarr 

335 
unfolding a 

336 
apply (intro associatedI) 

337 
apply (rule dividesI[of "inv u"], simp) 

338 
apply (simp add: m_assoc Units_closed Units_r_inv) 

339 
apply fast 

340 
done 

341 

342 
lemma (in monoid) associatedI2': 

343 
assumes a: "a = b \<otimes> u" 

344 
and uunit: "u \<in> Units G" 

345 
and bcarr: "b \<in> carrier G" 

346 
shows "a \<sim> b" 

347 
using assms by (intro associatedI2) 

348 

349 
lemma associatedD: 

350 
fixes G (structure) 

351 
assumes "a \<sim> b" 

352 
shows "a divides b" 

353 
using assms by (simp add: associated_def) 

354 

355 
lemma (in monoid_cancel) associatedD2: 

356 
assumes assoc: "a \<sim> b" 

357 
and carr: "a \<in> carrier G" "b \<in> carrier G" 

358 
shows "\<exists>u\<in>Units G. a = b \<otimes> u" 

359 
using assoc 

360 
unfolding associated_def 

361 
proof clarify 

362 
assume "b divides a" 

363 
hence "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD) 

364 
from this obtain u 

365 
where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u" 

366 
by auto 

367 

368 
assume "a divides b" 

369 
hence "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD) 

370 
from this obtain u' 

371 
where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'" 

372 
by auto 

373 
note carr = carr ucarr u'carr 

374 

375 
from carr 

376 
have "a \<otimes> \<one> = a" by simp 

377 
also have "\<dots> = b \<otimes> u" by (simp add: a) 

378 
also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b) 

379 
also from carr 

380 
have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc) 

381 
finally 

382 
have "a \<otimes> \<one> = a \<otimes> (u' \<otimes> u)" . 

383 
with carr 

384 
have u1: "\<one> = u' \<otimes> u" by (fast dest: l_cancel) 

385 

386 
from carr 

387 
have "b \<otimes> \<one> = b" by simp 

388 
also have "\<dots> = a \<otimes> u'" by (simp add: b) 

389 
also have "\<dots> = b \<otimes> u \<otimes> u'" by (simp add: a) 

390 
also from carr 

391 
have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc) 

392 
finally 

393 
have "b \<otimes> \<one> = b \<otimes> (u \<otimes> u')" . 

394 
with carr 

395 
have u2: "\<one> = u \<otimes> u'" by (fast dest: l_cancel) 

396 

397 
from u'carr u1[symmetric] u2[symmetric] 

398 
have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>" by fast 

399 
hence "u \<in> Units G" by (simp add: Units_def ucarr) 

400 

401 
from ucarr this a 

402 
show "\<exists>u\<in>Units G. a = b \<otimes> u" by fast 

403 
qed 

404 

405 
lemma associatedE: 

406 
fixes G (structure) 

407 
assumes assoc: "a \<sim> b" 

408 
and e: "\<lbrakk>a divides b; b divides a\<rbrakk> \<Longrightarrow> P" 

409 
shows "P" 

410 
proof  

411 
from assoc 

412 
have "a divides b" "b divides a" 

413 
by (simp add: associated_def)+ 

414 
thus "P" by (elim e) 

415 
qed 

416 

417 
lemma (in monoid_cancel) associatedE2: 

418 
assumes assoc: "a \<sim> b" 

419 
and e: "\<And>u. \<lbrakk>a = b \<otimes> u; u \<in> Units G\<rbrakk> \<Longrightarrow> P" 

420 
and carr: "a \<in> carrier G" "b \<in> carrier G" 

421 
shows "P" 

422 
proof  

423 
from assoc and carr 

424 
have "\<exists>u\<in>Units G. a = b \<otimes> u" by (rule associatedD2) 

425 
from this obtain u 

426 
where "u \<in> Units G" "a = b \<otimes> u" 

427 
by auto 

428 
thus "P" by (elim e) 

429 
qed 

430 

431 
lemma (in monoid) associated_refl [simp, intro!]: 

432 
assumes "a \<in> carrier G" 

433 
shows "a \<sim> a" 

434 
using assms 

435 
by (fast intro: associatedI) 

436 

437 
lemma (in monoid) associated_sym [sym]: 

438 
assumes "a \<sim> b" 

439 
and "a \<in> carrier G" "b \<in> carrier G" 

440 
shows "b \<sim> a" 

441 
using assms 

442 
by (iprover intro: associatedI elim: associatedE) 

443 

444 
lemma (in monoid) associated_trans [trans]: 

445 
assumes "a \<sim> b" "b \<sim> c" 

446 
and "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

447 
shows "a \<sim> c" 

448 
using assms 

449 
by (iprover intro: associatedI divides_trans elim: associatedE) 

450 

451 
lemma (in monoid) division_equiv [intro, simp]: 

452 
"equivalence (division_rel G)" 

453 
apply unfold_locales 

454 
apply simp_all 

455 
apply (rule associated_sym, assumption+) 

456 
apply (iprover intro: associated_trans) 

457 
done 

458 

459 

460 
subsubsection {* Division and associativity *} 

461 

462 
lemma divides_antisym: 

463 
fixes G (structure) 

464 
assumes "a divides b" "b divides a" 

465 
and "a \<in> carrier G" "b \<in> carrier G" 

466 
shows "a \<sim> b" 

467 
using assms 

468 
by (fast intro: associatedI) 

469 

470 
lemma (in monoid) divides_cong_l [trans]: 

471 
assumes xx': "x \<sim> x'" 

472 
and xdvdy: "x' divides y" 

473 
and carr [simp]: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" 

474 
shows "x divides y" 

475 
proof  

476 
from xx' 

477 
have "x divides x'" by (simp add: associatedD) 

478 
also note xdvdy 

479 
finally 

480 
show "x divides y" by simp 

481 
qed 

482 

483 
lemma (in monoid) divides_cong_r [trans]: 

484 
assumes xdvdy: "x divides y" 

485 
and yy': "y \<sim> y'" 

486 
and carr[simp]: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" 

487 
shows "x divides y'" 

488 
proof  

489 
note xdvdy 

490 
also from yy' 

491 
have "y divides y'" by (simp add: associatedD) 

492 
finally 

493 
show "x divides y'" by simp 

494 
qed 

495 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

496 
lemma (in monoid) division_weak_partial_order [simp, intro!]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

497 
"weak_partial_order (division_rel G)" 
27701  498 
apply unfold_locales 
499 
apply simp_all 

500 
apply (simp add: associated_sym) 

501 
apply (blast intro: associated_trans) 

502 
apply (simp add: divides_antisym) 

503 
apply (blast intro: divides_trans) 

504 
apply (blast intro: divides_cong_l divides_cong_r associated_sym) 

505 
done 

506 

507 

508 
subsubsection {* Multiplication and associativity *} 

509 

510 
lemma (in monoid_cancel) mult_cong_r: 

511 
assumes "b \<sim> b'" 

512 
and carr: "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" 

513 
shows "a \<otimes> b \<sim> a \<otimes> b'" 

514 
using assms 

515 
apply (elim associatedE2, intro associatedI2) 

516 
apply (auto intro: m_assoc[symmetric]) 

517 
done 

518 

519 
lemma (in comm_monoid_cancel) mult_cong_l: 

520 
assumes "a \<sim> a'" 

521 
and carr: "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" 

522 
shows "a \<otimes> b \<sim> a' \<otimes> b" 

523 
using assms 

524 
apply (elim associatedE2, intro associatedI2) 

525 
apply assumption 

526 
apply (simp add: m_assoc Units_closed) 

527 
apply (simp add: m_comm Units_closed) 

528 
apply simp+ 

529 
done 

530 

531 
lemma (in monoid_cancel) assoc_l_cancel: 

532 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" 

533 
and "a \<otimes> b \<sim> a \<otimes> b'" 

534 
shows "b \<sim> b'" 

535 
using assms 

536 
apply (elim associatedE2, intro associatedI2) 

537 
apply assumption 

538 
apply (rule l_cancel[of a]) 

539 
apply (simp add: m_assoc Units_closed) 

540 
apply fast+ 

541 
done 

542 

543 
lemma (in comm_monoid_cancel) assoc_r_cancel: 

544 
assumes "a \<otimes> b \<sim> a' \<otimes> b" 

545 
and carr: "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G" 

546 
shows "a \<sim> a'" 

547 
using assms 

548 
apply (elim associatedE2, intro associatedI2) 

549 
apply assumption 

550 
apply (rule r_cancel[of a b]) 

551 
apply (simp add: m_assoc Units_closed) 

552 
apply (simp add: m_comm Units_closed) 

553 
apply fast+ 

554 
done 

555 

556 

557 
subsubsection {* Units *} 

558 

559 
lemma (in monoid_cancel) assoc_unit_l [trans]: 

560 
assumes asc: "a \<sim> b" and bunit: "b \<in> Units G" 

561 
and carr: "a \<in> carrier G" 

562 
shows "a \<in> Units G" 

563 
using assms 

564 
by (fast elim: associatedE2) 

565 

566 
lemma (in monoid_cancel) assoc_unit_r [trans]: 

567 
assumes aunit: "a \<in> Units G" and asc: "a \<sim> b" 

568 
and bcarr: "b \<in> carrier G" 

569 
shows "b \<in> Units G" 

570 
using aunit bcarr associated_sym[OF asc] 

571 
by (blast intro: assoc_unit_l) 

572 

573 
lemma (in comm_monoid) Units_cong: 

574 
assumes aunit: "a \<in> Units G" and asc: "a \<sim> b" 

575 
and bcarr: "b \<in> carrier G" 

576 
shows "b \<in> Units G" 

577 
using assms 

578 
by (blast intro: divides_unit elim: associatedE) 

579 

580 
lemma (in monoid) Units_assoc: 

581 
assumes units: "a \<in> Units G" "b \<in> Units G" 

582 
shows "a \<sim> b" 

583 
using units 

584 
by (fast intro: associatedI unit_divides) 

585 

586 
lemma (in monoid) Units_are_ones: 

587 
"Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}" 

588 
apply (simp add: set_eq_def elem_def, rule, simp_all) 

589 
proof clarsimp 

590 
fix a 

591 
assume aunit: "a \<in> Units G" 

592 
show "a \<sim> \<one>" 

593 
apply (rule associatedI) 

594 
apply (fast intro: dividesI[of "inv a"] aunit Units_r_inv[symmetric]) 

595 
apply (fast intro: dividesI[of "a"] l_one[symmetric] Units_closed[OF aunit]) 

596 
done 

597 
next 

598 
have "\<one> \<in> Units G" by simp 

599 
moreover have "\<one> \<sim> \<one>" by simp 

600 
ultimately show "\<exists>a \<in> Units G. \<one> \<sim> a" by fast 

601 
qed 

602 

603 
lemma (in comm_monoid) Units_Lower: 

604 
"Units G = Lower (division_rel G) (carrier G)" 

605 
apply (simp add: Units_def Lower_def) 

606 
apply (rule, rule) 

607 
apply clarsimp 

608 
apply (rule unit_divides) 

609 
apply (unfold Units_def, fast) 

610 
apply assumption 

611 
apply clarsimp 

612 
proof  

613 
fix x 

614 
assume xcarr: "x \<in> carrier G" 

615 
assume r[rule_format]: "\<forall>y. y \<in> carrier G \<longrightarrow> x divides y" 

616 
have "\<one> \<in> carrier G" by simp 

617 
hence "x divides \<one>" by (rule r) 

618 
hence "\<exists>x'\<in>carrier G. \<one> = x \<otimes> x'" by (rule dividesE, fast) 

619 
from this obtain x' 

620 
where x'carr: "x' \<in> carrier G" 

621 
and xx': "\<one> = x \<otimes> x'" 

622 
by auto 

623 

624 
note xx' 

625 
also with xcarr x'carr 

626 
have "\<dots> = x' \<otimes> x" by (simp add: m_comm) 

627 
finally 

628 
have "\<one> = x' \<otimes> x" . 

629 

630 
from x'carr xx'[symmetric] this[symmetric] 

631 
show "\<exists>y\<in>carrier G. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by fast 

632 
qed 

633 

634 

635 
subsubsection {* Proper factors *} 

636 

637 
lemma properfactorI: 

638 
fixes G (structure) 

639 
assumes "a divides b" 

640 
and "\<not>(b divides a)" 

641 
shows "properfactor G a b" 

642 
using assms 

643 
unfolding properfactor_def 

644 
by simp 

645 

646 
lemma properfactorI2: 

647 
fixes G (structure) 

648 
assumes advdb: "a divides b" 

649 
and neq: "\<not>(a \<sim> b)" 

650 
shows "properfactor G a b" 

651 
apply (rule properfactorI, rule advdb) 

652 
proof (rule ccontr, simp) 

653 
assume "b divides a" 

654 
with advdb have "a \<sim> b" by (rule associatedI) 

655 
with neq show "False" by fast 

656 
qed 

657 

658 
lemma (in comm_monoid_cancel) properfactorI3: 

659 
assumes p: "p = a \<otimes> b" 

660 
and nunit: "b \<notin> Units G" 

661 
and carr: "a \<in> carrier G" "b \<in> carrier G" "p \<in> carrier G" 

662 
shows "properfactor G a p" 

663 
unfolding p 

664 
using carr 

665 
apply (intro properfactorI, fast) 

666 
proof (clarsimp, elim dividesE) 

667 
fix c 

668 
assume ccarr: "c \<in> carrier G" 

669 
note [simp] = carr ccarr 

670 

671 
have "a \<otimes> \<one> = a" by simp 

672 
also assume "a = a \<otimes> b \<otimes> c" 

673 
also have "\<dots> = a \<otimes> (b \<otimes> c)" by (simp add: m_assoc) 

674 
finally have "a \<otimes> \<one> = a \<otimes> (b \<otimes> c)" . 

675 

676 
hence rinv: "\<one> = b \<otimes> c" by (intro l_cancel[of "a" "\<one>" "b \<otimes> c"], simp+) 

677 
also have "\<dots> = c \<otimes> b" by (simp add: m_comm) 

678 
finally have linv: "\<one> = c \<otimes> b" . 

679 

680 
from ccarr linv[symmetric] rinv[symmetric] 

681 
have "b \<in> Units G" unfolding Units_def by fastsimp 

682 
with nunit 

683 
show "False" .. 

684 
qed 

685 

686 
lemma properfactorE: 

687 
fixes G (structure) 

688 
assumes pf: "properfactor G a b" 

689 
and r: "\<lbrakk>a divides b; \<not>(b divides a)\<rbrakk> \<Longrightarrow> P" 

690 
shows "P" 

691 
using pf 

692 
unfolding properfactor_def 

693 
by (fast intro: r) 

694 

695 
lemma properfactorE2: 

696 
fixes G (structure) 

697 
assumes pf: "properfactor G a b" 

698 
and elim: "\<lbrakk>a divides b; \<not>(a \<sim> b)\<rbrakk> \<Longrightarrow> P" 

699 
shows "P" 

700 
using pf 

701 
unfolding properfactor_def 

702 
by (fast elim: elim associatedE) 

703 

704 
lemma (in monoid) properfactor_unitE: 

705 
assumes uunit: "u \<in> Units G" 

706 
and pf: "properfactor G a u" 

707 
and acarr: "a \<in> carrier G" 

708 
shows "P" 

709 
using pf unit_divides[OF uunit acarr] 

710 
by (fast elim: properfactorE) 

711 

712 

713 
lemma (in monoid) properfactor_divides: 

714 
assumes pf: "properfactor G a b" 

715 
shows "a divides b" 

716 
using pf 

717 
by (elim properfactorE) 

718 

719 
lemma (in monoid) properfactor_trans1 [trans]: 

720 
assumes dvds: "a divides b" "properfactor G b c" 

721 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

722 
shows "properfactor G a c" 

723 
using dvds carr 

724 
apply (elim properfactorE, intro properfactorI) 

725 
apply (iprover intro: divides_trans)+ 

726 
done 

727 

728 
lemma (in monoid) properfactor_trans2 [trans]: 

729 
assumes dvds: "properfactor G a b" "b divides c" 

730 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

731 
shows "properfactor G a c" 

732 
using dvds carr 

733 
apply (elim properfactorE, intro properfactorI) 

734 
apply (iprover intro: divides_trans)+ 

735 
done 

736 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

737 
lemma properfactor_lless: 
27701  738 
fixes G (structure) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

739 
shows "properfactor G = lless (division_rel G)" 
27701  740 
apply (rule ext) apply (rule ext) apply rule 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

741 
apply (fastsimp elim: properfactorE2 intro: weak_llessI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

742 
apply (fastsimp elim: weak_llessE intro: properfactorI2) 
27701  743 
done 
744 

745 
lemma (in monoid) properfactor_cong_l [trans]: 

746 
assumes x'x: "x' \<sim> x" 

747 
and pf: "properfactor G x y" 

748 
and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" 

749 
shows "properfactor G x' y" 

750 
using pf 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

751 
unfolding properfactor_lless 
27701  752 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

753 
interpret weak_partial_order ["division_rel G"] .. 
27701  754 
from x'x 
755 
have "x' .=\<^bsub>division_rel G\<^esub> x" by simp 

756 
also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" 

757 
finally 

758 
show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr) 

759 
qed 

760 

761 
lemma (in monoid) properfactor_cong_r [trans]: 

762 
assumes pf: "properfactor G x y" 

763 
and yy': "y \<sim> y'" 

764 
and carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" 

765 
shows "properfactor G x y'" 

766 
using pf 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

767 
unfolding properfactor_lless 
27701  768 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

769 
interpret weak_partial_order ["division_rel G"] .. 
27701  770 
assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" 
771 
also from yy' 

772 
have "y .=\<^bsub>division_rel G\<^esub> y'" by simp 

773 
finally 

774 
show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr) 

775 
qed 

776 

777 
lemma (in monoid_cancel) properfactor_mult_lI [intro]: 

778 
assumes ab: "properfactor G a b" 

779 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

780 
shows "properfactor G (c \<otimes> a) (c \<otimes> b)" 

781 
using ab carr 

782 
by (fastsimp elim: properfactorE intro: properfactorI) 

783 

784 
lemma (in monoid_cancel) properfactor_mult_l [simp]: 

785 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

786 
shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b" 

787 
using carr 

788 
by (fastsimp elim: properfactorE intro: properfactorI) 

789 

790 
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: 

791 
assumes ab: "properfactor G a b" 

792 
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

793 
shows "properfactor G (a \<otimes> c) (b \<otimes> c)" 

794 
using ab carr 

795 
by (fastsimp elim: properfactorE intro: properfactorI) 

796 

797 
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: 

798 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

799 
shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b" 

800 
using carr 

801 
by (fastsimp elim: properfactorE intro: properfactorI) 

802 

803 
lemma (in monoid) properfactor_prod_r: 

804 
assumes ab: "properfactor G a b" 

805 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

806 
shows "properfactor G a (b \<otimes> c)" 

807 
by (intro properfactor_trans2[OF ab] divides_prod_r, simp+) 

808 

809 
lemma (in comm_monoid) properfactor_prod_l: 

810 
assumes ab: "properfactor G a b" 

811 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" 

812 
shows "properfactor G a (c \<otimes> b)" 

813 
by (intro properfactor_trans2[OF ab] divides_prod_l, simp+) 

814 

815 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

816 
subsection {* Irreducible Elements and Primes *} 
27701  817 

818 
subsubsection {* Irreducible elements *} 

819 

820 
lemma irreducibleI: 

821 
fixes G (structure) 

822 
assumes "a \<notin> Units G" 

823 
and "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b a\<rbrakk> \<Longrightarrow> b \<in> Units G" 

824 
shows "irreducible G a" 

825 
using assms 

826 
unfolding irreducible_def 

827 
by blast 

828 

829 
lemma irreducibleE: 

830 
fixes G (structure) 

831 
assumes irr: "irreducible G a" 

832 
and elim: "\<lbrakk>a \<notin> Units G; \<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G\<rbrakk> \<Longrightarrow> P" 

833 
shows "P" 

834 
using assms 

835 
unfolding irreducible_def 

836 
by blast 

837 

838 
lemma irreducibleD: 

839 
fixes G (structure) 

840 
assumes irr: "irreducible G a" 

841 
and pf: "properfactor G b a" 

842 
and bcarr: "b \<in> carrier G" 

843 
shows "b \<in> Units G" 

844 
using assms 

845 
by (fast elim: irreducibleE) 

846 

847 
lemma (in monoid_cancel) irreducible_cong [trans]: 

848 
assumes irred: "irreducible G a" 

849 
and aa': "a \<sim> a'" 

850 
and carr[simp]: "a \<in> carrier G" "a' \<in> carrier G" 

851 
shows "irreducible G a'" 

852 
using assms 

853 
apply (elim irreducibleE, intro irreducibleI) 

854 
apply simp_all 

855 
proof clarify 

856 
assume "a' \<in> Units G" 

857 
also note aa'[symmetric] 

858 
finally have aunit: "a \<in> Units G" by simp 

859 

860 
assume "a \<notin> Units G" 

861 
with aunit 

862 
show "False" by fast 

863 
next 

864 
fix b 

865 
assume r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G" 

866 
and bcarr[simp]: "b \<in> carrier G" 

867 
assume "properfactor G b a'" 

868 
also note aa'[symmetric] 

869 
finally 

870 
have "properfactor G b a" by simp 

871 

872 
with bcarr 

873 
show "b \<in> Units G" by (fast intro: r) 

874 
qed 

875 

876 

877 
lemma (in monoid) irreducible_prod_rI: 

878 
assumes airr: "irreducible G a" 

879 
and bunit: "b \<in> Units G" 

880 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" 

881 
shows "irreducible G (a \<otimes> b)" 

882 
using airr carr bunit 

883 
apply (elim irreducibleE, intro irreducibleI, clarify) 

884 
apply (subgoal_tac "a \<in> Units G", simp) 

885 
apply (intro prod_unit_r[of a b] carr bunit, assumption) 

886 
proof  

887 
fix c 

888 
assume [simp]: "c \<in> carrier G" 

889 
and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b a \<longrightarrow> b \<in> Units G" 

890 
assume "properfactor G c (a \<otimes> b)" 

891 
also have "a \<otimes> b \<sim> a" by (intro associatedI2[OF bunit], simp+) 

892 
finally 

893 
have pfa: "properfactor G c a" by simp 

894 
show "c \<in> Units G" by (rule r, simp add: pfa) 

895 
qed 

896 

897 
lemma (in comm_monoid) irreducible_prod_lI: 

898 
assumes birr: "irreducible G b" 

899 
and aunit: "a \<in> Units G" 

900 
and carr [simp]: "a \<in> carrier G" "b \<in> carrier G" 

901 
shows "irreducible G (a \<otimes> b)" 

902 
apply (subst m_comm, simp+) 

903 
apply (intro irreducible_prod_rI assms) 

904 
done 

905 

906 
lemma (in comm_monoid_cancel) irreducible_prodE [elim]: 

907 
assumes irr: "irreducible G (a \<otimes> b)" 

908 
and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" 

909 
and e1: "\<lbrakk>irreducible G a; b \<in> Units G\<rbrakk> \<Longrightarrow> P" 

910 
and e2: "\<lbrakk>a \<in> Units G; irreducible G b\<rbrakk> \<Longrightarrow> P" 

911 
shows "P" 

912 
using irr 

913 
proof (elim irreducibleE) 

914 
assume abnunit: "a \<otimes> b \<notin> Units G" 

915 
and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G" 

916 

917 
show "P" 

918 
proof (cases "a \<in> Units G") 

919 
assume aunit: "a \<in> Units G" 

920 

921 
have "irreducible G b" 

922 
apply (rule irreducibleI) 

923 
proof (rule ccontr, simp) 

924 
assume "b \<in> Units G" 

925 
with aunit have "(a \<otimes> b) \<in> Units G" by fast 

926 
with abnunit show "False" .. 

927 
next 

928 
fix c 

929 
assume ccarr: "c \<in> carrier G" 

930 
and "properfactor G c b" 

931 
hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_l[of c b a]) 

932 
from ccarr this show "c \<in> Units G" by (fast intro: isunit) 

933 
qed 

934 

935 
from aunit this show "P" by (rule e2) 

936 
next 

937 
assume anunit: "a \<notin> Units G" 

938 
with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3) 

939 
hence bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+) 

940 
hence bunit: "b \<in> Units G" by (intro isunit, simp) 

941 

942 
have "irreducible G a" 

943 
apply (rule irreducibleI) 

944 
proof (rule ccontr, simp) 

945 
assume "a \<in> Units G" 

946 
with bunit have "(a \<otimes> b) \<in> Units G" by fast 

947 
with abnunit show "False" .. 

948 
next 

949 
fix c 

950 
assume ccarr: "c \<in> carrier G" 

951 
and "properfactor G c a" 

952 
hence "properfactor G c (a \<otimes> b)" by (simp add: properfactor_prod_r[of c a b]) 

953 
from ccarr this show "c \<in> Units G" by (fast intro: isunit) 

954 
qed 

955 

956 
from this bunit show "P" by (rule e1) 

957 
qed 

958 
qed 

959 

960 

961 
subsubsection {* Prime elements *} 

962 

963 
lemma primeI: 

964 
fixes G (structure) 

965 
assumes "p \<notin> Units G" 

966 
and "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G; p divides (a \<otimes> b)\<rbrakk> \<Longrightarrow> p divides a \<or> p divides b" 

967 
shows "prime G p" 

968 
using assms 

969 
unfolding prime_def 

970 
by blast 

971 

972 
lemma primeE: 

973 
fixes G (structure) 

974 
assumes pprime: "prime G p" 

975 
and e: "\<lbrakk>p \<notin> Units G; \<forall>a\<in>carrier G. \<forall>b\<in>carrier G. 

976 
p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b\<rbrakk> \<Longrightarrow> P" 

977 
shows "P" 

978 
using pprime 

979 
unfolding prime_def 

980 
by (blast dest: e) 

981 

982 
lemma (in comm_monoid_cancel) prime_divides: 

983 
assumes carr: "a \<in> carrier G" "b \<in> carrier G" 

984 
and pprime: "prime G p" 

985 
and pdvd: "p divides a \<otimes> b" 

986 
shows "p divides a \<or> p divides b" 

987 
using assms 

988 
by (blast elim: primeE) 

989 

990 
lemma (in monoid_cancel) prime_cong [trans]: 

991 
assumes pprime: "prime G p" 

992 
and pp': "p \<sim> p'" 

993 
and carr[simp]: "p \<in> carrier G" "p' \<in> carrier G" 

994 
shows "prime G p'" 

995 
using pprime 

996 
apply (elim primeE, intro primeI) 

997 
proof clarify 

998 
assume pnunit: "p \<notin> Units G" 

999 
assume "p' \<in> Units G" 

1000 
also note pp'[symmetric] 

1001 
finally 

1002 
have "p \<in> Units G" by simp 

1003 
with pnunit 

1004 
show False .. 

1005 
next 

1006 
fix a b 

1007 
assume r[rule_format]: 

1008 
"\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides a \<otimes> b \<longrightarrow> p divides a \<or> p divides b" 

1009 
assume p'dvd: "p' divides a \<otimes> b" 

1010 
and carr'[simp]: "a \<in> carrier G" "b \<in> carrier G" 

1011 

1012 
note pp' 

1013 
also note p'dvd 

1014 
finally 

1015 
have "p divides a \<otimes> b" by simp 

1016 
hence "p divides a \<or> p divides b" by (intro r, simp+) 

1017 
moreover { 

1018 
note pp'[symmetric] 

1019 
also assume "p divides a" 

1020 
finally 

1021 
have "p' divides a" by simp 

1022 
hence "p' divides a \<or> p' divides b" by simp 

1023 
} 

1024 
moreover { 

1025 
note pp'[symmetric] 

1026 
also assume "p divides b" 

1027 
finally 

1028 
have "p' divides b" by simp 

1029 
hence "p' divides a \<or> p' divides b" by simp 

1030 
} 

1031 
ultimately 

1032 
show "p' divides a \<or> p' divides b" by fast 

1033 
qed 

1034 

1035 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

1036 
subsection {* Factorization and Factorial Monoids *} 
27701  1037 

1038 
subsubsection {* Function definitions *} 

1039 

1040 
constdefs (structure G) 

1041 
factors :: "[_, 'a list, 'a] \<Rightarrow> bool" 

1042 
"factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a" 

1043 

1044 
wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool" 

1045 
"wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a" 

1046 

1047 
abbreviation 

1048 
list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where 

1049 
"list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)" 

1050 

1051 
constdefs (structure G) 

1052 
essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool" 

1053 
"essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)" 

1054 

1055 

1056 
locale factorial_monoid = comm_monoid_cancel + 

1057 
assumes factors_exist: 

1058 
"\<lbrakk>a \<in> carrier G; a \<notin> Units G\<rbrakk> \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" 

1059 
and factors_unique: 

1060 
"\<lbrakk>factors G fs a; factors G fs' a; a \<in> carrier G; a \<notin> Units G; 

1061 
set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'" 

1062 

1063 

1064 
subsubsection {* Comparing lists of elements *} 

1065 

1066 
text {* Association on lists *} 

1067 

1068 
lemma (in monoid) listassoc_refl [simp, intro]: 

1069 
assumes "set as \<subseteq> carrier G" 

1070 
shows "as [\<sim>] as" 

1071 
using assms 

1072 
by (induct as) simp+ 

1073 

1074 
lemma (in monoid) listassoc_sym [sym]: 

1075 
assumes "as [\<sim>] bs" 

1076 
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" 

1077 
shows "bs [\<sim>] as" 

1078 
using assms 

1079 
proof (induct as arbitrary: bs, simp) 

1080 
case Cons 

1081 
thus ?case 

1082 
apply (induct bs, simp) 

1083 
apply clarsimp 

1084 
apply (iprover intro: associated_sym) 

1085 
done 

1086 
qed 

1087 

1088 
lemma (in monoid) listassoc_trans [trans]: 

1089 
assumes "as [\<sim>] bs" and "bs [\<sim>] cs" 

1090 
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" and "set cs \<subseteq> carrier G" 

1091 
shows "as [\<sim>] cs" 

1092 
using assms 

1093 
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) 

1094 
apply (rule associated_trans) 

1095 
apply (subgoal_tac "as ! i \<sim> bs ! i", assumption) 

1096 
apply (simp, simp) 

1097 
apply blast+ 

1098 
done 

1099 

1100 
lemma (in monoid_cancel) irrlist_listassoc_cong: 

1101 
assumes "\<forall>a\<in>set as. irreducible G a" 

1102 
and "as [\<sim>] bs" 

1103 
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" 

1104 
shows "\<forall>a\<in>set bs. irreducible G a" 

1105 
using assms 

1106 
apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) 

1107 
apply (blast intro: irreducible_cong) 

1108 
done 

1109 

1110 

1111 
text {* Permutations *} 

1112 

1113 
lemma perm_map [intro]: 

1114 
assumes p: "a <~~> b" 

1115 
shows "map f a <~~> map f b" 

1116 
using p 

1117 
by induct auto 

1118 

1119 
lemma perm_map_switch: 

1120 
assumes m: "map f a = map f b" and p: "b <~~> c" 

1121 
shows "\<exists>d. a <~~> d \<and> map f d = map f c" 

1122 
using p m 

1123 
by (induct arbitrary: a) (simp, force, force, blast) 

1124 

1125 
lemma (in monoid) perm_assoc_switch: 

1126 
assumes a:"as [\<sim>] bs" and p: "bs <~~> cs" 

1127 
shows "\<exists>bs'. as <~~> bs' \<and> bs' [\<sim>] cs" 

1128 
using p a 

1129 
apply (induct bs cs arbitrary: as, simp) 

1130 
apply (clarsimp simp add: list_all2_Cons2, blast) 

1131 
apply (clarsimp simp add: list_all2_Cons2) 

1132 
apply blast 

1133 
apply blast 

1134 
done 

1135 

1136 
lemma (in monoid) perm_assoc_switch_r: 

1137 
assumes p: "as <~~> bs" and a:"bs [\<sim>] cs" 

1138 
shows "\<exists>bs'. as [\<sim>] bs' \<and> bs' <~~> cs" 

1139 
using p a 

1140 
apply (induct as bs arbitrary: cs, simp) 

1141 
apply (clarsimp simp add: list_all2_Cons1, blast) 

1142 
apply (clarsimp simp add: list_all2_Cons1) 

1143 
apply blast 

1144 
apply blast 

1145 
done 

1146 

1147 
declare perm_sym [sym] 

1148 

1149 
lemma perm_setP: 

1150 
assumes perm: "as <~~> bs" 

1151 
and as: "P (set as)" 

1152 
shows "P (set bs)" 

1153 
proof  

1154 
from perm 

1155 
have "multiset_of as = multiset_of bs" 

1156 
by (simp add: multiset_of_eq_perm) 

1157 
hence "set as = set bs" by (rule multiset_of_eq_setD) 

1158 
with as 

1159 
show "P (set bs)" by simp 

1160 
qed 

1161 

1162 
lemmas (in monoid) perm_closed = 

1163 
perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"] 

1164 

1165 
lemmas (in monoid) irrlist_perm_cong = 

1166 
perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"] 

1167 

1168 

1169 
text {* Essentially equal factorizations *} 

1170 

1171 
lemma (in monoid) essentially_equalI: 

1172 
assumes ex: "fs1 <~~> fs1'" "fs1' [\<sim>] fs2" 

1173 
shows "essentially_equal G fs1 fs2" 

1174 
using ex 

1175 
unfolding essentially_equal_def 

1176 
by fast 

1177 

1178 
lemma (in monoid) essentially_equalE: 

1179 
assumes ee: "essentially_equal G fs1 fs2" 

1180 
and e: "\<And>fs1'. \<lbrakk>fs1 <~~> fs1'; fs1' [\<sim>] fs2\<rbrakk> \<Longrightarrow> P" 

1181 
shows "P" 

1182 
using ee 

1183 
unfolding essentially_equal_def 

1184 
by (fast intro: e) 

1185 

1186 
lemma (in monoid) ee_refl [simp,intro]: 

1187 
assumes carr: "set as \<subseteq> carrier G" 

1188 
shows "essentially_equal G as as" 

1189 
using carr 

1190 
by (fast intro: essentially_equalI) 

1191 

1192 
lemma (in monoid) ee_sym [sym]: 

1193 
assumes ee: "essentially_equal G as bs" 

1194 
and carr: "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" 

1195 
shows "essentially_equal G bs as" 

1196 
using ee 

1197 
proof (elim essentially_equalE) 

1198 
fix fs 

1199 
assume "as <~~> fs" "fs [\<sim>] bs" 

1200 
hence "\<exists>fs'. as [\<sim>] fs' \<and> fs' <~~> bs" by (rule perm_assoc_switch_r) 

1201 
from this obtain fs' 

1202 
where a: "as [\<sim>] fs'" and p: "fs' <~~> bs" 

1203 
by auto 

1204 
from p have "bs <~~> fs'" by (rule perm_sym) 

1205 
with a[symmetric] carr 

1206 
show ?thesis 

1207 
by (iprover intro: essentially_equalI perm_closed) 

1208 
qed 

1209 

1210 
lemma (in monoid) ee_trans [trans]: 

1211 
assumes ab: "essentially_equal G as bs" and bc: "essentially_equal G bs cs" 

1212 
and ascarr: "set as \<subseteq> carrier G" 

1213 
and bscarr: "set bs \<subseteq> carrier G" 

1214 
and cscarr: "set cs \<subseteq> carrier G" 

1215 
shows "essentially_equal G as cs" 

1216 
using ab bc 

1217 
proof (elim essentially_equalE) 

1218 
fix abs bcs 

1219 
assume "abs [\<sim>] bs" and pb: "bs <~~> bcs" 

1220 
hence "\<exists>bs'. abs <~~> bs' \<and> bs' [\<sim>] bcs" by (rule perm_assoc_switch) 

1221 
from this obtain bs' 

1222 
where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs" 

1223 
by auto 

1224 

1225 
assume "as <~~> abs" 

1226 
with p 

1227 
have pp: "as <~~> bs'" by fast 

1228 

1229 
from pp ascarr have c1: "set bs' \<subseteq> carrier G" by (rule perm_closed) 

1230 
from pb bscarr have c2: "set bcs \<subseteq> carrier G" by (rule perm_closed) 

1231 
note a 

1232 
also assume "bcs [\<sim>] cs" 

1233 
finally (listassoc_trans) have"bs' [\<sim>] cs" by (simp add: c1 c2 cscarr) 

1234 

1235 
with pp 

1236 
show ?thesis 

1237 
by (rule essentially_equalI) 

1238 
qed 

1239 

1240 

1241 
subsubsection {* Properties of lists of elements *} 

1242 

1243 
text {* Multiplication of factors in a list *} 

1244 

1245 
lemma (in monoid) multlist_closed [simp, intro]: 

1246 
assumes ascarr: "set fs \<subseteq> carrier G" 

1247 
shows "foldr (op \<otimes>) fs \<one> \<in> carrier G" 

1248 
by (insert ascarr, induct fs, simp+) 

1249 

1250 
lemma (in comm_monoid) multlist_dividesI (*[intro]*): 

1251 
assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G" 

1252 
shows "f divides (foldr (op \<otimes>) fs \<one>)" 

1253 
using assms 

1254 
apply (induct fs) 

1255 
apply simp 

1256 
apply (case_tac "f = a", simp) 

1257 
apply (fast intro: dividesI) 

1258 
apply clarsimp 

1259 
apply (elim dividesE, intro dividesI) 

1260 
defer 1 

1261 
apply (simp add: m_comm) 

1262 
apply (simp add: m_assoc[symmetric]) 

1263 
apply (simp add: m_comm) 

1264 
apply simp 

1265 
done 

1266 

1267 
lemma (in comm_monoid_cancel) multlist_listassoc_cong: 

1268 
assumes "fs [\<sim>] fs'" 

1269 
and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" 

1270 
shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>" 

1271 
using assms 

1272 
proof (induct fs arbitrary: fs', simp) 

1273 
case (Cons a as fs') 

1274 
thus ?case 

1275 
apply (induct fs', simp) 

1276 
proof clarsimp 

1277 
fix b bs 

1278 
assume "a \<sim> b" 

1279 
and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" 

1280 
and ascarr: "set as \<subseteq> carrier G" 

1281 
hence p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>" 

1282 
by (fast intro: mult_cong_l) 

1283 
also 

1284 
assume "as [\<sim>] bs" 

1285 
and bscarr: "set bs \<subseteq> carrier G" 

1286 
and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>" 

1287 
hence "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp 

1288 
with ascarr bscarr bcarr 

1289 
have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" 

1290 
by (fast intro: mult_cong_r) 

1291 
finally 

1292 
show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>" 

1293 
by (simp add: ascarr bscarr acarr bcarr) 

1294 
qed 

1295 
qed 

1296 

1297 
lemma (in comm_monoid) multlist_perm_cong: 

1298 
assumes prm: "as <~~> bs" 

1299 
and ascarr: "set as \<subseteq> carrier G" 

1300 
shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>" 

1301 
using prm ascarr 

1302 
apply (induct, simp, clarsimp simp add: m_ac, clarsimp) 

1303 
proof clarsimp 

1304 
fix xs ys zs 

1305 
assume "xs <~~> ys" "set xs \<subseteq> carrier G" 

1306 
hence "set ys \<subseteq> carrier G" by (rule perm_closed) 

1307 
moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" 

1308 
ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp 

1309 
qed 

1310 

1311 
lemma (in comm_monoid_cancel) multlist_ee_cong: 

1312 
assumes "essentially_equal G fs fs'" 

1313 
and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G" 

1314 
shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>" 

1315 
using assms 

1316 
apply (elim essentially_equalE) 

1317 
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) 

1318 
done 

1319 

1320 

1321 
subsubsection {* Factorization in irreducible elements *} 

1322 

1323 
lemma wfactorsI: 

1324 
includes (struct G) 

1325 
assumes "\<forall>f\<in>set fs. irreducible G f" 

1326 
and "foldr (op \<otimes>) fs \<one> \<sim> a" 

1327 
shows "wfactors G fs a" 

1328 
using assms 

1329 
unfolding wfactors_def 

1330 
by simp 

1331 

1332 
lemma wfactorsE: 

1333 
includes (struct G) 

1334 
assumes wf: "wfactors G fs a" 

1335 
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P" 

1336 
shows "P" 

1337 
using wf 

1338 
unfolding wfactors_def 

1339 
by (fast dest: e) 

1340 

1341 
lemma (in monoid) factorsI: 

1342 
includes (struct G) 

1343 
assumes "\<forall>f\<in>set fs. irreducible G f" 

1344 
and "foldr (op \<otimes>) fs \<one> = a" 

1345 
shows "factors G fs a" 

1346 
using assms 

1347 
unfolding factors_def 

1348 
by simp 

1349 

1350 
lemma factorsE: 

1351 
includes (struct G) 

1352 
assumes f: "factors G fs a" 

1353 
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P" 

1354 
shows "P" 

1355 
using f 

1356 
unfolding factors_def 

1357 
by (simp add: e) 

1358 

1359 
lemma (in monoid) factors_wfactors: 

1360 
assumes "factors G as a" and "set as \<subseteq> carrier G" 

1361 
shows "wfactors G as a" 

1362 
using assms 

1363 
by (blast elim: factorsE intro: wfactorsI) 

1364 

1365 
lemma (in monoid) wfactors_factors: 

1366 
assumes "wfactors G as a" and "set as \<subseteq> carrier G" 

1367 
shows "\<exists>a'. factors G as a' \<and> a' \<sim> a" 

1368 
using assms 

1369 
by (blast elim: wfactorsE intro: factorsI) 

1370 

1371 
lemma (in monoid) factors_closed [dest]: 

1372 
assumes "factors G fs a" and "set fs \<subseteq> carrier G" 

1373 
shows "a \<in> carrier G" 

1374 
using assms 

1375 
by (elim factorsE, clarsimp) 

1376 

1377 
lemma (in monoid) nunit_factors: 

1378 
assumes anunit: "a \<notin> Units G" 

1379 
and fs: "factors G as a" 

1380 
shows "length as > 0" 

1381 
apply (insert fs, elim factorsE) 

1382 
proof (cases "length as = 0") 

1383 
assume "length as = 0" 

1384 
hence fold: "foldr op \<otimes> as \<one> = \<one>" by force 

1385 

1386 
assume "foldr op \<otimes> as \<one> = a" 

1387 
with fold 

1388 
have "a = \<one>" by simp 

1389 
then have "a \<in> Units G" by fast 

1390 
with anunit 

1391 
have "False" by simp 

1392 
thus ?thesis .. 

1393 
qed simp 

1394 

1395 
lemma (in monoid) unit_wfactors [simp]: 

1396 
assumes aunit: "a \<in> Units G" 

1397 
shows "wfactors G [] a" 

1398 
using aunit 

1399 
by (intro wfactorsI) (simp, simp add: Units_assoc) 

1400 

1401 
lemma (in comm_monoid_cancel) unit_wfactors_empty: 

1402 
assumes aunit: "a \<in> Units G" 

1403 
and wf: "wfactors G fs a" 

1404 
and carr[simp]: "set fs \<subseteq> carrier G" 

1405 
shows "fs = []" 

1406 
proof (rule ccontr, cases fs, simp) 

1407 
fix f fs' 

1408 
assume fs: "fs = f # fs'" 

1409 

1410 
from carr 

1411 
have fcarr[simp]: "f \<in> carrier G" 

1412 
and carr'[simp]: "set fs' \<subseteq> carrier G" 

1413 
by (simp add: fs)+ 

1414 

1415 
from fs wf 

1416 
have "irreducible G f" by (simp add: wfactors_def) 

1417 
hence fnunit: "f \<notin> Units G" by (fast elim: irreducibleE) 

1418 

1419 
from fs wf 

1420 
have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) 

1421 

1422 
note aunit 

1423 
also from fs wf 

1424 
have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def) 

1425 
have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>" 

1426 
by (simp add: Units_closed[OF aunit] a[symmetric]) 

1427 
finally 

1428 
have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp 

1429 
hence "f \<in> Units G" by (intro unit_factor[of f], simp+) 

1430 

1431 
with fnunit show "False" by simp 

1432 
qed 

1433 

1434 

1435 
text {* Comparing wfactors *} 

1436 

1437 
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l: 

1438 
assumes fact: "wfactors G fs a" 

1439 
and asc: "fs [\<sim>] fs'" 

1440 
and carr: "a \<in> carrier G" "set fs \<subseteq> carrier G" "set fs' \<subseteq> carrier G" 

1441 
shows "wfactors G fs' a" 

1442 
using fact 

1443 
apply (elim wfactorsE, intro wfactorsI) 

1444 
proof  

1445 
assume "\<forall>f\<in>set fs. irreducible G f" 

1446 
also note asc 

1447 
finally (irrlist_listassoc_cong) 

1448 
show "\<forall>f\<in>set fs'. irreducible G f" by (simp add: carr) 

1449 
next 

1450 
from asc[symmetric] 

1451 
have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>" 

1452 
by (simp add: multlist_listassoc_cong carr) 

1453 
also assume "foldr op \<otimes> fs \<one> \<sim> a" 

1454 
finally 

1455 
show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr) 

1456 
qed 

1457 

1458 
lemma (in comm_monoid) wfactors_perm_cong_l: 

1459 
assumes "wfactors G fs a" 

1460 
and "fs <~~> fs'" 

1461 
and "set fs \<subseteq> carrier G" 

1462 
shows "wfactors G fs' a" 

1463 
using assms 

1464 
apply (elim wfactorsE, intro wfactorsI) 

1465 
apply (rule irrlist_perm_cong, assumption+) 

1466 
apply (simp add: multlist_perm_cong[symmetric]) 

1467 
done 

1468 

1469 
lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]: 

1470 
assumes ee: "essentially_equal G as bs" 

1471 
and bfs: "wfactors G bs b" 

1472 
and carr: "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" 

1473 
shows "wfactors G as b" 

1474 
using ee 

1475 
proof (elim essentially_equalE) 

ed7a2e0fab59
New theory on divisibility.
ball 