summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/Divisibility.thy

author | haftmann |

Sun Jun 23 21:16:07 2013 +0200 (2013-06-23) | |

changeset 52435 | 6646bb548c6b |

parent 50037 | f2a32197a33a |

child 53374 | a14d2a854c02 |

permissions | -rw-r--r-- |

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

1 (* Title: HOL/Algebra/Divisibility.thy

2 Author: Clemens Ballarin

3 Author: Stephan Hohe

4 *)

6 header {* Divisibility in monoids and rings *}

8 theory Divisibility

9 imports "~~/src/HOL/Library/Permutation" Coset Group

10 begin

12 section {* Factorial Monoids *}

14 subsection {* Monoids with Cancellation Law *}

16 locale monoid_cancel = monoid +

17 assumes l_cancel:

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

19 and r_cancel:

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

22 lemma (in monoid) monoid_cancelI:

23 assumes l_cancel:

24 "\<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"

25 and r_cancel:

26 "\<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"

27 shows "monoid_cancel G"

28 by default fact+

30 lemma (in monoid_cancel) is_monoid_cancel:

31 "monoid_cancel G"

32 ..

34 sublocale group \<subseteq> monoid_cancel

35 by default simp_all

38 locale comm_monoid_cancel = monoid_cancel + comm_monoid

40 lemma comm_monoid_cancelI:

41 fixes G (structure)

42 assumes "comm_monoid G"

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

47 interpret comm_monoid G by fact

48 show "comm_monoid_cancel G"

49 by unfold_locales (metis assms(2) m_ac(2))+

50 qed

52 lemma (in comm_monoid_cancel) is_comm_monoid_cancel:

53 "comm_monoid_cancel G"

54 by intro_locales

56 sublocale comm_group \<subseteq> comm_monoid_cancel

57 ..

60 subsection {* Products of Units in Monoids *}

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

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

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

65 unfolding Units_def

66 using assms

67 by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)

69 lemma (in monoid) prod_unit_l:

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

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

72 shows "b \<in> Units G"

73 proof -

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

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

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

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

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

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

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

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

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

85 by (simp add: m_assoc del: Units_l_inv)

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

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

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

90 from c li ri

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

92 qed

94 lemma (in monoid) prod_unit_r:

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

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

97 shows "a \<in> Units G"

98 proof -

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

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

102 by (simp add: m_assoc del: Units_r_inv)

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

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

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

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

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

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

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

111 by (simp add: m_assoc del: Units_l_inv)

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

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

115 from c li ri

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

117 qed

119 lemma (in comm_monoid) unit_factor:

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

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

122 shows "a \<in> Units G"

123 using abunit[simplified Units_def]

124 proof clarsimp

125 fix i

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

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

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

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

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

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

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

135 also note li

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

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

139 also note ri

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

142 from carr' li' ri'

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

144 qed

147 subsection {* Divisibility and Association *}

149 subsubsection {* Function definitions *}

151 definition

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

153 where "a divides\<^bsub>G\<^esub> b \<longleftrightarrow> (\<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c)"

155 definition

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

157 where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"

159 abbreviation

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

162 definition

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

164 where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"

166 definition

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

168 where "irreducible G a \<longleftrightarrow> a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"

170 definition

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

172 "prime G p \<longleftrightarrow>

173 p \<notin> Units G \<and>

174 (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"

177 subsubsection {* Divisibility *}

179 lemma dividesI:

180 fixes G (structure)

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

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

183 shows "a divides b"

184 unfolding factor_def

185 using assms by fast

187 lemma dividesI' [intro]:

188 fixes G (structure)

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

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

191 shows "a divides b"

192 using assms

193 by (fast intro: dividesI)

195 lemma dividesD:

196 fixes G (structure)

197 assumes "a divides b"

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

199 using assms

200 unfolding factor_def

201 by fast

203 lemma dividesE [elim]:

204 fixes G (structure)

205 assumes d: "a divides b"

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

207 shows "P"

208 proof -

209 from dividesD[OF d]

210 obtain c

211 where "c\<in>carrier G"

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

213 by auto

214 thus "P" by (elim elim)

215 qed

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

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

219 shows "a divides a"

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

221 apply (simp, simp add: carr)

222 done

224 lemma (in monoid) divides_trans [trans]:

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

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

227 shows "a divides c"

228 using dvds[THEN dividesD]

229 by (blast intro: dividesI m_assoc acarr)

231 lemma (in monoid) divides_mult_lI [intro]:

232 assumes ab: "a divides b"

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

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

235 using ab

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

237 apply (fast intro: dividesI)

238 done

240 lemma (in monoid_cancel) divides_mult_l [simp]:

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

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

243 apply safe

244 apply (elim dividesE, intro dividesI, assumption)

245 apply (rule l_cancel[of c])

246 apply (simp add: m_assoc carr)+

247 apply (fast intro: carr)

248 done

250 lemma (in comm_monoid) divides_mult_rI [intro]:

251 assumes ab: "a divides b"

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

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

254 using carr ab

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

256 apply (rule divides_mult_lI, assumption+)

257 done

259 lemma (in comm_monoid_cancel) divides_mult_r [simp]:

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

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

262 using carr

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

265 lemma (in monoid) divides_prod_r:

266 assumes ab: "a divides b"

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

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

269 using ab carr

270 by (fast intro: m_assoc)

272 lemma (in comm_monoid) divides_prod_l:

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

274 and ab: "a divides b"

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

276 using ab carr

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

278 apply (fast intro: divides_prod_r)

279 done

281 lemma (in monoid) unit_divides:

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

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

284 shows "u divides a"

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

286 from uunit acarr

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

289 from uunit acarr

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

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

292 also from acarr

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

294 finally

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

296 qed

298 lemma (in comm_monoid) divides_unit:

299 assumes udvd: "a divides u"

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

301 shows "a \<in> Units G"

302 using udvd carr

303 by (blast intro: unit_factor)

305 lemma (in comm_monoid) Unit_eq_dividesone:

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

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

308 using ucarr

309 by (fast dest: divides_unit intro: unit_divides)

312 subsubsection {* Association *}

314 lemma associatedI:

315 fixes G (structure)

316 assumes "a divides b" "b divides a"

317 shows "a \<sim> b"

318 using assms

319 by (simp add: associated_def)

321 lemma (in monoid) associatedI2:

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

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

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

325 shows "a \<sim> b"

326 using uunit bcarr

327 unfolding a

328 apply (intro associatedI)

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

330 apply (simp add: m_assoc Units_closed Units_r_inv)

331 apply fast

332 done

334 lemma (in monoid) associatedI2':

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

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

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

338 shows "a \<sim> b"

339 using assms by (intro associatedI2)

341 lemma associatedD:

342 fixes G (structure)

343 assumes "a \<sim> b"

344 shows "a divides b"

345 using assms by (simp add: associated_def)

347 lemma (in monoid_cancel) associatedD2:

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

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

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

351 using assoc

352 unfolding associated_def

353 proof clarify

354 assume "b divides a"

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

356 from this obtain u

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

358 by auto

360 assume "a divides b"

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

362 from this obtain u'

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

364 by auto

365 note carr = carr ucarr u'carr

367 from carr

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

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

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

371 also from carr

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

373 finally

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

375 with carr

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

378 from carr

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

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

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

382 also from carr

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

384 finally

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

386 with carr

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

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

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

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

393 from ucarr this a

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

395 qed

397 lemma associatedE:

398 fixes G (structure)

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

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

401 shows "P"

402 proof -

403 from assoc

404 have "a divides b" "b divides a"

405 by (simp add: associated_def)+

406 thus "P" by (elim e)

407 qed

409 lemma (in monoid_cancel) associatedE2:

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

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

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

413 shows "P"

414 proof -

415 from assoc and carr

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

417 from this obtain u

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

419 by auto

420 thus "P" by (elim e)

421 qed

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

424 assumes "a \<in> carrier G"

425 shows "a \<sim> a"

426 using assms

427 by (fast intro: associatedI)

429 lemma (in monoid) associated_sym [sym]:

430 assumes "a \<sim> b"

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

432 shows "b \<sim> a"

433 using assms

434 by (iprover intro: associatedI elim: associatedE)

436 lemma (in monoid) associated_trans [trans]:

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

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

439 shows "a \<sim> c"

440 using assms

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

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

444 "equivalence (division_rel G)"

445 apply unfold_locales

446 apply simp_all

447 apply (metis associated_def)

448 apply (iprover intro: associated_trans)

449 done

452 subsubsection {* Division and associativity *}

454 lemma divides_antisym:

455 fixes G (structure)

456 assumes "a divides b" "b divides a"

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

458 shows "a \<sim> b"

459 using assms

460 by (fast intro: associatedI)

462 lemma (in monoid) divides_cong_l [trans]:

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

464 and xdvdy: "x' divides y"

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

466 shows "x divides y"

467 proof -

468 from xx'

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

470 also note xdvdy

471 finally

472 show "x divides y" by simp

473 qed

475 lemma (in monoid) divides_cong_r [trans]:

476 assumes xdvdy: "x divides y"

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

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

479 shows "x divides y'"

480 proof -

481 note xdvdy

482 also from yy'

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

484 finally

485 show "x divides y'" by simp

486 qed

488 lemma (in monoid) division_weak_partial_order [simp, intro!]:

489 "weak_partial_order (division_rel G)"

490 apply unfold_locales

491 apply simp_all

492 apply (simp add: associated_sym)

493 apply (blast intro: associated_trans)

494 apply (simp add: divides_antisym)

495 apply (blast intro: divides_trans)

496 apply (blast intro: divides_cong_l divides_cong_r associated_sym)

497 done

500 subsubsection {* Multiplication and associativity *}

502 lemma (in monoid_cancel) mult_cong_r:

503 assumes "b \<sim> b'"

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

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

506 using assms

507 apply (elim associatedE2, intro associatedI2)

508 apply (auto intro: m_assoc[symmetric])

509 done

511 lemma (in comm_monoid_cancel) mult_cong_l:

512 assumes "a \<sim> a'"

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

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

515 using assms

516 apply (elim associatedE2, intro associatedI2)

517 apply assumption

518 apply (simp add: m_assoc Units_closed)

519 apply (simp add: m_comm Units_closed)

520 apply simp+

521 done

523 lemma (in monoid_cancel) assoc_l_cancel:

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

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

526 shows "b \<sim> b'"

527 using assms

528 apply (elim associatedE2, intro associatedI2)

529 apply assumption

530 apply (rule l_cancel[of a])

531 apply (simp add: m_assoc Units_closed)

532 apply fast+

533 done

535 lemma (in comm_monoid_cancel) assoc_r_cancel:

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

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

538 shows "a \<sim> a'"

539 using assms

540 apply (elim associatedE2, intro associatedI2)

541 apply assumption

542 apply (rule r_cancel[of a b])

543 apply (metis Units_closed assms(3) assms(4) m_ac)

544 apply fast+

545 done

548 subsubsection {* Units *}

550 lemma (in monoid_cancel) assoc_unit_l [trans]:

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

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

553 shows "a \<in> Units G"

554 using assms

555 by (fast elim: associatedE2)

557 lemma (in monoid_cancel) assoc_unit_r [trans]:

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

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

560 shows "b \<in> Units G"

561 using aunit bcarr associated_sym[OF asc]

562 by (blast intro: assoc_unit_l)

564 lemma (in comm_monoid) Units_cong:

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

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

567 shows "b \<in> Units G"

568 using assms

569 by (blast intro: divides_unit elim: associatedE)

571 lemma (in monoid) Units_assoc:

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

573 shows "a \<sim> b"

574 using units

575 by (fast intro: associatedI unit_divides)

577 lemma (in monoid) Units_are_ones:

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

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

580 proof clarsimp

581 fix a

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

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

584 apply (rule associatedI)

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

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

587 done

588 next

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

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

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

592 qed

594 lemma (in comm_monoid) Units_Lower:

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

596 apply (simp add: Units_def Lower_def)

597 apply (rule, rule)

598 apply clarsimp

599 apply (rule unit_divides)

600 apply (unfold Units_def, fast)

601 apply assumption

602 apply clarsimp

603 apply (metis Unit_eq_dividesone Units_r_inv_ex m_ac(2) one_closed)

604 done

607 subsubsection {* Proper factors *}

609 lemma properfactorI:

610 fixes G (structure)

611 assumes "a divides b"

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

613 shows "properfactor G a b"

614 using assms

615 unfolding properfactor_def

616 by simp

618 lemma properfactorI2:

619 fixes G (structure)

620 assumes advdb: "a divides b"

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

622 shows "properfactor G a b"

623 apply (rule properfactorI, rule advdb)

624 proof (rule ccontr, simp)

625 assume "b divides a"

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

627 with neq show "False" by fast

628 qed

630 lemma (in comm_monoid_cancel) properfactorI3:

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

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

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

634 shows "properfactor G a p"

635 unfolding p

636 using carr

637 apply (intro properfactorI, fast)

638 proof (clarsimp, elim dividesE)

639 fix c

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

641 note [simp] = carr ccarr

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

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

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

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

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

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

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

652 from ccarr linv[symmetric] rinv[symmetric]

653 have "b \<in> Units G" unfolding Units_def by fastforce

654 with nunit

655 show "False" ..

656 qed

658 lemma properfactorE:

659 fixes G (structure)

660 assumes pf: "properfactor G a b"

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

662 shows "P"

663 using pf

664 unfolding properfactor_def

665 by (fast intro: r)

667 lemma properfactorE2:

668 fixes G (structure)

669 assumes pf: "properfactor G a b"

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

671 shows "P"

672 using pf

673 unfolding properfactor_def

674 by (fast elim: elim associatedE)

676 lemma (in monoid) properfactor_unitE:

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

678 and pf: "properfactor G a u"

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

680 shows "P"

681 using pf unit_divides[OF uunit acarr]

682 by (fast elim: properfactorE)

685 lemma (in monoid) properfactor_divides:

686 assumes pf: "properfactor G a b"

687 shows "a divides b"

688 using pf

689 by (elim properfactorE)

691 lemma (in monoid) properfactor_trans1 [trans]:

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

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

694 shows "properfactor G a c"

695 using dvds carr

696 apply (elim properfactorE, intro properfactorI)

697 apply (iprover intro: divides_trans)+

698 done

700 lemma (in monoid) properfactor_trans2 [trans]:

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

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

703 shows "properfactor G a c"

704 using dvds carr

705 apply (elim properfactorE, intro properfactorI)

706 apply (iprover intro: divides_trans)+

707 done

709 lemma properfactor_lless:

710 fixes G (structure)

711 shows "properfactor G = lless (division_rel G)"

712 apply (rule ext) apply (rule ext) apply rule

713 apply (fastforce elim: properfactorE2 intro: weak_llessI)

714 apply (fastforce elim: weak_llessE intro: properfactorI2)

715 done

717 lemma (in monoid) properfactor_cong_l [trans]:

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

719 and pf: "properfactor G x y"

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

721 shows "properfactor G x' y"

722 using pf

723 unfolding properfactor_lless

724 proof -

725 interpret weak_partial_order "division_rel G" ..

726 from x'x

727 have "x' .=\<^bsub>division_rel G\<^esub> x" by simp

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

729 finally

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

731 qed

733 lemma (in monoid) properfactor_cong_r [trans]:

734 assumes pf: "properfactor G x y"

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

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

737 shows "properfactor G x y'"

738 using pf

739 unfolding properfactor_lless

740 proof -

741 interpret weak_partial_order "division_rel G" ..

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

743 also from yy'

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

745 finally

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

747 qed

749 lemma (in monoid_cancel) properfactor_mult_lI [intro]:

750 assumes ab: "properfactor G a b"

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

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

753 using ab carr

754 by (fastforce elim: properfactorE intro: properfactorI)

756 lemma (in monoid_cancel) properfactor_mult_l [simp]:

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

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

759 using carr

760 by (fastforce elim: properfactorE intro: properfactorI)

762 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:

763 assumes ab: "properfactor G a b"

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

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

766 using ab carr

767 by (fastforce elim: properfactorE intro: properfactorI)

769 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:

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

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

772 using carr

773 by (fastforce elim: properfactorE intro: properfactorI)

775 lemma (in monoid) properfactor_prod_r:

776 assumes ab: "properfactor G a b"

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

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

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

781 lemma (in comm_monoid) properfactor_prod_l:

782 assumes ab: "properfactor G a b"

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

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

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

788 subsection {* Irreducible Elements and Primes *}

790 subsubsection {* Irreducible elements *}

792 lemma irreducibleI:

793 fixes G (structure)

794 assumes "a \<notin> Units G"

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

796 shows "irreducible G a"

797 using assms

798 unfolding irreducible_def

799 by blast

801 lemma irreducibleE:

802 fixes G (structure)

803 assumes irr: "irreducible G a"

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

805 shows "P"

806 using assms

807 unfolding irreducible_def

808 by blast

810 lemma irreducibleD:

811 fixes G (structure)

812 assumes irr: "irreducible G a"

813 and pf: "properfactor G b a"

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

815 shows "b \<in> Units G"

816 using assms

817 by (fast elim: irreducibleE)

819 lemma (in monoid_cancel) irreducible_cong [trans]:

820 assumes irred: "irreducible G a"

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

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

823 shows "irreducible G a'"

824 using assms

825 apply (elim irreducibleE, intro irreducibleI)

826 apply simp_all

827 apply (metis assms(2) assms(3) assoc_unit_l)

828 apply (metis assms(2) assms(3) assms(4) associated_sym properfactor_cong_r)

829 done

831 lemma (in monoid) irreducible_prod_rI:

832 assumes airr: "irreducible G a"

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

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

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

836 using airr carr bunit

837 apply (elim irreducibleE, intro irreducibleI, clarify)

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

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

840 apply (metis assms associatedI2 m_closed properfactor_cong_r)

841 done

843 lemma (in comm_monoid) irreducible_prod_lI:

844 assumes birr: "irreducible G b"

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

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

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

848 apply (subst m_comm, simp+)

849 apply (intro irreducible_prod_rI assms)

850 done

852 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:

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

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

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

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

857 shows "P"

858 using irr

859 proof (elim irreducibleE)

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

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

863 show "P"

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

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

866 have "irreducible G b"

867 apply (rule irreducibleI)

868 proof (rule ccontr, simp)

869 assume "b \<in> Units G"

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

871 with abnunit show "False" ..

872 next

873 fix c

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

875 and "properfactor G c b"

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

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

878 qed

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

881 next

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

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

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

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

887 have "irreducible G a"

888 apply (rule irreducibleI)

889 proof (rule ccontr, simp)

890 assume "a \<in> Units G"

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

892 with abnunit show "False" ..

893 next

894 fix c

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

896 and "properfactor G c a"

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

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

899 qed

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

902 qed

903 qed

906 subsubsection {* Prime elements *}

908 lemma primeI:

909 fixes G (structure)

910 assumes "p \<notin> Units G"

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

912 shows "prime G p"

913 using assms

914 unfolding prime_def

915 by blast

917 lemma primeE:

918 fixes G (structure)

919 assumes pprime: "prime G p"

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

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

922 shows "P"

923 using pprime

924 unfolding prime_def

925 by (blast dest: e)

927 lemma (in comm_monoid_cancel) prime_divides:

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

929 and pprime: "prime G p"

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

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

932 using assms

933 by (blast elim: primeE)

935 lemma (in monoid_cancel) prime_cong [trans]:

936 assumes pprime: "prime G p"

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

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

939 shows "prime G p'"

940 using pprime

941 apply (elim primeE, intro primeI)

942 apply (metis assms(2) assms(3) assoc_unit_l)

943 apply (metis assms(2) assms(3) assms(4) associated_sym divides_cong_l m_closed)

944 done

946 subsection {* Factorization and Factorial Monoids *}

948 subsubsection {* Function definitions *}

950 definition

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

952 where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"

954 definition

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

956 where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"

958 abbreviation

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

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

962 definition

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

964 where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"

967 locale factorial_monoid = comm_monoid_cancel +

968 assumes factors_exist:

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

970 and factors_unique:

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

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

975 subsubsection {* Comparing lists of elements *}

977 text {* Association on lists *}

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

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

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

982 using assms

983 by (induct as) simp+

985 lemma (in monoid) listassoc_sym [sym]:

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

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

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

989 using assms

990 proof (induct as arbitrary: bs, simp)

991 case Cons

992 thus ?case

993 apply (induct bs, simp)

994 apply clarsimp

995 apply (iprover intro: associated_sym)

996 done

997 qed

999 lemma (in monoid) listassoc_trans [trans]:

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

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

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

1003 using assms

1004 apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)

1005 apply (rule associated_trans)

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

1007 apply (simp, simp)

1008 apply blast+

1009 done

1011 lemma (in monoid_cancel) irrlist_listassoc_cong:

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

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

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

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

1016 using assms

1017 apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)

1018 apply (blast intro: irreducible_cong)

1019 done

1022 text {* Permutations *}

1024 lemma perm_map [intro]:

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

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

1027 using p

1028 by induct auto

1030 lemma perm_map_switch:

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

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

1033 using p m

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

1036 lemma (in monoid) perm_assoc_switch:

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

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

1039 using p a

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

1041 apply (clarsimp simp add: list_all2_Cons2, blast)

1042 apply (clarsimp simp add: list_all2_Cons2)

1043 apply blast

1044 apply blast

1045 done

1047 lemma (in monoid) perm_assoc_switch_r:

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

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

1050 using p a

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

1052 apply (clarsimp simp add: list_all2_Cons1, blast)

1053 apply (clarsimp simp add: list_all2_Cons1)

1054 apply blast

1055 apply blast

1056 done

1058 declare perm_sym [sym]

1060 lemma perm_setP:

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

1062 and as: "P (set as)"

1063 shows "P (set bs)"

1064 proof -

1065 from perm

1066 have "multiset_of as = multiset_of bs"

1067 by (simp add: multiset_of_eq_perm)

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

1069 with as

1070 show "P (set bs)" by simp

1071 qed

1073 lemmas (in monoid) perm_closed =

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

1076 lemmas (in monoid) irrlist_perm_cong =

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

1080 text {* Essentially equal factorizations *}

1082 lemma (in monoid) essentially_equalI:

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

1084 shows "essentially_equal G fs1 fs2"

1085 using ex

1086 unfolding essentially_equal_def

1087 by fast

1089 lemma (in monoid) essentially_equalE:

1090 assumes ee: "essentially_equal G fs1 fs2"

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

1092 shows "P"

1093 using ee

1094 unfolding essentially_equal_def

1095 by (fast intro: e)

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

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

1099 shows "essentially_equal G as as"

1100 using carr

1101 by (fast intro: essentially_equalI)

1103 lemma (in monoid) ee_sym [sym]:

1104 assumes ee: "essentially_equal G as bs"

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

1106 shows "essentially_equal G bs as"

1107 using ee

1108 proof (elim essentially_equalE)

1109 fix fs

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

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

1112 from this obtain fs'

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

1114 by auto

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

1116 with a[symmetric] carr

1117 show ?thesis

1118 by (iprover intro: essentially_equalI perm_closed)

1119 qed

1121 lemma (in monoid) ee_trans [trans]:

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

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

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

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

1126 shows "essentially_equal G as cs"

1127 using ab bc

1128 proof (elim essentially_equalE)

1129 fix abs bcs

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

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

1132 from this obtain bs'

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

1134 by auto

1136 assume "as <~~> abs"

1137 with p

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

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

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

1142 note a

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

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

1146 with pp

1147 show ?thesis

1148 by (rule essentially_equalI)

1149 qed

1152 subsubsection {* Properties of lists of elements *}

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

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

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

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

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

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

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

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

1164 using assms

1165 apply (induct fs)

1166 apply simp

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

1168 apply (fast intro: dividesI)

1169 apply clarsimp

1170 apply (metis assms(2) divides_prod_l multlist_closed)

1171 done

1173 lemma (in comm_monoid_cancel) multlist_listassoc_cong:

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

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

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

1177 using assms

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

1179 case (Cons a as fs')

1180 thus ?case

1181 apply (induct fs', simp)

1182 proof clarsimp

1183 fix b bs

1184 assume "a \<sim> b"

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

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

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

1188 by (fast intro: mult_cong_l)

1189 also

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

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

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

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

1194 with ascarr bscarr bcarr

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

1196 by (fast intro: mult_cong_r)

1197 finally

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

1199 by (simp add: ascarr bscarr acarr bcarr)

1200 qed

1201 qed

1203 lemma (in comm_monoid) multlist_perm_cong:

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

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

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

1207 using prm ascarr

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

1209 proof clarsimp

1210 fix xs ys zs

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

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

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

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

1215 qed

1217 lemma (in comm_monoid_cancel) multlist_ee_cong:

1218 assumes "essentially_equal G fs fs'"

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

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

1221 using assms

1222 apply (elim essentially_equalE)

1223 apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)

1224 done

1227 subsubsection {* Factorization in irreducible elements *}

1229 lemma wfactorsI:

1230 fixes G (structure)

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

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

1233 shows "wfactors G fs a"

1234 using assms

1235 unfolding wfactors_def

1236 by simp

1238 lemma wfactorsE:

1239 fixes G (structure)

1240 assumes wf: "wfactors G fs a"

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

1242 shows "P"

1243 using wf

1244 unfolding wfactors_def

1245 by (fast dest: e)

1247 lemma (in monoid) factorsI:

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

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

1250 shows "factors G fs a"

1251 using assms

1252 unfolding factors_def

1253 by simp

1255 lemma factorsE:

1256 fixes G (structure)

1257 assumes f: "factors G fs a"

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

1259 shows "P"

1260 using f

1261 unfolding factors_def

1262 by (simp add: e)

1264 lemma (in monoid) factors_wfactors:

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

1266 shows "wfactors G as a"

1267 using assms

1268 by (blast elim: factorsE intro: wfactorsI)

1270 lemma (in monoid) wfactors_factors:

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

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

1273 using assms

1274 by (blast elim: wfactorsE intro: factorsI)

1276 lemma (in monoid) factors_closed [dest]:

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

1278 shows "a \<in> carrier G"

1279 using assms

1280 by (elim factorsE, clarsimp)

1282 lemma (in monoid) nunit_factors:

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

1284 and fs: "factors G as a"

1285 shows "length as > 0"

1286 proof -

1287 from anunit Units_one_closed have "a \<noteq> \<one>" by auto

1288 with fs show ?thesis by (auto elim: factorsE)

1289 qed

1291 lemma (in monoid) unit_wfactors [simp]:

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

1293 shows "wfactors G [] a"

1294 using aunit

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

1297 lemma (in comm_monoid_cancel) unit_wfactors_empty:

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

1299 and wf: "wfactors G fs a"

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

1301 shows "fs = []"

1302 proof (rule ccontr, cases fs, simp)

1303 fix f fs'

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

1306 from carr

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

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

1309 by (simp add: fs)+

1311 from fs wf

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

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

1315 from fs wf

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

1318 note aunit

1319 also from fs wf

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

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

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

1323 finally

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

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

1327 with fnunit show "False" by simp

1328 qed

1331 text {* Comparing wfactors *}

1333 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:

1334 assumes fact: "wfactors G fs a"

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

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

1337 shows "wfactors G fs' a"

1338 using fact

1339 apply (elim wfactorsE, intro wfactorsI)

1340 apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)

1341 proof -

1342 from asc[symmetric]

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

1344 by (simp add: multlist_listassoc_cong carr)

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

1346 finally

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

1348 qed

1350 lemma (in comm_monoid) wfactors_perm_cong_l:

1351 assumes "wfactors G fs a"

1352 and "fs <~~> fs'"

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

1354 shows "wfactors G fs' a"

1355 using assms

1356 apply (elim wfactorsE, intro wfactorsI)

1357 apply (rule irrlist_perm_cong, assumption+)

1358 apply (simp add: multlist_perm_cong[symmetric])

1359 done

1361 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:

1362 assumes ee: "essentially_equal G as bs"

1363 and bfs: "wfactors G bs b"

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

1365 shows "wfactors G as b"

1366 using ee

1367 proof (elim essentially_equalE)

1368 fix fs

1369 assume prm: "as <~~> fs"

1370 with carr

1371 have fscarr: "set fs \<subseteq> carrier G" by (simp add: perm_closed)

1373 note bfs

1374 also assume [symmetric]: "fs [\<sim>] bs"

1375 also (wfactors_listassoc_cong_l)

1376 note prm[symmetric]

1377 finally (wfactors_perm_cong_l)

1378 show "wfactors G as b" by (simp add: carr fscarr)

1379 qed

1381 lemma (in monoid) wfactors_cong_r [trans]:

1382 assumes fac: "wfactors G fs a" and aa': "a \<sim> a'"

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

1384 shows "wfactors G fs a'"

1385 using fac

1386 proof (elim wfactorsE, intro wfactorsI)

1387 assume "foldr op \<otimes> fs \<one> \<sim> a" also note aa'

1388 finally show "foldr op \<otimes> fs \<one> \<sim> a'" by simp

1389 qed

1392 subsubsection {* Essentially equal factorizations *}

1394 lemma (in comm_monoid_cancel) unitfactor_ee:

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

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

1397 shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as" (is "essentially_equal G ?as' as")

1398 using assms

1399 apply (intro essentially_equalI[of _ ?as'], simp)

1400 apply (cases as, simp)

1401 apply (clarsimp, fast intro: associatedI2[of u])

1402 done

1404 lemma (in comm_monoid_cancel) factors_cong_unit:

1405 assumes uunit: "u \<in> Units G" and anunit: "a \<notin> Units G"

1406 and afs: "factors G as a"

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

1408 shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)" (is "factors G ?as' ?a'")

1409 using assms

1410 apply (elim factorsE, clarify)

1411 apply (cases as)

1412 apply (simp add: nunit_factors)

1413 apply clarsimp

1414 apply (elim factorsE, intro factorsI)

1415 apply (clarsimp, fast intro: irreducible_prod_rI)

1416 apply (simp add: m_ac Units_closed)

1417 done

1419 lemma (in comm_monoid) perm_wfactorsD:

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

1421 and afs: "wfactors G as a" and bfs: "wfactors G bs b"

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

1423 and ascarr[simp]: "set as \<subseteq> carrier G"

1424 shows "a \<sim> b"

1425 using afs bfs

1426 proof (elim wfactorsE)

1427 from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)

1428 assume "foldr op \<otimes> as \<one> \<sim> a"

1429 hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)

1430 also from prm

1431 have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp)

1432 also assume "foldr op \<otimes> bs \<one> \<sim> b"

1433 finally

1434 show "a \<sim> b" by simp

1435 qed

1437 lemma (in comm_monoid_cancel) listassoc_wfactorsD:

1438 assumes assoc: "as [\<sim>] bs"

1439 and afs: "wfactors G as a" and bfs: "wfactors G bs b"

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

1441 and [simp]: "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G"

1442 shows "a \<sim> b"

1443 using afs bfs

1444 proof (elim wfactorsE)

1445 assume "foldr op \<otimes> as \<one> \<sim> a"

1446 hence "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)

1447 also from assoc

1448 have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+)

1449 also assume "foldr op \<otimes> bs \<one> \<sim> b"

1450 finally

1451 show "a \<sim> b" by simp

1452 qed

1454 lemma (in comm_monoid_cancel) ee_wfactorsD:

1455 assumes ee: "essentially_equal G as bs"

1456 and afs: "wfactors G as a" and bfs: "wfactors G bs b"

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

1458 and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"

1459 shows "a \<sim> b"

1460 using ee

1461 proof (elim essentially_equalE)

1462 fix fs

1463 assume prm: "as <~~> fs"

1464 hence as'carr[simp]: "set fs \<subseteq> carrier G" by (simp add: perm_closed)

1465 from afs prm

1466 have afs': "wfactors G fs a" by (rule wfactors_perm_cong_l, simp)

1467 assume "fs [\<sim>] bs"

1468 from this afs' bfs

1469 show "a \<sim> b" by (rule listassoc_wfactorsD, simp+)

1470 qed

1472 lemma (in comm_monoid_cancel) ee_factorsD:

1473 assumes ee: "essentially_equal G as bs"

1474 and afs: "factors G as a" and bfs:"factors G bs b"

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

1476 shows "a \<sim> b"

1477 using assms

1478 by (blast intro: factors_wfactors dest: ee_wfactorsD)

1480 lemma (in factorial_monoid) ee_factorsI:

1481 assumes ab: "a \<sim> b"

1482 and afs: "factors G as a" and anunit: "a \<notin> Units G"

1483 and bfs: "factors G bs b" and bnunit: "b \<notin> Units G"

1484 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"

1485 shows "essentially_equal G as bs"

1486 proof -

1487 note carr[simp] = factors_closed[OF afs ascarr] ascarr[THEN subsetD]

1488 factors_closed[OF bfs bscarr] bscarr[THEN subsetD]

1490 from ab carr

1491 have "\<exists>u\<in>Units G. a = b \<otimes> u" by (fast elim: associatedE2)

1492 from this obtain u

1493 where uunit: "u \<in> Units G"

1494 and a: "a = b \<otimes> u" by auto

1496 from uunit bscarr

1497 have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs"

1498 (is "essentially_equal G ?bs' bs")

1499 by (rule unitfactor_ee)

1501 from bscarr uunit

1502 have bs'carr: "set ?bs' \<subseteq> carrier G"

1503 by (cases bs) (simp add: Units_closed)+

1505 from uunit bnunit bfs bscarr

1506 have fac: "factors G ?bs' (b \<otimes> u)"

1507 by (rule factors_cong_unit)

1509 from afs fac[simplified a[symmetric]] ascarr bs'carr anunit

1510 have "essentially_equal G as ?bs'"

1511 by (blast intro: factors_unique)

1512 also note ee

1513 finally

1514 show "essentially_equal G as bs" by (simp add: ascarr bscarr bs'carr)

1515 qed

1517 lemma (in factorial_monoid) ee_wfactorsI:

1518 assumes asc: "a \<sim> b"

1519 and asf: "wfactors G as a" and bsf: "wfactors G bs b"

1520 and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"

1521 and ascarr[simp]: "set as \<subseteq> carrier G" and bscarr[simp]: "set bs \<subseteq> carrier G"

1522 shows "essentially_equal G as bs"

1523 using assms

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

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

1526 also note asc

1527 finally have bunit: "b \<in> Units G" by simp

1529 from aunit asf ascarr

1530 have e: "as = []" by (rule unit_wfactors_empty)

1531 from bunit bsf bscarr

1532 have e': "bs = []" by (rule unit_wfactors_empty)

1534 have "essentially_equal G [] []"

1535 by (fast intro: essentially_equalI)

1536 thus ?thesis by (simp add: e e')

1537 next

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

1539 have bnunit: "b \<notin> Units G"

1540 proof clarify

1541 assume "b \<in> Units G"

1542 also note asc[symmetric]

1543 finally have "a \<in> Units G" by simp

1544 with anunit

1545 show "False" ..

1546 qed

1548 have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors[OF asf ascarr])

1549 from this obtain a'

1550 where fa': "factors G as a'"

1551 and a': "a' \<sim> a"

1552 by auto

1553 from fa' ascarr

1554 have a'carr[simp]: "a' \<in> carrier G" by fast

1556 have a'nunit: "a' \<notin> Units G"

1557 proof (clarify)

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

1559 also note a'

1560 finally have "a \<in> Units G" by simp

1561 with anunit

1562 show "False" ..

1563 qed

1565 have "\<exists>b'. factors G bs b' \<and> b' \<sim> b" by (rule wfactors_factors[OF bsf bscarr])

1566 from this obtain b'

1567 where fb': "factors G bs b'"

1568 and b': "b' \<sim> b"

1569 by auto

1570 from fb' bscarr

1571 have b'carr[simp]: "b' \<in> carrier G" by fast

1573 have b'nunit: "b' \<notin> Units G"

1574 proof (clarify)

1575 assume "b' \<in> Units G"

1576 also note b'

1577 finally have "b \<in> Units G" by simp

1578 with bnunit

1579 show "False" ..

1580 qed

1582 note a'

1583 also note asc

1584 also note b'[symmetric]

1585 finally

1586 have "a' \<sim> b'" by simp

1588 from this fa' a'nunit fb' b'nunit ascarr bscarr

1589 show "essentially_equal G as bs"

1590 by (rule ee_factorsI)

1591 qed

1593 lemma (in factorial_monoid) ee_wfactors:

1594 assumes asf: "wfactors G as a"

1595 and bsf: "wfactors G bs b"

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

1597 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"

1598 shows asc: "a \<sim> b = essentially_equal G as bs"

1599 using assms

1600 by (fast intro: ee_wfactorsI ee_wfactorsD)

1602 lemma (in factorial_monoid) wfactors_exist [intro, simp]:

1603 assumes acarr[simp]: "a \<in> carrier G"

1604 shows "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"

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

1606 assume "a \<in> Units G"

1607 hence "wfactors G [] a" by (rule unit_wfactors)

1608 thus ?thesis by (intro exI) force

1609 next

1610 assume "a \<notin> Units G"

1611 hence "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (intro factors_exist acarr)

1612 from this obtain fs

1613 where fscarr: "set fs \<subseteq> carrier G"

1614 and f: "factors G fs a"

1615 by auto

1616 from f have "wfactors G fs a" by (rule factors_wfactors) fact

1617 from fscarr this

1618 show ?thesis by fast

1619 qed

1621 lemma (in monoid) wfactors_prod_exists [intro, simp]:

1622 assumes "\<forall>a \<in> set as. irreducible G a" and "set as \<subseteq> carrier G"

1623 shows "\<exists>a. a \<in> carrier G \<and> wfactors G as a"

1624 unfolding wfactors_def

1625 using assms

1626 by blast

1628 lemma (in factorial_monoid) wfactors_unique:

1629 assumes "wfactors G fs a" and "wfactors G fs' a"

1630 and "a \<in> carrier G"

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

1632 shows "essentially_equal G fs fs'"

1633 using assms

1634 by (fast intro: ee_wfactorsI[of a a])

1636 lemma (in monoid) factors_mult_single:

1637 assumes "irreducible G a" and "factors G fb b" and "a \<in> carrier G"

1638 shows "factors G (a # fb) (a \<otimes> b)"

1639 using assms

1640 unfolding factors_def

1641 by simp

1643 lemma (in monoid_cancel) wfactors_mult_single:

1644 assumes f: "irreducible G a" "wfactors G fb b"

1645 "a \<in> carrier G" "b \<in> carrier G" "set fb \<subseteq> carrier G"

1646 shows "wfactors G (a # fb) (a \<otimes> b)"

1647 using assms

1648 unfolding wfactors_def

1649 by (simp add: mult_cong_r)

1651 lemma (in monoid) factors_mult:

1652 assumes factors: "factors G fa a" "factors G fb b"

1653 and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G"

1654 shows "factors G (fa @ fb) (a \<otimes> b)"

1655 using assms

1656 unfolding factors_def

1657 apply (safe, force)

1658 apply (induct fa)

1659 apply simp

1660 apply (simp add: m_assoc)

1661 done

1663 lemma (in comm_monoid_cancel) wfactors_mult [intro]:

1664 assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"

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

1666 and ascarr: "set as \<subseteq> carrier G" and bscarr:"set bs \<subseteq> carrier G"

1667 shows "wfactors G (as @ bs) (a \<otimes> b)"

1668 apply (insert wfactors_factors[OF asf ascarr])

1669 apply (insert wfactors_factors[OF bsf bscarr])

1670 proof (clarsimp)

1671 fix a' b'

1672 assume asf': "factors G as a'" and a'a: "a' \<sim> a"

1673 and bsf': "factors G bs b'" and b'b: "b' \<sim> b"

1674 from asf' have a'carr: "a' \<in> carrier G" by (rule factors_closed) fact

1675 from bsf' have b'carr: "b' \<in> carrier G" by (rule factors_closed) fact

1677 note carr = acarr bcarr a'carr b'carr ascarr bscarr

1679 from asf' bsf'

1680 have "factors G (as @ bs) (a' \<otimes> b')" by (rule factors_mult) fact+

1682 with carr

1683 have abf': "wfactors G (as @ bs) (a' \<otimes> b')" by (intro factors_wfactors) simp+

1684 also from b'b carr

1685 have trb: "a' \<otimes> b' \<sim> a' \<otimes> b" by (intro mult_cong_r)

1686 also from a'a carr

1687 have tra: "a' \<otimes> b \<sim> a \<otimes> b" by (intro mult_cong_l)

1688 finally

1689 show "wfactors G (as @ bs) (a \<otimes> b)"

1690 by (simp add: carr)

1691 qed

1693 lemma (in comm_monoid) factors_dividesI:

1694 assumes "factors G fs a" and "f \<in> set fs"

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

1696 shows "f divides a"

1697 using assms

1698 by (fast elim: factorsE intro: multlist_dividesI)

1700 lemma (in comm_monoid) wfactors_dividesI:

1701 assumes p: "wfactors G fs a"

1702 and fscarr: "set fs \<subseteq> carrier G" and acarr: "a \<in> carrier G"

1703 and f: "f \<in> set fs"

1704 shows "f divides a"

1705 apply (insert wfactors_factors[OF p fscarr], clarsimp)

1706 proof -

1707 fix a'

1708 assume fsa': "factors G fs a'"

1709 and a'a: "a' \<sim> a"

1710 with fscarr

1711 have a'carr: "a' \<in> carrier G" by (simp add: factors_closed)

1713 from fsa' fscarr f

1714 have "f divides a'" by (fast intro: factors_dividesI)

1715 also note a'a

1716 finally

1717 show "f divides a" by (simp add: f fscarr[THEN subsetD] acarr a'carr)

1718 qed

1721 subsubsection {* Factorial monoids and wfactors *}

1723 lemma (in comm_monoid_cancel) factorial_monoidI:

1724 assumes wfactors_exists:

1725 "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"

1726 and wfactors_unique:

1727 "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G;

1728 wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"

1729 shows "factorial_monoid G"

1730 proof

1731 fix a

1732 assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"

1734 from wfactors_exists[OF acarr]

1735 obtain as

1736 where ascarr: "set as \<subseteq> carrier G"

1737 and afs: "wfactors G as a"

1738 by auto

1739 from afs ascarr

1740 have "\<exists>a'. factors G as a' \<and> a' \<sim> a" by (rule wfactors_factors)

1741 from this obtain a'

1742 where afs': "factors G as a'"

1743 and a'a: "a' \<sim> a"

1744 by auto

1745 from afs' ascarr

1746 have a'carr: "a' \<in> carrier G" by fast

1747 have a'nunit: "a' \<notin> Units G"

1748 proof clarify

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

1750 also note a'a

1751 finally have "a \<in> Units G" by (simp add: acarr)

1752 with anunit

1753 show "False" ..

1754 qed

1756 from a'carr acarr a'a

1757 have "\<exists>u. u \<in> Units G \<and> a' = a \<otimes> u" by (blast elim: associatedE2)

1758 from this obtain u

1759 where uunit: "u \<in> Units G"

1760 and a': "a' = a \<otimes> u"

1761 by auto

1763 note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]

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

1766 also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)

1767 also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])

1768 finally

1769 have a: "a = a' \<otimes> inv u" .

1771 from ascarr uunit

1772 have cr: "set (as[0:=(as!0 \<otimes> inv u)]) \<subseteq> carrier G"

1773 by (cases as, clarsimp+)

1775 from afs' uunit a'nunit acarr ascarr

1776 have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"

1777 by (simp add: a factors_cong_unit)

1779 with cr

1780 show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by fast

1781 qed (blast intro: factors_wfactors wfactors_unique)

1784 subsection {* Factorizations as Multisets *}

1786 text {* Gives useful operations like intersection *}

1788 (* FIXME: use class_of x instead of closure_of {x} *)

1790 abbreviation

1791 "assocs G x == eq_closure_of (division_rel G) {x}"

1793 definition

1794 "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"

1797 text {* Helper lemmas *}

1799 lemma (in monoid) assocs_repr_independence:

1800 assumes "y \<in> assocs G x"

1801 and "x \<in> carrier G"

1802 shows "assocs G x = assocs G y"

1803 using assms

1804 apply safe

1805 apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])

1806 apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)

1807 apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])

1808 apply (clarsimp, iprover intro: associated_trans, simp+)

1809 done

1811 lemma (in monoid) assocs_self:

1812 assumes "x \<in> carrier G"

1813 shows "x \<in> assocs G x"

1814 using assms

1815 by (fastforce intro: closure_ofI2)

1817 lemma (in monoid) assocs_repr_independenceD:

1818 assumes repr: "assocs G x = assocs G y"

1819 and ycarr: "y \<in> carrier G"

1820 shows "y \<in> assocs G x"

1821 unfolding repr

1822 using ycarr

1823 by (intro assocs_self)

1825 lemma (in comm_monoid) assocs_assoc:

1826 assumes "a \<in> assocs G b"

1827 and "b \<in> carrier G"

1828 shows "a \<sim> b"

1829 using assms

1830 by (elim closure_ofE2, simp)

1832 lemmas (in comm_monoid) assocs_eqD =

1833 assocs_repr_independenceD[THEN assocs_assoc]

1836 subsubsection {* Comparing multisets *}

1838 lemma (in monoid) fmset_perm_cong:

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

1840 shows "fmset G as = fmset G bs"

1841 using perm_map[OF prm]

1842 by (simp add: multiset_of_eq_perm fmset_def)

1844 lemma (in comm_monoid_cancel) eqc_listassoc_cong:

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

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

1847 shows "map (assocs G) as = map (assocs G) bs"

1848 using assms

1849 apply (induct as arbitrary: bs, simp)

1850 apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)

1851 apply (clarsimp elim!: closure_ofE2) defer 1

1852 apply (clarsimp elim!: closure_ofE2) defer 1

1853 proof -

1854 fix a x z

1855 assume carr[simp]: "a \<in> carrier G" "x \<in> carrier G" "z \<in> carrier G"

1856 assume "x \<sim> a"

1857 also assume "a \<sim> z"

1858 finally have "x \<sim> z" by simp

1859 with carr

1860 show "x \<in> assocs G z"

1861 by (intro closure_ofI2) simp+

1862 next

1863 fix a x z

1864 assume carr[simp]: "a \<in> carrier G" "x \<in> carrier G" "z \<in> carrier G"

1865 assume "x \<sim> z"

1866 also assume [symmetric]: "a \<sim> z"

1867 finally have "x \<sim> a" by simp

1868 with carr

1869 show "x \<in> assocs G a"

1870 by (intro closure_ofI2) simp+

1871 qed

1873 lemma (in comm_monoid_cancel) fmset_listassoc_cong:

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

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

1876 shows "fmset G as = fmset G bs"

1877 using assms

1878 unfolding fmset_def

1879 by (simp add: eqc_listassoc_cong)

1881 lemma (in comm_monoid_cancel) ee_fmset:

1882 assumes ee: "essentially_equal G as bs"

1883 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"

1884 shows "fmset G as = fmset G bs"

1885 using ee

1886 proof (elim essentially_equalE)

1887 fix as'

1888 assume prm: "as <~~> as'"

1889 from prm ascarr

1890 have as'carr: "set as' \<subseteq> carrier G" by (rule perm_closed)

1892 from prm

1893 have "fmset G as = fmset G as'" by (rule fmset_perm_cong)

1894 also assume "as' [\<sim>] bs"

1895 with as'carr bscarr

1896 have "fmset G as' = fmset G bs" by (simp add: fmset_listassoc_cong)

1897 finally

1898 show "fmset G as = fmset G bs" .

1899 qed

1901 lemma (in monoid_cancel) fmset_ee__hlp_induct:

1902 assumes prm: "cas <~~> cbs"

1903 and cdef: "cas = map (assocs G) as" "cbs = map (assocs G) bs"

1904 shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and>

1905 cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"

1906 apply (rule perm.induct[of cas cbs], rule prm)

1907 apply safe apply simp_all

1908 apply (simp add: map_eq_Cons_conv, blast)

1909 apply force

1910 proof -

1911 fix ys as bs

1912 assume p1: "map (assocs G) as <~~> ys"

1913 and r1[rule_format]:

1914 "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and>

1915 ys = map (assocs G) bs

1916 \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)"

1917 and p2: "ys <~~> map (assocs G) bs"

1918 and r2[rule_format]:

1919 "\<forall>as bsa. ys = map (assocs G) as \<and>

1920 map (assocs G) bs = map (assocs G) bsa

1921 \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)"

1922 and p3: "map (assocs G) as <~~> map (assocs G) bs"

1924 from p1

1925 have "multiset_of (map (assocs G) as) = multiset_of ys"

1926 by (simp add: multiset_of_eq_perm)

1927 hence setys: "set (map (assocs G) as) = set ys" by (rule multiset_of_eq_setD)

1929 have "set (map (assocs G) as) = { assocs G x | x. x \<in> set as}" by clarsimp fast

1930 with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp

1931 hence "\<exists>yy. ys = map (assocs G) yy"

1932 apply (induct ys, simp, clarsimp)

1933 proof -

1934 fix yy x

1935 show "\<exists>yya. (assocs G x) # map (assocs G) yy =

1936 map (assocs G) yya"

1937 by (rule exI[of _ "x#yy"], simp)

1938 qed

1939 from this obtain yy

1940 where ys: "ys = map (assocs G) yy"

1941 by auto

1943 from p1 ys

1944 have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"

1945 by (intro r1, simp)

1946 from this obtain as'

1947 where asas': "as <~~> as'"

1948 and as'yy: "map (assocs G) as' = map (assocs G) yy"

1949 by auto

1951 from p2 ys

1952 have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"

1953 by (intro r2, simp)

1954 from this obtain as''

1955 where yyas'': "yy <~~> as''"

1956 and as''bs: "map (assocs G) as'' = map (assocs G) bs"

1957 by auto

1959 from as'yy and yyas''

1960 have "\<exists>cs. as' <~~> cs \<and> map (assocs G) cs = map (assocs G) as''"

1961 by (rule perm_map_switch)

1962 from this obtain cs

1963 where as'cs: "as' <~~> cs"

1964 and csas'': "map (assocs G) cs = map (assocs G) as''"

1965 by auto

1967 from asas' and as'cs

1968 have ascs: "as <~~> cs" by fast

1969 from csas'' and as''bs

1970 have "map (assocs G) cs = map (assocs G) bs" by simp

1971 from ascs and this

1972 show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs" by fast

1973 qed

1975 lemma (in comm_monoid_cancel) fmset_ee:

1976 assumes mset: "fmset G as = fmset G bs"

1977 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"

1978 shows "essentially_equal G as bs"

1979 proof -

1980 from mset

1981 have mpp: "map (assocs G) as <~~> map (assocs G) bs"

1982 by (simp add: fmset_def multiset_of_eq_perm)

1984 have "\<exists>cas. cas = map (assocs G) as" by simp

1985 from this obtain cas where cas: "cas = map (assocs G) as" by simp

1987 have "\<exists>cbs. cbs = map (assocs G) bs" by simp

1988 from this obtain cbs where cbs: "cbs = map (assocs G) bs" by simp

1990 from cas cbs mpp

1991 have [rule_format]:

1992 "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and>

1993 cbs = map (assocs G) bs)

1994 \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"

1995 by (intro fmset_ee__hlp_induct, simp+)

1996 with mpp cas cbs

1997 have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"

1998 by simp

2000 from this obtain as'

2001 where tp: "as <~~> as'"

2002 and tm: "map (assocs G) as' = map (assocs G) bs"

2003 by auto

2004 from tm have lene: "length as' = length bs" by (rule map_eq_imp_length_eq)

2005 from tp have "set as = set as'" by (simp add: multiset_of_eq_perm multiset_of_eq_setD)

2006 with ascarr

2007 have as'carr: "set as' \<subseteq> carrier G" by simp

2009 from tm as'carr[THEN subsetD] bscarr[THEN subsetD]

2010 have "as' [\<sim>] bs"

2011 by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])

2013 from tp and this

2014 show "essentially_equal G as bs" by (fast intro: essentially_equalI)

2015 qed

2017 lemma (in comm_monoid_cancel) ee_is_fmset:

2018 assumes "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"

2019 shows "essentially_equal G as bs = (fmset G as = fmset G bs)"

2020 using assms

2021 by (fast intro: ee_fmset fmset_ee)

2024 subsubsection {* Interpreting multisets as factorizations *}

2026 lemma (in monoid) mset_fmsetEx:

2027 assumes elems: "\<And>X. X \<in> set_of Cs \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"

2028 shows "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> fmset G cs = Cs"

2029 proof -

2030 have "\<exists>Cs'. Cs = multiset_of Cs'"

2031 by (rule surjE[OF surj_multiset_of], fast)

2032 from this obtain Cs'

2033 where Cs: "Cs = multiset_of Cs'"

2034 by auto

2036 have "\<exists>cs. (\<forall>c \<in> set cs. P c) \<and> multiset_of (map (assocs G) cs) = Cs"

2037 using elems

2038 unfolding Cs

2039 apply (induct Cs', simp)

2040 apply clarsimp

2041 apply (subgoal_tac "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>

2042 multiset_of (map (assocs G) cs) = multiset_of Cs'")

2043 proof clarsimp

2044 fix a Cs' cs

2045 assume ih: "\<And>X. X = a \<or> X \<in> set Cs' \<Longrightarrow> \<exists>x. P x \<and> X = assocs G x"

2046 and csP: "\<forall>x\<in>set cs. P x"

2047 and mset: "multiset_of (map (assocs G) cs) = multiset_of Cs'"

2048 from ih

2049 have "\<exists>x. P x \<and> a = assocs G x" by fast

2050 from this obtain c

2051 where cP: "P c"

2052 and a: "a = assocs G c"

2053 by auto

2054 from cP csP

2055 have tP: "\<forall>x\<in>set (c#cs). P x" by simp

2056 from mset a

2057 have "multiset_of (map (assocs G) (c#cs)) = multiset_of Cs' + {#a#}" by simp

2058 from tP this

2059 show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>

2060 multiset_of (map (assocs G) cs) =

2061 multiset_of Cs' + {#a#}" by fast

2062 qed simp

2063 thus ?thesis by (simp add: fmset_def)

2064 qed

2066 lemma (in monoid) mset_wfactorsEx:

2067 assumes elems: "\<And>X. X \<in> set_of Cs

2068 \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2069 shows "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = Cs"

2070 proof -

2071 have "\<exists>cs. (\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c) \<and> fmset G cs = Cs"

2072 by (intro mset_fmsetEx, rule elems)

2073 from this obtain cs

2074 where p[rule_format]: "\<forall>c\<in>set cs. c \<in> carrier G \<and> irreducible G c"

2075 and Cs[symmetric]: "fmset G cs = Cs"

2076 by auto

2078 from p

2079 have cscarr: "set cs \<subseteq> carrier G" by fast

2081 from p

2082 have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"

2083 by (intro wfactors_prod_exists) fast+

2084 from this obtain c

2085 where ccarr: "c \<in> carrier G"

2086 and cfs: "wfactors G cs c"

2087 by auto

2089 with cscarr Cs

2090 show ?thesis by fast

2091 qed

2094 subsubsection {* Multiplication on multisets *}

2096 lemma (in factorial_monoid) mult_wfactors_fmset:

2097 assumes afs: "wfactors G as a" and bfs: "wfactors G bs b" and cfs: "wfactors G cs (a \<otimes> b)"

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

2099 "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G"

2100 shows "fmset G cs = fmset G as + fmset G bs"

2101 proof -

2102 from assms

2103 have "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)

2104 with carr cfs

2105 have "essentially_equal G cs (as@bs)" by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"], simp+)

2106 with carr

2107 have "fmset G cs = fmset G (as@bs)" by (intro ee_fmset, simp+)

2108 also have "fmset G (as@bs) = fmset G as + fmset G bs" by (simp add: fmset_def)

2109 finally show "fmset G cs = fmset G as + fmset G bs" .

2110 qed

2112 lemma (in factorial_monoid) mult_factors_fmset:

2113 assumes afs: "factors G as a" and bfs: "factors G bs b" and cfs: "factors G cs (a \<otimes> b)"

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

2115 shows "fmset G cs = fmset G as + fmset G bs"

2116 using assms

2117 by (blast intro: factors_wfactors mult_wfactors_fmset)

2119 lemma (in comm_monoid_cancel) fmset_wfactors_mult:

2120 assumes mset: "fmset G cs = fmset G as + fmset G bs"

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

2122 "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" "set cs \<subseteq> carrier G"

2123 and fs: "wfactors G as a" "wfactors G bs b" "wfactors G cs c"

2124 shows "c \<sim> a \<otimes> b"

2125 proof -

2126 from carr fs

2127 have m: "wfactors G (as @ bs) (a \<otimes> b)" by (intro wfactors_mult)

2129 from mset

2130 have "fmset G cs = fmset G (as@bs)" by (simp add: fmset_def)

2131 then have "essentially_equal G cs (as@bs)" by (rule fmset_ee) (simp add: carr)+

2132 then show "c \<sim> a \<otimes> b" by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp add: assms m)+

2133 qed

2136 subsubsection {* Divisibility on multisets *}

2138 lemma (in factorial_monoid) divides_fmsubset:

2139 assumes ab: "a divides b"

2140 and afs: "wfactors G as a" and bfs: "wfactors G bs b"

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

2142 shows "fmset G as \<le> fmset G bs"

2143 using ab

2144 proof (elim dividesE)

2145 fix c

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

2147 hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by (rule wfactors_exist)

2148 from this obtain cs

2149 where cscarr: "set cs \<subseteq> carrier G"

2150 and cfs: "wfactors G cs c" by auto

2151 note carr = carr ccarr cscarr

2153 assume "b = a \<otimes> c"

2154 with afs bfs cfs carr

2155 have "fmset G bs = fmset G as + fmset G cs"

2156 by (intro mult_wfactors_fmset[OF afs cfs]) simp+

2158 thus ?thesis by simp

2159 qed

2161 lemma (in comm_monoid_cancel) fmsubset_divides:

2162 assumes msubset: "fmset G as \<le> fmset G bs"

2163 and afs: "wfactors G as a" and bfs: "wfactors G bs b"

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

2165 and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"

2166 shows "a divides b"

2167 proof -

2168 from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)

2169 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)

2171 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = fmset G bs - fmset G as"

2172 proof (intro mset_wfactorsEx, simp)

2173 fix X

2174 assume "count (fmset G as) X < count (fmset G bs) X"

2175 hence "0 < count (fmset G bs) X" by simp

2176 hence "X \<in> set_of (fmset G bs)" by simp

2177 hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)

2178 hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto

2179 from this obtain x

2180 where xbs: "x \<in> set bs"

2181 and X: "X = assocs G x"

2182 by auto

2184 with bscarr have xcarr: "x \<in> carrier G" by fast

2185 from xbs birr have xirr: "irreducible G x" by simp

2187 from xcarr and xirr and X

2188 show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x" by fast

2189 qed

2190 from this obtain c cs

2191 where ccarr: "c \<in> carrier G"

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

2193 and csf: "wfactors G cs c"

2194 and csmset: "fmset G cs = fmset G bs - fmset G as" by auto

2196 from csmset msubset

2197 have "fmset G bs = fmset G as + fmset G cs"

2198 by (simp add: multiset_eq_iff mset_le_def)

2199 hence basc: "b \<sim> a \<otimes> c"

2200 by (rule fmset_wfactors_mult) fact+

2202 thus ?thesis

2203 proof (elim associatedE2)

2204 fix u

2205 assume "u \<in> Units G" "b = a \<otimes> c \<otimes> u"

2206 with acarr ccarr

2207 show "a divides b" by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)

2208 qed (simp add: acarr bcarr ccarr)+

2209 qed

2211 lemma (in factorial_monoid) divides_as_fmsubset:

2212 assumes "wfactors G as a" and "wfactors G bs b"

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

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

2215 shows "a divides b = (fmset G as \<le> fmset G bs)"

2216 using assms

2217 by (blast intro: divides_fmsubset fmsubset_divides)

2220 text {* Proper factors on multisets *}

2222 lemma (in factorial_monoid) fmset_properfactor:

2223 assumes asubb: "fmset G as \<le> fmset G bs"

2224 and anb: "fmset G as \<noteq> fmset G bs"

2225 and "wfactors G as a" and "wfactors G bs b"

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

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

2228 shows "properfactor G a b"

2229 apply (rule properfactorI)

2230 apply (rule fmsubset_divides[of as bs], fact+)

2231 proof

2232 assume "b divides a"

2233 hence "fmset G bs \<le> fmset G as"

2234 by (rule divides_fmsubset) fact+

2235 with asubb

2236 have "fmset G as = fmset G bs" by (rule order_antisym)

2237 with anb

2238 show "False" ..

2239 qed

2241 lemma (in factorial_monoid) properfactor_fmset:

2242 assumes pf: "properfactor G a b"

2243 and "wfactors G as a" and "wfactors G bs b"

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

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

2246 shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"

2247 using pf

2248 apply (elim properfactorE)

2249 apply rule

2250 apply (intro divides_fmsubset, assumption)

2251 apply (rule assms)+

2252 apply (metis assms divides_fmsubset fmsubset_divides)

2253 done

2255 subsection {* Irreducible Elements are Prime *}

2257 lemma (in factorial_monoid) irreducible_is_prime:

2258 assumes pirr: "irreducible G p"

2259 and pcarr: "p \<in> carrier G"

2260 shows "prime G p"

2261 using pirr

2262 proof (elim irreducibleE, intro primeI)

2263 fix a b

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

2265 and pdvdab: "p divides (a \<otimes> b)"

2266 and pnunit: "p \<notin> Units G"

2267 assume irreduc[rule_format]:

2268 "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"

2269 from pdvdab

2270 have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)

2271 from this obtain c

2272 where ccarr: "c \<in> carrier G"

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

2274 by auto

2276 from acarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a" by (rule wfactors_exist)

2277 from this obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a" by auto

2279 from bcarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs b" by (rule wfactors_exist)

2280 from this obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b" by auto

2282 from ccarr have "\<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs c" by (rule wfactors_exist)

2283 from this obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c" by auto

2285 note carr[simp] = pcarr acarr bcarr ccarr ascarr bscarr cscarr

2287 from afs and bfs

2288 have abfs: "wfactors G (as @ bs) (a \<otimes> b)" by (rule wfactors_mult) fact+

2290 from pirr cfs

2291 have pcfs: "wfactors G (p # cs) (p \<otimes> c)" by (rule wfactors_mult_single) fact+

2292 with abpc

2293 have abfs': "wfactors G (p # cs) (a \<otimes> b)" by simp

2295 from abfs' abfs

2296 have "essentially_equal G (p # cs) (as @ bs)"

2297 by (rule wfactors_unique) simp+

2299 hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"

2300 by (fast elim: essentially_equalE)

2301 from this obtain ds

2302 where "p # cs <~~> ds"

2303 and dsassoc: "ds [\<sim>] (as @ bs)"

2304 by auto

2306 then have "p \<in> set ds"

2307 by (simp add: perm_set_eq[symmetric])

2308 with dsassoc

2309 have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"

2310 unfolding list_all2_conv_all_nth set_conv_nth

2311 by force

2313 from this obtain p'

2314 where "p' \<in> set (as@bs)"

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

2316 by auto

2318 hence "p' \<in> set as \<or> p' \<in> set bs" by simp

2319 moreover

2320 {

2321 assume p'elem: "p' \<in> set as"

2322 with ascarr have [simp]: "p' \<in> carrier G" by fast

2324 note pp'

2325 also from afs

2326 have "p' divides a" by (rule wfactors_dividesI) fact+

2327 finally

2328 have "p divides a" by simp

2329 }

2330 moreover

2331 {

2332 assume p'elem: "p' \<in> set bs"

2333 with bscarr have [simp]: "p' \<in> carrier G" by fast

2335 note pp'

2336 also from bfs

2337 have "p' divides b" by (rule wfactors_dividesI) fact+

2338 finally

2339 have "p divides b" by simp

2340 }

2341 ultimately

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

2343 qed

2346 --"A version using @{const factors}, more complicated"

2347 lemma (in factorial_monoid) factors_irreducible_is_prime:

2348 assumes pirr: "irreducible G p"

2349 and pcarr: "p \<in> carrier G"

2350 shows "prime G p"

2351 using pirr

2352 apply (elim irreducibleE, intro primeI)

2353 apply assumption

2354 proof -

2355 fix a b

2356 assume acarr: "a \<in> carrier G"

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

2358 and pdvdab: "p divides (a \<otimes> b)"

2359 assume irreduc[rule_format]:

2360 "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"

2361 from pdvdab

2362 have "\<exists>c\<in>carrier G. a \<otimes> b = p \<otimes> c" by (rule dividesD)

2363 from this obtain c

2364 where ccarr: "c \<in> carrier G"

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

2366 by auto

2367 note [simp] = pcarr acarr bcarr ccarr

2369 show "p divides a \<or> p divides b"

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

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

2373 note pdvdab

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

2375 also from aunit

2376 have bab: "b \<otimes> a \<sim> b"

2377 by (intro associatedI2[of "a"], simp+)

2378 finally

2379 have "p divides b" by simp

2380 thus "p divides a \<or> p divides b" ..

2381 next

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

2384 show "p divides a \<or> p divides b"

2385 proof (cases "b \<in> Units G")

2386 assume bunit: "b \<in> Units G"

2388 note pdvdab

2389 also from bunit

2390 have baa: "a \<otimes> b \<sim> a"

2391 by (intro associatedI2[of "b"], simp+)

2392 finally

2393 have "p divides a" by simp

2394 thus "p divides a \<or> p divides b" ..

2395 next

2396 assume bnunit: "b \<notin> Units G"

2398 have cnunit: "c \<notin> Units G"

2399 proof (rule ccontr, simp)

2400 assume cunit: "c \<in> Units G"

2401 from bnunit

2402 have "properfactor G a (a \<otimes> b)"

2403 by (intro properfactorI3[of _ _ b], simp+)

2404 also note abpc

2405 also from cunit

2406 have "p \<otimes> c \<sim> p"

2407 by (intro associatedI2[of c], simp+)

2408 finally

2409 have "properfactor G a p" by simp

2411 with acarr

2412 have "a \<in> Units G" by (fast intro: irreduc)

2413 with anunit

2414 show "False" ..

2415 qed

2417 have abnunit: "a \<otimes> b \<notin> Units G"

2418 proof clarsimp

2419 assume abunit: "a \<otimes> b \<in> Units G"

2420 hence "a \<in> Units G" by (rule unit_factor) fact+

2421 with anunit

2422 show "False" ..

2423 qed

2425 from acarr anunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a" by (rule factors_exist)

2426 then obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a" by auto

2428 from bcarr bnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs b" by (rule factors_exist)

2429 then obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b" by auto

2431 from ccarr cnunit have "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs c" by (rule factors_exist)

2432 then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c" by auto

2434 note [simp] = ascarr bscarr cscarr

2436 from afac and bfac

2437 have abfac: "factors G (as @ bs) (a \<otimes> b)" by (rule factors_mult) fact+

2439 from pirr cfac

2440 have pcfac: "factors G (p # cs) (p \<otimes> c)" by (rule factors_mult_single) fact+

2441 with abpc

2442 have abfac': "factors G (p # cs) (a \<otimes> b)" by simp

2444 from abfac' abfac

2445 have "essentially_equal G (p # cs) (as @ bs)"

2446 by (rule factors_unique) (fact | simp)+

2448 hence "\<exists>ds. p # cs <~~> ds \<and> ds [\<sim>] (as @ bs)"

2449 by (fast elim: essentially_equalE)

2450 from this obtain ds

2451 where "p # cs <~~> ds"

2452 and dsassoc: "ds [\<sim>] (as @ bs)"

2453 by auto

2455 then have "p \<in> set ds"

2456 by (simp add: perm_set_eq[symmetric])

2457 with dsassoc

2458 have "\<exists>p'. p' \<in> set (as@bs) \<and> p \<sim> p'"

2459 unfolding list_all2_conv_all_nth set_conv_nth

2460 by force

2462 from this obtain p'

2463 where "p' \<in> set (as@bs)"

2464 and pp': "p \<sim> p'" by auto

2466 hence "p' \<in> set as \<or> p' \<in> set bs" by simp

2467 moreover

2468 {

2469 assume p'elem: "p' \<in> set as"

2470 with ascarr have [simp]: "p' \<in> carrier G" by fast

2472 note pp'

2473 also from afac p'elem

2474 have "p' divides a" by (rule factors_dividesI) fact+

2475 finally

2476 have "p divides a" by simp

2477 }

2478 moreover

2479 {

2480 assume p'elem: "p' \<in> set bs"

2481 with bscarr have [simp]: "p' \<in> carrier G" by fast

2483 note pp'

2484 also from bfac

2485 have "p' divides b" by (rule factors_dividesI) fact+

2486 finally have "p divides b" by simp

2487 }

2488 ultimately

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

2490 qed

2491 qed

2492 qed

2495 subsection {* Greatest Common Divisors and Lowest Common Multiples *}

2497 subsubsection {* Definitions *}

2499 definition

2500 isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)

2501 where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>

2502 (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"

2504 definition

2505 islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)

2506 where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>

2507 (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"

2509 definition

2510 somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2511 where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"

2513 definition

2514 somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2515 where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"

2517 definition

2518 "SomeGcd G A = inf (division_rel G) A"

2521 locale gcd_condition_monoid = comm_monoid_cancel +

2522 assumes gcdof_exists:

2523 "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"

2525 locale primeness_condition_monoid = comm_monoid_cancel +

2526 assumes irreducible_prime:

2527 "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"

2529 locale divisor_chain_condition_monoid = comm_monoid_cancel +

2530 assumes division_wellfounded:

2531 "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"

2534 subsubsection {* Connections to \texttt{Lattice.thy} *}

2536 lemma gcdof_greatestLower:

2537 fixes G (structure)

2538 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2539 shows "(x \<in> carrier G \<and> x gcdof a b) =

2540 greatest (division_rel G) x (Lower (division_rel G) {a, b})"

2541 unfolding isgcd_def greatest_def Lower_def elem_def

2542 by auto

2544 lemma lcmof_leastUpper:

2545 fixes G (structure)

2546 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2547 shows "(x \<in> carrier G \<and> x lcmof a b) =

2548 least (division_rel G) x (Upper (division_rel G) {a, b})"

2549 unfolding islcm_def least_def Upper_def elem_def

2550 by auto

2552 lemma somegcd_meet:

2553 fixes G (structure)

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

2555 shows "somegcd G a b = meet (division_rel G) a b"

2556 unfolding somegcd_def meet_def inf_def

2557 by (simp add: gcdof_greatestLower[OF carr])

2559 lemma (in monoid) isgcd_divides_l:

2560 assumes "a divides b"

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

2562 shows "a gcdof a b"

2563 using assms

2564 unfolding isgcd_def

2565 by fast

2567 lemma (in monoid) isgcd_divides_r:

2568 assumes "b divides a"

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

2570 shows "b gcdof a b"

2571 using assms

2572 unfolding isgcd_def

2573 by fast

2576 subsubsection {* Existence of gcd and lcm *}

2578 lemma (in factorial_monoid) gcdof_exists:

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

2580 shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2581 proof -

2582 from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)

2583 from this obtain as

2584 where ascarr: "set as \<subseteq> carrier G"

2585 and afs: "wfactors G as a"

2586 by auto

2587 from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)

2589 from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)

2590 from this obtain bs

2591 where bscarr: "set bs \<subseteq> carrier G"

2592 and bfs: "wfactors G bs b"

2593 by auto

2594 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)

2596 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2597 fmset G cs = fmset G as #\<inter> fmset G bs"

2598 proof (intro mset_wfactorsEx)

2599 fix X

2600 assume "X \<in> set_of (fmset G as #\<inter> fmset G bs)"

2601 hence "X \<in> set_of (fmset G as)" by (simp add: multiset_inter_def)

2602 hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)

2603 hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto

2604 from this obtain x

2605 where X: "X = assocs G x"

2606 and xas: "x \<in> set as"

2607 by auto

2608 with ascarr have xcarr: "x \<in> carrier G" by fast

2609 from xas airr have xirr: "irreducible G x" by simp

2611 from xcarr and xirr and X

2612 show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast

2613 qed

2615 from this obtain c cs

2616 where ccarr: "c \<in> carrier G"

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

2618 and csirr: "wfactors G cs c"

2619 and csmset: "fmset G cs = fmset G as #\<inter> fmset G bs" by auto

2621 have "c gcdof a b"

2622 proof (simp add: isgcd_def, safe)

2623 from csmset

2624 have "fmset G cs \<le> fmset G as"

2625 by (simp add: multiset_inter_def mset_le_def)

2626 thus "c divides a" by (rule fmsubset_divides) fact+

2627 next

2628 from csmset

2629 have "fmset G cs \<le> fmset G bs"

2630 by (simp add: multiset_inter_def mset_le_def, force)

2631 thus "c divides b" by (rule fmsubset_divides) fact+

2632 next

2633 fix y

2634 assume ycarr: "y \<in> carrier G"

2635 hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)

2636 from this obtain ys

2637 where yscarr: "set ys \<subseteq> carrier G"

2638 and yfs: "wfactors G ys y"

2639 by auto

2641 assume "y divides a"

2642 hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+

2644 assume "y divides b"

2645 hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+

2647 from ya yb csmset

2648 have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)

2649 thus "y divides c" by (rule fmsubset_divides) fact+

2650 qed

2652 with ccarr

2653 show "\<exists>c. c \<in> carrier G \<and> c gcdof a b" by fast

2654 qed

2656 lemma (in factorial_monoid) lcmof_exists:

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

2658 shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2659 proof -

2660 from acarr have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (rule wfactors_exist)

2661 from this obtain as

2662 where ascarr: "set as \<subseteq> carrier G"

2663 and afs: "wfactors G as a"

2664 by auto

2665 from afs have airr: "\<forall>a \<in> set as. irreducible G a" by (fast elim: wfactorsE)

2667 from bcarr have "\<exists>bs. set bs \<subseteq> carrier G \<and> wfactors G bs b" by (rule wfactors_exist)

2668 from this obtain bs

2669 where bscarr: "set bs \<subseteq> carrier G"

2670 and bfs: "wfactors G bs b"

2671 by auto

2672 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b" by (fast elim: wfactorsE)

2674 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2675 fmset G cs = (fmset G as - fmset G bs) + fmset G bs"

2676 proof (intro mset_wfactorsEx)

2677 fix X

2678 assume "X \<in> set_of ((fmset G as - fmset G bs) + fmset G bs)"

2679 hence "X \<in> set_of (fmset G as) \<or> X \<in> set_of (fmset G bs)"

2680 by (cases "X :# fmset G bs", simp, simp)

2681 moreover

2682 {

2683 assume "X \<in> set_of (fmset G as)"

2684 hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)

2685 hence "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto

2686 from this obtain x

2687 where xas: "x \<in> set as"

2688 and X: "X = assocs G x" by auto

2690 with ascarr have xcarr: "x \<in> carrier G" by fast

2691 from xas airr have xirr: "irreducible G x" by simp

2693 from xcarr and xirr and X

2694 have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast

2695 }

2696 moreover

2697 {

2698 assume "X \<in> set_of (fmset G bs)"

2699 hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)

2700 hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto

2701 from this obtain x

2702 where xbs: "x \<in> set bs"

2703 and X: "X = assocs G x" by auto

2705 with bscarr have xcarr: "x \<in> carrier G" by fast

2706 from xbs birr have xirr: "irreducible G x" by simp

2708 from xcarr and xirr and X

2709 have "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast

2710 }

2711 ultimately

2712 show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x" by fast

2713 qed

2715 from this obtain c cs

2716 where ccarr: "c \<in> carrier G"

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

2718 and csirr: "wfactors G cs c"

2719 and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs" by auto

2721 have "c lcmof a b"

2722 proof (simp add: islcm_def, safe)

2723 from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)

2724 thus "a divides c" by (rule fmsubset_divides) fact+

2725 next

2726 from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)

2727 thus "b divides c" by (rule fmsubset_divides) fact+

2728 next

2729 fix y

2730 assume ycarr: "y \<in> carrier G"

2731 hence "\<exists>ys. set ys \<subseteq> carrier G \<and> wfactors G ys y" by (rule wfactors_exist)

2732 from this obtain ys

2733 where yscarr: "set ys \<subseteq> carrier G"

2734 and yfs: "wfactors G ys y"

2735 by auto

2737 assume "a divides y"

2738 hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+

2740 assume "b divides y"

2741 hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+

2743 from ya yb csmset

2744 have "fmset G cs \<le> fmset G ys"

2745 apply (simp add: mset_le_def, clarify)

2746 apply (case_tac "count (fmset G as) a < count (fmset G bs) a")

2747 apply simp

2748 apply simp

2749 done

2750 thus "c divides y" by (rule fmsubset_divides) fact+

2751 qed

2753 with ccarr

2754 show "\<exists>c. c \<in> carrier G \<and> c lcmof a b" by fast

2755 qed

2758 subsection {* Conditions for Factoriality *}

2760 subsubsection {* Gcd condition *}

2762 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:

2763 shows "weak_lower_semilattice (division_rel G)"

2764 proof -

2765 interpret weak_partial_order "division_rel G" ..

2766 show ?thesis

2767 apply (unfold_locales, simp_all)

2768 proof -

2769 fix x y

2770 assume carr: "x \<in> carrier G" "y \<in> carrier G"

2771 hence "\<exists>z. z \<in> carrier G \<and> z gcdof x y" by (rule gcdof_exists)

2772 from this obtain z

2773 where zcarr: "z \<in> carrier G"

2774 and isgcd: "z gcdof x y"

2775 by auto

2776 with carr

2777 have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2778 by (subst gcdof_greatestLower[symmetric], simp+)

2779 thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast

2780 qed

2781 qed

2783 lemma (in gcd_condition_monoid) gcdof_cong_l:

2784 assumes a'a: "a' \<sim> a"

2785 and agcd: "a gcdof b c"

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

2787 shows "a' gcdof b c"

2788 proof -

2789 note carr = a'carr carr'

2790 interpret weak_lower_semilattice "division_rel G" by simp

2791 have "a' \<in> carrier G \<and> a' gcdof b c"

2792 apply (simp add: gcdof_greatestLower carr')

2793 apply (subst greatest_Lower_cong_l[of _ a])

2794 apply (simp add: a'a)

2795 apply (simp add: carr)

2796 apply (simp add: carr)

2797 apply (simp add: carr)

2798 apply (simp add: gcdof_greatestLower[symmetric] agcd carr)

2799 done

2800 thus ?thesis ..

2801 qed

2803 lemma (in gcd_condition_monoid) gcd_closed [simp]:

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

2805 shows "somegcd G a b \<in> carrier G"

2806 proof -

2807 interpret weak_lower_semilattice "division_rel G" by simp

2808 show ?thesis

2809 apply (simp add: somegcd_meet[OF carr])

2810 apply (rule meet_closed[simplified], fact+)

2811 done

2812 qed

2814 lemma (in gcd_condition_monoid) gcd_isgcd:

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

2816 shows "(somegcd G a b) gcdof a b"

2817 proof -

2818 interpret weak_lower_semilattice "division_rel G" by simp

2819 from carr

2820 have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"

2821 apply (subst gcdof_greatestLower, simp, simp)

2822 apply (simp add: somegcd_meet[OF carr] meet_def)

2823 apply (rule inf_of_two_greatest[simplified], assumption+)

2824 done

2825 thus "(somegcd G a b) gcdof a b" by simp

2826 qed

2828 lemma (in gcd_condition_monoid) gcd_exists:

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

2830 shows "\<exists>x\<in>carrier G. x = somegcd G a b"

2831 proof -

2832 interpret weak_lower_semilattice "division_rel G" by simp

2833 show ?thesis

2834 apply (simp add: somegcd_meet[OF carr])

2835 apply (rule meet_closed[simplified], fact+)

2836 done

2837 qed

2839 lemma (in gcd_condition_monoid) gcd_divides_l:

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

2841 shows "(somegcd G a b) divides a"

2842 proof -

2843 interpret weak_lower_semilattice "division_rel G" by simp

2844 show ?thesis

2845 apply (simp add: somegcd_meet[OF carr])

2846 apply (rule meet_left[simplified], fact+)

2847 done

2848 qed

2850 lemma (in gcd_condition_monoid) gcd_divides_r:

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

2852 shows "(somegcd G a b) divides b"

2853 proof -

2854 interpret weak_lower_semilattice "division_rel G" by simp

2855 show ?thesis

2856 apply (simp add: somegcd_meet[OF carr])

2857 apply (rule meet_right[simplified], fact+)

2858 done

2859 qed

2861 lemma (in gcd_condition_monoid) gcd_divides:

2862 assumes sub: "z divides x" "z divides y"

2863 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"

2864 shows "z divides (somegcd G x y)"

2865 proof -

2866 interpret weak_lower_semilattice "division_rel G" by simp

2867 show ?thesis

2868 apply (simp add: somegcd_meet L)

2869 apply (rule meet_le[simplified], fact+)

2870 done

2871 qed

2873 lemma (in gcd_condition_monoid) gcd_cong_l:

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

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

2876 shows "somegcd G x y \<sim> somegcd G x' y"

2877 proof -

2878 interpret weak_lower_semilattice "division_rel G" by simp

2879 show ?thesis

2880 apply (simp add: somegcd_meet carr)

2881 apply (rule meet_cong_l[simplified], fact+)

2882 done

2883 qed

2885 lemma (in gcd_condition_monoid) gcd_cong_r:

2886 assumes carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"

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

2888 shows "somegcd G x y \<sim> somegcd G x y'"

2889 proof -

2890 interpret weak_lower_semilattice "division_rel G" by simp

2891 show ?thesis

2892 apply (simp add: somegcd_meet carr)

2893 apply (rule meet_cong_r[simplified], fact+)

2894 done

2895 qed

2897 (*

2898 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:

2899 assumes carr: "b \<in> carrier G"

2900 shows "asc_cong (\<lambda>a. somegcd G a b)"

2901 using carr

2902 unfolding CONG_def

2903 by clarsimp (blast intro: gcd_cong_l)

2905 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:

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

2907 shows "asc_cong (\<lambda>b. somegcd G a b)"

2908 using carr

2909 unfolding CONG_def

2910 by clarsimp (blast intro: gcd_cong_r)

2912 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =

2913 assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]

2914 *)

2916 lemma (in gcd_condition_monoid) gcdI:

2917 assumes dvd: "a divides b" "a divides c"

2918 and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"

2919 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2920 shows "a \<sim> somegcd G b c"

2921 apply (simp add: somegcd_def)

2922 apply (rule someI2_ex)

2923 apply (rule exI[of _ a], simp add: isgcd_def)

2924 apply (simp add: assms)

2925 apply (simp add: isgcd_def assms, clarify)

2926 apply (insert assms, blast intro: associatedI)

2927 done

2929 lemma (in gcd_condition_monoid) gcdI2:

2930 assumes "a gcdof b c"

2931 and "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2932 shows "a \<sim> somegcd G b c"

2933 using assms

2934 unfolding isgcd_def

2935 by (blast intro: gcdI)

2937 lemma (in gcd_condition_monoid) SomeGcd_ex:

2938 assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"

2939 shows "\<exists>x\<in> carrier G. x = SomeGcd G A"

2940 proof -

2941 interpret weak_lower_semilattice "division_rel G" by simp

2942 show ?thesis

2943 apply (simp add: SomeGcd_def)

2944 apply (rule finite_inf_closed[simplified], fact+)

2945 done

2946 qed

2948 lemma (in gcd_condition_monoid) gcd_assoc:

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

2950 shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"

2951 proof -

2952 interpret weak_lower_semilattice "division_rel G" by simp

2953 show ?thesis

2954 apply (subst (2 3) somegcd_meet, (simp add: carr)+)

2955 apply (simp add: somegcd_meet carr)

2956 apply (rule weak_meet_assoc[simplified], fact+)

2957 done

2958 qed

2960 lemma (in gcd_condition_monoid) gcd_mult:

2961 assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2962 shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2963 proof - (* following Jacobson, Basic Algebra, p.140 *)

2964 let ?d = "somegcd G a b"

2965 let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"

2966 note carr[simp] = acarr bcarr ccarr

2967 have dcarr: "?d \<in> carrier G" by simp

2968 have ecarr: "?e \<in> carrier G" by simp

2969 note carr = carr dcarr ecarr

2971 have "?d divides a" by (simp add: gcd_divides_l)

2972 hence cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)

2974 have "?d divides b" by (simp add: gcd_divides_r)

2975 hence cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)

2977 from cd'ca cd'cb

2978 have cd'e: "c \<otimes> ?d divides ?e"

2979 by (rule gcd_divides) simp+

2981 hence "\<exists>u. u \<in> carrier G \<and> ?e = c \<otimes> ?d \<otimes> u"

2982 by (elim dividesE, fast)

2983 from this obtain u

2984 where ucarr[simp]: "u \<in> carrier G"

2985 and e_cdu: "?e = c \<otimes> ?d \<otimes> u"

2986 by auto

2988 note carr = carr ucarr

2990 have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp+

2991 hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> a = ?e \<otimes> x"

2992 by (elim dividesE, fast)

2993 from this obtain x

2994 where xcarr: "x \<in> carrier G"

2995 and ca_ex: "c \<otimes> a = ?e \<otimes> x"

2996 by auto

2997 with e_cdu

2998 have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x" by simp

3000 from ca_cdux xcarr

3001 have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)

3002 then have "a = ?d \<otimes> u \<otimes> x" by (rule l_cancel[of c a]) (simp add: xcarr)+

3003 hence du'a: "?d \<otimes> u divides a" by (rule dividesI[OF xcarr])

3005 have "?e divides c \<otimes> b" by (intro gcd_divides_r, simp+)

3006 hence "\<exists>x. x \<in> carrier G \<and> c \<otimes> b = ?e \<otimes> x"

3007 by (elim dividesE, fast)

3008 from this obtain x

3009 where xcarr: "x \<in> carrier G"

3010 and cb_ex: "c \<otimes> b = ?e \<otimes> x"

3011 by auto

3012 with e_cdu

3013 have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x" by simp

3015 from cb_cdux xcarr

3016 have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)" by (simp add: m_assoc)

3017 with xcarr

3018 have "b = ?d \<otimes> u \<otimes> x" by (intro l_cancel[of c b], simp+)

3019 hence du'b: "?d \<otimes> u divides b" by (intro dividesI[OF xcarr])

3021 from du'a du'b carr

3022 have du'd: "?d \<otimes> u divides ?d"

3023 by (intro gcd_divides, simp+)

3024 hence uunit: "u \<in> Units G"

3025 proof (elim dividesE)

3026 fix v

3027 assume vcarr[simp]: "v \<in> carrier G"

3028 assume d: "?d = ?d \<otimes> u \<otimes> v"

3029 have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact

3030 also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)

3031 finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .

3032 hence i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp+

3033 hence i1: "\<one> = v \<otimes> u" by (simp add: m_comm)

3034 from vcarr i1[symmetric] i2[symmetric]

3035 show "u \<in> Units G"

3036 by (unfold Units_def, simp, fast)

3037 qed

3039 from e_cdu uunit

3040 have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"

3041 by (intro associatedI2[of u], simp+)

3042 from this[symmetric]

3043 show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp

3044 qed

3046 lemma (in monoid) assoc_subst:

3047 assumes ab: "a \<sim> b"

3048 and cP: "ALL a b. a : carrier G & b : carrier G & a \<sim> b

3049 --> f a : carrier G & f b : carrier G & f a \<sim> f b"

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

3051 shows "f a \<sim> f b"

3052 using assms by auto

3054 lemma (in gcd_condition_monoid) relprime_mult:

3055 assumes abrelprime: "somegcd G a b \<sim> \<one>" and acrelprime: "somegcd G a c \<sim> \<one>"

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

3057 shows "somegcd G a (b \<otimes> c) \<sim> \<one>"

3058 proof -

3059 have "c = c \<otimes> \<one>" by simp

3060 also from abrelprime[symmetric]

3061 have "\<dots> \<sim> c \<otimes> somegcd G a b"

3062 by (rule assoc_subst) (simp add: mult_cong_r)+

3063 also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by (rule gcd_mult) fact+

3064 finally

3065 have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)" by simp

3067 from carr

3068 have a: "a \<sim> somegcd G a (c \<otimes> a)"

3069 by (fast intro: gcdI divides_prod_l)

3071 have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)" by (simp add: m_comm)

3072 also from a

3073 have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"

3074 by (rule assoc_subst) (simp add: gcd_cong_l)+

3075 also from gcd_assoc

3076 have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"

3077 by (rule assoc_subst) simp+

3078 also from c[symmetric]

3079 have "\<dots> \<sim> somegcd G a c"

3080 by (rule assoc_subst) (simp add: gcd_cong_r)+

3081 also note acrelprime

3082 finally

3083 show "somegcd G a (b \<otimes> c) \<sim> \<one>" by simp

3084 qed

3086 lemma (in gcd_condition_monoid) primeness_condition:

3087 "primeness_condition_monoid G"

3088 apply unfold_locales

3089 apply (rule primeI)

3090 apply (elim irreducibleE, assumption)

3091 proof -

3092 fix p a b

3093 assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"

3094 and pirr: "irreducible G p"

3095 and pdvdab: "p divides a \<otimes> b"

3096 from pirr

3097 have pnunit: "p \<notin> Units G"

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

3099 by - (fast elim: irreducibleE)+

3101 show "p divides a \<or> p divides b"

3102 proof (rule ccontr, clarsimp)

3103 assume npdvda: "\<not> p divides a"

3104 with pcarr acarr

3105 have "\<one> \<sim> somegcd G p a"

3106 apply (intro gcdI, simp, simp, simp)

3107 apply (fast intro: unit_divides)

3108 apply (fast intro: unit_divides)

3109 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

3110 apply (rule r, rule, assumption)

3111 apply (rule properfactorI, assumption)

3112 proof (rule ccontr, simp)

3113 fix y

3114 assume ycarr: "y \<in> carrier G"

3115 assume "p divides y"

3116 also assume "y divides a"

3117 finally

3118 have "p divides a" by (simp add: pcarr ycarr acarr)

3119 with npdvda

3120 show "False" ..

3121 qed simp+

3122 with pcarr acarr

3123 have pa: "somegcd G p a \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed)

3125 assume npdvdb: "\<not> p divides b"

3126 with pcarr bcarr

3127 have "\<one> \<sim> somegcd G p b"

3128 apply (intro gcdI, simp, simp, simp)

3129 apply (fast intro: unit_divides)

3130 apply (fast intro: unit_divides)

3131 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

3132 apply (rule r, rule, assumption)

3133 apply (rule properfactorI, assumption)

3134 proof (rule ccontr, simp)

3135 fix y

3136 assume ycarr: "y \<in> carrier G"

3137 assume "p divides y"

3138 also assume "y divides b"

3139 finally have "p divides b" by (simp add: pcarr ycarr bcarr)

3140 with npdvdb

3141 show "False" ..

3142 qed simp+

3143 with pcarr bcarr

3144 have pb: "somegcd G p b \<sim> \<one>" by (fast intro: associated_sym[of "\<one>"] gcd_closed)

3146 from pcarr acarr bcarr pdvdab

3147 have "p gcdof p (a \<otimes> b)" by (fast intro: isgcd_divides_l)

3149 with pcarr acarr bcarr

3150 have "p \<sim> somegcd G p (a \<otimes> b)" by (fast intro: gcdI2)

3151 also from pa pb pcarr acarr bcarr

3152 have "somegcd G p (a \<otimes> b) \<sim> \<one>" by (rule relprime_mult)

3153 finally have "p \<sim> \<one>" by (simp add: pcarr acarr bcarr)

3155 with pcarr

3156 have "p \<in> Units G" by (fast intro: assoc_unit_l)

3157 with pnunit

3158 show "False" ..

3159 qed

3160 qed

3162 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid

3163 by (rule primeness_condition)

3166 subsubsection {* Divisor chain condition *}

3168 lemma (in divisor_chain_condition_monoid) wfactors_exist:

3169 assumes acarr: "a \<in> carrier G"

3170 shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3171 proof -

3172 have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"

3173 apply (rule wf_induct[OF division_wellfounded])

3174 proof -

3175 fix x

3176 assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}

3177 \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)"

3179 show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)"

3180 apply clarify

3181 apply (cases "x \<in> Units G")

3182 apply (rule exI[of _ "[]"], simp)

3183 apply (cases "irreducible G x")

3184 apply (rule exI[of _ "[x]"], simp add: wfactors_def)

3185 proof -

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

3187 and xnunit: "x \<notin> Units G"

3188 and xnirr: "\<not> irreducible G x"

3189 hence "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"

3190 apply - apply (rule ccontr, simp)

3191 apply (subgoal_tac "irreducible G x", simp)

3192 apply (rule irreducibleI, simp, simp)

3193 done

3194 from this obtain y

3195 where ycarr: "y \<in> carrier G"

3196 and ynunit: "y \<notin> Units G"

3197 and pfyx: "properfactor G y x"

3198 by auto

3200 have ih':

3201 "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk>

3202 \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"

3203 by (rule ih[rule_format, simplified]) (simp add: xcarr)+

3205 from ycarr pfyx

3206 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"

3207 by (rule ih')

3208 from this obtain ys

3209 where yscarr: "set ys \<subseteq> carrier G"

3210 and yfs: "wfactors G ys y"

3211 by auto

3213 from pfyx

3214 have "y divides x"

3215 and nyx: "\<not> y \<sim> x"

3216 by - (fast elim: properfactorE2)+

3217 hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"

3218 by (fast elim: dividesE)

3220 from this obtain z

3221 where zcarr: "z \<in> carrier G"

3222 and x: "x = y \<otimes> z"

3223 by auto

3225 from zcarr ycarr

3226 have "properfactor G z x"

3227 apply (subst x)

3228 apply (intro properfactorI3[of _ _ y])

3229 apply (simp add: m_comm)

3230 apply (simp add: ynunit)+

3231 done

3232 with zcarr

3233 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as z"

3234 by (rule ih')

3235 from this obtain zs

3236 where zscarr: "set zs \<subseteq> carrier G"

3237 and zfs: "wfactors G zs z"

3238 by auto

3240 from yscarr zscarr

3241 have xscarr: "set (ys@zs) \<subseteq> carrier G" by simp

3242 from yfs zfs ycarr zcarr yscarr zscarr

3243 have "wfactors G (ys@zs) (y\<otimes>z)" by (rule wfactors_mult)

3244 hence "wfactors G (ys@zs) x" by (simp add: x)

3246 from xscarr this

3247 show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x" by fast

3248 qed

3249 qed

3251 from acarr

3252 show ?thesis by (rule r)

3253 qed

3256 subsubsection {* Primeness condition *}

3258 lemma (in comm_monoid_cancel) multlist_prime_pos:

3259 assumes carr: "a \<in> carrier G" "set as \<subseteq> carrier G"

3260 and aprime: "prime G a"

3261 and "a divides (foldr (op \<otimes>) as \<one>)"

3262 shows "\<exists>i<length as. a divides (as!i)"

3263 proof -

3264 have r[rule_format]:

3265 "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>)

3266 \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"

3267 apply (induct as)

3268 apply clarsimp defer 1

3269 apply clarsimp defer 1

3270 proof -

3271 assume "a divides \<one>"

3272 with carr

3273 have "a \<in> Units G"

3274 by (fast intro: divides_unit[of a \<one>])

3275 with aprime

3276 show "False" by (elim primeE, simp)

3277 next

3278 fix aa as

3279 assume ih[rule_format]: "a divides foldr op \<otimes> as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"

3280 and carr': "aa \<in> carrier G" "set as \<subseteq> carrier G"

3281 and "a divides aa \<otimes> foldr op \<otimes> as \<one>"

3282 with carr aprime

3283 have "a divides aa \<or> a divides foldr op \<otimes> as \<one>"

3284 by (intro prime_divides) simp+

3285 moreover {

3286 assume "a divides aa"

3287 hence p1: "a divides (aa#as)!0" by simp

3288 have "0 < Suc (length as)" by simp

3289 with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast

3290 }

3291 moreover {

3292 assume "a divides foldr op \<otimes> as \<one>"

3293 hence "\<exists>i. i < length as \<and> a divides as ! i" by (rule ih)

3294 from this obtain i where "a divides as ! i" and len: "i < length as" by auto

3295 hence p1: "a divides (aa#as) ! (Suc i)" by simp

3296 from len have "Suc i < Suc (length as)" by simp

3297 with p1 have "\<exists>i<Suc (length as). a divides (aa # as) ! i" by force

3298 }

3299 ultimately

3300 show "\<exists>i<Suc (length as). a divides (aa # as) ! i" by fast

3301 qed

3303 from assms

3304 show ?thesis

3305 by (intro r, safe)

3306 qed

3308 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:

3309 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>

3310 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"

3311 proof (induct as)

3312 case Nil show ?case apply auto

3313 proof -

3314 fix a as'

3315 assume a: "a \<in> carrier G"

3316 assume "wfactors G [] a"

3317 then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)

3318 with a have "a \<in> Units G" by (auto intro: assoc_unit_r)

3319 moreover assume "wfactors G as' a"

3320 moreover assume "set as' \<subseteq> carrier G"

3321 ultimately have "as' = []" by (rule unit_wfactors_empty)

3322 then show "essentially_equal G [] as'" by simp

3323 qed

3324 next

3325 case (Cons ah as) then show ?case apply clarsimp

3326 proof -

3327 fix a as'

3328 assume ih [rule_format]:

3329 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>

3330 wfactors G as' a \<longrightarrow> essentially_equal G as as'"

3331 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"

3332 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"

3333 and afs: "wfactors G (ah # as) a"

3334 and afs': "wfactors G as' a"

3335 hence ahdvda: "ah divides a"

3336 by (intro wfactors_dividesI[of "ah#as" "a"], simp+)

3337 hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)

3338 from this obtain a'

3339 where a'carr: "a' \<in> carrier G"

3340 and a: "a = ah \<otimes> a'"

3341 by auto

3342 have a'fs: "wfactors G as a'"

3343 apply (rule wfactorsE[OF afs], rule wfactorsI, simp)

3344 apply (simp add: a, insert ascarr a'carr)

3345 apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)

3346 done

3347 from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)

3348 with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)

3350 note carr [simp] = acarr ahcarr ascarr as'carr a'carr

3352 note ahdvda

3353 also from afs'

3354 have "a divides (foldr (op \<otimes>) as' \<one>)"

3355 by (elim wfactorsE associatedE, simp)

3356 finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp

3358 with ahprime

3359 have "\<exists>i<length as'. ah divides as'!i"

3360 by (intro multlist_prime_pos, simp+)

3361 from this obtain i

3362 where len: "i<length as'" and ahdvd: "ah divides as'!i"

3363 by auto

3364 from afs' carr have irrasi: "irreducible G (as'!i)"

3365 by (fast intro: nth_mem[OF len] elim: wfactorsE)

3366 from len carr

3367 have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)

3368 note carr = carr asicarr

3370 from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)

3371 from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto

3373 with carr irrasi[simplified asi]

3374 have asiah: "as'!i \<sim> ah" apply -

3375 apply (elim irreducible_prodE[of "ah" "x"], assumption+)

3376 apply (rule associatedI2[of x], assumption+)

3377 apply (rule irreducibleE[OF ahirr], simp)

3378 done

3380 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']

3381 note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]

3382 note carr = carr partscarr

3384 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"

3385 apply (intro wfactors_prod_exists)

3386 using setparts afs' by (fast elim: wfactorsE, simp)

3387 from this obtain aa_1

3388 where aa1carr: "aa_1 \<in> carrier G"

3389 and aa1fs: "wfactors G (take i as') aa_1"

3390 by auto

3392 have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"

3393 apply (intro wfactors_prod_exists)

3394 using setparts afs' by (fast elim: wfactorsE, simp)

3395 from this obtain aa_2

3396 where aa2carr: "aa_2 \<in> carrier G"

3397 and aa2fs: "wfactors G (drop (Suc i) as') aa_2"

3398 by auto

3400 note carr = carr aa1carr[simp] aa2carr[simp]

3402 from aa1fs aa2fs

3403 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"

3404 by (intro wfactors_mult, simp+)

3405 hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"

3406 apply (intro wfactors_mult_single)

3407 using setparts afs'

3408 by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)

3410 from aa2carr carr aa1fs aa2fs

3411 have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"

3412 apply (intro wfactors_mult_single)

3413 apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])

3414 apply (fast intro: nth_mem[OF len])

3415 apply fast

3416 apply fast

3417 apply assumption

3418 done

3419 with len carr aa1carr aa2carr aa1fs

3420 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"

3421 apply (intro wfactors_mult)

3422 apply fast

3423 apply (simp, (fast intro: nth_mem[OF len])?)+

3424 done

3426 from len

3427 have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"

3428 by (simp add: drop_Suc_conv_tl)

3429 with carr

3430 have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"

3431 by simp

3433 with v2 afs' carr aa1carr aa2carr nth_mem[OF len]

3434 have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"

3435 apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])

3436 apply fast+

3437 apply (simp, fast)

3438 done

3439 then

3440 have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"

3441 apply (simp add: m_assoc[symmetric])

3442 apply (simp add: m_comm)

3443 done

3444 from carr asiah

3445 have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"

3446 apply (intro mult_cong_l)

3447 apply (fast intro: associated_sym, simp+)

3448 done

3449 also note t1

3450 finally

3451 have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp

3453 with carr aa1carr aa2carr a'carr nth_mem[OF len]

3454 have a': "aa_1 \<otimes> aa_2 \<sim> a'"

3455 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])

3457 note v1

3458 also note a'

3459 finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp

3461 from a'fs this carr

3462 have "essentially_equal G as (take i as' @ drop (Suc i) as')"

3463 by (intro ih[of a']) simp

3465 hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"

3466 apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)

3467 done

3469 from carr

3470 have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')

3471 (as' ! i # take i as' @ drop (Suc i) as')"

3472 proof (intro essentially_equalI)

3473 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"

3474 by simp

3475 next

3476 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"

3477 apply (simp add: list_all2_append)

3478 apply (simp add: asiah[symmetric] ahcarr asicarr)

3479 done

3480 qed

3482 note ee1

3483 also note ee2

3484 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')

3485 (take i as' @ as' ! i # drop (Suc i) as')"

3486 apply (intro essentially_equalI)

3487 apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>

3488 take i as' @ as' ! i # drop (Suc i) as'")

3489 apply simp

3490 apply (rule perm_append_Cons)

3491 apply simp

3492 done

3493 finally

3494 have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp

3495 then show "essentially_equal G (ah # as) as'" by (subst as', assumption)

3496 qed

3497 qed

3499 lemma (in primeness_condition_monoid) wfactors_unique:

3500 assumes "wfactors G as a" "wfactors G as' a"

3501 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G"

3502 shows "essentially_equal G as as'"

3503 apply (rule wfactors_unique__hlp_induct[rule_format, of a])

3504 apply (simp add: assms)

3505 done

3508 subsubsection {* Application to factorial monoids *}

3510 text {* Number of factors for wellfoundedness *}

3512 definition

3513 factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where

3514 "factorcount G a =

3515 (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"

3517 lemma (in monoid) ee_length:

3518 assumes ee: "essentially_equal G as bs"

3519 shows "length as = length bs"

3520 apply (rule essentially_equalE[OF ee])

3521 apply (metis list_all2_conv_all_nth perm_length)

3522 done

3524 lemma (in factorial_monoid) factorcount_exists:

3525 assumes carr[simp]: "a \<in> carrier G"

3526 shows "EX c. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"

3527 proof -

3528 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (intro wfactors_exist, simp)

3529 from this obtain as

3530 where ascarr[simp]: "set as \<subseteq> carrier G"

3531 and afs: "wfactors G as a"

3532 by (auto simp del: carr)

3534 have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"

3535 by (metis afs ascarr assms ee_length wfactors_unique)

3536 thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..

3537 qed

3539 lemma (in factorial_monoid) factorcount_unique:

3540 assumes afs: "wfactors G as a"

3541 and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"

3542 shows "factorcount G a = length as"

3543 proof -

3544 have "EX ac. ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as" by (rule factorcount_exists, simp)

3545 from this obtain ac where

3546 alen: "ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

3547 by auto

3548 have ac: "ac = factorcount G a"

3549 apply (simp add: factorcount_def)

3550 apply (rule theI2)

3551 apply (rule alen)

3552 apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)

3553 apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)

3554 done

3556 from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])

3557 with ac show ?thesis by simp

3558 qed

3560 lemma (in factorial_monoid) divides_fcount:

3561 assumes dvd: "a divides b"

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

3563 shows "factorcount G a <= factorcount G b"

3564 apply (rule dividesE[OF dvd])

3565 proof -

3566 fix c

3567 from assms

3568 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast

3569 from this obtain as

3570 where ascarr: "set as \<subseteq> carrier G"

3571 and afs: "wfactors G as a"

3572 by auto

3573 with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)

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

3576 hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast

3577 from this obtain cs

3578 where cscarr: "set cs \<subseteq> carrier G"

3579 and cfs: "wfactors G cs c"

3580 by auto

3582 note [simp] = acarr bcarr ccarr ascarr cscarr

3584 assume b: "b = a \<otimes> c"

3585 from afs cfs

3586 have "wfactors G (as@cs) (a \<otimes> c)" by (intro wfactors_mult, simp+)

3587 with b have "wfactors G (as@cs) b" by simp

3588 hence "factorcount G b = length (as@cs)" by (intro factorcount_unique, simp+)

3589 hence "factorcount G b = length as + length cs" by simp

3590 with fca show ?thesis by simp

3591 qed

3593 lemma (in factorial_monoid) associated_fcount:

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

3595 and asc: "a \<sim> b"

3596 shows "factorcount G a = factorcount G b"

3597 apply (rule associatedE[OF asc])

3598 apply (drule divides_fcount[OF _ acarr bcarr])

3599 apply (drule divides_fcount[OF _ bcarr acarr])

3600 apply simp

3601 done

3603 lemma (in factorial_monoid) properfactor_fcount:

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

3605 and pf: "properfactor G a b"

3606 shows "factorcount G a < factorcount G b"

3607 apply (rule properfactorE[OF pf], elim dividesE)

3608 proof -

3609 fix c

3610 from assms

3611 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by fast

3612 from this obtain as

3613 where ascarr: "set as \<subseteq> carrier G"

3614 and afs: "wfactors G as a"

3615 by auto

3616 with acarr have fca: "factorcount G a = length as" by (intro factorcount_unique)

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

3619 hence "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c" by fast

3620 from this obtain cs

3621 where cscarr: "set cs \<subseteq> carrier G"

3622 and cfs: "wfactors G cs c"

3623 by auto

3625 assume b: "b = a \<otimes> c"

3627 have "wfactors G (as@cs) (a \<otimes> c)" by (rule wfactors_mult) fact+

3628 with b

3629 have "wfactors G (as@cs) b" by simp

3630 with ascarr cscarr bcarr

3631 have "factorcount G b = length (as@cs)" by (simp add: factorcount_unique)

3632 hence fcb: "factorcount G b = length as + length cs" by simp

3634 assume nbdvda: "\<not> b divides a"

3635 have "c \<notin> Units G"

3636 proof (rule ccontr, simp)

3637 assume cunit:"c \<in> Units G"

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

3640 also with ccarr acarr cunit

3641 have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)

3642 also with ccarr cunit

3643 have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)

3644 also with acarr

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

3646 finally have "a = b \<otimes> inv c" by simp

3647 with ccarr cunit

3648 have "b divides a" by (fast intro: dividesI[of "inv c"])

3649 with nbdvda show False by simp

3650 qed

3652 with cfs have "length cs > 0"

3653 apply -

3654 apply (rule ccontr, simp)

3655 apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)

3656 done

3657 with fca fcb show ?thesis by simp

3658 qed

3660 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid

3661 apply unfold_locales

3662 apply (rule wfUNIVI)

3663 apply (rule measure_induct[of "factorcount G"])

3664 apply simp

3665 apply (metis properfactor_fcount)

3666 done

3668 sublocale factorial_monoid \<subseteq> primeness_condition_monoid

3669 by default (rule irreducible_is_prime)

3672 lemma (in factorial_monoid) primeness_condition:

3673 shows "primeness_condition_monoid G"

3674 ..

3676 lemma (in factorial_monoid) gcd_condition [simp]:

3677 shows "gcd_condition_monoid G"

3678 by default (rule gcdof_exists)

3680 sublocale factorial_monoid \<subseteq> gcd_condition_monoid

3681 by default (rule gcdof_exists)

3683 lemma (in factorial_monoid) division_weak_lattice [simp]:

3684 shows "weak_lattice (division_rel G)"

3685 proof -

3686 interpret weak_lower_semilattice "division_rel G" by simp

3688 show "weak_lattice (division_rel G)"

3689 apply (unfold_locales, simp_all)

3690 proof -

3691 fix x y

3692 assume carr: "x \<in> carrier G" "y \<in> carrier G"

3694 hence "\<exists>z. z \<in> carrier G \<and> z lcmof x y" by (rule lcmof_exists)

3695 from this obtain z

3696 where zcarr: "z \<in> carrier G"

3697 and isgcd: "z lcmof x y"

3698 by auto

3699 with carr

3700 have "least (division_rel G) z (Upper (division_rel G) {x, y})"

3701 by (simp add: lcmof_leastUpper[symmetric])

3702 thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast

3703 qed

3704 qed

3707 subsection {* Factoriality Theorems *}

3709 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)

3710 shows "(divisor_chain_condition_monoid G \<and> primeness_condition_monoid G) =

3711 factorial_monoid G"

3712 apply rule

3713 proof clarify

3714 assume dcc: "divisor_chain_condition_monoid G"

3715 and pc: "primeness_condition_monoid G"

3716 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3717 interpret primeness_condition_monoid "G" by (rule pc)

3719 show "factorial_monoid G"

3720 by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)

3721 next

3722 assume fm: "factorial_monoid G"

3723 interpret factorial_monoid "G" by (rule fm)

3724 show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"

3725 by rule unfold_locales

3726 qed

3728 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)

3729 shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"

3730 apply rule

3731 proof clarify

3732 assume dcc: "divisor_chain_condition_monoid G"

3733 and gc: "gcd_condition_monoid G"

3734 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3735 interpret gcd_condition_monoid "G" by (rule gc)

3736 show "factorial_monoid G"

3737 by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)

3738 next

3739 assume fm: "factorial_monoid G"

3740 interpret factorial_monoid "G" by (rule fm)

3741 show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"

3742 by rule unfold_locales

3743 qed

3745 end