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

src/HOL/Algebra/Divisibility.thy

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

Sat Jun 30 15:44:04 2018 +0100 (12 months ago) | |

changeset 68551 | b680e74eb6f2 |

parent 68488 | dfbd80c3d180 |

child 68604 | 57721285d4ef |

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

More on Algebra by Paulo and Martin

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 "a divides b" "a \<in> carrier G" "c \<in> carrier G"

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

200 by (metis assms factor_def m_assoc)

202 lemma (in monoid_cancel) divides_mult_l [simp]:

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

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

205 proof

206 show "c \<otimes> a divides c \<otimes> b \<Longrightarrow> a divides b"

207 using carr monoid.m_assoc monoid_axioms monoid_cancel.l_cancel monoid_cancel_axioms by fastforce

208 show "a divides b \<Longrightarrow> c \<otimes> a divides c \<otimes> b"

209 using carr(1) carr(3) by blast

210 qed

212 lemma (in comm_monoid) divides_mult_rI [intro]:

213 assumes ab: "a divides b"

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

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

216 using carr ab by (metis divides_mult_lI m_comm)

218 lemma (in comm_monoid_cancel) divides_mult_r [simp]:

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

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

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

223 lemma (in monoid) divides_prod_r:

224 assumes ab: "a divides b"

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

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

227 using ab carr by (fast intro: m_assoc)

229 lemma (in comm_monoid) divides_prod_l:

230 assumes "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" "a divides b"

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

232 using assms by (simp add: divides_prod_r m_comm)

234 lemma (in monoid) unit_divides:

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

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

237 shows "u divides a"

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

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

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

241 by (fast intro: m_assoc[symmetric])

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

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

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

245 qed

247 lemma (in comm_monoid) divides_unit:

248 assumes udvd: "a divides u"

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

250 shows "a \<in> Units G"

251 using udvd carr by (blast intro: unit_factor)

253 lemma (in comm_monoid) Unit_eq_dividesone:

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

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

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

259 subsubsection \<open>Association\<close>

261 lemma associatedI:

262 fixes G (structure)

263 assumes "a divides b" "b divides a"

264 shows "a \<sim> b"

265 using assms by (simp add: associated_def)

267 lemma (in monoid) associatedI2:

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

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

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

271 shows "a \<sim> b"

272 using uunit bcarr

273 unfolding a

274 apply (intro associatedI)

275 apply (metis Units_closed divides_mult_lI one_closed r_one unit_divides)

276 by blast

278 lemma (in monoid) associatedI2':

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

280 and "u \<in> Units G"

281 and "b \<in> carrier G"

282 shows "a \<sim> b"

283 using assms by (intro associatedI2)

285 lemma associatedD:

286 fixes G (structure)

287 assumes "a \<sim> b"

288 shows "a divides b"

289 using assms by (simp add: associated_def)

291 lemma (in monoid_cancel) associatedD2:

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

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

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

295 using assoc

296 unfolding associated_def

297 proof clarify

298 assume "b divides a"

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

300 by (rule dividesE)

302 assume "a divides b"

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

304 by (rule dividesE)

305 note carr = carr ucarr u'carr

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

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

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

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

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

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

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

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

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

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

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

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

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

322 by fast

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

324 by (simp add: Units_def ucarr)

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

326 qed

328 lemma associatedE:

329 fixes G (structure)

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

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

332 shows "P"

333 proof -

334 from assoc have "a divides b" "b divides a"

335 by (simp_all add: associated_def)

336 then show P by (elim e)

337 qed

339 lemma (in monoid_cancel) associatedE2:

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

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

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

343 shows "P"

344 proof -

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

346 by (rule associatedD2)

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

348 by auto

349 then show P by (elim e)

350 qed

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

353 assumes "a \<in> carrier G"

354 shows "a \<sim> a"

355 using assms by (fast intro: associatedI)

357 lemma (in monoid) associated_sym [sym]:

358 assumes "a \<sim> b"

359 shows "b \<sim> a"

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

362 lemma (in monoid) associated_trans [trans]:

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

364 and "a \<in> carrier G" "c \<in> carrier G"

365 shows "a \<sim> c"

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

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

369 apply unfold_locales

370 apply simp_all

371 apply (metis associated_def)

372 apply (iprover intro: associated_trans)

373 done

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

378 lemmas divides_antisym = associatedI

380 lemma (in monoid) divides_cong_l [trans]:

381 assumes "x \<sim> x'" "x' divides y" "x \<in> carrier G"

382 shows "x divides y"

383 by (meson assms associatedD divides_trans)

385 lemma (in monoid) divides_cong_r [trans]:

386 assumes "x divides y" "y \<sim> y'" "x \<in> carrier G"

387 shows "x divides y'"

388 by (meson assms associatedD divides_trans)

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

391 "weak_partial_order (division_rel G)"

392 apply unfold_locales

393 apply (simp_all add: associated_sym divides_antisym)

394 apply (metis associated_trans)

395 apply (metis divides_trans)

396 by (meson associated_def divides_trans)

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

401 lemma (in monoid_cancel) mult_cong_r:

402 assumes "b \<sim> b'" "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G"

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

404 by (meson assms associated_def divides_mult_lI)

406 lemma (in comm_monoid_cancel) mult_cong_l:

407 assumes "a \<sim> a'" "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G"

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

409 using assms m_comm mult_cong_r by auto

411 lemma (in monoid_cancel) assoc_l_cancel:

412 assumes "a \<in> carrier G" "b \<in> carrier G" "b' \<in> carrier G" "a \<otimes> b \<sim> a \<otimes> b'"

413 shows "b \<sim> b'"

414 by (meson assms associated_def divides_mult_l)

416 lemma (in comm_monoid_cancel) assoc_r_cancel:

417 assumes "a \<otimes> b \<sim> a' \<otimes> b" "a \<in> carrier G" "a' \<in> carrier G" "b \<in> carrier G"

418 shows "a \<sim> a'"

419 using assms assoc_l_cancel m_comm by presburger

422 subsubsection \<open>Units\<close>

424 lemma (in monoid_cancel) assoc_unit_l [trans]:

425 assumes "a \<sim> b"

426 and "b \<in> Units G"

427 and "a \<in> carrier G"

428 shows "a \<in> Units G"

429 using assms by (fast elim: associatedE2)

431 lemma (in monoid_cancel) assoc_unit_r [trans]:

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

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

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

435 shows "b \<in> Units G"

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

438 lemma (in comm_monoid) Units_cong:

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

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

441 shows "b \<in> Units G"

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

444 lemma (in monoid) Units_assoc:

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

446 shows "a \<sim> b"

447 using units by (fast intro: associatedI unit_divides)

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

450 proof -

451 have "a .\<in>\<^bsub>division_rel G\<^esub> {\<one>}" if "a \<in> Units G" for a

452 proof -

453 have "a \<sim> \<one>"

454 by (rule associatedI) (simp_all add: Units_closed that unit_divides)

455 then show ?thesis

456 by (simp add: elem_def)

457 qed

458 moreover have "\<one> .\<in>\<^bsub>division_rel G\<^esub> Units G"

459 by (simp add: equivalence.mem_imp_elem)

460 ultimately show ?thesis

461 by (auto simp: set_eq_def)

462 qed

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

465 apply (auto simp add: Units_def Lower_def)

466 apply (metis Units_one_closed unit_divides unit_factor)

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

468 done

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

473 lemma properfactorI:

474 fixes G (structure)

475 assumes "a divides b"

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

477 shows "properfactor G a b"

478 using assms unfolding properfactor_def by simp

480 lemma properfactorI2:

481 fixes G (structure)

482 assumes advdb: "a divides b"

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

484 shows "properfactor G a b"

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

486 assume "b divides a"

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

488 with neq show "False" by fast

489 qed

491 lemma (in comm_monoid_cancel) properfactorI3:

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

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

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

495 shows "properfactor G a p"

496 unfolding p

497 using carr

498 apply (intro properfactorI, fast)

499 proof (clarsimp, elim dividesE)

500 fix c

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

502 note [simp] = carr ccarr

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

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

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

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

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

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

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

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

514 unfolding Units_def by fastforce

515 with nunit show False ..

516 qed

518 lemma properfactorE:

519 fixes G (structure)

520 assumes pf: "properfactor G a b"

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

522 shows "P"

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

525 lemma properfactorE2:

526 fixes G (structure)

527 assumes pf: "properfactor G a b"

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

529 shows "P"

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

532 lemma (in monoid) properfactor_unitE:

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

534 and pf: "properfactor G a u"

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

536 shows "P"

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

539 lemma (in monoid) properfactor_divides:

540 assumes pf: "properfactor G a b"

541 shows "a divides b"

542 using pf by (elim properfactorE)

544 lemma (in monoid) properfactor_trans1 [trans]:

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

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

547 shows "properfactor G a c"

548 using dvds carr

549 apply (elim properfactorE, intro properfactorI)

550 apply (iprover intro: divides_trans)+

551 done

553 lemma (in monoid) properfactor_trans2 [trans]:

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

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

556 shows "properfactor G a c"

557 using dvds carr

558 apply (elim properfactorE, intro properfactorI)

559 apply (iprover intro: divides_trans)+

560 done

562 lemma properfactor_lless:

563 fixes G (structure)

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

565 by (force simp: lless_def properfactor_def associated_def)

567 lemma (in monoid) properfactor_cong_l [trans]:

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

569 and pf: "properfactor G x y"

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

571 shows "properfactor G x' y"

572 using pf

573 unfolding properfactor_lless

574 proof -

575 interpret weak_partial_order "division_rel G" ..

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

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

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

579 qed

581 lemma (in monoid) properfactor_cong_r [trans]:

582 assumes pf: "properfactor G x y"

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

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

585 shows "properfactor G x y'"

586 using pf

587 unfolding properfactor_lless

588 proof -

589 interpret weak_partial_order "division_rel G" ..

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

591 also from yy'

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

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

594 qed

596 lemma (in monoid_cancel) properfactor_mult_lI [intro]:

597 assumes ab: "properfactor G a b"

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

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

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

602 lemma (in monoid_cancel) properfactor_mult_l [simp]:

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

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

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

607 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:

608 assumes ab: "properfactor G a b"

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

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

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

613 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:

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

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

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

618 lemma (in monoid) properfactor_prod_r:

619 assumes ab: "properfactor G a b"

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

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

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

624 lemma (in comm_monoid) properfactor_prod_l:

625 assumes ab: "properfactor G a b"

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

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

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

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

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

635 lemma irreducibleI:

636 fixes G (structure)

637 assumes "a \<notin> Units G"

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

639 shows "irreducible G a"

640 using assms unfolding irreducible_def by blast

642 lemma irreducibleE:

643 fixes G (structure)

644 assumes irr: "irreducible G a"

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

646 shows "P"

647 using assms unfolding irreducible_def by blast

649 lemma irreducibleD:

650 fixes G (structure)

651 assumes irr: "irreducible G a"

652 and pf: "properfactor G b a"

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

654 shows "b \<in> Units G"

655 using assms by (fast elim: irreducibleE)

657 lemma (in monoid_cancel) irreducible_cong [trans]:

658 assumes irred: "irreducible G a"

659 and aa': "a \<sim> a'" "a \<in> carrier G" "a' \<in> carrier G"

660 shows "irreducible G a'"

661 using assms

662 apply (auto simp: irreducible_def assoc_unit_l)

663 apply (metis aa' associated_sym properfactor_cong_r)

664 done

666 lemma (in monoid) irreducible_prod_rI:

667 assumes airr: "irreducible G a"

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

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

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

671 using airr carr bunit

672 apply (elim irreducibleE, intro irreducibleI)

673 using prod_unit_r apply blast

674 using associatedI2' properfactor_cong_r by auto

676 lemma (in comm_monoid) irreducible_prod_lI:

677 assumes birr: "irreducible G b"

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

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

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

681 by (metis aunit birr carr irreducible_prod_rI m_comm)

683 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:

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

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

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

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

688 shows P

689 using irr

690 proof (elim irreducibleE)

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

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

693 show P

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

695 case aunit: True

696 have "irreducible G b"

697 proof (rule irreducibleI, rule notI)

698 assume "b \<in> Units G"

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

700 with abnunit show "False" ..

701 next

702 fix c

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

704 and "properfactor G c b"

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

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

707 qed

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

709 next

710 case anunit: False

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

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

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

715 have "irreducible G a"

716 proof (rule irreducibleI, rule notI)

717 assume "a \<in> Units G"

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

719 with abnunit show "False" ..

720 next

721 fix c

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

723 and "properfactor G c a"

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

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

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

727 qed

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

729 qed

730 qed

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

735 lemma primeI:

736 fixes G (structure)

737 assumes "p \<notin> Units G"

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

739 shows "prime G p"

740 using assms unfolding prime_def by blast

742 lemma primeE:

743 fixes G (structure)

744 assumes pprime: "prime G p"

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

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

747 shows "P"

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

750 lemma (in comm_monoid_cancel) prime_divides:

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

752 and pprime: "prime G p"

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

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

755 using assms by (blast elim: primeE)

757 lemma (in monoid_cancel) prime_cong [trans]:

758 assumes "prime G p"

759 and pp': "p \<sim> p'" "p \<in> carrier G" "p' \<in> carrier G"

760 shows "prime G p'"

761 using assms

762 apply (auto simp: prime_def assoc_unit_l)

763 apply (metis pp' associated_sym divides_cong_l)

764 done

766 (*by Paulo EmÃlio de Vilhena*)

767 lemma (in comm_monoid_cancel) prime_irreducible:

768 assumes "prime G p"

769 shows "irreducible G p"

770 proof (rule irreducibleI)

771 show "p \<notin> Units G"

772 using assms unfolding prime_def by simp

773 next

774 fix b assume A: "b \<in> carrier G" "properfactor G b p"

775 then obtain c where c: "c \<in> carrier G" "p = b \<otimes> c"

776 unfolding properfactor_def factor_def by auto

777 hence "p divides c"

778 using A assms unfolding prime_def properfactor_def by auto

779 then obtain b' where b': "b' \<in> carrier G" "c = p \<otimes> b'"

780 unfolding factor_def by auto

781 hence "\<one> = b \<otimes> b'"

782 by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)

783 thus "b \<in> Units G"

784 using A(1) Units_one_closed b'(1) unit_factor by presburger

785 qed

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

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

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

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

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

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

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

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

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

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

805 locale factorial_monoid = comm_monoid_cancel +

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

807 and factors_unique:

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

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

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

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

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

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

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

819 using assms by (induct as) simp_all

821 lemma (in monoid) listassoc_sym [sym]:

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

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

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

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

826 using assms

827 proof (induction as arbitrary: bs)

828 case Cons

829 then show ?case

830 by (induction bs) (use associated_sym in auto)

831 qed auto

833 lemma (in monoid) listassoc_trans [trans]:

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

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

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

837 using assms

838 apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)

839 by (metis (mono_tags, lifting) associated_trans nth_mem subsetCE)

841 lemma (in monoid_cancel) irrlist_listassoc_cong:

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

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

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

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

846 using assms

847 apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)

848 apply (blast intro: irreducible_cong)

849 done

852 text \<open>Permutations\<close>

854 lemma perm_map [intro]:

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

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

857 using p by induct auto

859 lemma perm_map_switch:

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

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

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

864 lemma (in monoid) perm_assoc_switch:

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

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

867 using p a

868 proof (induction bs cs arbitrary: as)

869 case (swap y x l)

870 then show ?case

871 by (metis (no_types, hide_lams) list_all2_Cons2 perm.swap)

872 next

873 case (Cons xs ys z)

874 then show ?case

875 by (metis list_all2_Cons2 perm.Cons)

876 next

877 case (trans xs ys zs)

878 then show ?case

879 by (meson perm.trans)

880 qed auto

882 lemma (in monoid) perm_assoc_switch_r:

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

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

885 using p a

886 proof (induction as bs arbitrary: cs)

887 case Nil

888 then show ?case

889 by auto

890 next

891 case (swap y x l)

892 then show ?case

893 by (metis (no_types, hide_lams) list_all2_Cons1 perm.swap)

894 next

895 case (Cons xs ys z)

896 then show ?case

897 by (metis list_all2_Cons1 perm.Cons)

898 next

899 case (trans xs ys zs)

900 then show ?case

901 by (blast intro: elim: )

902 qed

904 declare perm_sym [sym]

906 lemma perm_setP:

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

908 and as: "P (set as)"

909 shows "P (set bs)"

910 proof -

911 from perm have "mset as = mset bs"

912 by (simp add: mset_eq_perm)

913 then have "set as = set bs"

914 by (rule mset_eq_setD)

915 with as show "P (set bs)"

916 by simp

917 qed

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

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

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

926 lemma (in monoid) essentially_equalI:

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

928 shows "essentially_equal G fs1 fs2"

929 using ex unfolding essentially_equal_def by fast

931 lemma (in monoid) essentially_equalE:

932 assumes ee: "essentially_equal G fs1 fs2"

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

934 shows "P"

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

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

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

939 shows "essentially_equal G as as"

940 using carr by (fast intro: essentially_equalI)

942 lemma (in monoid) ee_sym [sym]:

943 assumes ee: "essentially_equal G as bs"

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

945 shows "essentially_equal G bs as"

946 using ee

947 proof (elim essentially_equalE)

948 fix fs

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

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

951 by blast

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

953 with a[symmetric] carr show ?thesis

954 by (iprover intro: essentially_equalI perm_closed)

955 qed

957 lemma (in monoid) ee_trans [trans]:

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

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

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

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

962 shows "essentially_equal G as cs"

963 using ab bc

964 proof (elim essentially_equalE)

965 fix abs bcs

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

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

968 by blast

969 assume "as <~~> abs"

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

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

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

973 assume "bcs [\<sim>] cs"

974 then have "bs' [\<sim>] cs"

975 using a c1 c2 cscarr listassoc_trans by blast

976 with pp show ?thesis

977 by (rule essentially_equalI)

978 qed

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

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

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

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

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

988 using ascarr by (induct fs) simp_all

990 lemma (in comm_monoid) multlist_dividesI:

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

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

993 using assms

994 proof (induction fs)

995 case (Cons a fs)

996 then have f: "f \<in> carrier G"

997 by blast

998 show ?case

999 proof (cases "f = a")

1000 case True

1001 then show ?thesis

1002 using Cons.prems by auto

1003 next

1004 case False

1005 with Cons show ?thesis

1006 by clarsimp (metis f divides_prod_l multlist_closed)

1007 qed

1008 qed auto

1010 lemma (in comm_monoid_cancel) multlist_listassoc_cong:

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

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

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

1014 using assms

1015 proof (induct fs arbitrary: fs')

1016 case (Cons a as fs')

1017 then show ?case

1018 proof (induction fs')

1019 case (Cons b bs)

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

1021 by (simp add: mult_cong_l)

1022 then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>"

1023 using Cons by auto

1024 with Cons have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"

1025 by (simp add: mult_cong_r)

1026 then show ?case

1027 using Cons.prems(3) Cons.prems(4) monoid.associated_trans monoid_axioms p by force

1028 qed auto

1029 qed auto

1031 lemma (in comm_monoid) multlist_perm_cong:

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

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

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

1035 using prm ascarr

1036 proof induction

1037 case (swap y x l) then show ?case

1038 by (simp add: m_lcomm)

1039 next

1040 case (trans xs ys zs) then show ?case

1041 using perm_closed by auto

1042 qed auto

1044 lemma (in comm_monoid_cancel) multlist_ee_cong:

1045 assumes "essentially_equal G fs fs'"

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

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

1048 using assms

1049 apply (elim essentially_equalE)

1050 apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)

1051 done

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

1056 lemma wfactorsI:

1057 fixes G (structure)

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

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

1060 shows "wfactors G fs a"

1061 using assms unfolding wfactors_def by simp

1063 lemma wfactorsE:

1064 fixes G (structure)

1065 assumes wf: "wfactors G fs a"

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

1067 shows "P"

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

1070 lemma (in monoid) factorsI:

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

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

1073 shows "factors G fs a"

1074 using assms unfolding factors_def by simp

1076 lemma factorsE:

1077 fixes G (structure)

1078 assumes f: "factors G fs a"

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

1080 shows "P"

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

1083 lemma (in monoid) factors_wfactors:

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

1085 shows "wfactors G as a"

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

1088 lemma (in monoid) wfactors_factors:

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

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

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

1093 lemma (in monoid) factors_closed [dest]:

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

1095 shows "a \<in> carrier G"

1096 using assms by (elim factorsE, clarsimp)

1098 lemma (in monoid) nunit_factors:

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

1100 and fs: "factors G as a"

1101 shows "length as > 0"

1102 proof -

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

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

1105 qed

1107 lemma (in monoid) unit_wfactors [simp]:

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

1109 shows "wfactors G [] a"

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

1112 lemma (in comm_monoid_cancel) unit_wfactors_empty:

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

1114 and wf: "wfactors G fs a"

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

1116 shows "fs = []"

1117 proof (cases fs)

1118 case Nil

1119 then show ?thesis .

1120 next

1121 case fs: (Cons f fs')

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

1123 by (simp_all add: fs)

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

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

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

1130 note aunit

1131 also from fs wf

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

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

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

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

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

1137 with fnunit show ?thesis by contradiction

1138 qed

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

1143 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:

1144 assumes fact: "wfactors G fs a"

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

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

1147 shows "wfactors G fs' a"

1148 proof -

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

1150 by (simp add: multlist_listassoc_cong carr)

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

1152 finally have "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr) }

1153 then show ?thesis

1154 using fact

1155 by (meson asc carr(2) carr(3) irrlist_listassoc_cong wfactors_def)

1156 qed

1158 lemma (in comm_monoid) wfactors_perm_cong_l:

1159 assumes "wfactors G fs a"

1160 and "fs <~~> fs'"

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

1162 shows "wfactors G fs' a"

1163 using assms irrlist_perm_cong multlist_perm_cong wfactors_def by fastforce

1165 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:

1166 assumes ee: "essentially_equal G as bs"

1167 and bfs: "wfactors G bs b"

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

1169 shows "wfactors G as b"

1170 using ee

1171 proof (elim essentially_equalE)

1172 fix fs

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

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

1176 note bfs

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

1178 also (wfactors_listassoc_cong_l)

1179 note prm[symmetric]

1180 finally (wfactors_perm_cong_l)

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

1182 qed

1184 lemma (in monoid) wfactors_cong_r [trans]:

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

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

1187 shows "wfactors G fs a'"

1188 using fac

1189 proof (elim wfactorsE, intro wfactorsI)

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

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

1192 qed

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

1197 lemma (in comm_monoid_cancel) unitfactor_ee:

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

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

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

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

1202 proof -

1203 have "as[0 := as ! 0 \<otimes> u] [\<sim>] as"

1204 proof (cases as)

1205 case (Cons a as')

1206 then show ?thesis

1207 using associatedI2 carr uunit by auto

1208 qed auto

1209 then show ?thesis

1210 using essentially_equal_def by blast

1211 qed

1213 lemma (in comm_monoid_cancel) factors_cong_unit:

1214 assumes u: "u \<in> Units G"

1215 and a: "a \<notin> Units G"

1216 and afs: "factors G as a"

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

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

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

1220 proof (cases as)

1221 case Nil

1222 then show ?thesis

1223 using afs a nunit_factors by auto

1224 next

1225 case (Cons b bs)

1226 have *: "\<forall>f\<in>set as. irreducible G f" "foldr (\<otimes>) as \<one> = a"

1227 using afs by (auto simp: factors_def)

1228 show ?thesis

1229 proof (intro factorsI)

1230 show "foldr (\<otimes>) (as[0 := as ! 0 \<otimes> u]) \<one> = a \<otimes> u"

1231 using Cons u ascarr * by (auto simp add: m_ac Units_closed)

1232 show "\<forall>f\<in>set (as[0 := as ! 0 \<otimes> u]). irreducible G f"

1233 using Cons u ascarr * by (force intro: irreducible_prod_rI)

1234 qed

1235 qed

1237 lemma (in comm_monoid) perm_wfactorsD:

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

1239 and afs: "wfactors G as a"

1240 and bfs: "wfactors G bs b"

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

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

1243 shows "a \<sim> b"

1244 using afs bfs

1245 proof (elim wfactorsE)

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

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

1248 then have "a \<sim> foldr (\<otimes>) as \<one>"

1249 by (simp add: associated_sym)

1250 also from prm

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

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

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

1254 qed

1256 lemma (in comm_monoid_cancel) listassoc_wfactorsD:

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

1258 and afs: "wfactors G as a"

1259 and bfs: "wfactors G bs b"

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

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

1262 shows "a \<sim> b"

1263 using afs bfs

1264 proof (elim wfactorsE)

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

1266 then have "a \<sim> foldr (\<otimes>) as \<one>" by (simp add: associated_sym)

1267 also from assoc

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

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

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

1271 qed

1273 lemma (in comm_monoid_cancel) ee_wfactorsD:

1274 assumes ee: "essentially_equal G as bs"

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

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

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

1278 shows "a \<sim> b"

1279 using ee

1280 proof (elim essentially_equalE)

1281 fix fs

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

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

1284 by (simp add: perm_closed)

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

1286 by (rule wfactors_perm_cong_l) simp

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

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

1289 by (rule listassoc_wfactorsD) simp_all

1290 qed

1292 lemma (in comm_monoid_cancel) ee_factorsD:

1293 assumes ee: "essentially_equal G as bs"

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

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

1296 shows "a \<sim> b"

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

1299 lemma (in factorial_monoid) ee_factorsI:

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

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

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

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

1304 shows "essentially_equal G as bs"

1305 proof -

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

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

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

1310 by (elim associatedE2)

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

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

1314 by (rule unitfactor_ee)

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

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

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

1320 by (rule factors_cong_unit)

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

1323 have "essentially_equal G as ?bs'"

1324 by (blast intro: factors_unique)

1325 also note ee

1326 finally show "essentially_equal G as bs"

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

1328 qed

1330 lemma (in factorial_monoid) ee_wfactorsI:

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

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

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

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

1335 shows "essentially_equal G as bs"

1336 using assms

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

1338 case aunit: True

1339 also note asc

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

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

1343 by (rule unit_wfactors_empty)

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

1345 by (rule unit_wfactors_empty)

1347 have "essentially_equal G [] []"

1348 by (fast intro: essentially_equalI)

1349 then show ?thesis

1350 by (simp add: e e')

1351 next

1352 case anunit: False

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

1354 proof clarify

1355 assume "b \<in> Units G"

1356 also note asc[symmetric]

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

1358 with anunit show False ..

1359 qed

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

1362 by blast

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

1364 by fast

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

1367 proof clarify

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

1369 also note a'

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

1371 with anunit

1372 show "False" ..

1373 qed

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

1376 by blast

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

1378 by fast

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

1381 proof clarify

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

1383 also note b'

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

1385 with bnunit show False ..

1386 qed

1388 note a'

1389 also note asc

1390 also note b'[symmetric]

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

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

1393 by (rule ee_factorsI)

1394 qed

1396 lemma (in factorial_monoid) ee_wfactors:

1397 assumes asf: "wfactors G as a"

1398 and bsf: "wfactors G bs b"

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

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

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

1402 using assms by (fast intro: ee_wfactorsI ee_wfactorsD)

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

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

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

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

1408 case True

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

1410 then show ?thesis by (intro exI) force

1411 next

1412 case False

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

1414 by blast

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

1416 with fscarr show ?thesis by fast

1417 qed

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

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

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

1422 unfolding wfactors_def using assms by blast

1424 lemma (in factorial_monoid) wfactors_unique:

1425 assumes "wfactors G fs a"

1426 and "wfactors G fs' a"

1427 and "a \<in> carrier G"

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

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

1430 shows "essentially_equal G fs fs'"

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

1433 lemma (in monoid) factors_mult_single:

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

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

1436 using assms unfolding factors_def by simp

1438 lemma (in monoid_cancel) wfactors_mult_single:

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

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

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

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

1444 lemma (in monoid) factors_mult:

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

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

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

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

1449 proof -

1450 have "foldr (\<otimes>) (fa @ fb) \<one> = foldr (\<otimes>) fa \<one> \<otimes> foldr (\<otimes>) fb \<one>" if "set fa \<subseteq> carrier G"

1451 "Ball (set fa) (irreducible G)"

1452 using that bscarr by (induct fa) (simp_all add: m_assoc)

1453 then show ?thesis

1454 using assms unfolding factors_def by force

1455 qed

1457 lemma (in comm_monoid_cancel) wfactors_mult [intro]:

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

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

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

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

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

1463 proof clarsimp

1464 fix a' b'

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

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

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

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

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

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

1473 by (rule factors_mult) fact+

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

1476 by (intro factors_wfactors) simp_all

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

1478 by (intro mult_cong_r)

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

1480 by (intro mult_cong_l)

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

1482 by (simp add: carr)

1483 qed

1485 lemma (in comm_monoid) factors_dividesI:

1486 assumes "factors G fs a"

1487 and "f \<in> set fs"

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

1489 shows "f divides a"

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

1492 lemma (in comm_monoid) wfactors_dividesI:

1493 assumes p: "wfactors G fs a"

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

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

1496 shows "f divides a"

1497 using wfactors_factors[OF p fscarr]

1498 proof clarsimp

1499 fix a'

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

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

1502 by (simp add: factors_closed)

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

1505 by (fast intro: factors_dividesI)

1506 also note a'a

1507 finally show "f divides a"

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

1509 qed

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

1514 lemma (in comm_monoid_cancel) factorial_monoidI:

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

1516 and wfactors_unique:

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

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

1519 shows "factorial_monoid G"

1520 proof

1521 fix a

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

1524 from wfactors_exists[OF acarr]

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

1526 by blast

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

1528 by blast

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

1530 by fast

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

1532 proof clarify

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

1534 also note a'a

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

1536 with anunit show False ..

1537 qed

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

1540 by (blast elim: associatedE2)

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

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

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

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

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

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

1550 by (cases as) auto

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

1553 by (simp add: a factors_cong_unit)

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

1555 by fast

1556 qed (blast intro: factors_wfactors wfactors_unique)

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

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

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

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

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

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

1572 lemma (in monoid) assocs_repr_independence:

1573 assumes "y \<in> assocs G x" "x \<in> carrier G"

1574 shows "assocs G x = assocs G y"

1575 using assms

1576 by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in \<open>blast+\<close>)

1578 lemma (in monoid) assocs_self:

1579 assumes "x \<in> carrier G"

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

1581 using assms by (fastforce intro: closure_ofI2)

1583 lemma (in monoid) assocs_repr_independenceD:

1584 assumes repr: "assocs G x = assocs G y" and ycarr: "y \<in> carrier G"

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

1586 unfolding repr using ycarr by (intro assocs_self)

1588 lemma (in comm_monoid) assocs_assoc:

1589 assumes "a \<in> assocs G b" "b \<in> carrier G"

1590 shows "a \<sim> b"

1591 using assms by (elim closure_ofE2) simp

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

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

1598 lemma (in monoid) fmset_perm_cong:

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

1600 shows "fmset G as = fmset G bs"

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

1603 lemma (in comm_monoid_cancel) eqc_listassoc_cong:

1604 assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"

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

1606 using assms

1607 proof (induction as arbitrary: bs)

1608 case Nil

1609 then show ?case by simp

1610 next

1611 case (Cons a as)

1612 then show ?case

1613 proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)

1614 fix z zs

1615 assume zzs: "a \<in> carrier G" "set as \<subseteq> carrier G" "bs = z # zs" "a \<sim> z"

1616 "as [\<sim>] zs" "z \<in> carrier G" "set zs \<subseteq> carrier G"

1617 then show "assocs G a = assocs G z"

1618 apply (simp add: eq_closure_of_def elem_def)

1619 using \<open>a \<in> carrier G\<close> \<open>z \<in> carrier G\<close> \<open>a \<sim> z\<close> associated_sym associated_trans by blast+

1620 qed

1621 qed

1623 lemma (in comm_monoid_cancel) fmset_listassoc_cong:

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

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

1626 shows "fmset G as = fmset G bs"

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

1629 lemma (in comm_monoid_cancel) ee_fmset:

1630 assumes ee: "essentially_equal G as bs"

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

1632 shows "fmset G as = fmset G bs"

1633 using ee

1634 proof (elim essentially_equalE)

1635 fix as'

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

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

1638 by (rule perm_closed)

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

1640 by (rule fmset_perm_cong)

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

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

1643 by (simp add: fmset_listassoc_cong)

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

1645 qed

1647 lemma (in monoid_cancel) fmset_ee_aux:

1648 assumes "cas <~~> cbs" "cas = map (assocs G) as" "cbs = map (assocs G) bs"

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

1650 using assms

1651 proof (induction cas cbs arbitrary: as bs rule: perm.induct)

1652 case (Cons xs ys z)

1653 then show ?case

1654 by (clarsimp simp add: map_eq_Cons_conv) blast

1655 next

1656 case (trans xs ys zs)

1657 then show ?case

1658 by (smt ex_map_conv perm.trans perm_setP)

1659 qed auto

1661 lemma (in comm_monoid_cancel) fmset_ee:

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

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

1664 shows "essentially_equal G as bs"

1665 proof -

1666 from mset have "map (assocs G) as <~~> map (assocs G) bs"

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

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

1669 using fmset_ee_aux by blast

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

1671 using perm_closed by blast

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

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

1674 with tp show "essentially_equal G as bs"

1675 by (fast intro: essentially_equalI)

1676 qed

1678 lemma (in comm_monoid_cancel) ee_is_fmset:

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

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

1681 using assms by (fast intro: ee_fmset fmset_ee)

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

1686 lemma (in monoid) mset_fmsetEx:

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

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

1689 proof -

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

1691 by blast

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

1693 using elems unfolding Cs

1694 proof (induction Cs')

1695 case (Cons a Cs')

1696 then obtain c cs where csP: "\<forall>x\<in>set cs. P x" and mset: "mset (map (assocs G) cs) = mset Cs'"

1697 and cP: "P c" and a: "a = assocs G c"

1698 by force

1699 then have tP: "\<forall>x\<in>set (c#cs). P x"

1700 by simp

1701 show ?case

1702 using tP mset a by fastforce

1703 qed auto

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

1705 qed

1707 lemma (in monoid) mset_wfactorsEx:

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

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

1710 proof -

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

1712 by (intro mset_fmsetEx, rule elems)

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

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

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

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

1717 by (intro wfactors_prod_exists) auto

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

1719 with cscarr Cs show ?thesis by fast

1720 qed

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

1725 lemma (in factorial_monoid) mult_wfactors_fmset:

1726 assumes afs: "wfactors G as a"

1727 and bfs: "wfactors G bs b"

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

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

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

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

1732 proof -

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

1734 by (intro wfactors_mult)

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

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

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

1738 by (intro ee_fmset) simp_all

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

1740 by (simp add: fmset_def)

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

1742 qed

1744 lemma (in factorial_monoid) mult_factors_fmset:

1745 assumes afs: "factors G as a"

1746 and bfs: "factors G bs b"

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

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

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

1750 using assms by (blast intro: factors_wfactors mult_wfactors_fmset)

1752 lemma (in comm_monoid_cancel) fmset_wfactors_mult:

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

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

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

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

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

1758 proof -

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

1760 by (intro wfactors_mult)

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

1763 by (simp add: fmset_def)

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

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

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

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

1768 qed

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

1773 lemma (in factorial_monoid) divides_fmsubset:

1774 assumes ab: "a divides b"

1775 and afs: "wfactors G as a"

1776 and bfs: "wfactors G bs b"

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

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

1779 using ab

1780 proof (elim dividesE)

1781 fix c

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

1783 from wfactors_exist [OF this]

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

1785 by blast

1786 note carr = carr ccarr cscarr

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

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

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

1791 then show ?thesis by simp

1792 qed

1794 lemma (in comm_monoid_cancel) fmsubset_divides:

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

1796 and afs: "wfactors G as a"

1797 and bfs: "wfactors G bs b"

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

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

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

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

1802 shows "a divides b"

1803 proof -

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

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

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

1808 proof (intro mset_wfactorsEx, simp)

1809 fix X

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

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

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

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

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

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

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

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

1819 by fast

1820 qed

1821 then obtain c cs

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

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

1824 and csf: "wfactors G cs c"

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

1827 from csmset msubset

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

1829 by (simp add: multiset_eq_iff subseteq_mset_def)

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

1831 by (rule fmset_wfactors_mult) fact+

1832 then show ?thesis

1833 proof (elim associatedE2)

1834 fix u

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

1836 with acarr ccarr show "a divides b"

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

1838 qed (simp_all add: acarr bcarr ccarr)

1839 qed

1841 lemma (in factorial_monoid) divides_as_fmsubset:

1842 assumes "wfactors G as a"

1843 and "wfactors G bs b"

1844 and "a \<in> carrier G"

1845 and "b \<in> carrier G"

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

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

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

1849 using assms

1850 by (blast intro: divides_fmsubset fmsubset_divides)

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

1855 lemma (in factorial_monoid) fmset_properfactor:

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

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

1858 and "wfactors G as a"

1859 and "wfactors G bs b"

1860 and "a \<in> carrier G"

1861 and "b \<in> carrier G"

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

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

1864 shows "properfactor G a b"

1865 proof (rule properfactorI)

1866 show "a divides b"

1867 using assms asubb fmsubset_divides by blast

1868 show "\<not> b divides a"

1869 by (meson anb assms asubb factorial_monoid.divides_fmsubset factorial_monoid_axioms subset_mset.antisym)

1870 qed

1872 lemma (in factorial_monoid) properfactor_fmset:

1873 assumes pf: "properfactor G a b"

1874 and "wfactors G as a"

1875 and "wfactors G bs b"

1876 and "a \<in> carrier G"

1877 and "b \<in> carrier G"

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

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

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

1881 using pf

1882 apply safe

1883 apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)

1884 by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)

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

1888 lemma (in factorial_monoid) irreducible_prime:

1889 assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"

1890 shows "prime G p"

1891 using pirr

1892 proof (elim irreducibleE, intro primeI)

1893 fix a b

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

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

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

1897 assume irreduc[rule_format]:

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

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

1900 by (rule dividesE)

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

1902 using wfactors_exist [OF acarr] by blast

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

1904 using wfactors_exist [OF bcarr] by blast

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

1906 using wfactors_exist [OF ccarr] by blast

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

1908 from pirr cfs abpc have "wfactors G (p # cs) (a \<otimes> b)"

1909 by (simp add: wfactors_mult_single)

1910 moreover have "wfactors G (as @ bs) (a \<otimes> b)"

1911 by (rule wfactors_mult [OF afs bfs]) fact+

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

1913 by (rule wfactors_unique) simp+

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

1915 by (fast elim: essentially_equalE)

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

1917 by (simp add: perm_set_eq[symmetric])

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

1919 unfolding list_all2_conv_all_nth set_conv_nth by force

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

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

1922 using afs bfs divides_cong_l pp' wfactors_dividesI

1923 by (meson acarr ascarr bcarr bscarr pcarr)

1924 qed

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

1928 lemma (in factorial_monoid) factors_irreducible_prime:

1929 assumes pirr: "irreducible G p" and pcarr: "p \<in> carrier G"

1930 shows "prime G p"

1931 proof (rule primeI)

1932 show "p \<notin> Units G"

1933 by (meson irreducibleE pirr)

1934 have irreduc: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"

1935 using pirr by (auto simp: irreducible_def)

1936 show "p divides a \<or> p divides b"

1937 if acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and pdvdab: "p divides (a \<otimes> b)" for a b

1938 proof -

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

1940 by (rule dividesE)

1941 note [simp] = pcarr acarr bcarr ccarr

1943 show "p divides a \<or> p divides b"

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

1945 case True

1946 then have "p divides b"

1947 by (metis acarr associatedI2' associated_def bcarr divides_trans m_comm pcarr pdvdab)

1948 then show ?thesis ..

1949 next

1950 case anunit: False

1951 show ?thesis

1952 proof (cases "b \<in> Units G")

1953 case True

1954 then have "p divides a"

1955 by (meson acarr bcarr divides_unit irreducible_prime pcarr pdvdab pirr prime_def)

1956 then show ?thesis ..

1957 next

1958 case bnunit: False

1959 then have cnunit: "c \<notin> Units G"

1960 by (metis abpc acarr anunit bcarr ccarr irreducible_prodE irreducible_prod_rI pcarr pirr)

1961 then have abnunit: "a \<otimes> b \<notin> Units G"

1962 using acarr anunit bcarr unit_factor by blast

1963 obtain as where ascarr: "set as \<subseteq> carrier G" and afac: "factors G as a"

1964 using factors_exist [OF acarr anunit] by blast

1965 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfac: "factors G bs b"

1966 using factors_exist [OF bcarr bnunit] by blast

1967 obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfac: "factors G cs c"

1968 using factors_exist [OF ccarr cnunit] by auto

1969 note [simp] = ascarr bscarr cscarr

1970 from pirr cfac abpc have abfac': "factors G (p # cs) (a \<otimes> b)"

1971 by (simp add: factors_mult_single)

1972 from afac and bfac have "factors G (as @ bs) (a \<otimes> b)"

1973 by (rule factors_mult) fact+

1974 with abfac' have "essentially_equal G (p # cs) (as @ bs)"

1975 using abnunit factors_unique by auto

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

1977 by (fast elim: essentially_equalE)

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

1979 by (simp add: perm_set_eq[symmetric])

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

1981 unfolding list_all2_conv_all_nth set_conv_nth by force

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

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

1984 by (meson afac bfac divides_cong_l factors_dividesI pp' ascarr bscarr pcarr)

1985 qed

1986 qed

1987 qed

1988 qed

1991 subsection \<open>Greatest Common Divisors and Lowest Common Multiples\<close>

1993 subsubsection \<open>Definitions\<close>

1995 definition isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ gcdof\<index> _ _)" [81,81,81] 80)

1996 where "x gcdof\<^bsub>G\<^esub> a b \<longleftrightarrow> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and>

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

1999 definition islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool" ("(_ lcmof\<index> _ _)" [81,81,81] 80)

2000 where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>

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

2003 definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2004 where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"

2006 definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2007 where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"

2009 definition "SomeGcd G A = inf (division_rel G) A"

2012 locale gcd_condition_monoid = comm_monoid_cancel +

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

2015 locale primeness_condition_monoid = comm_monoid_cancel +

2016 assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"

2018 locale divisor_chain_condition_monoid = comm_monoid_cancel +

2019 assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"

2022 subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>

2024 lemma gcdof_greatestLower:

2025 fixes G (structure)

2026 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2027 shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"

2028 by (auto simp: isgcd_def greatest_def Lower_def elem_def)

2030 lemma lcmof_leastUpper:

2031 fixes G (structure)

2032 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2033 shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"

2034 by (auto simp: islcm_def least_def Upper_def elem_def)

2036 lemma somegcd_meet:

2037 fixes G (structure)

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

2039 shows "somegcd G a b = meet (division_rel G) a b"

2040 by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])

2042 lemma (in monoid) isgcd_divides_l:

2043 assumes "a divides b"

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

2045 shows "a gcdof a b"

2046 using assms unfolding isgcd_def by fast

2048 lemma (in monoid) isgcd_divides_r:

2049 assumes "b divides a"

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

2051 shows "b gcdof a b"

2052 using assms unfolding isgcd_def by fast

2055 subsubsection \<open>Existence of gcd and lcm\<close>

2057 lemma (in factorial_monoid) gcdof_exists:

2058 assumes acarr: "a \<in> carrier G"

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

2060 shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2061 proof -

2062 from wfactors_exist [OF acarr]

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

2064 by blast

2065 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2066 by (fast elim: wfactorsE)

2068 from wfactors_exist [OF bcarr]

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

2070 by blast

2071 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2072 by (fast elim: wfactorsE)

2074 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2075 fmset G cs = fmset G as \<inter># fmset G bs"

2076 proof (intro mset_wfactorsEx)

2077 fix X

2078 assume "X \<in># fmset G as \<inter># fmset G bs"

2079 then have "X \<in># fmset G as" by simp

2080 then have "X \<in> set (map (assocs G) as)"

2081 by (simp add: fmset_def)

2082 then have "\<exists>x. X = assocs G x \<and> x \<in> set as"

2083 by (induct as) auto

2084 then obtain x where X: "X = assocs G x" and xas: "x \<in> set as"

2085 by blast

2086 with ascarr have xcarr: "x \<in> carrier G"

2087 by blast

2088 from xas airr have xirr: "irreducible G x"

2089 by simp

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

2091 by blast

2092 qed

2093 then obtain c cs

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

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

2096 and csirr: "wfactors G cs c"

2097 and csmset: "fmset G cs = fmset G as \<inter># fmset G bs"

2098 by auto

2100 have "c gcdof a b"

2101 proof (simp add: isgcd_def, safe)

2102 from csmset

2103 have "fmset G cs \<subseteq># fmset G as"

2104 by (simp add: multiset_inter_def subset_mset_def)

2105 then show "c divides a" by (rule fmsubset_divides) fact+

2106 next

2107 from csmset have "fmset G cs \<subseteq># fmset G bs"

2108 by (simp add: multiset_inter_def subseteq_mset_def, force)

2109 then show "c divides b"

2110 by (rule fmsubset_divides) fact+

2111 next

2112 fix y

2113 assume "y \<in> carrier G"

2114 from wfactors_exist [OF this]

2115 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2116 by blast

2118 assume "y divides a"

2119 then have ya: "fmset G ys \<subseteq># fmset G as"

2120 by (rule divides_fmsubset) fact+

2122 assume "y divides b"

2123 then have yb: "fmset G ys \<subseteq># fmset G bs"

2124 by (rule divides_fmsubset) fact+

2126 from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"

2127 by (simp add: subset_mset_def)

2128 then show "y divides c"

2129 by (rule fmsubset_divides) fact+

2130 qed

2131 with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2132 by fast

2133 qed

2135 lemma (in factorial_monoid) lcmof_exists:

2136 assumes acarr: "a \<in> carrier G"

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

2138 shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2139 proof -

2140 from wfactors_exist [OF acarr]

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

2142 by blast

2143 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2144 by (fast elim: wfactorsE)

2146 from wfactors_exist [OF bcarr]

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

2148 by blast

2149 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2150 by (fast elim: wfactorsE)

2152 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2153 fmset G cs = (fmset G as - fmset G bs) + fmset G bs"

2154 proof (intro mset_wfactorsEx)

2155 fix X

2156 assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"

2157 then have "X \<in># fmset G as \<or> X \<in># fmset G bs"

2158 by (auto dest: in_diffD)

2159 then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)"

2160 by fast

2161 then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2162 proof cases

2163 case 1

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

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

2166 then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto

2167 with ascarr have xcarr: "x \<in> carrier G" by fast

2168 from xas airr have xirr: "irreducible G x" by simp

2169 from xcarr and xirr and X show ?thesis by fast

2170 next

2171 case 2

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

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

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

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

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

2177 from xcarr and xirr and X show ?thesis by fast

2178 qed

2179 qed

2180 then obtain c cs

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

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

2183 and csirr: "wfactors G cs c"

2184 and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"

2185 by auto

2187 have "c lcmof a b"

2188 proof (simp add: islcm_def, safe)

2189 from csmset have "fmset G as \<subseteq># fmset G cs"

2190 by (simp add: subseteq_mset_def, force)

2191 then show "a divides c"

2192 by (rule fmsubset_divides) fact+

2193 next

2194 from csmset have "fmset G bs \<subseteq># fmset G cs"

2195 by (simp add: subset_mset_def)

2196 then show "b divides c"

2197 by (rule fmsubset_divides) fact+

2198 next

2199 fix y

2200 assume "y \<in> carrier G"

2201 from wfactors_exist [OF this]

2202 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2203 by blast

2205 assume "a divides y"

2206 then have ya: "fmset G as \<subseteq># fmset G ys"

2207 by (rule divides_fmsubset) fact+

2209 assume "b divides y"

2210 then have yb: "fmset G bs \<subseteq># fmset G ys"

2211 by (rule divides_fmsubset) fact+

2213 from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"

2214 using subset_eq_diff_conv subset_mset.le_diff_conv2 by fastforce

2215 then show "c divides y"

2216 by (rule fmsubset_divides) fact+

2217 qed

2218 with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2219 by fast

2220 qed

2223 subsection \<open>Conditions for Factoriality\<close>

2225 subsubsection \<open>Gcd condition\<close>

2227 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:

2228 "weak_lower_semilattice (division_rel G)"

2229 proof -

2230 interpret weak_partial_order "division_rel G" ..

2231 show ?thesis

2232 proof (unfold_locales, simp_all)

2233 fix x y

2234 assume carr: "x \<in> carrier G" "y \<in> carrier G"

2235 from gcdof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"

2236 by blast

2237 with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2238 by (subst gcdof_greatestLower[symmetric], simp+)

2239 then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2240 by fast

2241 qed

2242 qed

2244 lemma (in gcd_condition_monoid) gcdof_cong_l:

2245 assumes a'a: "a' \<sim> a"

2246 and agcd: "a gcdof b c"

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

2248 shows "a' gcdof b c"

2249 proof -

2250 note carr = a'carr carr'

2251 interpret weak_lower_semilattice "division_rel G" by simp

2252 have "is_glb (division_rel G) a' {b, c}"

2253 by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)

2254 then have "a' \<in> carrier G \<and> a' gcdof b c"

2255 by (simp add: gcdof_greatestLower carr')

2256 then show ?thesis ..

2257 qed

2259 lemma (in gcd_condition_monoid) gcd_closed [simp]:

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

2261 shows "somegcd G a b \<in> carrier G"

2262 proof -

2263 interpret weak_lower_semilattice "division_rel G" by simp

2264 show ?thesis

2265 apply (simp add: somegcd_meet[OF carr])

2266 apply (rule meet_closed[simplified], fact+)

2267 done

2268 qed

2270 lemma (in gcd_condition_monoid) gcd_isgcd:

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

2272 shows "(somegcd G a b) gcdof a b"

2273 proof -

2274 interpret weak_lower_semilattice "division_rel G"

2275 by simp

2276 from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"

2277 by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)

2278 then show "(somegcd G a b) gcdof a b"

2279 by simp

2280 qed

2282 lemma (in gcd_condition_monoid) gcd_exists:

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

2284 shows "\<exists>x\<in>carrier G. x = somegcd G a b"

2285 proof -

2286 interpret weak_lower_semilattice "division_rel G"

2287 by simp

2288 show ?thesis

2289 by (metis carr(1) carr(2) gcd_closed)

2290 qed

2292 lemma (in gcd_condition_monoid) gcd_divides_l:

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

2294 shows "(somegcd G a b) divides a"

2295 proof -

2296 interpret weak_lower_semilattice "division_rel G"

2297 by simp

2298 show ?thesis

2299 by (metis carr(1) carr(2) gcd_isgcd isgcd_def)

2300 qed

2302 lemma (in gcd_condition_monoid) gcd_divides_r:

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

2304 shows "(somegcd G a b) divides b"

2305 proof -

2306 interpret weak_lower_semilattice "division_rel G"

2307 by simp

2308 show ?thesis

2309 by (metis carr gcd_isgcd isgcd_def)

2310 qed

2312 lemma (in gcd_condition_monoid) gcd_divides:

2313 assumes sub: "z divides x" "z divides y"

2314 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"

2315 shows "z divides (somegcd G x y)"

2316 proof -

2317 interpret weak_lower_semilattice "division_rel G"

2318 by simp

2319 show ?thesis

2320 by (metis gcd_isgcd isgcd_def assms)

2321 qed

2323 lemma (in gcd_condition_monoid) gcd_cong_l:

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

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

2326 shows "somegcd G x y \<sim> somegcd G x' y"

2327 proof -

2328 interpret weak_lower_semilattice "division_rel G"

2329 by simp

2330 show ?thesis

2331 apply (simp add: somegcd_meet carr)

2332 apply (rule meet_cong_l[simplified], fact+)

2333 done

2334 qed

2336 lemma (in gcd_condition_monoid) gcd_cong_r:

2337 assumes carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"

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

2339 shows "somegcd G x y \<sim> somegcd G x y'"

2340 proof -

2341 interpret weak_lower_semilattice "division_rel G" by simp

2342 show ?thesis

2343 apply (simp add: somegcd_meet carr)

2344 apply (rule meet_cong_r[simplified], fact+)

2345 done

2346 qed

2348 (*

2349 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:

2350 assumes carr: "b \<in> carrier G"

2351 shows "asc_cong (\<lambda>a. somegcd G a b)"

2352 using carr

2353 unfolding CONG_def

2354 by clarsimp (blast intro: gcd_cong_l)

2356 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:

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

2358 shows "asc_cong (\<lambda>b. somegcd G a b)"

2359 using carr

2360 unfolding CONG_def

2361 by clarsimp (blast intro: gcd_cong_r)

2363 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =

2364 assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]

2365 *)

2367 lemma (in gcd_condition_monoid) gcdI:

2368 assumes dvd: "a divides b" "a divides c"

2369 and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"

2370 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2371 shows "a \<sim> somegcd G b c"

2372 proof -

2373 have "\<exists>a. a \<in> carrier G \<and> a gcdof b c"

2374 by (simp add: bcarr ccarr gcdof_exists)

2375 moreover have "\<And>x. x \<in> carrier G \<and> x gcdof b c \<Longrightarrow> a \<sim> x"

2376 by (simp add: acarr associated_def dvd isgcd_def others)

2377 ultimately show ?thesis

2378 unfolding somegcd_def by (blast intro: someI2_ex)

2379 qed

2381 lemma (in gcd_condition_monoid) gcdI2:

2382 assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"

2383 shows "a \<sim> somegcd G b c"

2384 using assms unfolding isgcd_def

2385 by (simp add: gcdI)

2387 lemma (in gcd_condition_monoid) SomeGcd_ex:

2388 assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"

2389 shows "\<exists>x\<in> carrier G. x = SomeGcd G A"

2390 proof -

2391 interpret weak_lower_semilattice "division_rel G"

2392 by simp

2393 show ?thesis

2394 apply (simp add: SomeGcd_def)

2395 apply (rule finite_inf_closed[simplified], fact+)

2396 done

2397 qed

2399 lemma (in gcd_condition_monoid) gcd_assoc:

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

2401 shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"

2402 proof -

2403 interpret weak_lower_semilattice "division_rel G"

2404 by simp

2405 show ?thesis

2406 unfolding associated_def

2407 by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)

2408 qed

2410 lemma (in gcd_condition_monoid) gcd_mult:

2411 assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2412 shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2413 proof - (* following Jacobson, Basic Algebra, p.140 *)

2414 let ?d = "somegcd G a b"

2415 let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"

2416 note carr[simp] = acarr bcarr ccarr

2417 have dcarr: "?d \<in> carrier G" by simp

2418 have ecarr: "?e \<in> carrier G" by simp

2419 note carr = carr dcarr ecarr

2421 have "?d divides a" by (simp add: gcd_divides_l)

2422 then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)

2424 have "?d divides b" by (simp add: gcd_divides_r)

2425 then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)

2427 from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e"

2428 by (rule gcd_divides) simp_all

2429 then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u"

2430 by blast

2432 note carr = carr ucarr

2434 have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all

2435 then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x"

2436 by blast

2437 with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x"

2438 by simp

2440 from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)"

2441 by (simp add: m_assoc)

2442 then have "a = ?d \<otimes> u \<otimes> x"

2443 by (rule l_cancel[of c a]) (simp add: xcarr)+

2444 then have du'a: "?d \<otimes> u divides a"

2445 by (rule dividesI[OF xcarr])

2447 have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all

2448 then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x"

2449 by blast

2450 with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x"

2451 by simp

2453 from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)"

2454 by (simp add: m_assoc)

2455 with xcarr have "b = ?d \<otimes> u \<otimes> x"

2456 by (intro l_cancel[of c b]) simp_all

2457 then have du'b: "?d \<otimes> u divides b"

2458 by (intro dividesI[OF xcarr])

2460 from du'a du'b carr have du'd: "?d \<otimes> u divides ?d"

2461 by (intro gcd_divides) simp_all

2462 then have uunit: "u \<in> Units G"

2463 proof (elim dividesE)

2464 fix v

2465 assume vcarr[simp]: "v \<in> carrier G"

2466 assume d: "?d = ?d \<otimes> u \<otimes> v"

2467 have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact

2468 also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)

2469 finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .

2470 then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all

2471 then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm)

2472 from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G"

2473 by (auto simp: Units_def)

2474 qed

2476 from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"

2477 by (intro associatedI2[of u]) simp_all

2478 from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2479 by simp

2480 qed

2482 lemma (in monoid) assoc_subst:

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

2484 and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b

2485 \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b"

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

2487 shows "f a \<sim> f b"

2488 using assms by auto

2490 lemma (in gcd_condition_monoid) relprime_mult:

2491 assumes abrelprime: "somegcd G a b \<sim> \<one>"

2492 and acrelprime: "somegcd G a c \<sim> \<one>"

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

2494 shows "somegcd G a (b \<otimes> c) \<sim> \<one>"

2495 proof -

2496 have "c = c \<otimes> \<one>" by simp

2497 also from abrelprime[symmetric]

2498 have "\<dots> \<sim> c \<otimes> somegcd G a b"

2499 by (rule assoc_subst) (simp add: mult_cong_r)+

2500 also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2501 by (rule gcd_mult) fact+

2502 finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2503 by simp

2505 from carr have a: "a \<sim> somegcd G a (c \<otimes> a)"

2506 by (fast intro: gcdI divides_prod_l)

2508 have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)"

2509 by (simp add: m_comm)

2510 also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"

2511 by (rule assoc_subst) (simp add: gcd_cong_l)+

2512 also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"

2513 by (rule assoc_subst) simp+

2514 also from c[symmetric] have "\<dots> \<sim> somegcd G a c"

2515 by (rule assoc_subst) (simp add: gcd_cong_r)+

2516 also note acrelprime

2517 finally show "somegcd G a (b \<otimes> c) \<sim> \<one>"

2518 by simp

2519 qed

2521 lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"

2522 proof -

2523 have *: "p divides a \<or> p divides b"

2524 if pcarr[simp]: "p \<in> carrier G" and acarr[simp]: "a \<in> carrier G" and bcarr[simp]: "b \<in> carrier G"

2525 and pirr: "irreducible G p" and pdvdab: "p divides a \<otimes> b"

2526 for p a b

2527 proof -

2528 from pirr have pnunit: "p \<notin> Units G"

2529 and r: "\<And>b. \<lbrakk>b \<in> carrier G; properfactor G b p\<rbrakk> \<Longrightarrow> b \<in> Units G"

2530 by (fast elim: irreducibleE)+

2531 show "p divides a \<or> p divides b"

2532 proof (rule ccontr, clarsimp)

2533 assume npdvda: "\<not> p divides a" and npdvdb: "\<not> p divides b"

2534 have "\<one> \<sim> somegcd G p a"

2535 proof (intro gcdI unit_divides)

2536 show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides a\<rbrakk> \<Longrightarrow> y \<in> Units G"

2537 by (meson divides_trans npdvda pcarr properfactorI r)

2538 qed auto

2539 with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"

2540 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2541 have "\<one> \<sim> somegcd G p b"

2542 proof (intro gcdI unit_divides)

2543 show "\<And>y. \<lbrakk>y \<in> carrier G; y divides p; y divides b\<rbrakk> \<Longrightarrow> y \<in> Units G"

2544 by (meson divides_trans npdvdb pcarr properfactorI r)

2545 qed auto

2546 with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"

2547 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2548 have "p \<sim> somegcd G p (a \<otimes> b)"

2549 using pdvdab by (simp add: gcdI2 isgcd_divides_l)

2550 also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"

2551 by (rule relprime_mult)

2552 finally have "p \<sim> \<one>"

2553 by simp

2554 with pcarr have "p \<in> Units G"

2555 by (fast intro: assoc_unit_l)

2556 with pnunit show False ..

2557 qed

2558 qed

2559 show ?thesis

2560 by unfold_locales (metis * primeI irreducibleE)

2561 qed

2564 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid

2565 by (rule primeness_condition)

2568 subsubsection \<open>Divisor chain condition\<close>

2570 lemma (in divisor_chain_condition_monoid) wfactors_exist:

2571 assumes acarr: "a \<in> carrier G"

2572 shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2573 proof -

2574 have r: "a \<in> carrier G \<Longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"

2575 using division_wellfounded

2576 proof (induction rule: wf_induct_rule)

2577 case (less x)

2578 then have xcarr: "x \<in> carrier G"

2579 by auto

2580 show ?case

2581 proof (cases "x \<in> Units G")

2582 case True

2583 then show ?thesis

2584 by (metis bot.extremum list.set(1) unit_wfactors)

2585 next

2586 case xnunit: False

2587 show ?thesis

2588 proof (cases "irreducible G x")

2589 case True

2590 then show ?thesis

2591 by (rule_tac x="[x]" in exI) (simp add: wfactors_def xcarr)

2592 next

2593 case False

2594 then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G" and pfyx: "properfactor G y x"

2595 by (meson irreducible_def xnunit)

2596 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2597 using less ycarr pfyx by blast

2598 then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"

2599 by (meson dividesE pfyx properfactorE2)

2600 from zcarr ycarr have "properfactor G z x"

2601 using m_comm properfactorI3 x ynunit by blast

2602 with less zcarr obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"

2603 by blast

2604 from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"

2605 by simp

2606 have "wfactors G (ys@zs) (y\<otimes>z)"

2607 using xscarr ycarr yfs zcarr zfs by auto

2608 then have "wfactors G (ys@zs) x"

2609 by (simp add: x)

2610 with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"

2611 by fast

2612 qed

2613 qed

2614 qed

2615 from acarr show ?thesis by (rule r)

2616 qed

2619 subsubsection \<open>Primeness condition\<close>

2621 lemma (in comm_monoid_cancel) multlist_prime_pos:

2622 assumes aprime: "prime G a" and carr: "a \<in> carrier G"

2623 and as: "set as \<subseteq> carrier G" "a divides (foldr (\<otimes>) as \<one>)"

2624 shows "\<exists>i<length as. a divides (as!i)"

2625 using as

2626 proof (induction as)

2627 case Nil

2628 then show ?case

2629 by simp (meson Units_one_closed aprime carr divides_unit primeE)

2630 next

2631 case (Cons x as)

2632 then have "x \<in> carrier G" "set as \<subseteq> carrier G" and "a divides x \<otimes> foldr (\<otimes>) as \<one>"

2633 by (auto simp: )

2634 with carr aprime have "a divides x \<or> a divides foldr (\<otimes>) as \<one>"

2635 by (intro prime_divides) simp+

2636 then show ?case

2637 using Cons.IH Cons.prems(1) by force

2638 qed

2641 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:

2642 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>

2643 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2644 proof (induct as)

2645 case Nil

2646 show ?case

2647 apply (clarsimp simp: wfactors_def)

2648 by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)

2649 next

2650 case (Cons ah as)

2651 then show ?case

2652 proof clarsimp

2653 fix a as'

2654 assume ih [rule_format]:

2655 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>

2656 wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2657 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"

2658 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"

2659 and afs: "wfactors G (ah # as) a"

2660 and afs': "wfactors G as' a"

2661 then have ahdvda: "ah divides a"

2662 by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all

2663 then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"

2664 by blast

2665 have a'fs: "wfactors G as a'"

2666 apply (rule wfactorsE[OF afs], rule wfactorsI, simp)

2667 by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)

2668 from afs have ahirr: "irreducible G ah"

2669 by (elim wfactorsE) simp

2670 with ascarr have ahprime: "prime G ah"

2671 by (intro irreducible_prime ahcarr)

2673 note carr [simp] = acarr ahcarr ascarr as'carr a'carr

2675 note ahdvda

2676 also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"

2677 by (elim wfactorsE associatedE, simp)

2678 finally have "ah divides (foldr (\<otimes>) as' \<one>)"

2679 by simp

2680 with ahprime have "\<exists>i<length as'. ah divides as'!i"

2681 by (intro multlist_prime_pos) simp_all

2682 then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"

2683 by blast

2684 from afs' carr have irrasi: "irreducible G (as'!i)"

2685 by (fast intro: nth_mem[OF len] elim: wfactorsE)

2686 from len carr have asicarr[simp]: "as'!i \<in> carrier G"

2687 unfolding set_conv_nth by force

2688 note carr = carr asicarr

2690 from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"

2691 by blast

2692 with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"

2693 by (metis ahprime associatedI2 irreducible_prodE primeE)

2694 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']

2695 note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]

2696 note carr = carr partscarr

2698 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"

2699 by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)

2700 then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"

2701 by auto

2703 have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"

2704 by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)

2705 then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"

2706 and aa2fs: "wfactors G (drop (Suc i) as') aa_2"

2707 by auto

2709 note carr = carr aa1carr[simp] aa2carr[simp]

2711 from aa1fs aa2fs

2712 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"

2713 by (intro wfactors_mult, simp+)

2714 then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"

2715 using irrasi wfactors_mult_single by auto

2716 from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"

2717 by (metis irrasi wfactors_mult_single)

2718 with len carr aa1carr aa2carr aa1fs

2719 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"

2720 using wfactors_mult by auto

2721 from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"

2722 by (simp add: Cons_nth_drop_Suc)

2723 with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"

2724 by simp

2725 with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"

2726 by (metis as' ee_wfactorsD m_closed)

2727 then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"

2728 by (metis aa1carr aa2carr asicarr m_lcomm)

2729 from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"

2730 by (metis associated_sym m_closed mult_cong_l)

2731 also note t1

2732 finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp

2734 with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"

2735 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])

2737 note v1

2738 also note a'

2739 finally have "wfactors G (take i as' @ drop (Suc i) as') a'"

2740 by simp

2742 from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"

2743 by (intro ih[of a']) simp

2744 then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"

2745 by (elim essentially_equalE) (fastforce intro: essentially_equalI)

2747 from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')

2748 (as' ! i # take i as' @ drop (Suc i) as')"

2749 proof (intro essentially_equalI)

2750 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"

2751 by simp

2752 next

2753 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"

2754 by (simp add: list_all2_append) (simp add: asiah[symmetric])

2755 qed

2757 note ee1

2758 also note ee2

2759 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')

2760 (take i as' @ as' ! i # drop (Suc i) as')"

2761 by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)

2762 finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"

2763 by simp

2764 then show "essentially_equal G (ah # as) as'"

2765 by (subst as')

2766 qed

2767 qed

2769 lemma (in primeness_condition_monoid) wfactors_unique:

2770 assumes "wfactors G as a" "wfactors G as' a"

2771 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G"

2772 shows "essentially_equal G as as'"

2773 by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)

2776 subsubsection \<open>Application to factorial monoids\<close>

2778 text \<open>Number of factors for wellfoundedness\<close>

2780 definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"

2781 where "factorcount G a =

2782 (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)"

2784 lemma (in monoid) ee_length:

2785 assumes ee: "essentially_equal G as bs"

2786 shows "length as = length bs"

2787 by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)

2789 lemma (in factorial_monoid) factorcount_exists:

2790 assumes carr[simp]: "a \<in> carrier G"

2791 shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"

2792 proof -

2793 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2794 by (intro wfactors_exist) simp

2795 then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2796 by (auto simp del: carr)

2797 have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"

2798 by (metis afs ascarr assms ee_length wfactors_unique)

2799 then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..

2800 qed

2802 lemma (in factorial_monoid) factorcount_unique:

2803 assumes afs: "wfactors G as a"

2804 and acarr[simp]: "a \<in> carrier G" and ascarr: "set as \<subseteq> carrier G"

2805 shows "factorcount G a = length as"

2806 proof -

2807 have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

2808 by (rule factorcount_exists) simp

2809 then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

2810 by auto

2811 then have ac: "ac = factorcount G a"

2812 unfolding factorcount_def using ascarr by (blast intro: theI2 afs)

2813 from ascarr afs have "ac = length as"

2814 by (simp add: alen)

2815 with ac show ?thesis

2816 by simp

2817 qed

2819 lemma (in factorial_monoid) divides_fcount:

2820 assumes dvd: "a divides b"

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

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

2823 shows "factorcount G a \<le> factorcount G b"

2824 proof (rule dividesE[OF dvd])

2825 fix c

2826 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2827 by blast

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

2829 by blast

2830 with acarr have fca: "factorcount G a = length as"

2831 by (intro factorcount_unique)

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

2834 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

2835 by blast

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

2837 by blast

2839 note [simp] = acarr bcarr ccarr ascarr cscarr

2841 assume b: "b = a \<otimes> c"

2842 from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"

2843 by (intro wfactors_mult) simp_all

2844 with b have "wfactors G (as@cs) b"

2845 by simp

2846 then have "factorcount G b = length (as@cs)"

2847 by (intro factorcount_unique) simp_all

2848 then have "factorcount G b = length as + length cs"

2849 by simp

2850 with fca show ?thesis

2851 by simp

2852 qed

2854 lemma (in factorial_monoid) associated_fcount:

2855 assumes acarr: "a \<in> carrier G"

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

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

2858 shows "factorcount G a = factorcount G b"

2859 using assms

2860 by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)

2862 lemma (in factorial_monoid) properfactor_fcount:

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

2864 and pf: "properfactor G a b"

2865 shows "factorcount G a < factorcount G b"

2866 proof (rule properfactorE[OF pf], elim dividesE)

2867 fix c

2868 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2869 by blast

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

2871 by blast

2872 with acarr have fca: "factorcount G a = length as"

2873 by (intro factorcount_unique)

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

2876 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

2877 by blast

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

2879 by blast

2881 assume b: "b = a \<otimes> c"

2883 have "wfactors G (as@cs) (a \<otimes> c)"

2884 by (rule wfactors_mult) fact+

2885 with b have "wfactors G (as@cs) b"

2886 by simp

2887 with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"

2888 by (simp add: factorcount_unique)

2889 then have fcb: "factorcount G b = length as + length cs"

2890 by simp

2892 assume nbdvda: "\<not> b divides a"

2893 have "c \<notin> Units G"

2894 proof

2895 assume cunit:"c \<in> Units G"

2896 have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"

2897 by (simp add: b)

2898 also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"

2899 by (fast intro: m_assoc)

2900 also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp

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

2902 finally have "a = b \<otimes> inv c" by simp

2903 with ccarr cunit have "b divides a"

2904 by (fast intro: dividesI[of "inv c"])

2905 with nbdvda show False by simp

2906 qed

2907 with cfs have "length cs > 0"

2908 by (metis Units_one_closed assoc_unit_r ccarr foldr.simps(1) id_apply length_greater_0_conv wfactors_def)

2909 with fca fcb show ?thesis

2910 by simp

2911 qed

2913 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid

2914 apply unfold_locales

2915 apply (rule wfUNIVI)

2916 apply (rule measure_induct[of "factorcount G"])

2917 apply simp

2918 apply (metis properfactor_fcount)

2919 done

2921 sublocale factorial_monoid \<subseteq> primeness_condition_monoid

2922 by standard (rule irreducible_prime)

2925 lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..

2927 lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"

2928 by standard (rule gcdof_exists)

2930 sublocale factorial_monoid \<subseteq> gcd_condition_monoid

2931 by standard (rule gcdof_exists)

2933 lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"

2934 proof -

2935 interpret weak_lower_semilattice "division_rel G"

2936 by simp

2937 show "weak_lattice (division_rel G)"

2938 proof (unfold_locales, simp_all)

2939 fix x y

2940 assume carr: "x \<in> carrier G" "y \<in> carrier G"

2941 from lcmof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y"

2942 by blast

2943 with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"

2944 by (simp add: lcmof_leastUpper[symmetric])

2945 then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})"

2946 by blast

2947 qed

2948 qed

2951 subsection \<open>Factoriality Theorems\<close>

2953 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)

2954 "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G \<longleftrightarrow> factorial_monoid G"

2955 proof (rule iffI, clarify)

2956 assume dcc: "divisor_chain_condition_monoid G"

2957 and pc: "primeness_condition_monoid G"

2958 interpret divisor_chain_condition_monoid "G" by (rule dcc)

2959 interpret primeness_condition_monoid "G" by (rule pc)

2960 show "factorial_monoid G"

2961 by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)

2962 next

2963 assume "factorial_monoid G"

2964 then interpret factorial_monoid "G" .

2965 show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"

2966 by rule unfold_locales

2967 qed

2969 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)

2970 "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G \<longleftrightarrow> factorial_monoid G"

2971 proof (rule iffI, clarify)

2972 assume dcc: "divisor_chain_condition_monoid G"

2973 and gc: "gcd_condition_monoid G"

2974 interpret divisor_chain_condition_monoid "G" by (rule dcc)

2975 interpret gcd_condition_monoid "G" by (rule gc)

2976 show "factorial_monoid G"

2977 by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)

2978 next

2979 assume "factorial_monoid G"

2980 then interpret factorial_monoid "G" .

2981 show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"

2982 by rule unfold_locales

2983 qed

2985 end