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

src/HOL/Algebra/Divisibility.thy

author | paulson <lp15@cam.ac.uk> |

Wed Jun 06 14:25:53 2018 +0100 (12 months ago) | |

changeset 68399 | 0b71d08528f0 |

parent 68004 | a8a20be7053a |

child 68470 | 7ddcce75c3ee |

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

resolution of name clashes in Algebra

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

2 Author: Clemens Ballarin

3 Author: Stephan Hohe

4 *)

6 section \<open>Divisibility in monoids and rings\<close>

8 theory Divisibility

9 imports "HOL-Library.Permutation" Coset Group

10 begin

12 section \<open>Factorial Monoids\<close>

14 subsection \<open>Monoids with Cancellation Law\<close>

16 locale monoid_cancel = monoid +

17 assumes l_cancel: "\<lbrakk>c \<otimes> a = c \<otimes> b; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"

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

20 lemma (in monoid) monoid_cancelI:

21 assumes l_cancel: "\<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"

22 and r_cancel: "\<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"

23 shows "monoid_cancel G"

24 by standard fact+

26 lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" ..

28 sublocale group \<subseteq> monoid_cancel

29 by standard simp_all

32 locale comm_monoid_cancel = monoid_cancel + comm_monoid

34 lemma comm_monoid_cancelI:

35 fixes G (structure)

36 assumes "comm_monoid G"

37 assumes cancel: "\<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"

38 shows "comm_monoid_cancel G"

39 proof -

40 interpret comm_monoid G by fact

41 show "comm_monoid_cancel G"

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

43 qed

45 lemma (in comm_monoid_cancel) is_comm_monoid_cancel: "comm_monoid_cancel G"

46 by intro_locales

48 sublocale comm_group \<subseteq> comm_monoid_cancel ..

51 subsection \<open>Products of Units in Monoids\<close>

53 lemma (in monoid) prod_unit_l:

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

55 and aunit[simp]: "a \<in> Units G"

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

57 shows "b \<in> Units G"

58 proof -

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

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

62 by (simp add: m_assoc)

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

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

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

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

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

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

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

71 by (simp add: m_assoc del: Units_l_inv)

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

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

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

76 from c li ri show "b \<in> Units G" by (auto simp: Units_def)

77 qed

79 lemma (in monoid) prod_unit_r:

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

81 and bunit[simp]: "b \<in> Units G"

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

83 shows "a \<in> Units G"

84 proof -

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

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

88 by (simp add: m_assoc del: Units_r_inv)

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

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

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

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

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

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

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

97 by (simp add: m_assoc del: Units_l_inv)

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

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

101 from c li ri show "a \<in> Units G" by (auto simp: Units_def)

102 qed

104 lemma (in comm_monoid) unit_factor:

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

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

107 shows "a \<in> Units G"

108 using abunit[simplified Units_def]

109 proof clarsimp

110 fix i

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

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

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

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

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

118 also assume "i \<otimes> (a \<otimes> b) = \<one>"

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

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

122 also assume "a \<otimes> b \<otimes> i = \<one>"

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

125 from carr' li' ri'

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

127 qed

130 subsection \<open>Divisibility and Association\<close>

132 subsubsection \<open>Function definitions\<close>

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

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

137 definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55)

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

140 abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = (\<sim>\<^bsub>G\<^esub>), le = (divides\<^bsub>G\<^esub>)\<rparr>"

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

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

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

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

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

149 where "prime G p \<longleftrightarrow>

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

151 (\<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)"

154 subsubsection \<open>Divisibility\<close>

156 lemma dividesI:

157 fixes G (structure)

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

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

160 shows "a divides b"

161 unfolding factor_def using assms by fast

163 lemma dividesI' [intro]:

164 fixes G (structure)

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

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

167 shows "a divides b"

168 using assms by (fast intro: dividesI)

170 lemma dividesD:

171 fixes G (structure)

172 assumes "a divides b"

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

174 using assms unfolding factor_def by fast

176 lemma dividesE [elim]:

177 fixes G (structure)

178 assumes d: "a divides b"

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

180 shows "P"

181 proof -

182 from dividesD[OF d] obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto

183 then show P by (elim elim)

184 qed

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

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

188 shows "a divides a"

189 by (intro dividesI[of "\<one>"]) (simp_all add: carr)

191 lemma (in monoid) divides_trans [trans]:

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

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

194 shows "a divides c"

195 using dvds[THEN dividesD] by (blast intro: dividesI m_assoc acarr)

197 lemma (in monoid) divides_mult_lI [intro]:

198 assumes ab: "a divides b"

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

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

201 using ab

202 apply (elim dividesE)

203 apply (simp add: m_assoc[symmetric] carr)

204 apply (fast intro: dividesI)

205 done

207 lemma (in monoid_cancel) divides_mult_l [simp]:

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

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

210 apply safe

211 apply (elim dividesE, intro dividesI, assumption)

212 apply (rule l_cancel[of c])

213 apply (simp add: m_assoc carr)+

214 apply (fast intro: carr)

215 done

217 lemma (in comm_monoid) divides_mult_rI [intro]:

218 assumes ab: "a divides b"

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

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

221 using carr ab

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

223 apply (rule divides_mult_lI, assumption+)

224 done

226 lemma (in comm_monoid_cancel) divides_mult_r [simp]:

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

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

229 using carr by (simp add: m_comm[of a c] m_comm[of b c])

231 lemma (in monoid) divides_prod_r:

232 assumes ab: "a divides b"

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

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

235 using ab carr by (fast intro: m_assoc)

237 lemma (in comm_monoid) divides_prod_l:

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

239 and ab: "a divides b"

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

241 using ab carr

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

243 apply (fast intro: divides_prod_r)

244 done

246 lemma (in monoid) unit_divides:

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

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

249 shows "u divides a"

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

251 from uunit acarr have xcarr: "inv u \<otimes> a \<in> carrier G" by fast

252 from uunit acarr have "u \<otimes> (inv u \<otimes> a) = (u \<otimes> inv u) \<otimes> a"

253 by (fast intro: m_assoc[symmetric])

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

255 also from acarr have "\<dots> = a" by simp

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

257 qed

259 lemma (in comm_monoid) divides_unit:

260 assumes udvd: "a divides u"

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

262 shows "a \<in> Units G"

263 using udvd carr by (blast intro: unit_factor)

265 lemma (in comm_monoid) Unit_eq_dividesone:

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

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

268 using ucarr by (fast dest: divides_unit intro: unit_divides)

271 subsubsection \<open>Association\<close>

273 lemma associatedI:

274 fixes G (structure)

275 assumes "a divides b" "b divides a"

276 shows "a \<sim> b"

277 using assms by (simp add: associated_def)

279 lemma (in monoid) associatedI2:

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

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

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

283 shows "a \<sim> b"

284 using uunit bcarr

285 unfolding a

286 apply (intro associatedI)

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

288 apply (simp add: m_assoc Units_closed)

289 apply fast

290 done

292 lemma (in monoid) associatedI2':

293 assumes "a = b \<otimes> u"

294 and "u \<in> Units G"

295 and "b \<in> carrier G"

296 shows "a \<sim> b"

297 using assms by (intro associatedI2)

299 lemma associatedD:

300 fixes G (structure)

301 assumes "a \<sim> b"

302 shows "a divides b"

303 using assms by (simp add: associated_def)

305 lemma (in monoid_cancel) associatedD2:

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

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

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

309 using assoc

310 unfolding associated_def

311 proof clarify

312 assume "b divides a"

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

314 by (rule dividesE)

316 assume "a divides b"

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

318 by (rule dividesE)

319 note carr = carr ucarr u'carr

321 from carr have "a \<otimes> \<one> = a" by simp

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

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

324 also from carr have "\<dots> = a \<otimes> (u' \<otimes> u)" by (simp add: m_assoc)

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

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

328 from carr have "b \<otimes> \<one> = b" by simp

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

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

331 also from carr have "\<dots> = b \<otimes> (u \<otimes> u')" by (simp add: m_assoc)

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

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

335 from u'carr u1[symmetric] u2[symmetric] have "\<exists>u'\<in>carrier G. u' \<otimes> u = \<one> \<and> u \<otimes> u' = \<one>"

336 by fast

337 then have "u \<in> Units G"

338 by (simp add: Units_def ucarr)

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

340 qed

342 lemma associatedE:

343 fixes G (structure)

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

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

346 shows "P"

347 proof -

348 from assoc have "a divides b" "b divides a"

349 by (simp_all add: associated_def)

350 then show P by (elim e)

351 qed

353 lemma (in monoid_cancel) associatedE2:

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

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

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

357 shows "P"

358 proof -

359 from assoc and carr have "\<exists>u\<in>Units G. a = b \<otimes> u"

360 by (rule associatedD2)

361 then obtain u where "u \<in> Units G" "a = b \<otimes> u"

362 by auto

363 then show P by (elim e)

364 qed

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

367 assumes "a \<in> carrier G"

368 shows "a \<sim> a"

369 using assms by (fast intro: associatedI)

371 lemma (in monoid) associated_sym [sym]:

372 assumes "a \<sim> b"

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

374 shows "b \<sim> a"

375 using assms by (iprover intro: associatedI elim: associatedE)

377 lemma (in monoid) associated_trans [trans]:

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

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

380 shows "a \<sim> c"

381 using assms by (iprover intro: associatedI divides_trans elim: associatedE)

383 lemma (in monoid) division_equiv [intro, simp]: "equivalence (division_rel G)"

384 apply unfold_locales

385 apply simp_all

386 apply (metis associated_def)

387 apply (iprover intro: associated_trans)

388 done

391 subsubsection \<open>Division and associativity\<close>

393 lemma divides_antisym:

394 fixes G (structure)

395 assumes "a divides b" "b divides a"

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

397 shows "a \<sim> b"

398 using assms by (fast intro: associatedI)

400 lemma (in monoid) divides_cong_l [trans]:

401 assumes "x \<sim> x'"

402 and "x' divides y"

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

404 shows "x divides y"

405 proof -

406 from assms(1) have "x divides x'" by (simp add: associatedD)

407 also note assms(2)

408 finally show "x divides y" by simp

409 qed

411 lemma (in monoid) divides_cong_r [trans]:

412 assumes "x divides y"

413 and "y \<sim> y'"

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

415 shows "x divides y'"

416 proof -

417 note assms(1)

418 also from assms(2) have "y divides y'" by (simp add: associatedD)

419 finally show "x divides y'" by simp

420 qed

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

423 "weak_partial_order (division_rel G)"

424 apply unfold_locales

425 apply simp_all

426 apply (simp add: associated_sym)

427 apply (blast intro: associated_trans)

428 apply (simp add: divides_antisym)

429 apply (blast intro: divides_trans)

430 apply (blast intro: divides_cong_l divides_cong_r associated_sym)

431 done

434 subsubsection \<open>Multiplication and associativity\<close>

436 lemma (in monoid_cancel) mult_cong_r:

437 assumes "b \<sim> b'"

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

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

440 using assms

441 apply (elim associatedE2, intro associatedI2)

442 apply (auto intro: m_assoc[symmetric])

443 done

445 lemma (in comm_monoid_cancel) mult_cong_l:

446 assumes "a \<sim> a'"

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

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

449 using assms

450 apply (elim associatedE2, intro associatedI2)

451 apply assumption

452 apply (simp add: m_assoc Units_closed)

453 apply (simp add: m_comm Units_closed)

454 apply simp_all

455 done

457 lemma (in monoid_cancel) assoc_l_cancel:

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

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

460 shows "b \<sim> b'"

461 using assms

462 apply (elim associatedE2, intro associatedI2)

463 apply assumption

464 apply (rule l_cancel[of a])

465 apply (simp add: m_assoc Units_closed)

466 apply fast+

467 done

469 lemma (in comm_monoid_cancel) assoc_r_cancel:

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

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

472 shows "a \<sim> a'"

473 using assms

474 apply (elim associatedE2, intro associatedI2)

475 apply assumption

476 apply (rule r_cancel[of a b])

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

478 apply fast+

479 done

482 subsubsection \<open>Units\<close>

484 lemma (in monoid_cancel) assoc_unit_l [trans]:

485 assumes "a \<sim> b"

486 and "b \<in> Units G"

487 and "a \<in> carrier G"

488 shows "a \<in> Units G"

489 using assms by (fast elim: associatedE2)

491 lemma (in monoid_cancel) assoc_unit_r [trans]:

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

493 and asc: "a \<sim> b"

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

495 shows "b \<in> Units G"

496 using aunit bcarr associated_sym[OF asc] by (blast intro: assoc_unit_l)

498 lemma (in comm_monoid) Units_cong:

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

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

501 shows "b \<in> Units G"

502 using assms by (blast intro: divides_unit elim: associatedE)

504 lemma (in monoid) Units_assoc:

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

506 shows "a \<sim> b"

507 using units by (fast intro: associatedI unit_divides)

509 lemma (in monoid) Units_are_ones: "Units G {.=}\<^bsub>(division_rel G)\<^esub> {\<one>}"

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

511 proof clarsimp

512 fix a

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

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

515 apply (rule associatedI)

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

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

518 done

519 next

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

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

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

523 qed

525 lemma (in comm_monoid) Units_Lower: "Units G = Lower (division_rel G) (carrier G)"

526 apply (simp add: Units_def Lower_def)

527 apply (rule, rule)

528 apply clarsimp

529 apply (rule unit_divides)

530 apply (unfold Units_def, fast)

531 apply assumption

532 apply clarsimp

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

534 done

537 subsubsection \<open>Proper factors\<close>

539 lemma properfactorI:

540 fixes G (structure)

541 assumes "a divides b"

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

543 shows "properfactor G a b"

544 using assms unfolding properfactor_def by simp

546 lemma properfactorI2:

547 fixes G (structure)

548 assumes advdb: "a divides b"

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

550 shows "properfactor G a b"

551 proof (rule properfactorI, rule advdb, rule notI)

552 assume "b divides a"

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

554 with neq show "False" by fast

555 qed

557 lemma (in comm_monoid_cancel) properfactorI3:

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

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

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

561 shows "properfactor G a p"

562 unfolding p

563 using carr

564 apply (intro properfactorI, fast)

565 proof (clarsimp, elim dividesE)

566 fix c

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

568 note [simp] = carr ccarr

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

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

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

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

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

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

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

579 from ccarr linv[symmetric] rinv[symmetric] have "b \<in> Units G"

580 unfolding Units_def by fastforce

581 with nunit show False ..

582 qed

584 lemma properfactorE:

585 fixes G (structure)

586 assumes pf: "properfactor G a b"

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

588 shows "P"

589 using pf unfolding properfactor_def by (fast intro: r)

591 lemma properfactorE2:

592 fixes G (structure)

593 assumes pf: "properfactor G a b"

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

595 shows "P"

596 using pf unfolding properfactor_def by (fast elim: elim associatedE)

598 lemma (in monoid) properfactor_unitE:

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

600 and pf: "properfactor G a u"

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

602 shows "P"

603 using pf unit_divides[OF uunit acarr] by (fast elim: properfactorE)

605 lemma (in monoid) properfactor_divides:

606 assumes pf: "properfactor G a b"

607 shows "a divides b"

608 using pf by (elim properfactorE)

610 lemma (in monoid) properfactor_trans1 [trans]:

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

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

613 shows "properfactor G a c"

614 using dvds carr

615 apply (elim properfactorE, intro properfactorI)

616 apply (iprover intro: divides_trans)+

617 done

619 lemma (in monoid) properfactor_trans2 [trans]:

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

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

622 shows "properfactor G a c"

623 using dvds carr

624 apply (elim properfactorE, intro properfactorI)

625 apply (iprover intro: divides_trans)+

626 done

628 lemma properfactor_lless:

629 fixes G (structure)

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

631 apply (rule ext)

632 apply (rule ext)

633 apply rule

634 apply (fastforce elim: properfactorE2 intro: weak_llessI)

635 apply (fastforce elim: weak_llessE intro: properfactorI2)

636 done

638 lemma (in monoid) properfactor_cong_l [trans]:

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

640 and pf: "properfactor G x y"

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

642 shows "properfactor G x' y"

643 using pf

644 unfolding properfactor_lless

645 proof -

646 interpret weak_partial_order "division_rel G" ..

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

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

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

650 qed

652 lemma (in monoid) properfactor_cong_r [trans]:

653 assumes pf: "properfactor G x y"

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

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

656 shows "properfactor G x y'"

657 using pf

658 unfolding properfactor_lless

659 proof -

660 interpret weak_partial_order "division_rel G" ..

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

662 also from yy'

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

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

665 qed

667 lemma (in monoid_cancel) properfactor_mult_lI [intro]:

668 assumes ab: "properfactor G a b"

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

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

671 using ab carr by (fastforce elim: properfactorE intro: properfactorI)

673 lemma (in monoid_cancel) properfactor_mult_l [simp]:

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

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

676 using carr by (fastforce elim: properfactorE intro: properfactorI)

678 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:

679 assumes ab: "properfactor G a b"

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

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

682 using ab carr by (fastforce elim: properfactorE intro: properfactorI)

684 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:

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

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

687 using carr by (fastforce elim: properfactorE intro: properfactorI)

689 lemma (in monoid) properfactor_prod_r:

690 assumes ab: "properfactor G a b"

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

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

693 by (intro properfactor_trans2[OF ab] divides_prod_r) simp_all

695 lemma (in comm_monoid) properfactor_prod_l:

696 assumes ab: "properfactor G a b"

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

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

699 by (intro properfactor_trans2[OF ab] divides_prod_l) simp_all

702 subsection \<open>Irreducible Elements and Primes\<close>

704 subsubsection \<open>Irreducible elements\<close>

706 lemma irreducibleI:

707 fixes G (structure)

708 assumes "a \<notin> Units G"

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

710 shows "irreducible G a"

711 using assms unfolding irreducible_def by blast

713 lemma irreducibleE:

714 fixes G (structure)

715 assumes irr: "irreducible G a"

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

717 shows "P"

718 using assms unfolding irreducible_def by blast

720 lemma irreducibleD:

721 fixes G (structure)

722 assumes irr: "irreducible G a"

723 and pf: "properfactor G b a"

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

725 shows "b \<in> Units G"

726 using assms by (fast elim: irreducibleE)

728 lemma (in monoid_cancel) irreducible_cong [trans]:

729 assumes irred: "irreducible G a"

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

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

732 shows "irreducible G a'"

733 using assms

734 apply (elim irreducibleE, intro irreducibleI)

735 apply simp_all

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

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

738 done

740 lemma (in monoid) irreducible_prod_rI:

741 assumes airr: "irreducible G a"

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

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

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

745 using airr carr bunit

746 apply (elim irreducibleE, intro irreducibleI, clarify)

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

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

749 apply (metis assms(2,3) associatedI2 m_closed properfactor_cong_r)

750 done

752 lemma (in comm_monoid) irreducible_prod_lI:

753 assumes birr: "irreducible G b"

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

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

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

757 apply (subst m_comm, simp+)

758 apply (intro irreducible_prod_rI assms)

759 done

761 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:

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

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

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

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

766 shows P

767 using irr

768 proof (elim irreducibleE)

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

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

771 show P

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

773 case aunit: True

774 have "irreducible G b"

775 proof (rule irreducibleI, rule notI)

776 assume "b \<in> Units G"

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

778 with abnunit show "False" ..

779 next

780 fix c

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

782 and "properfactor G c b"

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

784 with ccarr show "c \<in> Units G" by (fast intro: isunit)

785 qed

786 with aunit show "P" by (rule e2)

787 next

788 case anunit: False

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

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

791 then have bunit: "b \<in> Units G" by (intro isunit, simp)

793 have "irreducible G a"

794 proof (rule irreducibleI, rule notI)

795 assume "a \<in> Units G"

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

797 with abnunit show "False" ..

798 next

799 fix c

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

801 and "properfactor G c a"

802 then have "properfactor G c (a \<otimes> b)"

803 by (simp add: properfactor_prod_r[of c a b])

804 with ccarr show "c \<in> Units G" by (fast intro: isunit)

805 qed

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

807 qed

808 qed

811 subsubsection \<open>Prime elements\<close>

813 lemma primeI:

814 fixes G (structure)

815 assumes "p \<notin> Units G"

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

817 shows "prime G p"

818 using assms unfolding prime_def by blast

820 lemma primeE:

821 fixes G (structure)

822 assumes pprime: "prime G p"

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

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

825 shows "P"

826 using pprime unfolding prime_def by (blast dest: e)

828 lemma (in comm_monoid_cancel) prime_divides:

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

830 and pprime: "prime G p"

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

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

833 using assms by (blast elim: primeE)

835 lemma (in monoid_cancel) prime_cong [trans]:

836 assumes pprime: "prime G p"

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

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

839 shows "prime G p'"

840 using pprime

841 apply (elim primeE, intro primeI)

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

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

844 done

847 subsection \<open>Factorization and Factorial Monoids\<close>

849 subsubsection \<open>Function definitions\<close>

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

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

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

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

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

858 where "list_assoc G \<equiv> list_all2 (\<sim>\<^bsub>G\<^esub>)"

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

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

864 locale factorial_monoid = comm_monoid_cancel +

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

866 and factors_unique:

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

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

871 subsubsection \<open>Comparing lists of elements\<close>

873 text \<open>Association on lists\<close>

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

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

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

878 using assms by (induct as) simp_all

880 lemma (in monoid) listassoc_sym [sym]:

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

882 and "set as \<subseteq> carrier G"

883 and "set bs \<subseteq> carrier G"

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

885 using assms

886 proof (induct as arbitrary: bs, simp)

887 case Cons

888 then show ?case

889 apply (induct bs)

890 apply simp

891 apply clarsimp

892 apply (iprover intro: associated_sym)

893 done

894 qed

896 lemma (in monoid) listassoc_trans [trans]:

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

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

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

900 using assms

901 apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)

902 apply (rule associated_trans)

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

904 apply (simp, simp)

905 apply blast+

906 done

908 lemma (in monoid_cancel) irrlist_listassoc_cong:

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

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

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

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

913 using assms

914 apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)

915 apply (blast intro: irreducible_cong)

916 done

919 text \<open>Permutations\<close>

921 lemma perm_map [intro]:

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

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

924 using p by induct auto

926 lemma perm_map_switch:

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

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

929 using p m by (induct arbitrary: a) (simp, force, force, blast)

931 lemma (in monoid) perm_assoc_switch:

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

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

934 using p a

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

936 apply (clarsimp simp add: list_all2_Cons2, blast)

937 apply (clarsimp simp add: list_all2_Cons2)

938 apply blast

939 apply blast

940 done

942 lemma (in monoid) perm_assoc_switch_r:

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

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

945 using p a

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

947 apply (clarsimp simp add: list_all2_Cons1, blast)

948 apply (clarsimp simp add: list_all2_Cons1)

949 apply blast

950 apply blast

951 done

953 declare perm_sym [sym]

955 lemma perm_setP:

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

957 and as: "P (set as)"

958 shows "P (set bs)"

959 proof -

960 from perm have "mset as = mset bs"

961 by (simp add: mset_eq_perm)

962 then have "set as = set bs"

963 by (rule mset_eq_setD)

964 with as show "P (set bs)"

965 by simp

966 qed

968 lemmas (in monoid) perm_closed = perm_setP[of _ _ "\<lambda>as. as \<subseteq> carrier G"]

970 lemmas (in monoid) irrlist_perm_cong = perm_setP[of _ _ "\<lambda>as. \<forall>a\<in>as. irreducible G a"]

973 text \<open>Essentially equal factorizations\<close>

975 lemma (in monoid) essentially_equalI:

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

977 shows "essentially_equal G fs1 fs2"

978 using ex unfolding essentially_equal_def by fast

980 lemma (in monoid) essentially_equalE:

981 assumes ee: "essentially_equal G fs1 fs2"

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

983 shows "P"

984 using ee unfolding essentially_equal_def by (fast intro: e)

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

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

988 shows "essentially_equal G as as"

989 using carr by (fast intro: essentially_equalI)

991 lemma (in monoid) ee_sym [sym]:

992 assumes ee: "essentially_equal G as bs"

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

994 shows "essentially_equal G bs as"

995 using ee

996 proof (elim essentially_equalE)

997 fix fs

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

999 from perm_assoc_switch_r [OF this] obtain fs' where a: "as [\<sim>] fs'" and p: "fs' <~~> bs"

1000 by blast

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

1002 with a[symmetric] carr show ?thesis

1003 by (iprover intro: essentially_equalI perm_closed)

1004 qed

1006 lemma (in monoid) ee_trans [trans]:

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

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

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

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

1011 shows "essentially_equal G as cs"

1012 using ab bc

1013 proof (elim essentially_equalE)

1014 fix abs bcs

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

1016 from perm_assoc_switch [OF this] obtain bs' where p: "abs <~~> bs'" and a: "bs' [\<sim>] bcs"

1017 by blast

1019 assume "as <~~> abs"

1020 with p have pp: "as <~~> bs'" by fast

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

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

1024 note a

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

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

1027 with pp show ?thesis

1028 by (rule essentially_equalI)

1029 qed

1032 subsubsection \<open>Properties of lists of elements\<close>

1034 text \<open>Multiplication of factors in a list\<close>

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

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

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

1039 using ascarr by (induct fs) simp_all

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

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

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

1044 using assms

1045 apply (induct fs)

1046 apply simp

1047 apply (case_tac "f = a")

1048 apply simp

1049 apply (fast intro: dividesI)

1050 apply clarsimp

1051 apply (metis assms(2) divides_prod_l multlist_closed)

1052 done

1054 lemma (in comm_monoid_cancel) multlist_listassoc_cong:

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

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

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

1058 using assms

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

1060 case (Cons a as fs')

1061 then show ?case

1062 apply (induct fs', simp)

1063 proof clarsimp

1064 fix b bs

1065 assume "a \<sim> b"

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

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

1068 then have p: "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) as \<one>"

1069 by (fast intro: mult_cong_l)

1070 also

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

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

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

1074 then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by simp

1075 with ascarr bscarr bcarr have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"

1076 by (fast intro: mult_cong_r)

1077 finally show "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"

1078 by (simp add: ascarr bscarr acarr bcarr)

1079 qed

1080 qed

1082 lemma (in comm_monoid) multlist_perm_cong:

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

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

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

1086 using prm ascarr

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

1088 proof clarsimp

1089 fix xs ys zs

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

1091 then have "set ys \<subseteq> carrier G" by (rule perm_closed)

1092 moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>"

1093 ultimately show "foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>" by simp

1094 qed

1096 lemma (in comm_monoid_cancel) multlist_ee_cong:

1097 assumes "essentially_equal G fs fs'"

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

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

1100 using assms

1101 apply (elim essentially_equalE)

1102 apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)

1103 done

1106 subsubsection \<open>Factorization in irreducible elements\<close>

1108 lemma wfactorsI:

1109 fixes G (structure)

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

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

1112 shows "wfactors G fs a"

1113 using assms unfolding wfactors_def by simp

1115 lemma wfactorsE:

1116 fixes G (structure)

1117 assumes wf: "wfactors G fs a"

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

1119 shows "P"

1120 using wf unfolding wfactors_def by (fast dest: e)

1122 lemma (in monoid) factorsI:

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

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

1125 shows "factors G fs a"

1126 using assms unfolding factors_def by simp

1128 lemma factorsE:

1129 fixes G (structure)

1130 assumes f: "factors G fs a"

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

1132 shows "P"

1133 using f unfolding factors_def by (simp add: e)

1135 lemma (in monoid) factors_wfactors:

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

1137 shows "wfactors G as a"

1138 using assms by (blast elim: factorsE intro: wfactorsI)

1140 lemma (in monoid) wfactors_factors:

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

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

1143 using assms by (blast elim: wfactorsE intro: factorsI)

1145 lemma (in monoid) factors_closed [dest]:

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

1147 shows "a \<in> carrier G"

1148 using assms by (elim factorsE, clarsimp)

1150 lemma (in monoid) nunit_factors:

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

1152 and fs: "factors G as a"

1153 shows "length as > 0"

1154 proof -

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

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

1157 qed

1159 lemma (in monoid) unit_wfactors [simp]:

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

1161 shows "wfactors G [] a"

1162 using aunit by (intro wfactorsI) (simp, simp add: Units_assoc)

1164 lemma (in comm_monoid_cancel) unit_wfactors_empty:

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

1166 and wf: "wfactors G fs a"

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

1168 shows "fs = []"

1169 proof (cases fs)

1170 case Nil

1171 then show ?thesis .

1172 next

1173 case fs: (Cons f fs')

1174 from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"

1175 by (simp_all add: fs)

1177 from fs wf have "irreducible G f" by (simp add: wfactors_def)

1178 then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)

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

1182 note aunit

1183 also from fs wf

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

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

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

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

1188 then have "f \<in> Units G" by (intro unit_factor[of f], simp+)

1189 with fnunit show ?thesis by contradiction

1190 qed

1193 text \<open>Comparing wfactors\<close>

1195 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:

1196 assumes fact: "wfactors G fs a"

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

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

1199 shows "wfactors G fs' a"

1200 using fact

1201 apply (elim wfactorsE, intro wfactorsI)

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

1203 proof -

1204 from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"

1205 by (simp add: multlist_listassoc_cong carr)

1206 also assume "foldr (\<otimes>) fs \<one> \<sim> a"

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

1208 qed

1210 lemma (in comm_monoid) wfactors_perm_cong_l:

1211 assumes "wfactors G fs a"

1212 and "fs <~~> fs'"

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

1214 shows "wfactors G fs' a"

1215 using assms

1216 apply (elim wfactorsE, intro wfactorsI)

1217 apply (rule irrlist_perm_cong, assumption+)

1218 apply (simp add: multlist_perm_cong[symmetric])

1219 done

1221 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:

1222 assumes ee: "essentially_equal G as bs"

1223 and bfs: "wfactors G bs b"

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

1225 shows "wfactors G as b"

1226 using ee

1227 proof (elim essentially_equalE)

1228 fix fs

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

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

1232 note bfs

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

1234 also (wfactors_listassoc_cong_l)

1235 note prm[symmetric]

1236 finally (wfactors_perm_cong_l)

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

1238 qed

1240 lemma (in monoid) wfactors_cong_r [trans]:

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

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

1243 shows "wfactors G fs a'"

1244 using fac

1245 proof (elim wfactorsE, intro wfactorsI)

1246 assume "foldr (\<otimes>) fs \<one> \<sim> a" also note aa'

1247 finally show "foldr (\<otimes>) fs \<one> \<sim> a'" by simp

1248 qed

1251 subsubsection \<open>Essentially equal factorizations\<close>

1253 lemma (in comm_monoid_cancel) unitfactor_ee:

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

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

1256 shows "essentially_equal G (as[0 := (as!0 \<otimes> u)]) as"

1257 (is "essentially_equal G ?as' as")

1258 using assms

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

1260 apply (cases as, simp)

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

1262 done

1264 lemma (in comm_monoid_cancel) factors_cong_unit:

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

1266 and anunit: "a \<notin> Units G"

1267 and afs: "factors G as a"

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

1269 shows "factors G (as[0 := (as!0 \<otimes> u)]) (a \<otimes> u)"

1270 (is "factors G ?as' ?a'")

1271 using assms

1272 apply (elim factorsE, clarify)

1273 apply (cases as)

1274 apply (simp add: nunit_factors)

1275 apply clarsimp

1276 apply (elim factorsE, intro factorsI)

1277 apply (clarsimp, fast intro: irreducible_prod_rI)

1278 apply (simp add: m_ac Units_closed)

1279 done

1281 lemma (in comm_monoid) perm_wfactorsD:

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

1283 and afs: "wfactors G as a"

1284 and bfs: "wfactors G bs b"

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

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

1287 shows "a \<sim> b"

1288 using afs bfs

1289 proof (elim wfactorsE)

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

1291 assume "foldr (\<otimes>) as \<one> \<sim> a"

1292 then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)

1293 also from prm

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

1295 also assume "foldr (\<otimes>) bs \<one> \<sim> b"

1296 finally show "a \<sim> b" by simp

1297 qed

1299 lemma (in comm_monoid_cancel) listassoc_wfactorsD:

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

1301 and afs: "wfactors G as a"

1302 and bfs: "wfactors G bs b"

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

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

1305 shows "a \<sim> b"

1306 using afs bfs

1307 proof (elim wfactorsE)

1308 assume "foldr (\<otimes>) as \<one> \<sim> a"

1309 then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)

1310 also from assoc

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

1312 also assume "foldr (\<otimes>) bs \<one> \<sim> b"

1313 finally show "a \<sim> b" by simp

1314 qed

1316 lemma (in comm_monoid_cancel) ee_wfactorsD:

1317 assumes ee: "essentially_equal G as bs"

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

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

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

1321 shows "a \<sim> b"

1322 using ee

1323 proof (elim essentially_equalE)

1324 fix fs

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

1326 then have as'carr[simp]: "set fs \<subseteq> carrier G"

1327 by (simp add: perm_closed)

1328 from afs prm have afs': "wfactors G fs a"

1329 by (rule wfactors_perm_cong_l) simp

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

1331 from this afs' bfs show "a \<sim> b"

1332 by (rule listassoc_wfactorsD) simp_all

1333 qed

1335 lemma (in comm_monoid_cancel) ee_factorsD:

1336 assumes ee: "essentially_equal G as bs"

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

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

1339 shows "a \<sim> b"

1340 using assms by (blast intro: factors_wfactors dest: ee_wfactorsD)

1342 lemma (in factorial_monoid) ee_factorsI:

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

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

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

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

1347 shows "essentially_equal G as bs"

1348 proof -

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

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

1352 from ab carr obtain u where uunit: "u \<in> Units G" and a: "a = b \<otimes> u"

1353 by (elim associatedE2)

1355 from uunit bscarr have ee: "essentially_equal G (bs[0 := (bs!0 \<otimes> u)]) bs"

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

1357 by (rule unitfactor_ee)

1359 from bscarr uunit have bs'carr: "set ?bs' \<subseteq> carrier G"

1360 by (cases bs) (simp_all add: Units_closed)

1362 from uunit bnunit bfs bscarr have fac: "factors G ?bs' (b \<otimes> u)"

1363 by (rule factors_cong_unit)

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

1366 have "essentially_equal G as ?bs'"

1367 by (blast intro: factors_unique)

1368 also note ee

1369 finally show "essentially_equal G as bs"

1370 by (simp add: ascarr bscarr bs'carr)

1371 qed

1373 lemma (in factorial_monoid) ee_wfactorsI:

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

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

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

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

1378 shows "essentially_equal G as bs"

1379 using assms

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

1381 case aunit: True

1382 also note asc

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

1385 from aunit asf ascarr have e: "as = []"

1386 by (rule unit_wfactors_empty)

1387 from bunit bsf bscarr have e': "bs = []"

1388 by (rule unit_wfactors_empty)

1390 have "essentially_equal G [] []"

1391 by (fast intro: essentially_equalI)

1392 then show ?thesis

1393 by (simp add: e e')

1394 next

1395 case anunit: False

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

1397 proof clarify

1398 assume "b \<in> Units G"

1399 also note asc[symmetric]

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

1401 with anunit show False ..

1402 qed

1404 from wfactors_factors[OF asf ascarr] obtain a' where fa': "factors G as a'" and a': "a' \<sim> a"

1405 by blast

1406 from fa' ascarr have a'carr[simp]: "a' \<in> carrier G"

1407 by fast

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

1410 proof clarify

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

1412 also note a'

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

1414 with anunit

1415 show "False" ..

1416 qed

1418 from wfactors_factors[OF bsf bscarr] obtain b' where fb': "factors G bs b'" and b': "b' \<sim> b"

1419 by blast

1420 from fb' bscarr have b'carr[simp]: "b' \<in> carrier G"

1421 by fast

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

1424 proof clarify

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

1426 also note b'

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

1428 with bnunit show False ..

1429 qed

1431 note a'

1432 also note asc

1433 also note b'[symmetric]

1434 finally have "a' \<sim> b'" by simp

1435 from this fa' a'nunit fb' b'nunit ascarr bscarr show "essentially_equal G as bs"

1436 by (rule ee_factorsI)

1437 qed

1439 lemma (in factorial_monoid) ee_wfactors:

1440 assumes asf: "wfactors G as a"

1441 and bsf: "wfactors G bs b"

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

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

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

1445 using assms by (fast intro: ee_wfactorsI ee_wfactorsD)

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

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

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

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

1451 case True

1452 then have "wfactors G [] a" by (rule unit_wfactors)

1453 then show ?thesis by (intro exI) force

1454 next

1455 case False

1456 with factors_exist [OF acarr] obtain fs where fscarr: "set fs \<subseteq> carrier G" and f: "factors G fs a"

1457 by blast

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

1459 with fscarr show ?thesis by fast

1460 qed

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

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

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

1465 unfolding wfactors_def using assms by blast

1467 lemma (in factorial_monoid) wfactors_unique:

1468 assumes "wfactors G fs a"

1469 and "wfactors G fs' a"

1470 and "a \<in> carrier G"

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

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

1473 shows "essentially_equal G fs fs'"

1474 using assms by (fast intro: ee_wfactorsI[of a a])

1476 lemma (in monoid) factors_mult_single:

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

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

1479 using assms unfolding factors_def by simp

1481 lemma (in monoid_cancel) wfactors_mult_single:

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

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

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

1485 using assms unfolding wfactors_def by (simp add: mult_cong_r)

1487 lemma (in monoid) factors_mult:

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

1489 and ascarr: "set fa \<subseteq> carrier G"

1490 and bscarr: "set fb \<subseteq> carrier G"

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

1492 using assms

1493 unfolding factors_def

1494 apply safe

1495 apply force

1496 apply hypsubst_thin

1497 apply (induct fa)

1498 apply simp

1499 apply (simp add: m_assoc)

1500 done

1502 lemma (in comm_monoid_cancel) wfactors_mult [intro]:

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

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

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

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

1507 using wfactors_factors[OF asf ascarr] and wfactors_factors[OF bsf bscarr]

1508 proof clarsimp

1509 fix a' b'

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

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

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

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

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

1517 from asf' bsf' have "factors G (as @ bs) (a' \<otimes> b')"

1518 by (rule factors_mult) fact+

1520 with carr have abf': "wfactors G (as @ bs) (a' \<otimes> b')"

1521 by (intro factors_wfactors) simp_all

1522 also from b'b carr have trb: "a' \<otimes> b' \<sim> a' \<otimes> b"

1523 by (intro mult_cong_r)

1524 also from a'a carr have tra: "a' \<otimes> b \<sim> a \<otimes> b"

1525 by (intro mult_cong_l)

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

1527 by (simp add: carr)

1528 qed

1530 lemma (in comm_monoid) factors_dividesI:

1531 assumes "factors G fs a"

1532 and "f \<in> set fs"

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

1534 shows "f divides a"

1535 using assms by (fast elim: factorsE intro: multlist_dividesI)

1537 lemma (in comm_monoid) wfactors_dividesI:

1538 assumes p: "wfactors G fs a"

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

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

1541 shows "f divides a"

1542 using wfactors_factors[OF p fscarr]

1543 proof clarsimp

1544 fix a'

1545 assume fsa': "factors G fs a'" and a'a: "a' \<sim> a"

1546 with fscarr have a'carr: "a' \<in> carrier G"

1547 by (simp add: factors_closed)

1549 from fsa' fscarr f have "f divides a'"

1550 by (fast intro: factors_dividesI)

1551 also note a'a

1552 finally show "f divides a"

1553 by (simp add: f fscarr[THEN subsetD] acarr a'carr)

1554 qed

1557 subsubsection \<open>Factorial monoids and wfactors\<close>

1559 lemma (in comm_monoid_cancel) factorial_monoidI:

1560 assumes wfactors_exists: "\<And>a. a \<in> carrier G \<Longrightarrow> \<exists>fs. set fs \<subseteq> carrier G \<and> wfactors G fs a"

1561 and wfactors_unique:

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

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

1564 shows "factorial_monoid G"

1565 proof

1566 fix a

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

1569 from wfactors_exists[OF acarr]

1570 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

1571 by blast

1572 from wfactors_factors [OF afs ascarr] obtain a' where afs': "factors G as a'" and a'a: "a' \<sim> a"

1573 by blast

1574 from afs' ascarr have a'carr: "a' \<in> carrier G"

1575 by fast

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

1577 proof clarify

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

1579 also note a'a

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

1581 with anunit show False ..

1582 qed

1584 from a'carr acarr a'a obtain u where uunit: "u \<in> Units G" and a': "a' = a \<otimes> u"

1585 by (blast elim: associatedE2)

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

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

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

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

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

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

1595 by (cases as) auto

1597 from afs' uunit a'nunit acarr ascarr have "factors G (as[0:=(as!0 \<otimes> inv u)]) a"

1598 by (simp add: a factors_cong_unit)

1599 with cr show "\<exists>fs. set fs \<subseteq> carrier G \<and> factors G fs a"

1600 by fast

1601 qed (blast intro: factors_wfactors wfactors_unique)

1604 subsection \<open>Factorizations as Multisets\<close>

1606 text \<open>Gives useful operations like intersection\<close>

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

1610 abbreviation "assocs G x \<equiv> eq_closure_of (division_rel G) {x}"

1612 definition "fmset G as = mset (map (\<lambda>a. assocs G a) as)"

1615 text \<open>Helper lemmas\<close>

1617 lemma (in monoid) assocs_repr_independence:

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

1619 and "x \<in> carrier G"

1620 shows "assocs G x = assocs G y"

1621 using assms

1622 apply safe

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

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

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

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

1627 done

1629 lemma (in monoid) assocs_self:

1630 assumes "x \<in> carrier G"

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

1632 using assms by (fastforce intro: closure_ofI2)

1634 lemma (in monoid) assocs_repr_independenceD:

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

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

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

1638 unfolding repr using ycarr by (intro assocs_self)

1640 lemma (in comm_monoid) assocs_assoc:

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

1642 and "b \<in> carrier G"

1643 shows "a \<sim> b"

1644 using assms by (elim closure_ofE2) simp

1646 lemmas (in comm_monoid) assocs_eqD = assocs_repr_independenceD[THEN assocs_assoc]

1649 subsubsection \<open>Comparing multisets\<close>

1651 lemma (in monoid) fmset_perm_cong:

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

1653 shows "fmset G as = fmset G bs"

1654 using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast

1656 lemma (in comm_monoid_cancel) eqc_listassoc_cong:

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

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

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

1660 using assms

1661 apply (induct as arbitrary: bs, simp)

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

1663 apply (clarsimp elim!: closure_ofE2) defer 1

1664 apply (clarsimp elim!: closure_ofE2) defer 1

1665 proof -

1666 fix a x z

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

1668 assume "x \<sim> a"

1669 also assume "a \<sim> z"

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

1671 with carr show "x \<in> assocs G z"

1672 by (intro closure_ofI2) simp_all

1673 next

1674 fix a x z

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

1676 assume "x \<sim> z"

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

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

1679 with carr show "x \<in> assocs G a"

1680 by (intro closure_ofI2) simp_all

1681 qed

1683 lemma (in comm_monoid_cancel) fmset_listassoc_cong:

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

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

1686 shows "fmset G as = fmset G bs"

1687 using assms unfolding fmset_def by (simp add: eqc_listassoc_cong)

1689 lemma (in comm_monoid_cancel) ee_fmset:

1690 assumes ee: "essentially_equal G as bs"

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

1692 shows "fmset G as = fmset G bs"

1693 using ee

1694 proof (elim essentially_equalE)

1695 fix as'

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

1697 from prm ascarr have as'carr: "set as' \<subseteq> carrier G"

1698 by (rule perm_closed)

1700 from prm have "fmset G as = fmset G as'"

1701 by (rule fmset_perm_cong)

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

1703 with as'carr bscarr have "fmset G as' = fmset G bs"

1704 by (simp add: fmset_listassoc_cong)

1705 finally show "fmset G as = fmset G bs" .

1706 qed

1708 lemma (in monoid_cancel) fmset_ee__hlp_induct:

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

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

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

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

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

1714 apply safe

1715 apply (simp_all del: mset_map)

1716 apply (simp add: map_eq_Cons_conv)

1717 apply blast

1718 apply force

1719 proof -

1720 fix ys as bs

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

1722 and r1[rule_format]:

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

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

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

1726 and r2[rule_format]: "\<forall>as bsa. ys = map (assocs G) as \<and> map (assocs G) bs = map (assocs G) bsa

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

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

1730 from p1 have "mset (map (assocs G) as) = mset ys"

1731 by (simp add: mset_eq_perm del: mset_map)

1732 then have setys: "set (map (assocs G) as) = set ys"

1733 by (rule mset_eq_setD)

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

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

1737 then have "\<exists>yy. ys = map (assocs G) yy"

1738 proof (induct ys)

1739 case Nil

1740 then show ?case by simp

1741 next

1742 case Cons

1743 then show ?case

1744 proof clarsimp

1745 fix yy x

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

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

1748 qed

1749 qed

1750 then obtain yy where ys: "ys = map (assocs G) yy" ..

1752 from p1 ys have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"

1753 by (intro r1) simp

1754 then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy"

1755 by auto

1757 from p2 ys have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"

1758 by (intro r2) simp

1759 then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs"

1760 by auto

1762 from perm_map_switch [OF as'yy yyas'']

1763 obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''"

1764 by blast

1766 from asas' and as'cs have ascs: "as <~~> cs"

1767 by fast

1768 from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs"

1769 by simp

1770 with ascs show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"

1771 by fast

1772 qed

1774 lemma (in comm_monoid_cancel) fmset_ee:

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

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

1777 shows "essentially_equal G as bs"

1778 proof -

1779 from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs"

1780 by (simp add: fmset_def mset_eq_perm del: mset_map)

1782 define cas where "cas = map (assocs G) as"

1783 define cbs where "cbs = map (assocs G) bs"

1785 from cas_def cbs_def mpp have [rule_format]:

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

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

1788 by (intro fmset_ee__hlp_induct, simp+)

1789 with mpp cas_def cbs_def have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"

1790 by simp

1792 then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"

1793 by auto

1794 from tm have lene: "length as' = length bs"

1795 by (rule map_eq_imp_length_eq)

1796 from tp have "set as = set as'"

1797 by (simp add: mset_eq_perm mset_eq_setD)

1798 with ascarr have as'carr: "set as' \<subseteq> carrier G"

1799 by simp

1801 from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\<sim>] bs"

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

1803 with tp show "essentially_equal G as bs"

1804 by (fast intro: essentially_equalI)

1805 qed

1807 lemma (in comm_monoid_cancel) ee_is_fmset:

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

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

1810 using assms by (fast intro: ee_fmset fmset_ee)

1813 subsubsection \<open>Interpreting multisets as factorizations\<close>

1815 lemma (in monoid) mset_fmsetEx:

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

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

1818 proof -

1819 from surjE[OF surj_mset] obtain Cs' where Cs: "Cs = mset Cs'"

1820 by blast

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

1822 using elems

1823 unfolding Cs

1824 apply (induct Cs', simp)

1825 proof (clarsimp simp del: mset_map)

1826 fix a Cs' cs

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

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

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

1830 from ih obtain c where cP: "P c" and a: "a = assocs G c"

1831 by auto

1832 from cP csP have tP: "\<forall>x\<in>set (c#cs). P x"

1833 by simp

1834 from mset a have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')"

1835 by simp

1836 with tP show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and> mset (map (assocs G) cs) = add_mset a (mset Cs')"

1837 by fast

1838 qed

1839 then show ?thesis by (simp add: fmset_def)

1840 qed

1842 lemma (in monoid) mset_wfactorsEx:

1843 assumes elems: "\<And>X. X \<in> set_mset Cs \<Longrightarrow> \<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

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

1845 proof -

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

1847 by (intro mset_fmsetEx, rule elems)

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

1849 and Cs[symmetric]: "fmset G cs = Cs" by auto

1850 from p have cscarr: "set cs \<subseteq> carrier G" by fast

1851 from p have "\<exists>c. c \<in> carrier G \<and> wfactors G cs c"

1852 by (intro wfactors_prod_exists) auto

1853 then obtain c where ccarr: "c \<in> carrier G" and cfs: "wfactors G cs c" by auto

1854 with cscarr Cs show ?thesis by fast

1855 qed

1858 subsubsection \<open>Multiplication on multisets\<close>

1860 lemma (in factorial_monoid) mult_wfactors_fmset:

1861 assumes afs: "wfactors G as a"

1862 and bfs: "wfactors G bs b"

1863 and cfs: "wfactors G cs (a \<otimes> b)"

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

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

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

1867 proof -

1868 from assms have "wfactors G (as @ bs) (a \<otimes> b)"

1869 by (intro wfactors_mult)

1870 with carr cfs have "essentially_equal G cs (as@bs)"

1871 by (intro ee_wfactorsI[of "a\<otimes>b" "a\<otimes>b"]) simp_all

1872 with carr have "fmset G cs = fmset G (as@bs)"

1873 by (intro ee_fmset) simp_all

1874 also have "fmset G (as@bs) = fmset G as + fmset G bs"

1875 by (simp add: fmset_def)

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

1877 qed

1879 lemma (in factorial_monoid) mult_factors_fmset:

1880 assumes afs: "factors G as a"

1881 and bfs: "factors G bs b"

1882 and cfs: "factors G cs (a \<otimes> b)"

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

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

1885 using assms by (blast intro: factors_wfactors mult_wfactors_fmset)

1887 lemma (in comm_monoid_cancel) fmset_wfactors_mult:

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

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

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

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

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

1893 proof -

1894 from carr fs have m: "wfactors G (as @ bs) (a \<otimes> b)"

1895 by (intro wfactors_mult)

1897 from mset have "fmset G cs = fmset G (as@bs)"

1898 by (simp add: fmset_def)

1899 then have "essentially_equal G cs (as@bs)"

1900 by (rule fmset_ee) (simp_all add: carr)

1901 then show "c \<sim> a \<otimes> b"

1902 by (rule ee_wfactorsD[of "cs" "as@bs"]) (simp_all add: assms m)

1903 qed

1906 subsubsection \<open>Divisibility on multisets\<close>

1908 lemma (in factorial_monoid) divides_fmsubset:

1909 assumes ab: "a divides b"

1910 and afs: "wfactors G as a"

1911 and bfs: "wfactors G bs b"

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

1913 shows "fmset G as \<subseteq># fmset G bs"

1914 using ab

1915 proof (elim dividesE)

1916 fix c

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

1918 from wfactors_exist [OF this]

1919 obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

1920 by blast

1921 note carr = carr ccarr cscarr

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

1924 with afs bfs cfs carr have "fmset G bs = fmset G as + fmset G cs"

1925 by (intro mult_wfactors_fmset[OF afs cfs]) simp_all

1926 then show ?thesis by simp

1927 qed

1929 lemma (in comm_monoid_cancel) fmsubset_divides:

1930 assumes msubset: "fmset G as \<subseteq># fmset G bs"

1931 and afs: "wfactors G as a"

1932 and bfs: "wfactors G bs b"

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

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

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

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

1937 shows "a divides b"

1938 proof -

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

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

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

1943 proof (intro mset_wfactorsEx, simp)

1944 fix X

1945 assume "X \<in># fmset G bs - fmset G as"

1946 then have "X \<in># fmset G bs" by (rule in_diffD)

1947 then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)

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

1949 then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto

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

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

1953 from xcarr and xirr and X show "\<exists>x. x \<in> carrier G \<and> irreducible G x \<and> X = assocs G x"

1954 by fast

1955 qed

1956 then obtain c cs

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

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

1959 and csf: "wfactors G cs c"

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

1962 from csmset msubset

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

1964 by (simp add: multiset_eq_iff subseteq_mset_def)

1965 then have basc: "b \<sim> a \<otimes> c"

1966 by (rule fmset_wfactors_mult) fact+

1967 then show ?thesis

1968 proof (elim associatedE2)

1969 fix u

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

1971 with acarr ccarr show "a divides b"

1972 by (fast intro: dividesI[of "c \<otimes> u"] m_assoc)

1973 qed (simp_all add: acarr bcarr ccarr)

1974 qed

1976 lemma (in factorial_monoid) divides_as_fmsubset:

1977 assumes "wfactors G as a"

1978 and "wfactors G bs b"

1979 and "a \<in> carrier G"

1980 and "b \<in> carrier G"

1981 and "set as \<subseteq> carrier G"

1982 and "set bs \<subseteq> carrier G"

1983 shows "a divides b = (fmset G as \<subseteq># fmset G bs)"

1984 using assms

1985 by (blast intro: divides_fmsubset fmsubset_divides)

1988 text \<open>Proper factors on multisets\<close>

1990 lemma (in factorial_monoid) fmset_properfactor:

1991 assumes asubb: "fmset G as \<subseteq># fmset G bs"

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

1993 and "wfactors G as a"

1994 and "wfactors G bs b"

1995 and "a \<in> carrier G"

1996 and "b \<in> carrier G"

1997 and "set as \<subseteq> carrier G"

1998 and "set bs \<subseteq> carrier G"

1999 shows "properfactor G a b"

2000 apply (rule properfactorI)

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

2002 proof

2003 assume "b divides a"

2004 then have "fmset G bs \<subseteq># fmset G as"

2005 by (rule divides_fmsubset) fact+

2006 with asubb have "fmset G as = fmset G bs"

2007 by (rule subset_mset.antisym)

2008 with anb show False ..

2009 qed

2011 lemma (in factorial_monoid) properfactor_fmset:

2012 assumes pf: "properfactor G a b"

2013 and "wfactors G as a"

2014 and "wfactors G bs b"

2015 and "a \<in> carrier G"

2016 and "b \<in> carrier G"

2017 and "set as \<subseteq> carrier G"

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

2019 shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"

2020 using pf

2021 apply (elim properfactorE)

2022 apply rule

2023 apply (intro divides_fmsubset, assumption)

2024 apply (rule assms)+

2025 using assms(2,3,4,6,7) divides_as_fmsubset

2026 apply auto

2027 done

2029 subsection \<open>Irreducible Elements are Prime\<close>

2031 lemma (in factorial_monoid) irreducible_prime:

2032 assumes pirr: "irreducible G p"

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

2034 shows "prime G p"

2035 using pirr

2036 proof (elim irreducibleE, intro primeI)

2037 fix a b

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

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

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

2041 assume irreduc[rule_format]:

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

2043 from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"

2044 by (rule dividesE)

2046 from wfactors_exist [OF acarr]

2047 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2048 by blast

2050 from wfactors_exist [OF bcarr]

2051 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"

2052 by auto

2054 from wfactors_exist [OF ccarr]

2055 obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

2056 by auto

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

2060 from afs and bfs have abfs: "wfactors G (as @ bs) (a \<otimes> b)"

2061 by (rule wfactors_mult) fact+

2063 from pirr cfs have pcfs: "wfactors G (p # cs) (p \<otimes> c)"

2064 by (rule wfactors_mult_single) fact+

2065 with abpc have abfs': "wfactors G (p # cs) (a \<otimes> b)"

2066 by simp

2068 from abfs' abfs have "essentially_equal G (p # cs) (as @ bs)"

2069 by (rule wfactors_unique) simp+

2071 then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"

2072 by (fast elim: essentially_equalE)

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

2074 by (simp add: perm_set_eq[symmetric])

2075 with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"

2076 unfolding list_all2_conv_all_nth set_conv_nth by force

2077 then consider "p' \<in> set as" | "p' \<in> set bs" by auto

2078 then show "p divides a \<or> p divides b"

2079 proof cases

2080 case 1

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

2083 note pp'

2084 also from afs

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

2086 finally have "p divides a" by simp

2087 then show ?thesis ..

2088 next

2089 case 2

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

2092 note pp'

2093 also from bfs

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

2095 finally have "p divides b" by simp

2096 then show ?thesis ..

2097 qed

2098 qed

2101 \<comment> \<open>A version using @{const factors}, more complicated\<close>

2102 lemma (in factorial_monoid) factors_irreducible_prime:

2103 assumes pirr: "irreducible G p"

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

2105 shows "prime G p"

2106 using pirr

2107 apply (elim irreducibleE, intro primeI)

2108 apply assumption

2109 proof -

2110 fix a b

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

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

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

2114 assume irreduc[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"

2115 from pdvdab obtain c where ccarr: "c \<in> carrier G" and abpc: "a \<otimes> b = p \<otimes> c"

2116 by (rule dividesE)

2117 note [simp] = pcarr acarr bcarr ccarr

2119 show "p divides a \<or> p divides b"

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

2121 case aunit: True

2123 note pdvdab

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

2125 also from aunit have bab: "b \<otimes> a \<sim> b"

2126 by (intro associatedI2[of "a"], simp+)

2127 finally have "p divides b" by simp

2128 then show ?thesis ..

2129 next

2130 case anunit: False

2131 show ?thesis

2132 proof (cases "b \<in> Units G")

2133 case bunit: True

2134 note pdvdab

2135 also from bunit

2136 have baa: "a \<otimes> b \<sim> a"

2137 by (intro associatedI2[of "b"], simp+)

2138 finally have "p divides a" by simp

2139 then show ?thesis ..

2140 next

2141 case bnunit: False

2142 have cnunit: "c \<notin> Units G"

2143 proof

2144 assume cunit: "c \<in> Units G"

2145 from bnunit have "properfactor G a (a \<otimes> b)"

2146 by (intro properfactorI3[of _ _ b], simp+)

2147 also note abpc

2148 also from cunit have "p \<otimes> c \<sim> p"

2149 by (intro associatedI2[of c], simp+)

2150 finally have "properfactor G a p" by simp

2151 with acarr have "a \<in> Units G" by (fast intro: irreduc)

2152 with anunit show False ..

2153 qed

2155 have abnunit: "a \<otimes> b \<notin> Units G"

2156 proof clarsimp

2157 assume "a \<otimes> b \<in> Units G"

2158 then have "a \<in> Units G" by (rule unit_factor) fact+

2159 with anunit show False ..

2160 qed

2162 from factors_exist [OF acarr anunit]

2163 obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"

2164 by blast

2166 from factors_exist [OF bcarr bnunit]

2167 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"

2168 by blast

2170 from factors_exist [OF ccarr cnunit]

2171 obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c"

2172 by auto

2174 note [simp] = ascarr bscarr cscarr

2176 from afac and bfac have abfac: "factors G (as @ bs) (a \<otimes> b)"

2177 by (rule factors_mult) fact+

2179 from pirr cfac have pcfac: "factors G (p # cs) (p \<otimes> c)"

2180 by (rule factors_mult_single) fact+

2181 with abpc have abfac': "factors G (p # cs) (a \<otimes> b)"

2182 by simp

2184 from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)"

2185 by (rule factors_unique) (fact | simp)+

2186 then obtain ds where "p # cs <~~> ds" and dsassoc: "ds [\<sim>] (as @ bs)"

2187 by (fast elim: essentially_equalE)

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

2189 by (simp add: perm_set_eq[symmetric])

2190 with dsassoc obtain p' where "p' \<in> set (as@bs)" and pp': "p \<sim> p'"

2191 unfolding list_all2_conv_all_nth set_conv_nth by force

2192 then consider "p' \<in> set as" | "p' \<in> set bs" by auto

2193 then show "p divides a \<or> p divides b"

2194 proof cases

2195 case 1

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

2198 note pp'

2199 also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+

2200 finally have "p divides a" by simp

2201 then show ?thesis ..

2202 next

2203 case 2

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

2206 note pp'

2207 also from bfac

2208 have "p' divides b" by (rule factors_dividesI) fact+

2209 finally have "p divides b" by simp

2210 then show ?thesis ..

2211 qed

2212 qed

2213 qed

2214 qed

2217 subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>

2219 subsubsection \<open>Definitions\<close>

2221 definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)

2222 where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>

2223 (\<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))"

2225 definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)

2226 where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>

2227 (\<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))"

2229 definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2230 where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"

2232 definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2233 where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"

2235 definition "SomeGcd G A = inf (division_rel G) A"

2238 locale gcd_condition_monoid = comm_monoid_cancel +

2239 assumes gcdof_exists: "\<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> carrier G \<and> c gcdof a b"

2241 locale primeness_condition_monoid = comm_monoid_cancel +

2242 assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"

2244 locale divisor_chain_condition_monoid = comm_monoid_cancel +

2245 assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"

2248 subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>

2250 lemma gcdof_greatestLower:

2251 fixes G (structure)

2252 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2253 shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"

2254 by (auto simp: isgcd_def greatest_def Lower_def elem_def)

2256 lemma lcmof_leastUpper:

2257 fixes G (structure)

2258 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2259 shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"

2260 by (auto simp: islcm_def least_def Upper_def elem_def)

2262 lemma somegcd_meet:

2263 fixes G (structure)

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

2265 shows "somegcd G a b = meet (division_rel G) a b"

2266 by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])

2268 lemma (in monoid) isgcd_divides_l:

2269 assumes "a divides b"

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

2271 shows "a gcdof a b"

2272 using assms unfolding isgcd_def by fast

2274 lemma (in monoid) isgcd_divides_r:

2275 assumes "b divides a"

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

2277 shows "b gcdof a b"

2278 using assms unfolding isgcd_def by fast

2281 subsubsection \<open>Existence of gcd and lcm\<close>

2283 lemma (in factorial_monoid) gcdof_exists:

2284 assumes acarr: "a \<in> carrier G"

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

2286 shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2287 proof -

2288 from wfactors_exist [OF acarr]

2289 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2290 by blast

2291 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2292 by (fast elim: wfactorsE)

2294 from wfactors_exist [OF bcarr]

2295 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"

2296 by blast

2297 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2298 by (fast elim: wfactorsE)

2300 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2301 fmset G cs = fmset G as \<inter># fmset G bs"

2302 proof (intro mset_wfactorsEx)

2303 fix X

2304 assume "X \<in># fmset G as \<inter># fmset G bs"

2305 then have "X \<in># fmset G as" by simp

2306 then have "X \<in> set (map (assocs G) as)"

2307 by (simp add: fmset_def)

2308 then have "\<exists>x. X = assocs G x \<and> x \<in> set as"

2309 by (induct as) auto

2310 then obtain x where X: "X = assocs G x" and xas: "x \<in> set as"

2311 by blast

2312 with ascarr have xcarr: "x \<in> carrier G"

2313 by blast

2314 from xas airr have xirr: "irreducible G x"

2315 by simp

2316 from xcarr and xirr and X show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2317 by blast

2318 qed

2319 then obtain c cs

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

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

2322 and csirr: "wfactors G cs c"

2323 and csmset: "fmset G cs = fmset G as \<inter># fmset G bs"

2324 by auto

2326 have "c gcdof a b"

2327 proof (simp add: isgcd_def, safe)

2328 from csmset

2329 have "fmset G cs \<subseteq># fmset G as"

2330 by (simp add: multiset_inter_def subset_mset_def)

2331 then show "c divides a" by (rule fmsubset_divides) fact+

2332 next

2333 from csmset have "fmset G cs \<subseteq># fmset G bs"

2334 by (simp add: multiset_inter_def subseteq_mset_def, force)

2335 then show "c divides b"

2336 by (rule fmsubset_divides) fact+

2337 next

2338 fix y

2339 assume "y \<in> carrier G"

2340 from wfactors_exist [OF this]

2341 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2342 by blast

2344 assume "y divides a"

2345 then have ya: "fmset G ys \<subseteq># fmset G as"

2346 by (rule divides_fmsubset) fact+

2348 assume "y divides b"

2349 then have yb: "fmset G ys \<subseteq># fmset G bs"

2350 by (rule divides_fmsubset) fact+

2352 from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"

2353 by (simp add: subset_mset_def)

2354 then show "y divides c"

2355 by (rule fmsubset_divides) fact+

2356 qed

2357 with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2358 by fast

2359 qed

2361 lemma (in factorial_monoid) lcmof_exists:

2362 assumes acarr: "a \<in> carrier G"

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

2364 shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2365 proof -

2366 from wfactors_exist [OF acarr]

2367 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2368 by blast

2369 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2370 by (fast elim: wfactorsE)

2372 from wfactors_exist [OF bcarr]

2373 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"

2374 by blast

2375 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2376 by (fast elim: wfactorsE)

2378 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2379 fmset G cs = (fmset G as - fmset G bs) + fmset G bs"

2380 proof (intro mset_wfactorsEx)

2381 fix X

2382 assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"

2383 then have "X \<in># fmset G as \<or> X \<in># fmset G bs"

2384 by (auto dest: in_diffD)

2385 then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)"

2386 by fast

2387 then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2388 proof cases

2389 case 1

2390 then have "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)

2391 then have "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto

2392 then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto

2393 with ascarr have xcarr: "x \<in> carrier G" by fast

2394 from xas airr have xirr: "irreducible G x" by simp

2395 from xcarr and xirr and X show ?thesis by fast

2396 next

2397 case 2

2398 then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)

2399 then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto

2400 then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto

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

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

2403 from xcarr and xirr and X show ?thesis by fast

2404 qed

2405 qed

2406 then obtain c cs

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

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

2409 and csirr: "wfactors G cs c"

2410 and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"

2411 by auto

2413 have "c lcmof a b"

2414 proof (simp add: islcm_def, safe)

2415 from csmset have "fmset G as \<subseteq># fmset G cs"

2416 by (simp add: subseteq_mset_def, force)

2417 then show "a divides c"

2418 by (rule fmsubset_divides) fact+

2419 next

2420 from csmset have "fmset G bs \<subseteq># fmset G cs"

2421 by (simp add: subset_mset_def)

2422 then show "b divides c"

2423 by (rule fmsubset_divides) fact+

2424 next

2425 fix y

2426 assume "y \<in> carrier G"

2427 from wfactors_exist [OF this]

2428 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2429 by blast

2431 assume "a divides y"

2432 then have ya: "fmset G as \<subseteq># fmset G ys"

2433 by (rule divides_fmsubset) fact+

2435 assume "b divides y"

2436 then have yb: "fmset G bs \<subseteq># fmset G ys"

2437 by (rule divides_fmsubset) fact+

2439 from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"

2440 apply (simp add: subseteq_mset_def, clarify)

2441 apply (case_tac "count (fmset G as) a < count (fmset G bs) a")

2442 apply simp

2443 apply simp

2444 done

2445 then show "c divides y"

2446 by (rule fmsubset_divides) fact+

2447 qed

2448 with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2449 by fast

2450 qed

2453 subsection \<open>Conditions for Factoriality\<close>

2455 subsubsection \<open>Gcd condition\<close>

2457 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:

2458 "weak_lower_semilattice (division_rel G)"

2459 proof -

2460 interpret weak_partial_order "division_rel G" ..

2461 show ?thesis

2462 apply (unfold_locales, simp_all)

2463 proof -

2464 fix x y

2465 assume carr: "x \<in> carrier G" "y \<in> carrier G"

2466 from gcdof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"

2467 by blast

2468 with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2469 by (subst gcdof_greatestLower[symmetric], simp+)

2470 then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2471 by fast

2472 qed

2473 qed

2475 lemma (in gcd_condition_monoid) gcdof_cong_l:

2476 assumes a'a: "a' \<sim> a"

2477 and agcd: "a gcdof b c"

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

2479 shows "a' gcdof b c"

2480 proof -

2481 note carr = a'carr carr'

2482 interpret weak_lower_semilattice "division_rel G" by simp

2483 have "a' \<in> carrier G \<and> a' gcdof b c"

2484 apply (simp add: gcdof_greatestLower carr')

2485 apply (subst greatest_Lower_cong_l[of _ a])

2486 apply (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)

2487 done

2488 then show ?thesis ..

2489 qed

2491 lemma (in gcd_condition_monoid) gcd_closed [simp]:

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

2493 shows "somegcd G a b \<in> carrier G"

2494 proof -

2495 interpret weak_lower_semilattice "division_rel G" by simp

2496 show ?thesis

2497 apply (simp add: somegcd_meet[OF carr])

2498 apply (rule meet_closed[simplified], fact+)

2499 done

2500 qed

2502 lemma (in gcd_condition_monoid) gcd_isgcd:

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

2504 shows "(somegcd G a b) gcdof a b"

2505 proof -

2506 interpret weak_lower_semilattice "division_rel G"

2507 by simp

2508 from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"

2509 apply (subst gcdof_greatestLower, simp, simp)

2510 apply (simp add: somegcd_meet[OF carr] meet_def)

2511 apply (rule inf_of_two_greatest[simplified], assumption+)

2512 done

2513 then show "(somegcd G a b) gcdof a b"

2514 by simp

2515 qed

2517 lemma (in gcd_condition_monoid) gcd_exists:

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

2519 shows "\<exists>x\<in>carrier G. x = somegcd G a b"

2520 proof -

2521 interpret weak_lower_semilattice "division_rel G"

2522 by simp

2523 show ?thesis

2524 by (metis carr(1) carr(2) gcd_closed)

2525 qed

2527 lemma (in gcd_condition_monoid) gcd_divides_l:

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

2529 shows "(somegcd G a b) divides a"

2530 proof -

2531 interpret weak_lower_semilattice "division_rel G"

2532 by simp

2533 show ?thesis

2534 by (metis carr(1) carr(2) gcd_isgcd isgcd_def)

2535 qed

2537 lemma (in gcd_condition_monoid) gcd_divides_r:

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

2539 shows "(somegcd G a b) divides b"

2540 proof -

2541 interpret weak_lower_semilattice "division_rel G"

2542 by simp

2543 show ?thesis

2544 by (metis carr gcd_isgcd isgcd_def)

2545 qed

2547 lemma (in gcd_condition_monoid) gcd_divides:

2548 assumes sub: "z divides x" "z divides y"

2549 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"

2550 shows "z divides (somegcd G x y)"

2551 proof -

2552 interpret weak_lower_semilattice "division_rel G"

2553 by simp

2554 show ?thesis

2555 by (metis gcd_isgcd isgcd_def assms)

2556 qed

2558 lemma (in gcd_condition_monoid) gcd_cong_l:

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

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

2561 shows "somegcd G x y \<sim> somegcd G x' y"

2562 proof -

2563 interpret weak_lower_semilattice "division_rel G"

2564 by simp

2565 show ?thesis

2566 apply (simp add: somegcd_meet carr)

2567 apply (rule meet_cong_l[simplified], fact+)

2568 done

2569 qed

2571 lemma (in gcd_condition_monoid) gcd_cong_r:

2572 assumes carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"

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

2574 shows "somegcd G x y \<sim> somegcd G x y'"

2575 proof -

2576 interpret weak_lower_semilattice "division_rel G" by simp

2577 show ?thesis

2578 apply (simp add: somegcd_meet carr)

2579 apply (rule meet_cong_r[simplified], fact+)

2580 done

2581 qed

2583 (*

2584 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:

2585 assumes carr: "b \<in> carrier G"

2586 shows "asc_cong (\<lambda>a. somegcd G a b)"

2587 using carr

2588 unfolding CONG_def

2589 by clarsimp (blast intro: gcd_cong_l)

2591 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:

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

2593 shows "asc_cong (\<lambda>b. somegcd G a b)"

2594 using carr

2595 unfolding CONG_def

2596 by clarsimp (blast intro: gcd_cong_r)

2598 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =

2599 assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]

2600 *)

2602 lemma (in gcd_condition_monoid) gcdI:

2603 assumes dvd: "a divides b" "a divides c"

2604 and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"

2605 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2606 shows "a \<sim> somegcd G b c"

2607 apply (simp add: somegcd_def)

2608 apply (rule someI2_ex)

2609 apply (rule exI[of _ a], simp add: isgcd_def)

2610 apply (simp add: assms)

2611 apply (simp add: isgcd_def assms, clarify)

2612 apply (insert assms, blast intro: associatedI)

2613 done

2615 lemma (in gcd_condition_monoid) gcdI2:

2616 assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"

2617 shows "a \<sim> somegcd G b c"

2618 using assms unfolding isgcd_def by (blast intro: gcdI)

2620 lemma (in gcd_condition_monoid) SomeGcd_ex:

2621 assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"

2622 shows "\<exists>x\<in> carrier G. x = SomeGcd G A"

2623 proof -

2624 interpret weak_lower_semilattice "division_rel G"

2625 by simp

2626 show ?thesis

2627 apply (simp add: SomeGcd_def)

2628 apply (rule finite_inf_closed[simplified], fact+)

2629 done

2630 qed

2632 lemma (in gcd_condition_monoid) gcd_assoc:

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

2634 shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"

2635 proof -

2636 interpret weak_lower_semilattice "division_rel G"

2637 by simp

2638 show ?thesis

2639 apply (subst (2 3) somegcd_meet, (simp add: carr)+)

2640 apply (simp add: somegcd_meet carr)

2641 apply (rule weak_meet_assoc[simplified], fact+)

2642 done

2643 qed

2645 lemma (in gcd_condition_monoid) gcd_mult:

2646 assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2647 shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2648 proof - (* following Jacobson, Basic Algebra, p.140 *)

2649 let ?d = "somegcd G a b"

2650 let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"

2651 note carr[simp] = acarr bcarr ccarr

2652 have dcarr: "?d \<in> carrier G" by simp

2653 have ecarr: "?e \<in> carrier G" by simp

2654 note carr = carr dcarr ecarr

2656 have "?d divides a" by (simp add: gcd_divides_l)

2657 then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)

2659 have "?d divides b" by (simp add: gcd_divides_r)

2660 then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)

2662 from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e"

2663 by (rule gcd_divides) simp_all

2664 then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u"

2665 by blast

2667 note carr = carr ucarr

2669 have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all

2670 then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x"

2671 by blast

2672 with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x"

2673 by simp

2675 from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)"

2676 by (simp add: m_assoc)

2677 then have "a = ?d \<otimes> u \<otimes> x"

2678 by (rule l_cancel[of c a]) (simp add: xcarr)+

2679 then have du'a: "?d \<otimes> u divides a"

2680 by (rule dividesI[OF xcarr])

2682 have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all

2683 then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x"

2684 by blast

2685 with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x"

2686 by simp

2688 from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)"

2689 by (simp add: m_assoc)

2690 with xcarr have "b = ?d \<otimes> u \<otimes> x"

2691 by (intro l_cancel[of c b]) simp_all

2692 then have du'b: "?d \<otimes> u divides b"

2693 by (intro dividesI[OF xcarr])

2695 from du'a du'b carr have du'd: "?d \<otimes> u divides ?d"

2696 by (intro gcd_divides) simp_all

2697 then have uunit: "u \<in> Units G"

2698 proof (elim dividesE)

2699 fix v

2700 assume vcarr[simp]: "v \<in> carrier G"

2701 assume d: "?d = ?d \<otimes> u \<otimes> v"

2702 have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact

2703 also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)

2704 finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .

2705 then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all

2706 then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm)

2707 from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G"

2708 by (auto simp: Units_def)

2709 qed

2711 from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"

2712 by (intro associatedI2[of u]) simp_all

2713 from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2714 by simp

2715 qed

2717 lemma (in monoid) assoc_subst:

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

2719 and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b

2720 \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b"

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

2722 shows "f a \<sim> f b"

2723 using assms by auto

2725 lemma (in gcd_condition_monoid) relprime_mult:

2726 assumes abrelprime: "somegcd G a b \<sim> \<one>"

2727 and acrelprime: "somegcd G a c \<sim> \<one>"

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

2729 shows "somegcd G a (b \<otimes> c) \<sim> \<one>"

2730 proof -

2731 have "c = c \<otimes> \<one>" by simp

2732 also from abrelprime[symmetric]

2733 have "\<dots> \<sim> c \<otimes> somegcd G a b"

2734 by (rule assoc_subst) (simp add: mult_cong_r)+

2735 also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2736 by (rule gcd_mult) fact+

2737 finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2738 by simp

2740 from carr have a: "a \<sim> somegcd G a (c \<otimes> a)"

2741 by (fast intro: gcdI divides_prod_l)

2743 have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)"

2744 by (simp add: m_comm)

2745 also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"

2746 by (rule assoc_subst) (simp add: gcd_cong_l)+

2747 also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"

2748 by (rule assoc_subst) simp+

2749 also from c[symmetric] have "\<dots> \<sim> somegcd G a c"

2750 by (rule assoc_subst) (simp add: gcd_cong_r)+

2751 also note acrelprime

2752 finally show "somegcd G a (b \<otimes> c) \<sim> \<one>"

2753 by simp

2754 qed

2756 lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"

2757 apply unfold_locales

2758 apply (rule primeI)

2759 apply (elim irreducibleE, assumption)

2760 proof -

2761 fix p a b

2762 assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"

2763 and pirr: "irreducible G p"

2764 and pdvdab: "p divides a \<otimes> b"

2765 from pirr have pnunit: "p \<notin> Units G"

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

2767 by (fast elim: irreducibleE)+

2769 show "p divides a \<or> p divides b"

2770 proof (rule ccontr, clarsimp)

2771 assume npdvda: "\<not> p divides a"

2772 with pcarr acarr have "\<one> \<sim> somegcd G p a"

2773 apply (intro gcdI, simp, simp, simp)

2774 apply (fast intro: unit_divides)

2775 apply (fast intro: unit_divides)

2776 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

2777 apply (rule r, rule, assumption)

2778 apply (rule properfactorI, assumption)

2779 proof

2780 fix y

2781 assume ycarr: "y \<in> carrier G"

2782 assume "p divides y"

2783 also assume "y divides a"

2784 finally have "p divides a"

2785 by (simp add: pcarr ycarr acarr)

2786 with npdvda show False ..

2787 qed simp_all

2788 with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"

2789 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2791 assume npdvdb: "\<not> p divides b"

2792 with pcarr bcarr have "\<one> \<sim> somegcd G p b"

2793 apply (intro gcdI, simp, simp, simp)

2794 apply (fast intro: unit_divides)

2795 apply (fast intro: unit_divides)

2796 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

2797 apply (rule r, rule, assumption)

2798 apply (rule properfactorI, assumption)

2799 proof

2800 fix y

2801 assume ycarr: "y \<in> carrier G"

2802 assume "p divides y"

2803 also assume "y divides b"

2804 finally have "p divides b" by (simp add: pcarr ycarr bcarr)

2805 with npdvdb

2806 show "False" ..

2807 qed simp_all

2808 with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"

2809 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2811 from pcarr acarr bcarr pdvdab have "p gcdof p (a \<otimes> b)"

2812 by (fast intro: isgcd_divides_l)

2813 with pcarr acarr bcarr have "p \<sim> somegcd G p (a \<otimes> b)"

2814 by (fast intro: gcdI2)

2815 also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"

2816 by (rule relprime_mult)

2817 finally have "p \<sim> \<one>"

2818 by (simp add: pcarr acarr bcarr)

2819 with pcarr have "p \<in> Units G"

2820 by (fast intro: assoc_unit_l)

2821 with pnunit show False ..

2822 qed

2823 qed

2825 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid

2826 by (rule primeness_condition)

2829 subsubsection \<open>Divisor chain condition\<close>

2831 lemma (in divisor_chain_condition_monoid) wfactors_exist:

2832 assumes acarr: "a \<in> carrier G"

2833 shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2834 proof -

2835 have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"

2836 proof (rule wf_induct[OF division_wellfounded])

2837 fix x

2838 assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}

2839 \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)"

2841 show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)"

2842 apply clarify

2843 apply (cases "x \<in> Units G")

2844 apply (rule exI[of _ "[]"], simp)

2845 apply (cases "irreducible G x")

2846 apply (rule exI[of _ "[x]"], simp add: wfactors_def)

2847 proof -

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

2849 and xnunit: "x \<notin> Units G"

2850 and xnirr: "\<not> irreducible G x"

2851 then have "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"

2852 apply -

2853 apply (rule ccontr)

2854 apply simp

2855 apply (subgoal_tac "irreducible G x", simp)

2856 apply (rule irreducibleI, simp, simp)

2857 done

2858 then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G"

2859 and pfyx: "properfactor G y x"

2860 by blast

2862 have ih': "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk>

2863 \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"

2864 by (rule ih[rule_format, simplified]) (simp add: xcarr)+

2866 from ih' [OF ycarr pfyx]

2867 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2868 by blast

2870 from pfyx have "y divides x" and nyx: "\<not> y \<sim> x"

2871 by (fast elim: properfactorE2)+

2872 then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"

2873 by blast

2875 from zcarr ycarr have "properfactor G z x"

2876 apply (subst x)

2877 apply (intro properfactorI3[of _ _ y])

2878 apply (simp add: m_comm)

2879 apply (simp add: ynunit)+

2880 done

2881 from ih' [OF zcarr this]

2882 obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"

2883 by blast

2884 from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"

2885 by simp

2886 from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y\<otimes>z)"

2887 by (rule wfactors_mult)

2888 then have "wfactors G (ys@zs) x"

2889 by (simp add: x)

2890 with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"

2891 by fast

2892 qed

2893 qed

2894 from acarr show ?thesis by (rule r)

2895 qed

2898 subsubsection \<open>Primeness condition\<close>

2900 lemma (in comm_monoid_cancel) multlist_prime_pos:

2901 assumes carr: "a \<in> carrier G" "set as \<subseteq> carrier G"

2902 and aprime: "prime G a"

2903 and "a divides (foldr (\<otimes>) as \<one>)"

2904 shows "\<exists>i<length as. a divides (as!i)"

2905 proof -

2906 have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (\<otimes>) as \<one>)

2907 \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"

2908 apply (induct as)

2909 apply clarsimp defer 1

2910 apply clarsimp defer 1

2911 proof -

2912 assume "a divides \<one>"

2913 with carr have "a \<in> Units G"

2914 by (fast intro: divides_unit[of a \<one>])

2915 with aprime show False

2916 by (elim primeE, simp)

2917 next

2918 fix aa as

2919 assume ih[rule_format]: "a divides foldr (\<otimes>) as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"

2920 and carr': "aa \<in> carrier G" "set as \<subseteq> carrier G"

2921 and "a divides aa \<otimes> foldr (\<otimes>) as \<one>"

2922 with carr aprime have "a divides aa \<or> a divides foldr (\<otimes>) as \<one>"

2923 by (intro prime_divides) simp+

2924 then show "\<exists>i<Suc (length as). a divides (aa # as) ! i"

2925 proof

2926 assume "a divides aa"

2927 then have p1: "a divides (aa#as)!0" by simp

2928 have "0 < Suc (length as)" by simp

2929 with p1 show ?thesis by fast

2930 next

2931 assume "a divides foldr (\<otimes>) as \<one>"

2932 from ih [OF this] obtain i where "a divides as ! i" and len: "i < length as" by auto

2933 then have p1: "a divides (aa#as) ! (Suc i)" by simp

2934 from len have "Suc i < Suc (length as)" by simp

2935 with p1 show ?thesis by force

2936 qed

2937 qed

2938 from assms show ?thesis

2939 by (intro r) auto

2940 qed

2942 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:

2943 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>

2944 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2945 proof (induct as)

2946 case Nil

2947 show ?case

2948 proof auto

2949 fix a as'

2950 assume a: "a \<in> carrier G"

2951 assume "wfactors G [] a"

2952 then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)

2953 with a have "a \<in> Units G" by (auto intro: assoc_unit_r)

2954 moreover assume "wfactors G as' a"

2955 moreover assume "set as' \<subseteq> carrier G"

2956 ultimately have "as' = []" by (rule unit_wfactors_empty)

2957 then show "essentially_equal G [] as'" by simp

2958 qed

2959 next

2960 case (Cons ah as)

2961 then show ?case

2962 proof clarsimp

2963 fix a as'

2964 assume ih [rule_format]:

2965 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>

2966 wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2967 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"

2968 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"

2969 and afs: "wfactors G (ah # as) a"

2970 and afs': "wfactors G as' a"

2971 then have ahdvda: "ah divides a"

2972 by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all

2973 then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"

2974 by blast

2975 have a'fs: "wfactors G as a'"

2976 apply (rule wfactorsE[OF afs], rule wfactorsI, simp)

2977 apply (simp add: a)

2978 apply (insert ascarr a'carr)

2979 apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)

2980 done

2981 from afs have ahirr: "irreducible G ah"

2982 by (elim wfactorsE) simp

2983 with ascarr have ahprime: "prime G ah"

2984 by (intro irreducible_prime ahcarr)

2986 note carr [simp] = acarr ahcarr ascarr as'carr a'carr

2988 note ahdvda

2989 also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"

2990 by (elim wfactorsE associatedE, simp)

2991 finally have "ah divides (foldr (\<otimes>) as' \<one>)"

2992 by simp

2993 with ahprime have "\<exists>i<length as'. ah divides as'!i"

2994 by (intro multlist_prime_pos) simp_all

2995 then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"

2996 by blast

2997 from afs' carr have irrasi: "irreducible G (as'!i)"

2998 by (fast intro: nth_mem[OF len] elim: wfactorsE)

2999 from len carr have asicarr[simp]: "as'!i \<in> carrier G"

3000 unfolding set_conv_nth by force

3001 note carr = carr asicarr

3003 from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"

3004 by blast

3005 with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"

3006 apply -

3007 apply (elim irreducible_prodE[of "ah" "x"], assumption+)

3008 apply (rule associatedI2[of x], assumption+)

3009 apply (rule irreducibleE[OF ahirr], simp)

3010 done

3012 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']

3013 note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]

3014 note carr = carr partscarr

3016 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"

3017 apply (intro wfactors_prod_exists)

3018 using setparts afs'

3019 apply (fast elim: wfactorsE)

3020 apply simp

3021 done

3022 then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"

3023 by auto

3025 have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"

3026 apply (intro wfactors_prod_exists)

3027 using setparts afs'

3028 apply (fast elim: wfactorsE)

3029 apply simp

3030 done

3031 then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"

3032 and aa2fs: "wfactors G (drop (Suc i) as') aa_2"

3033 by auto

3035 note carr = carr aa1carr[simp] aa2carr[simp]

3037 from aa1fs aa2fs

3038 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"

3039 by (intro wfactors_mult, simp+)

3040 then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"

3041 apply (intro wfactors_mult_single)

3042 using setparts afs'

3043 apply (fast intro: nth_mem[OF len] elim: wfactorsE)

3044 apply simp_all

3045 done

3047 from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"

3048 by (metis irrasi wfactors_mult_single)

3049 with len carr aa1carr aa2carr aa1fs

3050 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"

3051 apply (intro wfactors_mult)

3052 apply fast

3053 apply (simp, (fast intro: nth_mem[OF len])?)+

3054 done

3056 from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"

3057 by (simp add: Cons_nth_drop_Suc)

3058 with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"

3059 by simp

3060 with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"

3061 by (metis as' ee_wfactorsD m_closed)

3062 then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"

3063 by (metis aa1carr aa2carr asicarr m_lcomm)

3064 from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"

3065 by (metis associated_sym m_closed mult_cong_l)

3066 also note t1

3067 finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp

3069 with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"

3070 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])

3072 note v1

3073 also note a'

3074 finally have "wfactors G (take i as' @ drop (Suc i) as') a'"

3075 by simp

3077 from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"

3078 by (intro ih[of a']) simp

3079 then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"

3080 by (elim essentially_equalE) (fastforce intro: essentially_equalI)

3082 from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')

3083 (as' ! i # take i as' @ drop (Suc i) as')"

3084 proof (intro essentially_equalI)

3085 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"

3086 by simp

3087 next

3088 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"

3089 by (simp add: list_all2_append) (simp add: asiah[symmetric])

3090 qed

3092 note ee1

3093 also note ee2

3094 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')

3095 (take i as' @ as' ! i # drop (Suc i) as')"

3096 apply (intro essentially_equalI)

3097 apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>

3098 take i as' @ as' ! i # drop (Suc i) as'")

3099 apply simp

3100 apply (rule perm_append_Cons)

3101 apply simp

3102 done

3103 finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"

3104 by simp

3105 then show "essentially_equal G (ah # as) as'"

3106 by (subst as')

3107 qed

3108 qed

3110 lemma (in primeness_condition_monoid) wfactors_unique:

3111 assumes "wfactors G as a" "wfactors G as' a"

3112 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G"

3113 shows "essentially_equal G as as'"

3114 by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)

3117 subsubsection \<open>Application to factorial monoids\<close>

3119 text \<open>Number of factors for wellfoundedness\<close>

3121 definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"

3122 where "factorcount G a =

3123 (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)"

3125 lemma (in monoid) ee_length:

3126 assumes ee: "essentially_equal G as bs"

3127 shows "length as = length bs"

3128 by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)

3130 lemma (in factorial_monoid) factorcount_exists:

3131 assumes carr[simp]: "a \<in> carrier G"

3132 shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"

3133 proof -

3134 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3135 by (intro wfactors_exist) simp

3136 then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3137 by (auto simp del: carr)

3138 have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"

3139 by (metis afs ascarr assms ee_length wfactors_unique)

3140 then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..

3141 qed

3143 lemma (in factorial_monoid) factorcount_unique:

3144 assumes afs: "wfactors G as a"

3145 and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"

3146 shows "factorcount G a = length as"

3147 proof -

3148 have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

3149 by (rule factorcount_exists) simp

3150 then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

3151 by auto

3152 have ac: "ac = factorcount G a"

3153 apply (simp add: factorcount_def)

3154 apply (rule theI2)

3155 apply (rule alen)

3156 apply (metis afs alen ascarr)+

3157 done

3158 from ascarr afs have "ac = length as"

3159 by (iprover intro: alen[rule_format])

3160 with ac show ?thesis

3161 by simp

3162 qed

3164 lemma (in factorial_monoid) divides_fcount:

3165 assumes dvd: "a divides b"

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

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

3168 shows "factorcount G a \<le> factorcount G b"

3169 proof (rule dividesE[OF dvd])

3170 fix c

3171 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3172 by blast

3173 then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3174 by blast

3175 with acarr have fca: "factorcount G a = length as"

3176 by (intro factorcount_unique)

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

3179 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

3180 by blast

3181 then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

3182 by blast

3184 note [simp] = acarr bcarr ccarr ascarr cscarr

3186 assume b: "b = a \<otimes> c"

3187 from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"

3188 by (intro wfactors_mult) simp_all

3189 with b have "wfactors G (as@cs) b"

3190 by simp

3191 then have "factorcount G b = length (as@cs)"

3192 by (intro factorcount_unique) simp_all

3193 then have "factorcount G b = length as + length cs"

3194 by simp

3195 with fca show ?thesis

3196 by simp

3197 qed

3199 lemma (in factorial_monoid) associated_fcount:

3200 assumes acarr: "a \<in> carrier G"

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

3202 and asc: "a \<sim> b"

3203 shows "factorcount G a = factorcount G b"

3204 apply (rule associatedE[OF asc])

3205 apply (drule divides_fcount[OF _ acarr bcarr])

3206 apply (drule divides_fcount[OF _ bcarr acarr])

3207 apply simp

3208 done

3210 lemma (in factorial_monoid) properfactor_fcount:

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

3212 and pf: "properfactor G a b"

3213 shows "factorcount G a < factorcount G b"

3214 proof (rule properfactorE[OF pf], elim dividesE)

3215 fix c

3216 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3217 by blast

3218 then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3219 by blast

3220 with acarr have fca: "factorcount G a = length as"

3221 by (intro factorcount_unique)

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

3224 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

3225 by blast

3226 then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

3227 by blast

3229 assume b: "b = a \<otimes> c"

3231 have "wfactors G (as@cs) (a \<otimes> c)"

3232 by (rule wfactors_mult) fact+

3233 with b have "wfactors G (as@cs) b"

3234 by simp

3235 with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"

3236 by (simp add: factorcount_unique)

3237 then have fcb: "factorcount G b = length as + length cs"

3238 by simp

3240 assume nbdvda: "\<not> b divides a"

3241 have "c \<notin> Units G"

3242 proof

3243 assume cunit:"c \<in> Units G"

3244 have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"

3245 by (simp add: b)

3246 also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"

3247 by (fast intro: m_assoc)

3248 also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp

3249 also from acarr have "\<dots> = a" by simp

3250 finally have "a = b \<otimes> inv c" by simp

3251 with ccarr cunit have "b divides a"

3252 by (fast intro: dividesI[of "inv c"])

3253 with nbdvda show False by simp

3254 qed

3255 with cfs have "length cs > 0"

3256 apply -

3257 apply (rule ccontr, simp)

3258 apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)

3259 done

3260 with fca fcb show ?thesis

3261 by simp

3262 qed

3264 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid

3265 apply unfold_locales

3266 apply (rule wfUNIVI)

3267 apply (rule measure_induct[of "factorcount G"])

3268 apply simp

3269 apply (metis properfactor_fcount)

3270 done

3272 sublocale factorial_monoid \<subseteq> primeness_condition_monoid

3273 by standard (rule irreducible_prime)

3276 lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..

3278 lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"

3279 by standard (rule gcdof_exists)

3281 sublocale factorial_monoid \<subseteq> gcd_condition_monoid

3282 by standard (rule gcdof_exists)

3284 lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"

3285 proof -

3286 interpret weak_lower_semilattice "division_rel G"

3287 by simp

3288 show "weak_lattice (division_rel G)"

3289 proof (unfold_locales, simp_all)

3290 fix x y

3291 assume carr: "x \<in> carrier G" "y \<in> carrier G"

3292 from lcmof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y"

3293 by blast

3294 with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"

3295 by (simp add: lcmof_leastUpper[symmetric])

3296 then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})"

3297 by blast

3298 qed

3299 qed

3302 subsection \<open>Factoriality Theorems\<close>

3304 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)

3305 "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G \<longleftrightarrow> factorial_monoid G"

3306 proof (rule iffI, clarify)

3307 assume dcc: "divisor_chain_condition_monoid G"

3308 and pc: "primeness_condition_monoid G"

3309 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3310 interpret primeness_condition_monoid "G" by (rule pc)

3311 show "factorial_monoid G"

3312 by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)

3313 next

3314 assume "factorial_monoid G"

3315 then interpret factorial_monoid "G" .

3316 show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"

3317 by rule unfold_locales

3318 qed

3320 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)

3321 "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G \<longleftrightarrow> factorial_monoid G"

3322 proof (rule iffI, clarify)

3323 assume dcc: "divisor_chain_condition_monoid G"

3324 and gc: "gcd_condition_monoid G"

3325 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3326 interpret gcd_condition_monoid "G" by (rule gc)

3327 show "factorial_monoid G"

3328 by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)

3329 next

3330 assume "factorial_monoid G"

3331 then interpret factorial_monoid "G" .

3332 show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"

3333 by rule unfold_locales

3334 qed

3336 end