author  ballarin 
Tue, 29 Jul 2008 16:19:49 +0200  
changeset 27701  ed7a2e0fab59 
child 27713  95b36bfe7fc4 
permissions  rwrr 
27701  1 
(* 
2 
Title: Divisibility in monoids and rings 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 18 July 2008 

5 
Copyright: Clemens Ballarin 

6 
*) 

7 

8 
theory Divisibility 

9 
imports Permutation Coset Group GLattice 

10 
begin 

11 

12 
subsection {* Monoid with cancelation law *} 

13 

14 
locale monoid_cancel = monoid + 

15 
assumes l_cancel: 

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

17 
and r_cancel: 

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

19 

20 
lemma (in monoid) monoid_cancelI: 

21 
assumes l_cancel: 

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

23 
and r_cancel: 

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

25 
shows "monoid_cancel G" 

26 
by unfold_locales fact+ 

27 

28 
lemma (in monoid_cancel) is_monoid_cancel: 

29 
"monoid_cancel G" 

30 
by intro_locales 

31 

32 
interpretation group \<subseteq> monoid_cancel 

33 
by unfold_locales simp+ 

34 

35 

36 
locale comm_monoid_cancel = monoid_cancel + comm_monoid 

37 

38 
lemma comm_monoid_cancelI: 

39 
includes comm_monoid 

40 
assumes cancel: 

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

42 
shows "comm_monoid_cancel G" 

43 
apply unfold_locales 

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

45 
apply (iprover intro: cancel) 

46 
apply (simp add: m_comm) 

47 
apply (iprover intro: cancel) 

48 
done 

49 

50 
lemma (in comm_monoid_cancel) is_comm_monoid_cancel: 

51 
"comm_monoid_cancel G" 

52 
by intro_locales 

53 

54 
interpretation comm_group \<subseteq> comm_monoid_cancel 

55 
by unfold_locales 

56 

57 

58 
subsection {* Products of units in monoids *} 

59 

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

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

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

63 
unfolding Units_def 

64 
using assms 

65 
apply safe 

66 
apply fast 

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

68 
apply (simp add: m_assoc Units_closed) 

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

70 
apply (simp add: m_assoc Units_closed) 

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

72 
apply fast 

73 
done 

74 

75 
lemma (in monoid) prod_unit_l: 

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

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

78 
shows "b \<in> Units G" 

79 
proof  

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

81 

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

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

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

85 

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

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

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

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

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

91 
by (simp add: m_assoc del: Units_l_inv) 

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

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

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

95 

96 
from c li ri 

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

98 
qed 

99 

100 
lemma (in monoid) prod_unit_r: 

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

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

103 
shows "a \<in> Units G" 

104 
proof  

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

106 

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

108 
by (simp add: m_assoc del: Units_r_inv) 

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

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

111 

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

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

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

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

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

117 
by (simp add: m_assoc del: Units_l_inv) 

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

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

120 

121 
from c li ri 

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

123 
qed 

124 

125 
lemma (in comm_monoid) unit_factor: 

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

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

128 
shows "a \<in> Units G" 

129 
using abunit[simplified Units_def] 

130 
proof clarsimp 

131 
fix i 

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

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

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

135 

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

137 

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

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

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

141 
also note li 

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

143 

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

145 
also note ri 

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

147 

148 
from carr' li' ri' 

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

150 
qed 

151 

152 
subsection {* Divisibility and association *} 

153 

154 
subsubsection {* Function definitions *} 

155 

156 
constdefs (structure G) 

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

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

159 

160 
constdefs (structure G) 

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

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

163 

164 
abbreviation 

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

166 

167 
constdefs (structure G) 

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

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

170 

171 
constdefs (structure G) 

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

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

174 

175 
constdefs (structure G) 

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

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

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

179 

180 

181 

182 
subsubsection {* Divisibility *} 

183 

184 
lemma dividesI: 

185 
fixes G (structure) 

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

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

188 
shows "a divides b" 

189 
unfolding factor_def 

190 
using assms by fast 

191 

192 
lemma dividesI' [intro]: 

193 
fixes G (structure) 

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

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

196 
shows "a divides b" 

197 
using assms 

198 
by (fast intro: dividesI) 

199 

200 
lemma dividesD: 

201 
fixes G (structure) 

202 
assumes "a divides b" 

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

204 
using assms 

205 
unfolding factor_def 

206 
by fast 

207 

208 
lemma dividesE [elim]: 

209 
fixes G (structure) 

210 
assumes d: "a divides b" 

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

212 
shows "P" 

213 
proof  

214 
from dividesD[OF d] 

215 
obtain c 

216 
where "c\<in>carrier G" 

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

218 
by auto 

219 
thus "P" by (elim elim) 

220 
qed 

221 

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

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

224 
shows "a divides a" 

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

226 
apply (simp, simp add: carr) 

227 
done 

228 

229 
lemma (in monoid) divides_trans [trans]: 

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

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

232 
shows "a divides c" 

233 
using dvds[THEN dividesD] 

234 
by (blast intro: dividesI m_assoc acarr) 

235 

236 
lemma (in monoid) divides_mult_lI [intro]: 

237 
assumes ab: "a divides b" 

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

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

240 
using ab 

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

242 
apply (fast intro: dividesI) 

243 
done 

244 

245 
lemma (in monoid_cancel) divides_mult_l [simp]: 

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

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

248 
apply safe 

249 
apply (elim dividesE, intro dividesI, assumption) 

250 
apply (rule l_cancel[of c]) 

251 
apply (simp add: m_assoc carr)+ 

252 
apply (fast intro: divides_mult_lI carr) 

253 
done 

254 

255 
lemma (in comm_monoid) divides_mult_rI [intro]: 

256 
assumes ab: "a divides b" 

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

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

259 
using carr ab 

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

261 
apply (rule divides_mult_lI, assumption+) 

262 
done 

263 

264 
lemma (in comm_monoid_cancel) divides_mult_r [simp]: 

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

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

267 
using carr 

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

269 

270 
lemma (in monoid) divides_prod_r: 

271 
assumes ab: "a divides b" 

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

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

274 
using ab carr 

275 
by (fast intro: m_assoc) 

276 

277 
lemma (in comm_monoid) divides_prod_l: 

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

279 
and ab: "a divides b" 

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

281 
using ab carr 

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

283 
apply (fast intro: divides_prod_r) 

284 
done 

285 

286 
lemma (in monoid) unit_divides: 

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

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

289 
shows "u divides a" 

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

291 
from uunit acarr 

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

293 

294 
from uunit acarr 

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

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

297 
also from acarr 

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

299 
finally 

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

301 
qed 

302 

303 
lemma (in comm_monoid) divides_unit: 

304 
assumes udvd: "a divides u" 

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

306 
shows "a \<in> Units G" 

307 
using udvd carr 

308 
by (blast intro: unit_factor) 

309 

310 
lemma (in comm_monoid) Unit_eq_dividesone: 

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

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

313 
using ucarr 

314 
by (fast dest: divides_unit intro: unit_divides) 

315 

316 

317 
subsubsection {* Association *} 

318 

319 
lemma associatedI: 

320 
fixes G (structure) 

321 
assumes "a divides b" "b divides a" 

322 
shows "a \<sim> b" 

323 
using assms 

324 
by (simp add: associated_def) 

325 

326 
lemma (in monoid) associatedI2: 

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

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

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

330 
shows "a \<sim> b" 

331 
using uunit bcarr 

332 
unfolding a 

333 
apply (intro associatedI) 

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

335 
apply (simp add: m_assoc Units_closed Units_r_inv) 

336 
apply fast 

337 
done 

338 

339 
lemma (in monoid) associatedI2': 

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

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

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

343 
shows "a \<sim> b" 

344 
using assms by (intro associatedI2) 

345 

346 
lemma associatedD: 

347 
fixes G (structure) 

348 
assumes "a \<sim> b" 

349 
shows "a divides b" 

350 
using assms by (simp add: associated_def) 

351 

352 
lemma (in monoid_cancel) associatedD2: 

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

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

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

356 
using assoc 

357 
unfolding associated_def 

358 
proof clarify 

359 
assume "b divides a" 

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

361 
from this obtain u 

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

363 
by auto 

364 

365 
assume "a divides b" 

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

367 
from this obtain u' 

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

369 
by auto 

370 
note carr = carr ucarr u'carr 

371 

372 
from carr 

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

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

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

376 
also from carr 

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

378 
finally 

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

380 
with carr 

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

382 

383 
from carr 

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

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

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

387 
also from carr 

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

389 
finally 

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

391 
with carr 

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

393 

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

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

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

397 

398 
from ucarr this a 

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

400 
qed 

401 

402 
lemma associatedE: 

403 
fixes G (structure) 

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

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

406 
shows "P" 

407 
proof  

408 
from assoc 

409 
have "a divides b" "b divides a" 

410 
by (simp add: associated_def)+ 

411 
thus "P" by (elim e) 

412 
qed 

413 

414 
lemma (in monoid_cancel) associatedE2: 

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

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

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

418 
shows "P" 

419 
proof  

420 
from assoc and carr 

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

422 
from this obtain u 

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

424 
by auto 

425 
thus "P" by (elim e) 

426 
qed 

427 

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

429 
assumes "a \<in> carrier G" 

430 
shows "a \<sim> a" 

431 
using assms 

432 
by (fast intro: associatedI) 

433 

434 
lemma (in monoid) associated_sym [sym]: 

435 
assumes "a \<sim> b" 

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

437 
shows "b \<sim> a" 

438 
using assms 

439 
by (iprover intro: associatedI elim: associatedE) 

440 

441 
lemma (in monoid) associated_trans [trans]: 

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

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

444 
shows "a \<sim> c" 

445 
using assms 

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

447 

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

449 
"equivalence (division_rel G)" 

450 
apply unfold_locales 

451 
apply simp_all 

452 
apply (rule associated_sym, assumption+) 

453 
apply (iprover intro: associated_trans) 

454 
done 

455 

456 

457 
subsubsection {* Division and associativity *} 

458 

459 
lemma divides_antisym: 

460 
fixes G (structure) 

461 
assumes "a divides b" "b divides a" 

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

463 
shows "a \<sim> b" 

464 
using assms 

465 
by (fast intro: associatedI) 

466 

467 
lemma (in monoid) divides_cong_l [trans]: 

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

469 
and xdvdy: "x' divides y" 

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

471 
shows "x divides y" 

472 
proof  

473 
from xx' 

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

475 
also note xdvdy 

476 
finally 

477 
show "x divides y" by simp 

478 
qed 

479 

480 
lemma (in monoid) divides_cong_r [trans]: 

481 
assumes xdvdy: "x divides y" 

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

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

484 
shows "x divides y'" 

485 
proof  

486 
note xdvdy 

487 
also from yy' 

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

489 
finally 

490 
show "x divides y'" by simp 

491 
qed 

492 

493 
lemma (in monoid) division_gpartial_order [simp, intro!]: 

494 
"gpartial_order (division_rel G)" 

495 
apply unfold_locales 

496 
apply simp_all 

497 
apply (simp add: associated_sym) 

498 
apply (blast intro: associated_trans) 

499 
apply (simp add: divides_antisym) 

500 
apply (blast intro: divides_trans) 

501 
apply (blast intro: divides_cong_l divides_cong_r associated_sym) 

502 
done 

503 

504 

505 
subsubsection {* Multiplication and associativity *} 

506 

507 
lemma (in monoid_cancel) mult_cong_r: 

508 
assumes "b \<sim> b'" 

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

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

511 
using assms 

512 
apply (elim associatedE2, intro associatedI2) 

513 
apply (auto intro: m_assoc[symmetric]) 

514 
done 

515 

516 
lemma (in comm_monoid_cancel) mult_cong_l: 

517 
assumes "a \<sim> a'" 

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

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

520 
using assms 

521 
apply (elim associatedE2, intro associatedI2) 

522 
apply assumption 

523 
apply (simp add: m_assoc Units_closed) 

524 
apply (simp add: m_comm Units_closed) 

525 
apply simp+ 

526 
done 

527 

528 
lemma (in monoid_cancel) assoc_l_cancel: 

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

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

531 
shows "b \<sim> b'" 

532 
using assms 

533 
apply (elim associatedE2, intro associatedI2) 

534 
apply assumption 

535 
apply (rule l_cancel[of a]) 

536 
apply (simp add: m_assoc Units_closed) 

537 
apply fast+ 

538 
done 

539 

540 
lemma (in comm_monoid_cancel) assoc_r_cancel: 

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

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

543 
shows "a \<sim> a'" 

544 
using assms 

545 
apply (elim associatedE2, intro associatedI2) 

546 
apply assumption 

547 
apply (rule r_cancel[of a b]) 

548 
apply (simp add: m_assoc Units_closed) 

549 
apply (simp add: m_comm Units_closed) 

550 
apply fast+ 

551 
done 

552 

553 

554 
subsubsection {* Units *} 

555 

556 
lemma (in monoid_cancel) assoc_unit_l [trans]: 

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

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

559 
shows "a \<in> Units G" 

560 
using assms 

561 
by (fast elim: associatedE2) 

562 

563 
lemma (in monoid_cancel) assoc_unit_r [trans]: 

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

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

566 
shows "b \<in> Units G" 

567 
using aunit bcarr associated_sym[OF asc] 

568 
by (blast intro: assoc_unit_l) 

569 

570 
lemma (in comm_monoid) Units_cong: 

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

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

573 
shows "b \<in> Units G" 

574 
using assms 

575 
by (blast intro: divides_unit elim: associatedE) 

576 

577 
lemma (in monoid) Units_assoc: 

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

579 
shows "a \<sim> b" 

580 
using units 

581 
by (fast intro: associatedI unit_divides) 

582 

583 
lemma (in monoid) Units_are_ones: 

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

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

586 
proof clarsimp 

587 
fix a 

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

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

590 
apply (rule associatedI) 

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

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

593 
done 

594 
next 

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

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

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

598 
qed 

599 

600 
lemma (in comm_monoid) Units_Lower: 

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

602 
apply (simp add: Units_def Lower_def) 

603 
apply (rule, rule) 

604 
apply clarsimp 

605 
apply (rule unit_divides) 

606 
apply (unfold Units_def, fast) 

607 
apply assumption 

608 
apply clarsimp 

609 
proof  

610 
fix x 

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

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

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

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

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

616 
from this obtain x' 

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

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

619 
by auto 

620 

621 
note xx' 

622 
also with xcarr x'carr 

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

624 
finally 

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

626 

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

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

629 
qed 

630 

631 

632 
subsubsection {* Proper factors *} 

633 

634 
lemma properfactorI: 

635 
fixes G (structure) 

636 
assumes "a divides b" 

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

638 
shows "properfactor G a b" 

639 
using assms 

640 
unfolding properfactor_def 

641 
by simp 

642 

643 
lemma properfactorI2: 

644 
fixes G (structure) 

645 
assumes advdb: "a divides b" 

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

647 
shows "properfactor G a b" 

648 
apply (rule properfactorI, rule advdb) 

649 
proof (rule ccontr, simp) 

650 
assume "b divides a" 

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

652 
with neq show "False" by fast 

653 
qed 

654 

655 
lemma (in comm_monoid_cancel) properfactorI3: 

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

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

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

659 
shows "properfactor G a p" 

660 
unfolding p 

661 
using carr 

662 
apply (intro properfactorI, fast) 

663 
proof (clarsimp, elim dividesE) 

664 
fix c 

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

666 
note [simp] = carr ccarr 

667 

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

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

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

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

672 

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

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

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

676 

677 
from ccarr linv[symmetric] rinv[symmetric] 

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

679 
with nunit 

680 
show "False" .. 

681 
qed 

682 

683 
lemma properfactorE: 

684 
fixes G (structure) 

685 
assumes pf: "properfactor G a b" 

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

687 
shows "P" 

688 
using pf 

689 
unfolding properfactor_def 

690 
by (fast intro: r) 

691 

692 
lemma properfactorE2: 

693 
fixes G (structure) 

694 
assumes pf: "properfactor G a b" 

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

696 
shows "P" 

697 
using pf 

698 
unfolding properfactor_def 

699 
by (fast elim: elim associatedE) 

700 

701 
lemma (in monoid) properfactor_unitE: 

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

703 
and pf: "properfactor G a u" 

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

705 
shows "P" 

706 
using pf unit_divides[OF uunit acarr] 

707 
by (fast elim: properfactorE) 

708 

709 

710 
lemma (in monoid) properfactor_divides: 

711 
assumes pf: "properfactor G a b" 

712 
shows "a divides b" 

713 
using pf 

714 
by (elim properfactorE) 

715 

716 
lemma (in monoid) properfactor_trans1 [trans]: 

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

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

719 
shows "properfactor G a c" 

720 
using dvds carr 

721 
apply (elim properfactorE, intro properfactorI) 

722 
apply (iprover intro: divides_trans)+ 

723 
done 

724 

725 
lemma (in monoid) properfactor_trans2 [trans]: 

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

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

728 
shows "properfactor G a c" 

729 
using dvds carr 

730 
apply (elim properfactorE, intro properfactorI) 

731 
apply (iprover intro: divides_trans)+ 

732 
done 

733 

734 
lemma properfactor_glless: 

735 
fixes G (structure) 

736 
shows "properfactor G = glless (division_rel G)" 

737 
apply (rule ext) apply (rule ext) apply rule 

738 
apply (fastsimp elim: properfactorE2 intro: gllessI) 

739 
apply (fastsimp elim: gllessE intro: properfactorI2) 

740 
done 

741 

742 
lemma (in monoid) properfactor_cong_l [trans]: 

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

744 
and pf: "properfactor G x y" 

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

746 
shows "properfactor G x' y" 

747 
using pf 

748 
unfolding properfactor_glless 

749 
proof  

750 
interpret gpartial_order ["division_rel G"] .. 

751 
from x'x 

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

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

754 
finally 

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

756 
qed 

757 

758 
lemma (in monoid) properfactor_cong_r [trans]: 

759 
assumes pf: "properfactor G x y" 

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

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

762 
shows "properfactor G x y'" 

763 
using pf 

764 
unfolding properfactor_glless 

765 
proof  

766 
interpret gpartial_order ["division_rel G"] .. 

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

768 
also from yy' 

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

770 
finally 

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

772 
qed 

773 

774 
lemma (in monoid_cancel) properfactor_mult_lI [intro]: 

775 
assumes ab: "properfactor G a b" 

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

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

778 
using ab carr 

779 
by (fastsimp elim: properfactorE intro: properfactorI) 

780 

781 
lemma (in monoid_cancel) properfactor_mult_l [simp]: 

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

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

784 
using carr 

785 
by (fastsimp elim: properfactorE intro: properfactorI) 

786 

787 
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: 

788 
assumes ab: "properfactor G a b" 

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

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

791 
using ab carr 

792 
by (fastsimp elim: properfactorE intro: properfactorI) 

793 

794 
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: 

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

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

797 
using carr 

798 
by (fastsimp elim: properfactorE intro: properfactorI) 

799 

800 
lemma (in monoid) properfactor_prod_r: 

801 
assumes ab: "properfactor G a b" 

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

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

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

805 

806 
lemma (in comm_monoid) properfactor_prod_l: 

807 
assumes ab: "properfactor G a b" 

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

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

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

811 

812 

813 
subsection {* Irreducible elements and primes *} 

814 

815 
subsubsection {* Irreducible elements *} 

816 

817 
lemma irreducibleI: 

818 
fixes G (structure) 

819 
assumes "a \<notin> Units G" 

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

821 
shows "irreducible G a" 

822 
using assms 

823 
unfolding irreducible_def 

824 
by blast 

825 

826 
lemma irreducibleE: 

827 
fixes G (structure) 

828 
assumes irr: "irreducible G a" 

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

830 
shows "P" 

831 
using assms 

832 
unfolding irreducible_def 

833 
by blast 

834 

835 
lemma irreducibleD: 

836 
fixes G (structure) 

837 
assumes irr: "irreducible G a" 

838 
and pf: "properfactor G b a" 

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

840 
shows "b \<in> Units G" 

841 
using assms 

842 
by (fast elim: irreducibleE) 

843 

844 
lemma (in monoid_cancel) irreducible_cong [trans]: 

845 
assumes irred: "irreducible G a" 

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

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

848 
shows "irreducible G a'" 

849 
using assms 

850 
apply (elim irreducibleE, intro irreducibleI) 

851 
apply simp_all 

852 
proof clarify 

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

854 
also note aa'[symmetric] 

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

856 

857 
assume "a \<notin> Units G" 

858 
with aunit 

859 
show "False" by fast 

860 
next 

861 
fix b 

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

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

864 
assume "properfactor G b a'" 

865 
also note aa'[symmetric] 

866 
finally 

867 
have "properfactor G b a" by simp 

868 

869 
with bcarr 

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

871 
qed 

872 

873 

874 
lemma (in monoid) irreducible_prod_rI: 

875 
assumes airr: "irreducible G a" 

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

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

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

879 
using airr carr bunit 

880 
apply (elim irreducibleE, intro irreducibleI, clarify) 

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

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

883 
proof  

884 
fix c 

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

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

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

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

889 
finally 

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

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

892 
qed 

893 

894 
lemma (in comm_monoid) irreducible_prod_lI: 

895 
assumes birr: "irreducible G b" 

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

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

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

899 
apply (subst m_comm, simp+) 

900 
apply (intro irreducible_prod_rI assms) 

901 
done 

902 

903 
lemma (in comm_monoid_cancel) irreducible_prodE [elim]: 

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

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

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

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

908 
shows "P" 

909 
using irr 

910 
proof (elim irreducibleE) 

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

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

913 

914 
show "P" 

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

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

917 

918 
have "irreducible G b" 

919 
apply (rule irreducibleI) 

920 
proof (rule ccontr, simp) 

921 
assume "b \<in> Units G" 

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

923 
with abnunit show "False" .. 

924 
next 

925 
fix c 

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

927 
and "properfactor G c b" 

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

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

930 
qed 

931 

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

933 
next 

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

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

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

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

938 

939 
have "irreducible G a" 

940 
apply (rule irreducibleI) 

941 
proof (rule ccontr, simp) 

942 
assume "a \<in> Units G" 

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

944 
with abnunit show "False" .. 

945 
next 

946 
fix c 

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

948 
and "properfactor G c a" 

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

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

951 
qed 

952 

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

954 
qed 

955 
qed 

956 

957 

958 
subsubsection {* Prime elements *} 

959 

960 
lemma primeI: 

961 
fixes G (structure) 

962 
assumes "p \<notin> Units G" 

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

964 
shows "prime G p" 

965 
using assms 

966 
unfolding prime_def 

967 
by blast 

968 

969 
lemma primeE: 

970 
fixes G (structure) 

971 
assumes pprime: "prime G p" 

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

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

974 
shows "P" 

975 
using pprime 

976 
unfolding prime_def 

977 
by (blast dest: e) 

978 

979 
lemma (in comm_monoid_cancel) prime_divides: 

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

981 
and pprime: "prime G p" 

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

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

984 
using assms 

985 
by (blast elim: primeE) 

986 

987 
lemma (in monoid_cancel) prime_cong [trans]: 

988 
assumes pprime: "prime G p" 

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

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

991 
shows "prime G p'" 

992 
using pprime 

993 
apply (elim primeE, intro primeI) 

994 
proof clarify 

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

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

997 
also note pp'[symmetric] 

998 
finally 

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

1000 
with pnunit 

1001 
show False .. 

1002 
next 

1003 
fix a b 

1004 
assume r[rule_format]: 

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

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

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

1008 

1009 
note pp' 

1010 
also note p'dvd 

1011 
finally 

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

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

1014 
moreover { 

1015 
note pp'[symmetric] 

1016 
also assume "p divides a" 

1017 
finally 

1018 
have "p' divides a" by simp 

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

1020 
} 

1021 
moreover { 

1022 
note pp'[symmetric] 

1023 
also assume "p divides b" 

1024 
finally 

1025 
have "p' divides b" by simp 

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

1027 
} 

1028 
ultimately 

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

1030 
qed 

1031 

1032 

1033 
subsection {* Factorization and factorial monoids *} 

1034 

1035 
(* 

1036 
hide (open) const mult (* Multiset.mult, conflicting with monoid.mult *) 

1037 
*) 

1038 

1039 
subsubsection {* Function definitions *} 

1040 

1041 
constdefs (structure G) 

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

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

1044 

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

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

1047 

1048 
abbreviation 

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

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

1051 

1052 
constdefs (structure G) 

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

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

1055 

1056 

1057 
locale factorial_monoid = comm_monoid_cancel + 

1058 
assumes factors_exist: 

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

1060 
and factors_unique: 

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

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

1063 

1064 

1065 
subsubsection {* Comparing lists of elements *} 

1066 

1067 
text {* Association on lists *} 

1068 

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

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

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

1072 
using assms 

1073 
by (induct as) simp+ 

1074 

1075 
lemma (in monoid) listassoc_sym [sym]: 

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

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

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

1079 
using assms 

1080 
proof (induct as arbitrary: bs, simp) 

1081 
case Cons 

1082 
thus ?case 

1083 
apply (induct bs, simp) 

1084 
apply clarsimp 

1085 
apply (iprover intro: associated_sym) 

1086 
done 

1087 
qed 

1088 

1089 
lemma (in monoid) listassoc_trans [trans]: 

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

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

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

1093 
using assms 

1094 
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) 

1095 
apply (rule associated_trans) 

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

1097 
apply (simp, simp) 

1098 
apply blast+ 

1099 
done 

1100 

1101 
lemma (in monoid_cancel) irrlist_listassoc_cong: 

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

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

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

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

1106 
using assms 

1107 
apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) 

1108 
apply (blast intro: irreducible_cong) 

1109 
done 

1110 

1111 

1112 
text {* Permutations *} 

1113 

1114 
lemma perm_map [intro]: 

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

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

1117 
using p 

1118 
by induct auto 

1119 

1120 
lemma perm_map_switch: 

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

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

1123 
using p m 

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

1125 

1126 
lemma (in monoid) perm_assoc_switch: 

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

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

1129 
using p a 

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

1131 
apply (clarsimp simp add: list_all2_Cons2, blast) 

1132 
apply (clarsimp simp add: list_all2_Cons2) 

1133 
apply blast 

1134 
apply blast 

1135 
done 

1136 

1137 
lemma (in monoid) perm_assoc_switch_r: 

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

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

1140 
using p a 

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

1142 
apply (clarsimp simp add: list_all2_Cons1, blast) 

1143 
apply (clarsimp simp add: list_all2_Cons1) 

1144 
apply blast 

1145 
apply blast 

1146 
done 

1147 

1148 
declare perm_sym [sym] 

1149 

1150 
lemma perm_setP: 

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

1152 
and as: "P (set as)" 

1153 
shows "P (set bs)" 

1154 
proof  

1155 
from perm 

1156 
have "multiset_of as = multiset_of bs" 

1157 
by (simp add: multiset_of_eq_perm) 

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

1159 
with as 

1160 
show "P (set bs)" by simp 

1161 
qed 

1162 

1163 
lemmas (in monoid) perm_closed = 

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

1165 

1166 
lemmas (in monoid) irrlist_perm_cong = 

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

1168 

1169 

1170 
text {* Essentially equal factorizations *} 

1171 

1172 
lemma (in monoid) essentially_equalI: 

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

1174 
shows "essentially_equal G fs1 fs2" 

1175 
using ex 

1176 
unfolding essentially_equal_def 

1177 
by fast 

1178 

1179 
lemma (in monoid) essentially_equalE: 

1180 
assumes ee: "essentially_equal G fs1 fs2" 

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

1182 
shows "P" 

1183 
using ee 

1184 
unfolding essentially_equal_def 

1185 
by (fast intro: e) 

1186 

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

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

1189 
shows "essentially_equal G as as" 

1190 
using carr 

1191 
by (fast intro: essentially_equalI) 

1192 

1193 
lemma (in monoid) ee_sym [sym]: 

1194 
assumes ee: "essentially_equal G as bs" 

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

1196 
shows "essentially_equal G bs as" 

1197 
using ee 

1198 
proof (elim essentially_equalE) 

1199 
fix fs 

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

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

1202 
from this obtain fs' 

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

1204 
by auto 

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

1206 
with a[symmetric] carr 

1207 
show ?thesis 

1208 
by (iprover intro: essentially_equalI perm_closed) 

1209 
qed 

1210 

1211 
lemma (in monoid) ee_trans [trans]: 

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

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

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

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

1216 
shows "essentially_equal G as cs" 

1217 
using ab bc 

1218 
proof (elim essentially_equalE) 

1219 
fix abs bcs 

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

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

1222 
from this obtain bs' 

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

1224 
by auto 

1225 

1226 
assume "as <~~> abs" 

1227 
with p 

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

1229 

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

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

1232 
note a 

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

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

1235 

1236 
with pp 

1237 
show ?thesis 

1238 
by (rule essentially_equalI) 

1239 
qed 

1240 

1241 

1242 
subsubsection {* Properties of lists of elements *} 

1243 

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

1245 

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

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

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

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

1250 

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

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

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

1254 
using assms 

1255 
apply (induct fs) 

1256 
apply simp 

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

1258 
apply (fast intro: dividesI) 

1259 
apply clarsimp 

1260 
apply (elim dividesE, intro dividesI) 

1261 
defer 1 

1262 
apply (simp add: m_comm) 

1263 
apply (simp add: m_assoc[symmetric]) 

1264 
apply (simp add: m_comm) 

1265 
apply simp 

1266 
done 

1267 

1268 
lemma (in comm_monoid_cancel) multlist_listassoc_cong: 

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

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

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

1272 
using assms 

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

1274 
case (Cons a as fs') 

1275 
thus ?case 

1276 
apply (induct fs', simp) 

1277 
proof clarsimp 

1278 
fix b bs 

1279 
assume "a \<sim> b" 

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

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

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

1283 
by (fast intro: mult_cong_l) 

1284 
also 

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

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

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

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

1289 
with ascarr bscarr bcarr 

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

1291 
by (fast intro: mult_cong_r) 

1292 
finally 

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

1294 
by (simp add: ascarr bscarr acarr bcarr) 

1295 
qed 

1296 
qed 

1297 

1298 
lemma (in comm_monoid) multlist_perm_cong: 

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

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

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

1302 
using prm ascarr 

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

1304 
proof clarsimp 

1305 
fix xs ys zs 

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

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

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

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

1310 
qed 

1311 

1312 
lemma (in comm_monoid_cancel) multlist_ee_cong: 

1313 
assumes "essentially_equal G fs fs'" 

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

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

1316 
using assms 

1317 
apply (elim essentially_equalE) 

1318 
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) 

1319 
done 

1320 

1321 

1322 
subsubsection {* Factorization in irreducible elements *} 

1323 

1324 
lemma wfactorsI: 

1325 
includes (struct G) 

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

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

1328 
shows "wfactors G fs a" 

1329 
using assms 

1330 
unfolding wfactors_def 

1331 
by simp 

1332 

1333 
lemma wfactorsE: 

1334 
includes (struct G) 

1335 
assumes wf: "wfactors G fs a" 

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

1337 
shows "P" 

1338 
using wf 

1339 
unfolding wfactors_def 

1340 
by (fast dest: e) 

1341 

1342 
lemma (in monoid) factorsI: 

1343 
includes (struct G) 

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

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

1346 
shows "factors G fs a" 

1347 
using assms 

1348 
unfolding factors_def 

1349 
by simp 

1350 

1351 
lemma factorsE: 

1352 
includes (struct G) 

1353 
assumes f: "factors G fs a" 

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

1355 
shows "P" 

1356 
using f 

1357 
unfolding factors_def 

1358 
by (simp add: e) 

1359 

1360 
lemma (in monoid) factors_wfactors: 

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

1362 
shows "wfactors G as a" 

1363 
using assms 

1364 
by (blast elim: factorsE intro: wfactorsI) 

1365 

1366 
lemma (in monoid) wfactors_factors: 

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

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

1369 
using assms 

1370 
by (blast elim: wfactorsE intro: factorsI) 

1371 

1372 
lemma (in monoid) factors_closed [dest]: 

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

1374 
shows "a \<in> carrier G" 

1375 
using assms 

1376 
by (elim factorsE, clarsimp) 

1377 

1378 
lemma (in monoid) nunit_factors: 

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

1380 
and fs: "factors G as a" 

1381 
shows "length as > 0" 

1382 
apply (insert fs, elim factorsE) 

1383 
proof (cases "length as = 0") 

1384 
assume "length as = 0" 

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

1386 

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

1388 
with fold 

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

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

1391 
with anunit 

1392 
have "False" by simp 

1393 
thus ?thesis .. 

1394 
qed simp 

1395 

1396 
lemma (in monoid) unit_wfactors [simp]: 

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

1398 
shows "wfactors G [] a" 

1399 
using aunit 

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

1401 

1402 
lemma (in comm_monoid_cancel) unit_wfactors_empty: 

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

1404 
and wf: "wfactors G fs a" 

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

1406 
shows "fs = []" 

1407 
proof (rule ccontr, cases fs, simp) 

1408 
fix f fs' 

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

1410 

1411 
from carr 

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

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

1414 
by (simp add: fs)+ 

1415 

1416 
from fs wf 

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

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

1419 

1420 
from fs wf 

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

1422 

1423 
note aunit 

1424 
also from fs wf 

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

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

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

1428 
finally 

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

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

1431 

1432 
with fnunit show "False" by simp 

1433 
qed 

1434 

1435 

1436 
text {* Comparing wfactors *} 

1437 

1438 
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l: 

1439 
assumes fact: "wfactors G fs a" 

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

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

1442 
shows "wfactors G fs' a" 

1443 
using fact 

1444 
apply (elim wfactorsE, intro wfactorsI) 

1445 
proof  

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

1447 
also note asc 

1448 
finally (irrlist_listassoc_cong) 

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

1450 
next 

1451 
from asc[symmetric] 

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

1453 
by (simp add: multlist_listassoc_cong carr) 

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

1455 
finally 

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

1457 
qed 

1458 

1459 
lemma (in comm_monoid) wfactors_perm_cong_l: 

1460 
assumes "wfactors G fs a" 

1461 
and "fs <~~> fs'" 

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

1463 
shows "wfactors G fs' a" 

1464 
using assms 

1465 
apply (elim wfactorsE, intro wfactorsI) 

1466 
apply (rule irrlist_perm_cong, assumption+) 

1467 
apply (simp add: multlist_perm_cong[symmetric]) 

ed7a2e0fab59
New theory on divisibility.
ballari 