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

src/HOL/Algebra/Divisibility.thy

author | haftmann |

Sat Dec 17 15:22:13 2016 +0100 (2016-12-17) | |

changeset 64587 | 8355a6e2df79 |

parent 63919 | 9aed2da07200 |

child 66453 | cc19f7ca2ed6 |

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

standardized notation

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 "~~/src/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) Units_m_closed[simp, intro]:

54 assumes h1unit: "h1 \<in> Units G"

55 and h2unit: "h2 \<in> Units G"

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

57 unfolding Units_def

58 using assms

59 by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)

61 lemma (in monoid) prod_unit_l:

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

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

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

65 shows "b \<in> Units G"

66 proof -

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

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

70 by (simp add: m_assoc)

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

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

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

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

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

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

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

79 by (simp add: m_assoc del: Units_l_inv)

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

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

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

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

85 qed

87 lemma (in monoid) prod_unit_r:

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

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

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

91 shows "a \<in> Units G"

92 proof -

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

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

96 by (simp add: m_assoc del: Units_r_inv)

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

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

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

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

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

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

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

105 by (simp add: m_assoc del: Units_l_inv)

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

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

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

110 qed

112 lemma (in comm_monoid) unit_factor:

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

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

115 shows "a \<in> Units G"

116 using abunit[simplified Units_def]

117 proof clarsimp

118 fix i

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

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

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

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

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

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

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

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

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

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

133 from carr' li' ri'

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

135 qed

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

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

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

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

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

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

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

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

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

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

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

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

157 where "prime G p \<longleftrightarrow>

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

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

162 subsubsection \<open>Divisibility\<close>

164 lemma dividesI:

165 fixes G (structure)

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

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

168 shows "a divides b"

169 unfolding factor_def using assms by fast

171 lemma dividesI' [intro]:

172 fixes G (structure)

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

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

175 shows "a divides b"

176 using assms by (fast intro: dividesI)

178 lemma dividesD:

179 fixes G (structure)

180 assumes "a divides b"

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

182 using assms unfolding factor_def by fast

184 lemma dividesE [elim]:

185 fixes G (structure)

186 assumes d: "a divides b"

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

188 shows "P"

189 proof -

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

191 then show P by (elim elim)

192 qed

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

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

196 shows "a divides a"

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

199 lemma (in monoid) divides_trans [trans]:

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

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

202 shows "a divides c"

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

205 lemma (in monoid) divides_mult_lI [intro]:

206 assumes ab: "a divides b"

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

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

209 using ab

210 apply (elim dividesE)

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

212 apply (fast intro: dividesI)

213 done

215 lemma (in monoid_cancel) divides_mult_l [simp]:

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

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

218 apply safe

219 apply (elim dividesE, intro dividesI, assumption)

220 apply (rule l_cancel[of c])

221 apply (simp add: m_assoc carr)+

222 apply (fast intro: carr)

223 done

225 lemma (in comm_monoid) divides_mult_rI [intro]:

226 assumes ab: "a divides b"

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

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

229 using carr ab

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

231 apply (rule divides_mult_lI, assumption+)

232 done

234 lemma (in comm_monoid_cancel) divides_mult_r [simp]:

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

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

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

239 lemma (in monoid) divides_prod_r:

240 assumes ab: "a divides b"

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

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

243 using ab carr by (fast intro: m_assoc)

245 lemma (in comm_monoid) divides_prod_l:

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

247 and ab: "a divides b"

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

249 using ab carr

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

251 apply (fast intro: divides_prod_r)

252 done

254 lemma (in monoid) unit_divides:

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

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

257 shows "u divides a"

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

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

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

261 by (fast intro: m_assoc[symmetric])

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

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

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

265 qed

267 lemma (in comm_monoid) divides_unit:

268 assumes udvd: "a divides u"

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

270 shows "a \<in> Units G"

271 using udvd carr by (blast intro: unit_factor)

273 lemma (in comm_monoid) Unit_eq_dividesone:

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

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

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

279 subsubsection \<open>Association\<close>

281 lemma associatedI:

282 fixes G (structure)

283 assumes "a divides b" "b divides a"

284 shows "a \<sim> b"

285 using assms by (simp add: associated_def)

287 lemma (in monoid) associatedI2:

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

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

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

291 shows "a \<sim> b"

292 using uunit bcarr

293 unfolding a

294 apply (intro associatedI)

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

296 apply (simp add: m_assoc Units_closed)

297 apply fast

298 done

300 lemma (in monoid) associatedI2':

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

302 and "u \<in> Units G"

303 and "b \<in> carrier G"

304 shows "a \<sim> b"

305 using assms by (intro associatedI2)

307 lemma associatedD:

308 fixes G (structure)

309 assumes "a \<sim> b"

310 shows "a divides b"

311 using assms by (simp add: associated_def)

313 lemma (in monoid_cancel) associatedD2:

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

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

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

317 using assoc

318 unfolding associated_def

319 proof clarify

320 assume "b divides a"

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

322 by (rule dividesE)

324 assume "a divides b"

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

326 by (rule dividesE)

327 note carr = carr ucarr u'carr

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

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

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

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

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

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

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

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

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

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

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

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

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

344 by fast

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

346 by (simp add: Units_def ucarr)

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

348 qed

350 lemma associatedE:

351 fixes G (structure)

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

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

354 shows "P"

355 proof -

356 from assoc have "a divides b" "b divides a"

357 by (simp_all add: associated_def)

358 then show P by (elim e)

359 qed

361 lemma (in monoid_cancel) associatedE2:

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

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

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

365 shows "P"

366 proof -

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

368 by (rule associatedD2)

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

370 by auto

371 then show P by (elim e)

372 qed

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

375 assumes "a \<in> carrier G"

376 shows "a \<sim> a"

377 using assms by (fast intro: associatedI)

379 lemma (in monoid) associated_sym [sym]:

380 assumes "a \<sim> b"

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

382 shows "b \<sim> a"

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

385 lemma (in monoid) associated_trans [trans]:

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

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

388 shows "a \<sim> c"

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

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

392 apply unfold_locales

393 apply simp_all

394 apply (metis associated_def)

395 apply (iprover intro: associated_trans)

396 done

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

401 lemma divides_antisym:

402 fixes G (structure)

403 assumes "a divides b" "b divides a"

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

405 shows "a \<sim> b"

406 using assms by (fast intro: associatedI)

408 lemma (in monoid) divides_cong_l [trans]:

409 assumes "x \<sim> x'"

410 and "x' divides y"

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

412 shows "x divides y"

413 proof -

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

415 also note assms(2)

416 finally show "x divides y" by simp

417 qed

419 lemma (in monoid) divides_cong_r [trans]:

420 assumes "x divides y"

421 and "y \<sim> y'"

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

423 shows "x divides y'"

424 proof -

425 note assms(1)

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

427 finally show "x divides y'" by simp

428 qed

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

431 "weak_partial_order (division_rel G)"

432 apply unfold_locales

433 apply simp_all

434 apply (simp add: associated_sym)

435 apply (blast intro: associated_trans)

436 apply (simp add: divides_antisym)

437 apply (blast intro: divides_trans)

438 apply (blast intro: divides_cong_l divides_cong_r associated_sym)

439 done

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

444 lemma (in monoid_cancel) mult_cong_r:

445 assumes "b \<sim> b'"

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

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

448 using assms

449 apply (elim associatedE2, intro associatedI2)

450 apply (auto intro: m_assoc[symmetric])

451 done

453 lemma (in comm_monoid_cancel) mult_cong_l:

454 assumes "a \<sim> a'"

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

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

457 using assms

458 apply (elim associatedE2, intro associatedI2)

459 apply assumption

460 apply (simp add: m_assoc Units_closed)

461 apply (simp add: m_comm Units_closed)

462 apply simp_all

463 done

465 lemma (in monoid_cancel) assoc_l_cancel:

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

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

468 shows "b \<sim> b'"

469 using assms

470 apply (elim associatedE2, intro associatedI2)

471 apply assumption

472 apply (rule l_cancel[of a])

473 apply (simp add: m_assoc Units_closed)

474 apply fast+

475 done

477 lemma (in comm_monoid_cancel) assoc_r_cancel:

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

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

480 shows "a \<sim> a'"

481 using assms

482 apply (elim associatedE2, intro associatedI2)

483 apply assumption

484 apply (rule r_cancel[of a b])

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

486 apply fast+

487 done

490 subsubsection \<open>Units\<close>

492 lemma (in monoid_cancel) assoc_unit_l [trans]:

493 assumes "a \<sim> b"

494 and "b \<in> Units G"

495 and "a \<in> carrier G"

496 shows "a \<in> Units G"

497 using assms by (fast elim: associatedE2)

499 lemma (in monoid_cancel) assoc_unit_r [trans]:

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

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

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

503 shows "b \<in> Units G"

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

506 lemma (in comm_monoid) Units_cong:

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

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

509 shows "b \<in> Units G"

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

512 lemma (in monoid) Units_assoc:

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

514 shows "a \<sim> b"

515 using units by (fast intro: associatedI unit_divides)

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

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

519 proof clarsimp

520 fix a

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

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

523 apply (rule associatedI)

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

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

526 done

527 next

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

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

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

531 qed

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

534 apply (simp add: Units_def Lower_def)

535 apply (rule, rule)

536 apply clarsimp

537 apply (rule unit_divides)

538 apply (unfold Units_def, fast)

539 apply assumption

540 apply clarsimp

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

542 done

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

547 lemma properfactorI:

548 fixes G (structure)

549 assumes "a divides b"

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

551 shows "properfactor G a b"

552 using assms unfolding properfactor_def by simp

554 lemma properfactorI2:

555 fixes G (structure)

556 assumes advdb: "a divides b"

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

558 shows "properfactor G a b"

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

560 assume "b divides a"

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

562 with neq show "False" by fast

563 qed

565 lemma (in comm_monoid_cancel) properfactorI3:

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

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

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

569 shows "properfactor G a p"

570 unfolding p

571 using carr

572 apply (intro properfactorI, fast)

573 proof (clarsimp, elim dividesE)

574 fix c

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

576 note [simp] = carr ccarr

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

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

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

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

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

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

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

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

588 unfolding Units_def by fastforce

589 with nunit show False ..

590 qed

592 lemma properfactorE:

593 fixes G (structure)

594 assumes pf: "properfactor G a b"

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

596 shows "P"

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

599 lemma properfactorE2:

600 fixes G (structure)

601 assumes pf: "properfactor G a b"

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

603 shows "P"

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

606 lemma (in monoid) properfactor_unitE:

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

608 and pf: "properfactor G a u"

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

610 shows "P"

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

613 lemma (in monoid) properfactor_divides:

614 assumes pf: "properfactor G a b"

615 shows "a divides b"

616 using pf by (elim properfactorE)

618 lemma (in monoid) properfactor_trans1 [trans]:

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

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

621 shows "properfactor G a c"

622 using dvds carr

623 apply (elim properfactorE, intro properfactorI)

624 apply (iprover intro: divides_trans)+

625 done

627 lemma (in monoid) properfactor_trans2 [trans]:

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

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

630 shows "properfactor G a c"

631 using dvds carr

632 apply (elim properfactorE, intro properfactorI)

633 apply (iprover intro: divides_trans)+

634 done

636 lemma properfactor_lless:

637 fixes G (structure)

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

639 apply (rule ext)

640 apply (rule ext)

641 apply rule

642 apply (fastforce elim: properfactorE2 intro: weak_llessI)

643 apply (fastforce elim: weak_llessE intro: properfactorI2)

644 done

646 lemma (in monoid) properfactor_cong_l [trans]:

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

648 and pf: "properfactor G x y"

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

650 shows "properfactor G x' y"

651 using pf

652 unfolding properfactor_lless

653 proof -

654 interpret weak_partial_order "division_rel G" ..

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

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

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

658 qed

660 lemma (in monoid) properfactor_cong_r [trans]:

661 assumes pf: "properfactor G x y"

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

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

664 shows "properfactor G x y'"

665 using pf

666 unfolding properfactor_lless

667 proof -

668 interpret weak_partial_order "division_rel G" ..

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

670 also from yy'

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

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

673 qed

675 lemma (in monoid_cancel) properfactor_mult_lI [intro]:

676 assumes ab: "properfactor G a b"

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

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

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

681 lemma (in monoid_cancel) properfactor_mult_l [simp]:

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

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

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

686 lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:

687 assumes ab: "properfactor G a b"

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

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

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

692 lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:

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

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

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

697 lemma (in monoid) properfactor_prod_r:

698 assumes ab: "properfactor G a b"

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

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

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

703 lemma (in comm_monoid) properfactor_prod_l:

704 assumes ab: "properfactor G a b"

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

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

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

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

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

714 lemma irreducibleI:

715 fixes G (structure)

716 assumes "a \<notin> Units G"

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

718 shows "irreducible G a"

719 using assms unfolding irreducible_def by blast

721 lemma irreducibleE:

722 fixes G (structure)

723 assumes irr: "irreducible G a"

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

725 shows "P"

726 using assms unfolding irreducible_def by blast

728 lemma irreducibleD:

729 fixes G (structure)

730 assumes irr: "irreducible G a"

731 and pf: "properfactor G b a"

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

733 shows "b \<in> Units G"

734 using assms by (fast elim: irreducibleE)

736 lemma (in monoid_cancel) irreducible_cong [trans]:

737 assumes irred: "irreducible G a"

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

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

740 shows "irreducible G a'"

741 using assms

742 apply (elim irreducibleE, intro irreducibleI)

743 apply simp_all

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

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

746 done

748 lemma (in monoid) irreducible_prod_rI:

749 assumes airr: "irreducible G a"

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

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

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

753 using airr carr bunit

754 apply (elim irreducibleE, intro irreducibleI, clarify)

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

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

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

758 done

760 lemma (in comm_monoid) irreducible_prod_lI:

761 assumes birr: "irreducible G b"

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

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

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

765 apply (subst m_comm, simp+)

766 apply (intro irreducible_prod_rI assms)

767 done

769 lemma (in comm_monoid_cancel) irreducible_prodE [elim]:

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

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

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

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

774 shows P

775 using irr

776 proof (elim irreducibleE)

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

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

779 show P

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

781 case aunit: True

782 have "irreducible G b"

783 proof (rule irreducibleI, rule notI)

784 assume "b \<in> Units G"

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

786 with abnunit show "False" ..

787 next

788 fix c

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

790 and "properfactor G c b"

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

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

793 qed

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

795 next

796 case anunit: False

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

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

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

801 have "irreducible G a"

802 proof (rule irreducibleI, rule notI)

803 assume "a \<in> Units G"

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

805 with abnunit show "False" ..

806 next

807 fix c

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

809 and "properfactor G c a"

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

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

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

813 qed

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

815 qed

816 qed

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

821 lemma primeI:

822 fixes G (structure)

823 assumes "p \<notin> Units G"

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

825 shows "prime G p"

826 using assms unfolding prime_def by blast

828 lemma primeE:

829 fixes G (structure)

830 assumes pprime: "prime G p"

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

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

833 shows "P"

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

836 lemma (in comm_monoid_cancel) prime_divides:

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

838 and pprime: "prime G p"

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

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

841 using assms by (blast elim: primeE)

843 lemma (in monoid_cancel) prime_cong [trans]:

844 assumes pprime: "prime G p"

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

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

847 shows "prime G p'"

848 using pprime

849 apply (elim primeE, intro primeI)

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

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

852 done

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

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

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

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

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

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

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

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

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

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

872 locale factorial_monoid = comm_monoid_cancel +

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

874 and factors_unique:

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

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

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

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

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

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

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

886 using assms by (induct as) simp_all

888 lemma (in monoid) listassoc_sym [sym]:

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

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

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

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

893 using assms

894 proof (induct as arbitrary: bs, simp)

895 case Cons

896 then show ?case

897 apply (induct bs)

898 apply simp

899 apply clarsimp

900 apply (iprover intro: associated_sym)

901 done

902 qed

904 lemma (in monoid) listassoc_trans [trans]:

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

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

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

908 using assms

909 apply (simp add: list_all2_conv_all_nth set_conv_nth, safe)

910 apply (rule associated_trans)

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

912 apply (simp, simp)

913 apply blast+

914 done

916 lemma (in monoid_cancel) irrlist_listassoc_cong:

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

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

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

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

921 using assms

922 apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)

923 apply (blast intro: irreducible_cong)

924 done

927 text \<open>Permutations\<close>

929 lemma perm_map [intro]:

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

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

932 using p by induct auto

934 lemma perm_map_switch:

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

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

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

939 lemma (in monoid) perm_assoc_switch:

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

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

942 using p a

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

944 apply (clarsimp simp add: list_all2_Cons2, blast)

945 apply (clarsimp simp add: list_all2_Cons2)

946 apply blast

947 apply blast

948 done

950 lemma (in monoid) perm_assoc_switch_r:

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

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

953 using p a

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

955 apply (clarsimp simp add: list_all2_Cons1, blast)

956 apply (clarsimp simp add: list_all2_Cons1)

957 apply blast

958 apply blast

959 done

961 declare perm_sym [sym]

963 lemma perm_setP:

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

965 and as: "P (set as)"

966 shows "P (set bs)"

967 proof -

968 from perm have "mset as = mset bs"

969 by (simp add: mset_eq_perm)

970 then have "set as = set bs"

971 by (rule mset_eq_setD)

972 with as show "P (set bs)"

973 by simp

974 qed

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

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

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

983 lemma (in monoid) essentially_equalI:

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

985 shows "essentially_equal G fs1 fs2"

986 using ex unfolding essentially_equal_def by fast

988 lemma (in monoid) essentially_equalE:

989 assumes ee: "essentially_equal G fs1 fs2"

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

991 shows "P"

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

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

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

996 shows "essentially_equal G as as"

997 using carr by (fast intro: essentially_equalI)

999 lemma (in monoid) ee_sym [sym]:

1000 assumes ee: "essentially_equal G as bs"

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

1002 shows "essentially_equal G bs as"

1003 using ee

1004 proof (elim essentially_equalE)

1005 fix fs

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

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

1008 by blast

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

1010 with a[symmetric] carr show ?thesis

1011 by (iprover intro: essentially_equalI perm_closed)

1012 qed

1014 lemma (in monoid) ee_trans [trans]:

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

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

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

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

1019 shows "essentially_equal G as cs"

1020 using ab bc

1021 proof (elim essentially_equalE)

1022 fix abs bcs

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

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

1025 by blast

1027 assume "as <~~> abs"

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

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

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

1032 note a

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

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

1035 with pp show ?thesis

1036 by (rule essentially_equalI)

1037 qed

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

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

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

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

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

1047 using ascarr by (induct fs) simp_all

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

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

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

1052 using assms

1053 apply (induct fs)

1054 apply simp

1055 apply (case_tac "f = a")

1056 apply simp

1057 apply (fast intro: dividesI)

1058 apply clarsimp

1059 apply (metis assms(2) divides_prod_l multlist_closed)

1060 done

1062 lemma (in comm_monoid_cancel) multlist_listassoc_cong:

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

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

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

1066 using assms

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

1068 case (Cons a as fs')

1069 then show ?case

1070 apply (induct fs', simp)

1071 proof clarsimp

1072 fix b bs

1073 assume "a \<sim> b"

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

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

1076 then have p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>"

1077 by (fast intro: mult_cong_l)

1078 also

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

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

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

1082 then have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp

1083 with ascarr bscarr bcarr have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"

1084 by (fast intro: mult_cong_r)

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

1086 by (simp add: ascarr bscarr acarr bcarr)

1087 qed

1088 qed

1090 lemma (in comm_monoid) multlist_perm_cong:

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

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

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

1094 using prm ascarr

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

1096 proof clarsimp

1097 fix xs ys zs

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

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

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

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

1102 qed

1104 lemma (in comm_monoid_cancel) multlist_ee_cong:

1105 assumes "essentially_equal G fs fs'"

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

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

1108 using assms

1109 apply (elim essentially_equalE)

1110 apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)

1111 done

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

1116 lemma wfactorsI:

1117 fixes G (structure)

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

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

1120 shows "wfactors G fs a"

1121 using assms unfolding wfactors_def by simp

1123 lemma wfactorsE:

1124 fixes G (structure)

1125 assumes wf: "wfactors G fs a"

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

1127 shows "P"

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

1130 lemma (in monoid) factorsI:

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

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

1133 shows "factors G fs a"

1134 using assms unfolding factors_def by simp

1136 lemma factorsE:

1137 fixes G (structure)

1138 assumes f: "factors G fs a"

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

1140 shows "P"

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

1143 lemma (in monoid) factors_wfactors:

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

1145 shows "wfactors G as a"

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

1148 lemma (in monoid) wfactors_factors:

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

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

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

1153 lemma (in monoid) factors_closed [dest]:

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

1155 shows "a \<in> carrier G"

1156 using assms by (elim factorsE, clarsimp)

1158 lemma (in monoid) nunit_factors:

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

1160 and fs: "factors G as a"

1161 shows "length as > 0"

1162 proof -

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

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

1165 qed

1167 lemma (in monoid) unit_wfactors [simp]:

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

1169 shows "wfactors G [] a"

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

1172 lemma (in comm_monoid_cancel) unit_wfactors_empty:

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

1174 and wf: "wfactors G fs a"

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

1176 shows "fs = []"

1177 proof (cases fs)

1178 case Nil

1179 then show ?thesis .

1180 next

1181 case fs: (Cons f fs')

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

1183 by (simp_all add: fs)

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

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

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

1190 note aunit

1191 also from fs wf

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

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

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

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

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

1197 with fnunit show ?thesis by contradiction

1198 qed

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

1203 lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l:

1204 assumes fact: "wfactors G fs a"

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

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

1207 shows "wfactors G fs' a"

1208 using fact

1209 apply (elim wfactorsE, intro wfactorsI)

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

1211 proof -

1212 from asc[symmetric] have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>"

1213 by (simp add: multlist_listassoc_cong carr)

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

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

1216 qed

1218 lemma (in comm_monoid) wfactors_perm_cong_l:

1219 assumes "wfactors G fs a"

1220 and "fs <~~> fs'"

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

1222 shows "wfactors G fs' a"

1223 using assms

1224 apply (elim wfactorsE, intro wfactorsI)

1225 apply (rule irrlist_perm_cong, assumption+)

1226 apply (simp add: multlist_perm_cong[symmetric])

1227 done

1229 lemma (in comm_monoid_cancel) wfactors_ee_cong_l [trans]:

1230 assumes ee: "essentially_equal G as bs"

1231 and bfs: "wfactors G bs b"

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

1233 shows "wfactors G as b"

1234 using ee

1235 proof (elim essentially_equalE)

1236 fix fs

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

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

1240 note bfs

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

1242 also (wfactors_listassoc_cong_l)

1243 note prm[symmetric]

1244 finally (wfactors_perm_cong_l)

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

1246 qed

1248 lemma (in monoid) wfactors_cong_r [trans]:

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

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

1251 shows "wfactors G fs a'"

1252 using fac

1253 proof (elim wfactorsE, intro wfactorsI)

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

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

1256 qed

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

1261 lemma (in comm_monoid_cancel) unitfactor_ee:

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

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

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

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

1266 using assms

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

1268 apply (cases as, simp)

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

1270 done

1272 lemma (in comm_monoid_cancel) factors_cong_unit:

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

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

1275 and afs: "factors G as a"

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

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

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

1279 using assms

1280 apply (elim factorsE, clarify)

1281 apply (cases as)

1282 apply (simp add: nunit_factors)

1283 apply clarsimp

1284 apply (elim factorsE, intro factorsI)

1285 apply (clarsimp, fast intro: irreducible_prod_rI)

1286 apply (simp add: m_ac Units_closed)

1287 done

1289 lemma (in comm_monoid) perm_wfactorsD:

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

1291 and afs: "wfactors G as a"

1292 and bfs: "wfactors G bs b"

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

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

1295 shows "a \<sim> b"

1296 using afs bfs

1297 proof (elim wfactorsE)

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

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

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

1301 also from prm

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

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

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

1305 qed

1307 lemma (in comm_monoid_cancel) listassoc_wfactorsD:

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

1309 and afs: "wfactors G as a"

1310 and bfs: "wfactors G bs b"

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

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

1313 shows "a \<sim> b"

1314 using afs bfs

1315 proof (elim wfactorsE)

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

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

1318 also from assoc

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

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

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

1322 qed

1324 lemma (in comm_monoid_cancel) ee_wfactorsD:

1325 assumes ee: "essentially_equal G as bs"

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

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

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

1329 shows "a \<sim> b"

1330 using ee

1331 proof (elim essentially_equalE)

1332 fix fs

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

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

1335 by (simp add: perm_closed)

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

1337 by (rule wfactors_perm_cong_l) simp

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

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

1340 by (rule listassoc_wfactorsD) simp_all

1341 qed

1343 lemma (in comm_monoid_cancel) ee_factorsD:

1344 assumes ee: "essentially_equal G as bs"

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

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

1347 shows "a \<sim> b"

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

1350 lemma (in factorial_monoid) ee_factorsI:

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

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

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

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

1355 shows "essentially_equal G as bs"

1356 proof -

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

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

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

1361 by (elim associatedE2)

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

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

1365 by (rule unitfactor_ee)

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

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

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

1371 by (rule factors_cong_unit)

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

1374 have "essentially_equal G as ?bs'"

1375 by (blast intro: factors_unique)

1376 also note ee

1377 finally show "essentially_equal G as bs"

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

1379 qed

1381 lemma (in factorial_monoid) ee_wfactorsI:

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

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

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

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

1386 shows "essentially_equal G as bs"

1387 using assms

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

1389 case aunit: True

1390 also note asc

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

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

1394 by (rule unit_wfactors_empty)

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

1396 by (rule unit_wfactors_empty)

1398 have "essentially_equal G [] []"

1399 by (fast intro: essentially_equalI)

1400 then show ?thesis

1401 by (simp add: e e')

1402 next

1403 case anunit: False

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

1405 proof clarify

1406 assume "b \<in> Units G"

1407 also note asc[symmetric]

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

1409 with anunit show False ..

1410 qed

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

1413 by blast

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

1415 by fast

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

1418 proof clarify

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

1420 also note a'

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

1422 with anunit

1423 show "False" ..

1424 qed

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

1427 by blast

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

1429 by fast

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

1432 proof clarify

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

1434 also note b'

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

1436 with bnunit show False ..

1437 qed

1439 note a'

1440 also note asc

1441 also note b'[symmetric]

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

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

1444 by (rule ee_factorsI)

1445 qed

1447 lemma (in factorial_monoid) ee_wfactors:

1448 assumes asf: "wfactors G as a"

1449 and bsf: "wfactors G bs b"

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

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

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

1453 using assms by (fast intro: ee_wfactorsI ee_wfactorsD)

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

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

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

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

1459 case True

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

1461 then show ?thesis by (intro exI) force

1462 next

1463 case False

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

1465 by blast

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

1467 with fscarr show ?thesis by fast

1468 qed

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

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

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

1473 unfolding wfactors_def using assms by blast

1475 lemma (in factorial_monoid) wfactors_unique:

1476 assumes "wfactors G fs a"

1477 and "wfactors G fs' a"

1478 and "a \<in> carrier G"

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

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

1481 shows "essentially_equal G fs fs'"

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

1484 lemma (in monoid) factors_mult_single:

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

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

1487 using assms unfolding factors_def by simp

1489 lemma (in monoid_cancel) wfactors_mult_single:

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

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

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

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

1495 lemma (in monoid) factors_mult:

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

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

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

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

1500 using assms

1501 unfolding factors_def

1502 apply safe

1503 apply force

1504 apply hypsubst_thin

1505 apply (induct fa)

1506 apply simp

1507 apply (simp add: m_assoc)

1508 done

1510 lemma (in comm_monoid_cancel) wfactors_mult [intro]:

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

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

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

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

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

1516 proof clarsimp

1517 fix a' b'

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

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

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

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

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

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

1526 by (rule factors_mult) fact+

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

1529 by (intro factors_wfactors) simp_all

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

1531 by (intro mult_cong_r)

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

1533 by (intro mult_cong_l)

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

1535 by (simp add: carr)

1536 qed

1538 lemma (in comm_monoid) factors_dividesI:

1539 assumes "factors G fs a"

1540 and "f \<in> set fs"

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

1542 shows "f divides a"

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

1545 lemma (in comm_monoid) wfactors_dividesI:

1546 assumes p: "wfactors G fs a"

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

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

1549 shows "f divides a"

1550 using wfactors_factors[OF p fscarr]

1551 proof clarsimp

1552 fix a'

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

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

1555 by (simp add: factors_closed)

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

1558 by (fast intro: factors_dividesI)

1559 also note a'a

1560 finally show "f divides a"

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

1562 qed

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

1567 lemma (in comm_monoid_cancel) factorial_monoidI:

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

1569 and wfactors_unique:

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

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

1572 shows "factorial_monoid G"

1573 proof

1574 fix a

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

1577 from wfactors_exists[OF acarr]

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

1579 by blast

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

1581 by blast

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

1583 by fast

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

1585 proof clarify

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

1587 also note a'a

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

1589 with anunit show False ..

1590 qed

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

1593 by (blast elim: associatedE2)

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

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

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

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

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

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

1603 by (cases as) auto

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

1606 by (simp add: a factors_cong_unit)

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

1608 by fast

1609 qed (blast intro: factors_wfactors wfactors_unique)

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

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

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

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

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

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

1625 lemma (in monoid) assocs_repr_independence:

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

1627 and "x \<in> carrier G"

1628 shows "assocs G x = assocs G y"

1629 using assms

1630 apply safe

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

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

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

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

1635 done

1637 lemma (in monoid) assocs_self:

1638 assumes "x \<in> carrier G"

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

1640 using assms by (fastforce intro: closure_ofI2)

1642 lemma (in monoid) assocs_repr_independenceD:

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

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

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

1646 unfolding repr using ycarr by (intro assocs_self)

1648 lemma (in comm_monoid) assocs_assoc:

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

1650 and "b \<in> carrier G"

1651 shows "a \<sim> b"

1652 using assms by (elim closure_ofE2) simp

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

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

1659 lemma (in monoid) fmset_perm_cong:

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

1661 shows "fmset G as = fmset G bs"

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

1664 lemma (in comm_monoid_cancel) eqc_listassoc_cong:

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

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

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

1668 using assms

1669 apply (induct as arbitrary: bs, simp)

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

1671 apply (clarsimp elim!: closure_ofE2) defer 1

1672 apply (clarsimp elim!: closure_ofE2) defer 1

1673 proof -

1674 fix a x z

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

1676 assume "x \<sim> a"

1677 also assume "a \<sim> z"

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

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

1680 by (intro closure_ofI2) simp_all

1681 next

1682 fix a x z

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

1684 assume "x \<sim> z"

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

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

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

1688 by (intro closure_ofI2) simp_all

1689 qed

1691 lemma (in comm_monoid_cancel) fmset_listassoc_cong:

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

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

1694 shows "fmset G as = fmset G bs"

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

1697 lemma (in comm_monoid_cancel) ee_fmset:

1698 assumes ee: "essentially_equal G as bs"

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

1700 shows "fmset G as = fmset G bs"

1701 using ee

1702 proof (elim essentially_equalE)

1703 fix as'

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

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

1706 by (rule perm_closed)

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

1709 by (rule fmset_perm_cong)

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

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

1712 by (simp add: fmset_listassoc_cong)

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

1714 qed

1716 lemma (in monoid_cancel) fmset_ee__hlp_induct:

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

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

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

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

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

1722 apply safe

1723 apply (simp_all del: mset_map)

1724 apply (simp add: map_eq_Cons_conv)

1725 apply blast

1726 apply force

1727 proof -

1728 fix ys as bs

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

1730 and r1[rule_format]:

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

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

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

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

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

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

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

1739 by (simp add: mset_eq_perm del: mset_map)

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

1741 by (rule mset_eq_setD)

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

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

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

1746 proof (induct ys)

1747 case Nil

1748 then show ?case by simp

1749 next

1750 case Cons

1751 then show ?case

1752 proof clarsimp

1753 fix yy x

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

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

1756 qed

1757 qed

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

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

1761 by (intro r1) simp

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

1763 by auto

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

1766 by (intro r2) simp

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

1768 by auto

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

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

1772 by blast

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

1775 by fast

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

1777 by simp

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

1779 by fast

1780 qed

1782 lemma (in comm_monoid_cancel) fmset_ee:

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

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

1785 shows "essentially_equal G as bs"

1786 proof -

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

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

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

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

1793 from cas_def cbs_def mpp have [rule_format]:

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

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

1796 by (intro fmset_ee__hlp_induct, simp+)

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

1798 by simp

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

1801 by auto

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

1803 by (rule map_eq_imp_length_eq)

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

1805 by (simp add: mset_eq_perm mset_eq_setD)

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

1807 by simp

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

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

1811 with tp show "essentially_equal G as bs"

1812 by (fast intro: essentially_equalI)

1813 qed

1815 lemma (in comm_monoid_cancel) ee_is_fmset:

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

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

1818 using assms by (fast intro: ee_fmset fmset_ee)

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

1823 lemma (in monoid) mset_fmsetEx:

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

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

1826 proof -

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

1828 by blast

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

1830 using elems

1831 unfolding Cs

1832 apply (induct Cs', simp)

1833 proof (clarsimp simp del: mset_map)

1834 fix a Cs' cs

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

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

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

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

1839 by auto

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

1841 by simp

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

1843 by simp

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

1845 by fast

1846 qed

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

1848 qed

1850 lemma (in monoid) mset_wfactorsEx:

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

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

1853 proof -

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

1855 by (intro mset_fmsetEx, rule elems)

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

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

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

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

1860 by (intro wfactors_prod_exists) auto

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

1862 with cscarr Cs show ?thesis by fast

1863 qed

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

1868 lemma (in factorial_monoid) mult_wfactors_fmset:

1869 assumes afs: "wfactors G as a"

1870 and bfs: "wfactors G bs b"

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

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

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

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

1875 proof -

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

1877 by (intro wfactors_mult)

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

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

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

1881 by (intro ee_fmset) simp_all

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

1883 by (simp add: fmset_def)

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

1885 qed

1887 lemma (in factorial_monoid) mult_factors_fmset:

1888 assumes afs: "factors G as a"

1889 and bfs: "factors G bs b"

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

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

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

1893 using assms by (blast intro: factors_wfactors mult_wfactors_fmset)

1895 lemma (in comm_monoid_cancel) fmset_wfactors_mult:

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

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

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

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

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

1901 proof -

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

1903 by (intro wfactors_mult)

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

1906 by (simp add: fmset_def)

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

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

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

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

1911 qed

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

1916 lemma (in factorial_monoid) divides_fmsubset:

1917 assumes ab: "a divides b"

1918 and afs: "wfactors G as a"

1919 and bfs: "wfactors G bs b"

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

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

1922 using ab

1923 proof (elim dividesE)

1924 fix c

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

1926 from wfactors_exist [OF this]

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

1928 by blast

1929 note carr = carr ccarr cscarr

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

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

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

1934 then show ?thesis by simp

1935 qed

1937 lemma (in comm_monoid_cancel) fmsubset_divides:

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

1939 and afs: "wfactors G as a"

1940 and bfs: "wfactors G bs b"

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

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

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

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

1945 shows "a divides b"

1946 proof -

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

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

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

1951 proof (intro mset_wfactorsEx, simp)

1952 fix X

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

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

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

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

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

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

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

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

1962 by fast

1963 qed

1964 then obtain c cs

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

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

1967 and csf: "wfactors G cs c"

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

1970 from csmset msubset

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

1972 by (simp add: multiset_eq_iff subseteq_mset_def)

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

1974 by (rule fmset_wfactors_mult) fact+

1975 then show ?thesis

1976 proof (elim associatedE2)

1977 fix u

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

1979 with acarr ccarr show "a divides b"

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

1981 qed (simp_all add: acarr bcarr ccarr)

1982 qed

1984 lemma (in factorial_monoid) divides_as_fmsubset:

1985 assumes "wfactors G as a"

1986 and "wfactors G bs b"

1987 and "a \<in> carrier G"

1988 and "b \<in> carrier G"

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

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

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

1992 using assms

1993 by (blast intro: divides_fmsubset fmsubset_divides)

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

1998 lemma (in factorial_monoid) fmset_properfactor:

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

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

2001 and "wfactors G as a"

2002 and "wfactors G bs b"

2003 and "a \<in> carrier G"

2004 and "b \<in> carrier G"

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

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

2007 shows "properfactor G a b"

2008 apply (rule properfactorI)

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

2010 proof

2011 assume "b divides a"

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

2013 by (rule divides_fmsubset) fact+

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

2015 by (rule subset_mset.antisym)

2016 with anb show False ..

2017 qed

2019 lemma (in factorial_monoid) properfactor_fmset:

2020 assumes pf: "properfactor G a b"

2021 and "wfactors G as a"

2022 and "wfactors G bs b"

2023 and "a \<in> carrier G"

2024 and "b \<in> carrier G"

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

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

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

2028 using pf

2029 apply (elim properfactorE)

2030 apply rule

2031 apply (intro divides_fmsubset, assumption)

2032 apply (rule assms)+

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

2034 apply auto

2035 done

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

2039 lemma (in factorial_monoid) irreducible_prime:

2040 assumes pirr: "irreducible G p"

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

2042 shows "prime G p"

2043 using pirr

2044 proof (elim irreducibleE, intro primeI)

2045 fix a b

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

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

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

2049 assume irreduc[rule_format]:

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

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

2052 by (rule dividesE)

2054 from wfactors_exist [OF acarr]

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

2056 by blast

2058 from wfactors_exist [OF bcarr]

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

2060 by auto

2062 from wfactors_exist [OF ccarr]

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

2064 by auto

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

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

2069 by (rule wfactors_mult) fact+

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

2072 by (rule wfactors_mult_single) fact+

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

2074 by simp

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

2077 by (rule wfactors_unique) simp+

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

2080 by (fast elim: essentially_equalE)

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

2082 by (simp add: perm_set_eq[symmetric])

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

2084 unfolding list_all2_conv_all_nth set_conv_nth by force

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

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

2087 proof cases

2088 case 1

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

2091 note pp'

2092 also from afs

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

2094 finally have "p divides a" by simp

2095 then show ?thesis ..

2096 next

2097 case 2

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

2100 note pp'

2101 also from bfs

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

2103 finally have "p divides b" by simp

2104 then show ?thesis ..

2105 qed

2106 qed

2109 \<comment>"A version using @{const factors}, more complicated"

2110 lemma (in factorial_monoid) factors_irreducible_prime:

2111 assumes pirr: "irreducible G p"

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

2113 shows "prime G p"

2114 using pirr

2115 apply (elim irreducibleE, intro primeI)

2116 apply assumption

2117 proof -

2118 fix a b

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

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

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

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

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

2124 by (rule dividesE)

2125 note [simp] = pcarr acarr bcarr ccarr

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

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

2129 case aunit: True

2131 note pdvdab

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

2133 also from aunit have bab: "b \<otimes> a \<sim> b"

2134 by (intro associatedI2[of "a"], simp+)

2135 finally have "p divides b" by simp

2136 then show ?thesis ..

2137 next

2138 case anunit: False

2139 show ?thesis

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

2141 case bunit: True

2142 note pdvdab

2143 also from bunit

2144 have baa: "a \<otimes> b \<sim> a"

2145 by (intro associatedI2[of "b"], simp+)

2146 finally have "p divides a" by simp

2147 then show ?thesis ..

2148 next

2149 case bnunit: False

2150 have cnunit: "c \<notin> Units G"

2151 proof

2152 assume cunit: "c \<in> Units G"

2153 from bnunit have "properfactor G a (a \<otimes> b)"

2154 by (intro properfactorI3[of _ _ b], simp+)

2155 also note abpc

2156 also from cunit have "p \<otimes> c \<sim> p"

2157 by (intro associatedI2[of c], simp+)

2158 finally have "properfactor G a p" by simp

2159 with acarr have "a \<in> Units G" by (fast intro: irreduc)

2160 with anunit show False ..

2161 qed

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

2164 proof clarsimp

2165 assume "a \<otimes> b \<in> Units G"

2166 then have "a \<in> Units G" by (rule unit_factor) fact+

2167 with anunit show False ..

2168 qed

2170 from factors_exist [OF acarr anunit]

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

2172 by blast

2174 from factors_exist [OF bcarr bnunit]

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

2176 by blast

2178 from factors_exist [OF ccarr cnunit]

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

2180 by auto

2182 note [simp] = ascarr bscarr cscarr

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

2185 by (rule factors_mult) fact+

2187 from pirr cfac have pcfac: "factors G (p # cs) (p \<otimes> c)"

2188 by (rule factors_mult_single) fact+

2189 with abpc have abfac': "factors G (p # cs) (a \<otimes> b)"

2190 by simp

2192 from abfac' abfac have "essentially_equal G (p # cs) (as @ bs)"

2193 by (rule factors_unique) (fact | simp)+

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

2195 by (fast elim: essentially_equalE)

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

2197 by (simp add: perm_set_eq[symmetric])

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

2199 unfolding list_all2_conv_all_nth set_conv_nth by force

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

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

2202 proof cases

2203 case 1

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

2206 note pp'

2207 also from afac 1 have "p' divides a" by (rule factors_dividesI) fact+

2208 finally have "p divides a" by simp

2209 then show ?thesis ..

2210 next

2211 case 2

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

2214 note pp'

2215 also from bfac

2216 have "p' divides b" by (rule factors_dividesI) fact+

2217 finally have "p divides b" by simp

2218 then show ?thesis ..

2219 qed

2220 qed

2221 qed

2222 qed

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

2227 subsubsection \<open>Definitions\<close>

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

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

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

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

2234 where "x lcmof\<^bsub>G\<^esub> a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and>

2235 (\<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))"

2237 definition somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2238 where "somegcd G a b = (SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b)"

2240 definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"

2241 where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"

2243 definition "SomeGcd G A = inf (division_rel G) A"

2246 locale gcd_condition_monoid = comm_monoid_cancel +

2247 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"

2249 locale primeness_condition_monoid = comm_monoid_cancel +

2250 assumes irreducible_prime: "\<lbrakk>a \<in> carrier G; irreducible G a\<rbrakk> \<Longrightarrow> prime G a"

2252 locale divisor_chain_condition_monoid = comm_monoid_cancel +

2253 assumes division_wellfounded: "wf {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}"

2256 subsubsection \<open>Connections to \texttt{Lattice.thy}\<close>

2258 lemma gcdof_greatestLower:

2259 fixes G (structure)

2260 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2261 shows "(x \<in> carrier G \<and> x gcdof a b) = greatest (division_rel G) x (Lower (division_rel G) {a, b})"

2262 by (auto simp: isgcd_def greatest_def Lower_def elem_def)

2264 lemma lcmof_leastUpper:

2265 fixes G (structure)

2266 assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G"

2267 shows "(x \<in> carrier G \<and> x lcmof a b) = least (division_rel G) x (Upper (division_rel G) {a, b})"

2268 by (auto simp: islcm_def least_def Upper_def elem_def)

2270 lemma somegcd_meet:

2271 fixes G (structure)

2272 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2273 shows "somegcd G a b = meet (division_rel G) a b"

2274 by (simp add: somegcd_def meet_def inf_def gcdof_greatestLower[OF carr])

2276 lemma (in monoid) isgcd_divides_l:

2277 assumes "a divides b"

2278 and "a \<in> carrier G" "b \<in> carrier G"

2279 shows "a gcdof a b"

2280 using assms unfolding isgcd_def by fast

2282 lemma (in monoid) isgcd_divides_r:

2283 assumes "b divides a"

2284 and "a \<in> carrier G" "b \<in> carrier G"

2285 shows "b gcdof a b"

2286 using assms unfolding isgcd_def by fast

2289 subsubsection \<open>Existence of gcd and lcm\<close>

2291 lemma (in factorial_monoid) gcdof_exists:

2292 assumes acarr: "a \<in> carrier G"

2293 and bcarr: "b \<in> carrier G"

2294 shows "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2295 proof -

2296 from wfactors_exist [OF acarr]

2297 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2298 by blast

2299 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2300 by (fast elim: wfactorsE)

2302 from wfactors_exist [OF bcarr]

2303 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"

2304 by blast

2305 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2306 by (fast elim: wfactorsE)

2308 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2309 fmset G cs = fmset G as \<inter># fmset G bs"

2310 proof (intro mset_wfactorsEx)

2311 fix X

2312 assume "X \<in># fmset G as \<inter># fmset G bs"

2313 then have "X \<in># fmset G as" by simp

2314 then have "X \<in> set (map (assocs G) as)"

2315 by (simp add: fmset_def)

2316 then have "\<exists>x. X = assocs G x \<and> x \<in> set as"

2317 by (induct as) auto

2318 then obtain x where X: "X = assocs G x" and xas: "x \<in> set as"

2319 by blast

2320 with ascarr have xcarr: "x \<in> carrier G"

2321 by blast

2322 from xas airr have xirr: "irreducible G x"

2323 by simp

2324 from xcarr and xirr and X show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2325 by blast

2326 qed

2327 then obtain c cs

2328 where ccarr: "c \<in> carrier G"

2329 and cscarr: "set cs \<subseteq> carrier G"

2330 and csirr: "wfactors G cs c"

2331 and csmset: "fmset G cs = fmset G as \<inter># fmset G bs"

2332 by auto

2334 have "c gcdof a b"

2335 proof (simp add: isgcd_def, safe)

2336 from csmset

2337 have "fmset G cs \<subseteq># fmset G as"

2338 by (simp add: multiset_inter_def subset_mset_def)

2339 then show "c divides a" by (rule fmsubset_divides) fact+

2340 next

2341 from csmset have "fmset G cs \<subseteq># fmset G bs"

2342 by (simp add: multiset_inter_def subseteq_mset_def, force)

2343 then show "c divides b"

2344 by (rule fmsubset_divides) fact+

2345 next

2346 fix y

2347 assume "y \<in> carrier G"

2348 from wfactors_exist [OF this]

2349 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2350 by blast

2352 assume "y divides a"

2353 then have ya: "fmset G ys \<subseteq># fmset G as"

2354 by (rule divides_fmsubset) fact+

2356 assume "y divides b"

2357 then have yb: "fmset G ys \<subseteq># fmset G bs"

2358 by (rule divides_fmsubset) fact+

2360 from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"

2361 by (simp add: subset_mset_def)

2362 then show "y divides c"

2363 by (rule fmsubset_divides) fact+

2364 qed

2365 with ccarr show "\<exists>c. c \<in> carrier G \<and> c gcdof a b"

2366 by fast

2367 qed

2369 lemma (in factorial_monoid) lcmof_exists:

2370 assumes acarr: "a \<in> carrier G"

2371 and bcarr: "b \<in> carrier G"

2372 shows "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2373 proof -

2374 from wfactors_exist [OF acarr]

2375 obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

2376 by blast

2377 from afs have airr: "\<forall>a \<in> set as. irreducible G a"

2378 by (fast elim: wfactorsE)

2380 from wfactors_exist [OF bcarr]

2381 obtain bs where bscarr: "set bs \<subseteq> carrier G" and bfs: "wfactors G bs b"

2382 by blast

2383 from bfs have birr: "\<forall>b \<in> set bs. irreducible G b"

2384 by (fast elim: wfactorsE)

2386 have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and>

2387 fmset G cs = (fmset G as - fmset G bs) + fmset G bs"

2388 proof (intro mset_wfactorsEx)

2389 fix X

2390 assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"

2391 then have "X \<in># fmset G as \<or> X \<in># fmset G bs"

2392 by (auto dest: in_diffD)

2393 then consider "X \<in> set_mset (fmset G as)" | "X \<in> set_mset (fmset G bs)"

2394 by fast

2395 then show "\<exists>x. (x \<in> carrier G \<and> irreducible G x) \<and> X = assocs G x"

2396 proof cases

2397 case 1

2398 then have "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)

2399 then have "\<exists>x. x \<in> set as \<and> X = assocs G x" by (induct as) auto

2400 then obtain x where xas: "x \<in> set as" and X: "X = assocs G x" by auto

2401 with ascarr have xcarr: "x \<in> carrier G" by fast

2402 from xas airr have xirr: "irreducible G x" by simp

2403 from xcarr and xirr and X show ?thesis by fast

2404 next

2405 case 2

2406 then have "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)

2407 then have "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct as) auto

2408 then obtain x where xbs: "x \<in> set bs" and X: "X = assocs G x" by auto

2409 with bscarr have xcarr: "x \<in> carrier G" by fast

2410 from xbs birr have xirr: "irreducible G x" by simp

2411 from xcarr and xirr and X show ?thesis by fast

2412 qed

2413 qed

2414 then obtain c cs

2415 where ccarr: "c \<in> carrier G"

2416 and cscarr: "set cs \<subseteq> carrier G"

2417 and csirr: "wfactors G cs c"

2418 and csmset: "fmset G cs = fmset G as - fmset G bs + fmset G bs"

2419 by auto

2421 have "c lcmof a b"

2422 proof (simp add: islcm_def, safe)

2423 from csmset have "fmset G as \<subseteq># fmset G cs"

2424 by (simp add: subseteq_mset_def, force)

2425 then show "a divides c"

2426 by (rule fmsubset_divides) fact+

2427 next

2428 from csmset have "fmset G bs \<subseteq># fmset G cs"

2429 by (simp add: subset_mset_def)

2430 then show "b divides c"

2431 by (rule fmsubset_divides) fact+

2432 next

2433 fix y

2434 assume "y \<in> carrier G"

2435 from wfactors_exist [OF this]

2436 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2437 by blast

2439 assume "a divides y"

2440 then have ya: "fmset G as \<subseteq># fmset G ys"

2441 by (rule divides_fmsubset) fact+

2443 assume "b divides y"

2444 then have yb: "fmset G bs \<subseteq># fmset G ys"

2445 by (rule divides_fmsubset) fact+

2447 from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"

2448 apply (simp add: subseteq_mset_def, clarify)

2449 apply (case_tac "count (fmset G as) a < count (fmset G bs) a")

2450 apply simp

2451 apply simp

2452 done

2453 then show "c divides y"

2454 by (rule fmsubset_divides) fact+

2455 qed

2456 with ccarr show "\<exists>c. c \<in> carrier G \<and> c lcmof a b"

2457 by fast

2458 qed

2461 subsection \<open>Conditions for Factoriality\<close>

2463 subsubsection \<open>Gcd condition\<close>

2465 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:

2466 "weak_lower_semilattice (division_rel G)"

2467 proof -

2468 interpret weak_partial_order "division_rel G" ..

2469 show ?thesis

2470 apply (unfold_locales, simp_all)

2471 proof -

2472 fix x y

2473 assume carr: "x \<in> carrier G" "y \<in> carrier G"

2474 from gcdof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"

2475 by blast

2476 with carr have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2477 by (subst gcdof_greatestLower[symmetric], simp+)

2478 then show "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})"

2479 by fast

2480 qed

2481 qed

2483 lemma (in gcd_condition_monoid) gcdof_cong_l:

2484 assumes a'a: "a' \<sim> a"

2485 and agcd: "a gcdof b c"

2486 and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"

2487 shows "a' gcdof b c"

2488 proof -

2489 note carr = a'carr carr'

2490 interpret weak_lower_semilattice "division_rel G" by simp

2491 have "a' \<in> carrier G \<and> a' gcdof b c"

2492 apply (simp add: gcdof_greatestLower carr')

2493 apply (subst greatest_Lower_cong_l[of _ a])

2494 apply (simp add: a'a)

2495 apply (simp add: carr)

2496 apply (simp add: carr)

2497 apply (simp add: carr)

2498 apply (simp add: gcdof_greatestLower[symmetric] agcd carr)

2499 done

2500 then show ?thesis ..

2501 qed

2503 lemma (in gcd_condition_monoid) gcd_closed [simp]:

2504 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2505 shows "somegcd G a b \<in> carrier G"

2506 proof -

2507 interpret weak_lower_semilattice "division_rel G" by simp

2508 show ?thesis

2509 apply (simp add: somegcd_meet[OF carr])

2510 apply (rule meet_closed[simplified], fact+)

2511 done

2512 qed

2514 lemma (in gcd_condition_monoid) gcd_isgcd:

2515 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2516 shows "(somegcd G a b) gcdof a b"

2517 proof -

2518 interpret weak_lower_semilattice "division_rel G"

2519 by simp

2520 from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"

2521 apply (subst gcdof_greatestLower, simp, simp)

2522 apply (simp add: somegcd_meet[OF carr] meet_def)

2523 apply (rule inf_of_two_greatest[simplified], assumption+)

2524 done

2525 then show "(somegcd G a b) gcdof a b"

2526 by simp

2527 qed

2529 lemma (in gcd_condition_monoid) gcd_exists:

2530 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2531 shows "\<exists>x\<in>carrier G. x = somegcd G a b"

2532 proof -

2533 interpret weak_lower_semilattice "division_rel G"

2534 by simp

2535 show ?thesis

2536 by (metis carr(1) carr(2) gcd_closed)

2537 qed

2539 lemma (in gcd_condition_monoid) gcd_divides_l:

2540 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2541 shows "(somegcd G a b) divides a"

2542 proof -

2543 interpret weak_lower_semilattice "division_rel G"

2544 by simp

2545 show ?thesis

2546 by (metis carr(1) carr(2) gcd_isgcd isgcd_def)

2547 qed

2549 lemma (in gcd_condition_monoid) gcd_divides_r:

2550 assumes carr: "a \<in> carrier G" "b \<in> carrier G"

2551 shows "(somegcd G a b) divides b"

2552 proof -

2553 interpret weak_lower_semilattice "division_rel G"

2554 by simp

2555 show ?thesis

2556 by (metis carr gcd_isgcd isgcd_def)

2557 qed

2559 lemma (in gcd_condition_monoid) gcd_divides:

2560 assumes sub: "z divides x" "z divides y"

2561 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"

2562 shows "z divides (somegcd G x y)"

2563 proof -

2564 interpret weak_lower_semilattice "division_rel G"

2565 by simp

2566 show ?thesis

2567 by (metis gcd_isgcd isgcd_def assms)

2568 qed

2570 lemma (in gcd_condition_monoid) gcd_cong_l:

2571 assumes xx': "x \<sim> x'"

2572 and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G"

2573 shows "somegcd G x y \<sim> somegcd G x' y"

2574 proof -

2575 interpret weak_lower_semilattice "division_rel G"

2576 by simp

2577 show ?thesis

2578 apply (simp add: somegcd_meet carr)

2579 apply (rule meet_cong_l[simplified], fact+)

2580 done

2581 qed

2583 lemma (in gcd_condition_monoid) gcd_cong_r:

2584 assumes carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"

2585 and yy': "y \<sim> y'"

2586 shows "somegcd G x y \<sim> somegcd G x y'"

2587 proof -

2588 interpret weak_lower_semilattice "division_rel G" by simp

2589 show ?thesis

2590 apply (simp add: somegcd_meet carr)

2591 apply (rule meet_cong_r[simplified], fact+)

2592 done

2593 qed

2595 (*

2596 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:

2597 assumes carr: "b \<in> carrier G"

2598 shows "asc_cong (\<lambda>a. somegcd G a b)"

2599 using carr

2600 unfolding CONG_def

2601 by clarsimp (blast intro: gcd_cong_l)

2603 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:

2604 assumes carr: "a \<in> carrier G"

2605 shows "asc_cong (\<lambda>b. somegcd G a b)"

2606 using carr

2607 unfolding CONG_def

2608 by clarsimp (blast intro: gcd_cong_r)

2610 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =

2611 assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]

2612 *)

2614 lemma (in gcd_condition_monoid) gcdI:

2615 assumes dvd: "a divides b" "a divides c"

2616 and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"

2617 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2618 shows "a \<sim> somegcd G b c"

2619 apply (simp add: somegcd_def)

2620 apply (rule someI2_ex)

2621 apply (rule exI[of _ a], simp add: isgcd_def)

2622 apply (simp add: assms)

2623 apply (simp add: isgcd_def assms, clarify)

2624 apply (insert assms, blast intro: associatedI)

2625 done

2627 lemma (in gcd_condition_monoid) gcdI2:

2628 assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"

2629 shows "a \<sim> somegcd G b c"

2630 using assms unfolding isgcd_def by (blast intro: gcdI)

2632 lemma (in gcd_condition_monoid) SomeGcd_ex:

2633 assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}"

2634 shows "\<exists>x\<in> carrier G. x = SomeGcd G A"

2635 proof -

2636 interpret weak_lower_semilattice "division_rel G"

2637 by simp

2638 show ?thesis

2639 apply (simp add: SomeGcd_def)

2640 apply (rule finite_inf_closed[simplified], fact+)

2641 done

2642 qed

2644 lemma (in gcd_condition_monoid) gcd_assoc:

2645 assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"

2646 shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"

2647 proof -

2648 interpret weak_lower_semilattice "division_rel G"

2649 by simp

2650 show ?thesis

2651 apply (subst (2 3) somegcd_meet, (simp add: carr)+)

2652 apply (simp add: somegcd_meet carr)

2653 apply (rule weak_meet_assoc[simplified], fact+)

2654 done

2655 qed

2657 lemma (in gcd_condition_monoid) gcd_mult:

2658 assumes acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"

2659 shows "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2660 proof - (* following Jacobson, Basic Algebra, p.140 *)

2661 let ?d = "somegcd G a b"

2662 let ?e = "somegcd G (c \<otimes> a) (c \<otimes> b)"

2663 note carr[simp] = acarr bcarr ccarr

2664 have dcarr: "?d \<in> carrier G" by simp

2665 have ecarr: "?e \<in> carrier G" by simp

2666 note carr = carr dcarr ecarr

2668 have "?d divides a" by (simp add: gcd_divides_l)

2669 then have cd'ca: "c \<otimes> ?d divides (c \<otimes> a)" by (simp add: divides_mult_lI)

2671 have "?d divides b" by (simp add: gcd_divides_r)

2672 then have cd'cb: "c \<otimes> ?d divides (c \<otimes> b)" by (simp add: divides_mult_lI)

2674 from cd'ca cd'cb have cd'e: "c \<otimes> ?d divides ?e"

2675 by (rule gcd_divides) simp_all

2676 then obtain u where ucarr[simp]: "u \<in> carrier G" and e_cdu: "?e = c \<otimes> ?d \<otimes> u"

2677 by blast

2679 note carr = carr ucarr

2681 have "?e divides c \<otimes> a" by (rule gcd_divides_l) simp_all

2682 then obtain x where xcarr: "x \<in> carrier G" and ca_ex: "c \<otimes> a = ?e \<otimes> x"

2683 by blast

2684 with e_cdu have ca_cdux: "c \<otimes> a = c \<otimes> ?d \<otimes> u \<otimes> x"

2685 by simp

2687 from ca_cdux xcarr have "c \<otimes> a = c \<otimes> (?d \<otimes> u \<otimes> x)"

2688 by (simp add: m_assoc)

2689 then have "a = ?d \<otimes> u \<otimes> x"

2690 by (rule l_cancel[of c a]) (simp add: xcarr)+

2691 then have du'a: "?d \<otimes> u divides a"

2692 by (rule dividesI[OF xcarr])

2694 have "?e divides c \<otimes> b" by (intro gcd_divides_r) simp_all

2695 then obtain x where xcarr: "x \<in> carrier G" and cb_ex: "c \<otimes> b = ?e \<otimes> x"

2696 by blast

2697 with e_cdu have cb_cdux: "c \<otimes> b = c \<otimes> ?d \<otimes> u \<otimes> x"

2698 by simp

2700 from cb_cdux xcarr have "c \<otimes> b = c \<otimes> (?d \<otimes> u \<otimes> x)"

2701 by (simp add: m_assoc)

2702 with xcarr have "b = ?d \<otimes> u \<otimes> x"

2703 by (intro l_cancel[of c b]) simp_all

2704 then have du'b: "?d \<otimes> u divides b"

2705 by (intro dividesI[OF xcarr])

2707 from du'a du'b carr have du'd: "?d \<otimes> u divides ?d"

2708 by (intro gcd_divides) simp_all

2709 then have uunit: "u \<in> Units G"

2710 proof (elim dividesE)

2711 fix v

2712 assume vcarr[simp]: "v \<in> carrier G"

2713 assume d: "?d = ?d \<otimes> u \<otimes> v"

2714 have "?d \<otimes> \<one> = ?d \<otimes> u \<otimes> v" by simp fact

2715 also have "?d \<otimes> u \<otimes> v = ?d \<otimes> (u \<otimes> v)" by (simp add: m_assoc)

2716 finally have "?d \<otimes> \<one> = ?d \<otimes> (u \<otimes> v)" .

2717 then have i2: "\<one> = u \<otimes> v" by (rule l_cancel) simp_all

2718 then have i1: "\<one> = v \<otimes> u" by (simp add: m_comm)

2719 from vcarr i1[symmetric] i2[symmetric] show "u \<in> Units G"

2720 by (auto simp: Units_def)

2721 qed

2723 from e_cdu uunit have "somegcd G (c \<otimes> a) (c \<otimes> b) \<sim> c \<otimes> somegcd G a b"

2724 by (intro associatedI2[of u]) simp_all

2725 from this[symmetric] show "c \<otimes> somegcd G a b \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2726 by simp

2727 qed

2729 lemma (in monoid) assoc_subst:

2730 assumes ab: "a \<sim> b"

2731 and cP: "\<forall>a b. a \<in> carrier G \<and> b \<in> carrier G \<and> a \<sim> b

2732 \<longrightarrow> f a \<in> carrier G \<and> f b \<in> carrier G \<and> f a \<sim> f b"

2733 and carr: "a \<in> carrier G" "b \<in> carrier G"

2734 shows "f a \<sim> f b"

2735 using assms by auto

2737 lemma (in gcd_condition_monoid) relprime_mult:

2738 assumes abrelprime: "somegcd G a b \<sim> \<one>"

2739 and acrelprime: "somegcd G a c \<sim> \<one>"

2740 and carr[simp]: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"

2741 shows "somegcd G a (b \<otimes> c) \<sim> \<one>"

2742 proof -

2743 have "c = c \<otimes> \<one>" by simp

2744 also from abrelprime[symmetric]

2745 have "\<dots> \<sim> c \<otimes> somegcd G a b"

2746 by (rule assoc_subst) (simp add: mult_cong_r)+

2747 also have "\<dots> \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2748 by (rule gcd_mult) fact+

2749 finally have c: "c \<sim> somegcd G (c \<otimes> a) (c \<otimes> b)"

2750 by simp

2752 from carr have a: "a \<sim> somegcd G a (c \<otimes> a)"

2753 by (fast intro: gcdI divides_prod_l)

2755 have "somegcd G a (b \<otimes> c) \<sim> somegcd G a (c \<otimes> b)"

2756 by (simp add: m_comm)

2757 also from a have "\<dots> \<sim> somegcd G (somegcd G a (c \<otimes> a)) (c \<otimes> b)"

2758 by (rule assoc_subst) (simp add: gcd_cong_l)+

2759 also from gcd_assoc have "\<dots> \<sim> somegcd G a (somegcd G (c \<otimes> a) (c \<otimes> b))"

2760 by (rule assoc_subst) simp+

2761 also from c[symmetric] have "\<dots> \<sim> somegcd G a c"

2762 by (rule assoc_subst) (simp add: gcd_cong_r)+

2763 also note acrelprime

2764 finally show "somegcd G a (b \<otimes> c) \<sim> \<one>"

2765 by simp

2766 qed

2768 lemma (in gcd_condition_monoid) primeness_condition: "primeness_condition_monoid G"

2769 apply unfold_locales

2770 apply (rule primeI)

2771 apply (elim irreducibleE, assumption)

2772 proof -

2773 fix p a b

2774 assume pcarr: "p \<in> carrier G" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"

2775 and pirr: "irreducible G p"

2776 and pdvdab: "p divides a \<otimes> b"

2777 from pirr have pnunit: "p \<notin> Units G"

2778 and r[rule_format]: "\<forall>b. b \<in> carrier G \<and> properfactor G b p \<longrightarrow> b \<in> Units G"

2779 by (fast elim: irreducibleE)+

2781 show "p divides a \<or> p divides b"

2782 proof (rule ccontr, clarsimp)

2783 assume npdvda: "\<not> p divides a"

2784 with pcarr acarr have "\<one> \<sim> somegcd G p a"

2785 apply (intro gcdI, simp, simp, simp)

2786 apply (fast intro: unit_divides)

2787 apply (fast intro: unit_divides)

2788 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

2789 apply (rule r, rule, assumption)

2790 apply (rule properfactorI, assumption)

2791 proof

2792 fix y

2793 assume ycarr: "y \<in> carrier G"

2794 assume "p divides y"

2795 also assume "y divides a"

2796 finally have "p divides a"

2797 by (simp add: pcarr ycarr acarr)

2798 with npdvda show False ..

2799 qed simp_all

2800 with pcarr acarr have pa: "somegcd G p a \<sim> \<one>"

2801 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2803 assume npdvdb: "\<not> p divides b"

2804 with pcarr bcarr have "\<one> \<sim> somegcd G p b"

2805 apply (intro gcdI, simp, simp, simp)

2806 apply (fast intro: unit_divides)

2807 apply (fast intro: unit_divides)

2808 apply (clarsimp simp add: Unit_eq_dividesone[symmetric])

2809 apply (rule r, rule, assumption)

2810 apply (rule properfactorI, assumption)

2811 proof

2812 fix y

2813 assume ycarr: "y \<in> carrier G"

2814 assume "p divides y"

2815 also assume "y divides b"

2816 finally have "p divides b" by (simp add: pcarr ycarr bcarr)

2817 with npdvdb

2818 show "False" ..

2819 qed simp_all

2820 with pcarr bcarr have pb: "somegcd G p b \<sim> \<one>"

2821 by (fast intro: associated_sym[of "\<one>"] gcd_closed)

2823 from pcarr acarr bcarr pdvdab have "p gcdof p (a \<otimes> b)"

2824 by (fast intro: isgcd_divides_l)

2825 with pcarr acarr bcarr have "p \<sim> somegcd G p (a \<otimes> b)"

2826 by (fast intro: gcdI2)

2827 also from pa pb pcarr acarr bcarr have "somegcd G p (a \<otimes> b) \<sim> \<one>"

2828 by (rule relprime_mult)

2829 finally have "p \<sim> \<one>"

2830 by (simp add: pcarr acarr bcarr)

2831 with pcarr have "p \<in> Units G"

2832 by (fast intro: assoc_unit_l)

2833 with pnunit show False ..

2834 qed

2835 qed

2837 sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid

2838 by (rule primeness_condition)

2841 subsubsection \<open>Divisor chain condition\<close>

2843 lemma (in divisor_chain_condition_monoid) wfactors_exist:

2844 assumes acarr: "a \<in> carrier G"

2845 shows "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

2846 proof -

2847 have r[rule_format]: "a \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a)"

2848 proof (rule wf_induct[OF division_wellfounded])

2849 fix x

2850 assume ih: "\<forall>y. (y, x) \<in> {(x, y). x \<in> carrier G \<and> y \<in> carrier G \<and> properfactor G x y}

2851 \<longrightarrow> y \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y)"

2853 show "x \<in> carrier G \<longrightarrow> (\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as x)"

2854 apply clarify

2855 apply (cases "x \<in> Units G")

2856 apply (rule exI[of _ "[]"], simp)

2857 apply (cases "irreducible G x")

2858 apply (rule exI[of _ "[x]"], simp add: wfactors_def)

2859 proof -

2860 assume xcarr: "x \<in> carrier G"

2861 and xnunit: "x \<notin> Units G"

2862 and xnirr: "\<not> irreducible G x"

2863 then have "\<exists>y. y \<in> carrier G \<and> properfactor G y x \<and> y \<notin> Units G"

2864 apply -

2865 apply (rule ccontr)

2866 apply simp

2867 apply (subgoal_tac "irreducible G x", simp)

2868 apply (rule irreducibleI, simp, simp)

2869 done

2870 then obtain y where ycarr: "y \<in> carrier G" and ynunit: "y \<notin> Units G"

2871 and pfyx: "properfactor G y x"

2872 by blast

2874 have ih': "\<And>y. \<lbrakk>y \<in> carrier G; properfactor G y x\<rbrakk>

2875 \<Longrightarrow> \<exists>as. set as \<subseteq> carrier G \<and> wfactors G as y"

2876 by (rule ih[rule_format, simplified]) (simp add: xcarr)+

2878 from ih' [OF ycarr pfyx]

2879 obtain ys where yscarr: "set ys \<subseteq> carrier G" and yfs: "wfactors G ys y"

2880 by blast

2882 from pfyx have "y divides x" and nyx: "\<not> y \<sim> x"

2883 by (fast elim: properfactorE2)+

2884 then obtain z where zcarr: "z \<in> carrier G" and x: "x = y \<otimes> z"

2885 by blast

2887 from zcarr ycarr have "properfactor G z x"

2888 apply (subst x)

2889 apply (intro properfactorI3[of _ _ y])

2890 apply (simp add: m_comm)

2891 apply (simp add: ynunit)+

2892 done

2893 from ih' [OF zcarr this]

2894 obtain zs where zscarr: "set zs \<subseteq> carrier G" and zfs: "wfactors G zs z"

2895 by blast

2896 from yscarr zscarr have xscarr: "set (ys@zs) \<subseteq> carrier G"

2897 by simp

2898 from yfs zfs ycarr zcarr yscarr zscarr have "wfactors G (ys@zs) (y\<otimes>z)"

2899 by (rule wfactors_mult)

2900 then have "wfactors G (ys@zs) x"

2901 by (simp add: x)

2902 with xscarr show "\<exists>xs. set xs \<subseteq> carrier G \<and> wfactors G xs x"

2903 by fast

2904 qed

2905 qed

2906 from acarr show ?thesis by (rule r)

2907 qed

2910 subsubsection \<open>Primeness condition\<close>

2912 lemma (in comm_monoid_cancel) multlist_prime_pos:

2913 assumes carr: "a \<in> carrier G" "set as \<subseteq> carrier G"

2914 and aprime: "prime G a"

2915 and "a divides (foldr (op \<otimes>) as \<one>)"

2916 shows "\<exists>i<length as. a divides (as!i)"

2917 proof -

2918 have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>)

2919 \<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"

2920 apply (induct as)

2921 apply clarsimp defer 1

2922 apply clarsimp defer 1

2923 proof -

2924 assume "a divides \<one>"

2925 with carr have "a \<in> Units G"

2926 by (fast intro: divides_unit[of a \<one>])

2927 with aprime show False

2928 by (elim primeE, simp)

2929 next

2930 fix aa as

2931 assume ih[rule_format]: "a divides foldr op \<otimes> as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"

2932 and carr': "aa \<in> carrier G" "set as \<subseteq> carrier G"

2933 and "a divides aa \<otimes> foldr op \<otimes> as \<one>"

2934 with carr aprime have "a divides aa \<or> a divides foldr op \<otimes> as \<one>"

2935 by (intro prime_divides) simp+

2936 then show "\<exists>i<Suc (length as). a divides (aa # as) ! i"

2937 proof

2938 assume "a divides aa"

2939 then have p1: "a divides (aa#as)!0" by simp

2940 have "0 < Suc (length as)" by simp

2941 with p1 show ?thesis by fast

2942 next

2943 assume "a divides foldr op \<otimes> as \<one>"

2944 from ih [OF this] obtain i where "a divides as ! i" and len: "i < length as" by auto

2945 then have p1: "a divides (aa#as) ! (Suc i)" by simp

2946 from len have "Suc i < Suc (length as)" by simp

2947 with p1 show ?thesis by force

2948 qed

2949 qed

2950 from assms show ?thesis

2951 by (intro r) auto

2952 qed

2954 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:

2955 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>

2956 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2957 proof (induct as)

2958 case Nil

2959 show ?case

2960 proof auto

2961 fix a as'

2962 assume a: "a \<in> carrier G"

2963 assume "wfactors G [] a"

2964 then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)

2965 with a have "a \<in> Units G" by (auto intro: assoc_unit_r)

2966 moreover assume "wfactors G as' a"

2967 moreover assume "set as' \<subseteq> carrier G"

2968 ultimately have "as' = []" by (rule unit_wfactors_empty)

2969 then show "essentially_equal G [] as'" by simp

2970 qed

2971 next

2972 case (Cons ah as)

2973 then show ?case

2974 proof clarsimp

2975 fix a as'

2976 assume ih [rule_format]:

2977 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>

2978 wfactors G as' a \<longrightarrow> essentially_equal G as as'"

2979 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"

2980 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"

2981 and afs: "wfactors G (ah # as) a"

2982 and afs': "wfactors G as' a"

2983 then have ahdvda: "ah divides a"

2984 by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all

2985 then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"

2986 by blast

2987 have a'fs: "wfactors G as a'"

2988 apply (rule wfactorsE[OF afs], rule wfactorsI, simp)

2989 apply (simp add: a)

2990 apply (insert ascarr a'carr)

2991 apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)

2992 done

2993 from afs have ahirr: "irreducible G ah"

2994 by (elim wfactorsE) simp

2995 with ascarr have ahprime: "prime G ah"

2996 by (intro irreducible_prime ahcarr)

2998 note carr [simp] = acarr ahcarr ascarr as'carr a'carr

3000 note ahdvda

3001 also from afs' have "a divides (foldr (op \<otimes>) as' \<one>)"

3002 by (elim wfactorsE associatedE, simp)

3003 finally have "ah divides (foldr (op \<otimes>) as' \<one>)"

3004 by simp

3005 with ahprime have "\<exists>i<length as'. ah divides as'!i"

3006 by (intro multlist_prime_pos) simp_all

3007 then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"

3008 by blast

3009 from afs' carr have irrasi: "irreducible G (as'!i)"

3010 by (fast intro: nth_mem[OF len] elim: wfactorsE)

3011 from len carr have asicarr[simp]: "as'!i \<in> carrier G"

3012 unfolding set_conv_nth by force

3013 note carr = carr asicarr

3015 from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"

3016 by blast

3017 with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"

3018 apply -

3019 apply (elim irreducible_prodE[of "ah" "x"], assumption+)

3020 apply (rule associatedI2[of x], assumption+)

3021 apply (rule irreducibleE[OF ahirr], simp)

3022 done

3024 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']

3025 note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]

3026 note carr = carr partscarr

3028 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"

3029 apply (intro wfactors_prod_exists)

3030 using setparts afs'

3031 apply (fast elim: wfactorsE)

3032 apply simp

3033 done

3034 then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"

3035 by auto

3037 have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"

3038 apply (intro wfactors_prod_exists)

3039 using setparts afs'

3040 apply (fast elim: wfactorsE)

3041 apply simp

3042 done

3043 then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"

3044 and aa2fs: "wfactors G (drop (Suc i) as') aa_2"

3045 by auto

3047 note carr = carr aa1carr[simp] aa2carr[simp]

3049 from aa1fs aa2fs

3050 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"

3051 by (intro wfactors_mult, simp+)

3052 then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"

3053 apply (intro wfactors_mult_single)

3054 using setparts afs'

3055 apply (fast intro: nth_mem[OF len] elim: wfactorsE)

3056 apply simp_all

3057 done

3059 from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"

3060 by (metis irrasi wfactors_mult_single)

3061 with len carr aa1carr aa2carr aa1fs

3062 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"

3063 apply (intro wfactors_mult)

3064 apply fast

3065 apply (simp, (fast intro: nth_mem[OF len])?)+

3066 done

3068 from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"

3069 by (simp add: Cons_nth_drop_Suc)

3070 with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"

3071 by simp

3072 with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"

3073 by (metis as' ee_wfactorsD m_closed)

3074 then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"

3075 by (metis aa1carr aa2carr asicarr m_lcomm)

3076 from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"

3077 by (metis associated_sym m_closed mult_cong_l)

3078 also note t1

3079 finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp

3081 with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"

3082 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])

3084 note v1

3085 also note a'

3086 finally have "wfactors G (take i as' @ drop (Suc i) as') a'"

3087 by simp

3089 from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"

3090 by (intro ih[of a']) simp

3091 then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"

3092 by (elim essentially_equalE) (fastforce intro: essentially_equalI)

3094 from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')

3095 (as' ! i # take i as' @ drop (Suc i) as')"

3096 proof (intro essentially_equalI)

3097 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"

3098 by simp

3099 next

3100 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"

3101 by (simp add: list_all2_append) (simp add: asiah[symmetric])

3102 qed

3104 note ee1

3105 also note ee2

3106 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')

3107 (take i as' @ as' ! i # drop (Suc i) as')"

3108 apply (intro essentially_equalI)

3109 apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>

3110 take i as' @ as' ! i # drop (Suc i) as'")

3111 apply simp

3112 apply (rule perm_append_Cons)

3113 apply simp

3114 done

3115 finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"

3116 by simp

3117 then show "essentially_equal G (ah # as) as'"

3118 by (subst as')

3119 qed

3120 qed

3122 lemma (in primeness_condition_monoid) wfactors_unique:

3123 assumes "wfactors G as a" "wfactors G as' a"

3124 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G"

3125 shows "essentially_equal G as as'"

3126 by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)

3129 subsubsection \<open>Application to factorial monoids\<close>

3131 text \<open>Number of factors for wellfoundedness\<close>

3133 definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat"

3134 where "factorcount G a =

3135 (THE c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as)"

3137 lemma (in monoid) ee_length:

3138 assumes ee: "essentially_equal G as bs"

3139 shows "length as = length bs"

3140 by (rule essentially_equalE[OF ee]) (metis list_all2_conv_all_nth perm_length)

3142 lemma (in factorial_monoid) factorcount_exists:

3143 assumes carr[simp]: "a \<in> carrier G"

3144 shows "\<exists>c. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as"

3145 proof -

3146 have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3147 by (intro wfactors_exist) simp

3148 then obtain as where ascarr[simp]: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3149 by (auto simp del: carr)

3150 have "\<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"

3151 by (metis afs ascarr assms ee_length wfactors_unique)

3152 then show "\<exists>c. \<forall>as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..

3153 qed

3155 lemma (in factorial_monoid) factorcount_unique:

3156 assumes afs: "wfactors G as a"

3157 and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"

3158 shows "factorcount G a = length as"

3159 proof -

3160 have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

3161 by (rule factorcount_exists) simp

3162 then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"

3163 by auto

3164 have ac: "ac = factorcount G a"

3165 apply (simp add: factorcount_def)

3166 apply (rule theI2)

3167 apply (rule alen)

3168 apply (metis afs alen ascarr)+

3169 done

3170 from ascarr afs have "ac = length as"

3171 by (iprover intro: alen[rule_format])

3172 with ac show ?thesis

3173 by simp

3174 qed

3176 lemma (in factorial_monoid) divides_fcount:

3177 assumes dvd: "a divides b"

3178 and acarr: "a \<in> carrier G"

3179 and bcarr:"b \<in> carrier G"

3180 shows "factorcount G a \<le> factorcount G b"

3181 proof (rule dividesE[OF dvd])

3182 fix c

3183 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3184 by blast

3185 then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3186 by blast

3187 with acarr have fca: "factorcount G a = length as"

3188 by (intro factorcount_unique)

3190 assume ccarr: "c \<in> carrier G"

3191 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

3192 by blast

3193 then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

3194 by blast

3196 note [simp] = acarr bcarr ccarr ascarr cscarr

3198 assume b: "b = a \<otimes> c"

3199 from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"

3200 by (intro wfactors_mult) simp_all

3201 with b have "wfactors G (as@cs) b"

3202 by simp

3203 then have "factorcount G b = length (as@cs)"

3204 by (intro factorcount_unique) simp_all

3205 then have "factorcount G b = length as + length cs"

3206 by simp

3207 with fca show ?thesis

3208 by simp

3209 qed

3211 lemma (in factorial_monoid) associated_fcount:

3212 assumes acarr: "a \<in> carrier G"

3213 and bcarr: "b \<in> carrier G"

3214 and asc: "a \<sim> b"

3215 shows "factorcount G a = factorcount G b"

3216 apply (rule associatedE[OF asc])

3217 apply (drule divides_fcount[OF _ acarr bcarr])

3218 apply (drule divides_fcount[OF _ bcarr acarr])

3219 apply simp

3220 done

3222 lemma (in factorial_monoid) properfactor_fcount:

3223 assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"

3224 and pf: "properfactor G a b"

3225 shows "factorcount G a < factorcount G b"

3226 proof (rule properfactorE[OF pf], elim dividesE)

3227 fix c

3228 from assms have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a"

3229 by blast

3230 then obtain as where ascarr: "set as \<subseteq> carrier G" and afs: "wfactors G as a"

3231 by blast

3232 with acarr have fca: "factorcount G a = length as"

3233 by (intro factorcount_unique)

3235 assume ccarr: "c \<in> carrier G"

3236 then have "\<exists>cs. set cs \<subseteq> carrier G \<and> wfactors G cs c"

3237 by blast

3238 then obtain cs where cscarr: "set cs \<subseteq> carrier G" and cfs: "wfactors G cs c"

3239 by blast

3241 assume b: "b = a \<otimes> c"

3243 have "wfactors G (as@cs) (a \<otimes> c)"

3244 by (rule wfactors_mult) fact+

3245 with b have "wfactors G (as@cs) b"

3246 by simp

3247 with ascarr cscarr bcarr have "factorcount G b = length (as@cs)"

3248 by (simp add: factorcount_unique)

3249 then have fcb: "factorcount G b = length as + length cs"

3250 by simp

3252 assume nbdvda: "\<not> b divides a"

3253 have "c \<notin> Units G"

3254 proof

3255 assume cunit:"c \<in> Units G"

3256 have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"

3257 by (simp add: b)

3258 also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"

3259 by (fast intro: m_assoc)

3260 also from ccarr cunit have "\<dots> = a \<otimes> \<one>" by simp

3261 also from acarr have "\<dots> = a" by simp

3262 finally have "a = b \<otimes> inv c" by simp

3263 with ccarr cunit have "b divides a"

3264 by (fast intro: dividesI[of "inv c"])

3265 with nbdvda show False by simp

3266 qed

3267 with cfs have "length cs > 0"

3268 apply -

3269 apply (rule ccontr, simp)

3270 apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)

3271 done

3272 with fca fcb show ?thesis

3273 by simp

3274 qed

3276 sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid

3277 apply unfold_locales

3278 apply (rule wfUNIVI)

3279 apply (rule measure_induct[of "factorcount G"])

3280 apply simp

3281 apply (metis properfactor_fcount)

3282 done

3284 sublocale factorial_monoid \<subseteq> primeness_condition_monoid

3285 by standard (rule irreducible_prime)

3288 lemma (in factorial_monoid) primeness_condition: "primeness_condition_monoid G" ..

3290 lemma (in factorial_monoid) gcd_condition [simp]: "gcd_condition_monoid G"

3291 by standard (rule gcdof_exists)

3293 sublocale factorial_monoid \<subseteq> gcd_condition_monoid

3294 by standard (rule gcdof_exists)

3296 lemma (in factorial_monoid) division_weak_lattice [simp]: "weak_lattice (division_rel G)"

3297 proof -

3298 interpret weak_lower_semilattice "division_rel G"

3299 by simp

3300 show "weak_lattice (division_rel G)"

3301 proof (unfold_locales, simp_all)

3302 fix x y

3303 assume carr: "x \<in> carrier G" "y \<in> carrier G"

3304 from lcmof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z lcmof x y"

3305 by blast

3306 with carr have "least (division_rel G) z (Upper (division_rel G) {x, y})"

3307 by (simp add: lcmof_leastUpper[symmetric])

3308 then show "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})"

3309 by blast

3310 qed

3311 qed

3314 subsection \<open>Factoriality Theorems\<close>

3316 theorem factorial_condition_one: (* Jacobson theorem 2.21 *)

3317 "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G \<longleftrightarrow> factorial_monoid G"

3318 proof (rule iffI, clarify)

3319 assume dcc: "divisor_chain_condition_monoid G"

3320 and pc: "primeness_condition_monoid G"

3321 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3322 interpret primeness_condition_monoid "G" by (rule pc)

3323 show "factorial_monoid G"

3324 by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)

3325 next

3326 assume "factorial_monoid G"

3327 then interpret factorial_monoid "G" .

3328 show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"

3329 by rule unfold_locales

3330 qed

3332 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)

3333 "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G \<longleftrightarrow> factorial_monoid G"

3334 proof (rule iffI, clarify)

3335 assume dcc: "divisor_chain_condition_monoid G"

3336 and gc: "gcd_condition_monoid G"

3337 interpret divisor_chain_condition_monoid "G" by (rule dcc)

3338 interpret gcd_condition_monoid "G" by (rule gc)

3339 show "factorial_monoid G"

3340 by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)

3341 next

3342 assume "factorial_monoid G"

3343 then interpret factorial_monoid "G" .

3344 show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"

3345 by rule unfold_locales

3346 qed

3348 end