author  ballarin 
Wed, 15 Oct 2008 16:06:59 +0200  
changeset 28600  54352ed7114f 
parent 28599  12d914277b8d 
child 28823  dcbef866c9e2 
permissions  rwrr 
27701  1 
(* 
2 
Title: Divisibility in monoids and rings 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 18 July 2008 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

5 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

6 
Based on work by Stephan Hohe. 
27701  7 
*) 
8 

9 
theory Divisibility 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

10 
imports Permutation Coset Group 
27701  11 
begin 
12 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

13 
section {* Factorial Monoids *} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

14 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

15 
subsection {* Monoids with Cancellation Law *} 
27701  16 

17 
locale monoid_cancel = monoid + 

18 
assumes l_cancel: 

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

20 
and r_cancel: 

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

22 

23 
lemma (in monoid) monoid_cancelI: 

24 
assumes l_cancel: 

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

26 
and r_cancel: 

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

28 
shows "monoid_cancel G" 

29 
by unfold_locales fact+ 

30 

31 
lemma (in monoid_cancel) is_monoid_cancel: 

32 
"monoid_cancel G" 

33 
by intro_locales 

34 

35 
interpretation group \<subseteq> monoid_cancel 

36 
by unfold_locales simp+ 

37 

38 

39 
locale comm_monoid_cancel = monoid_cancel + comm_monoid 

40 

41 
lemma comm_monoid_cancelI: 

28599  42 
fixes G (structure) 
43 
assumes "comm_monoid G" 

27701  44 
assumes cancel: 
45 
"\<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" 

46 
shows "comm_monoid_cancel G" 

28599  47 
proof  
48 
interpret comm_monoid [G] by fact 

49 
show "comm_monoid_cancel G" 

50 
apply unfold_locales 

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

52 
apply (iprover intro: cancel) 

53 
apply (simp add: m_comm) 

54 
apply (iprover intro: cancel) 

55 
done 

56 
qed 

27701  57 

58 
lemma (in comm_monoid_cancel) is_comm_monoid_cancel: 

59 
"comm_monoid_cancel G" 

60 
by intro_locales 

61 

62 
interpretation comm_group \<subseteq> comm_monoid_cancel 

63 
by unfold_locales 

64 

65 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

66 
subsection {* Products of Units in Monoids *} 
27701  67 

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

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

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

71 
unfolding Units_def 

72 
using assms 

73 
apply safe 

74 
apply fast 

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

76 
apply (simp add: m_assoc Units_closed) 

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

78 
apply (simp add: m_assoc Units_closed) 

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

80 
apply fast 

81 
done 

82 

83 
lemma (in monoid) prod_unit_l: 

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

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

86 
shows "b \<in> Units G" 

87 
proof  

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

89 

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

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

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

93 

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

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

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

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

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

99 
by (simp add: m_assoc del: Units_l_inv) 

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

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

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

103 

104 
from c li ri 

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

106 
qed 

107 

108 
lemma (in monoid) prod_unit_r: 

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

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

111 
shows "a \<in> Units G" 

112 
proof  

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

114 

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

116 
by (simp add: m_assoc del: Units_r_inv) 

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

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

119 

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

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

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

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

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

125 
by (simp add: m_assoc del: Units_l_inv) 

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

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

128 

129 
from c li ri 

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

131 
qed 

132 

133 
lemma (in comm_monoid) unit_factor: 

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

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

136 
shows "a \<in> Units G" 

137 
using abunit[simplified Units_def] 

138 
proof clarsimp 

139 
fix i 

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

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

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

143 

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

145 

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

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

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

149 
also note li 

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

151 

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

153 
also note ri 

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

155 

156 
from carr' li' ri' 

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

158 
qed 

159 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

160 
subsection {* Divisibility and Association *} 
27701  161 

162 
subsubsection {* Function definitions *} 

163 

164 
constdefs (structure G) 

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

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

167 

168 
constdefs (structure G) 

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

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

171 

172 
abbreviation 

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

174 

175 
constdefs (structure G) 

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

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

178 

179 
constdefs (structure G) 

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

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

182 

183 
constdefs (structure G) 

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

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

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

187 

188 

189 

190 
subsubsection {* Divisibility *} 

191 

192 
lemma dividesI: 

193 
fixes G (structure) 

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

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

196 
shows "a divides b" 

197 
unfolding factor_def 

198 
using assms by fast 

199 

200 
lemma dividesI' [intro]: 

201 
fixes G (structure) 

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

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

204 
shows "a divides b" 

205 
using assms 

206 
by (fast intro: dividesI) 

207 

208 
lemma dividesD: 

209 
fixes G (structure) 

210 
assumes "a divides b" 

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

212 
using assms 

213 
unfolding factor_def 

214 
by fast 

215 

216 
lemma dividesE [elim]: 

217 
fixes G (structure) 

218 
assumes d: "a divides b" 

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

220 
shows "P" 

221 
proof  

222 
from dividesD[OF d] 

223 
obtain c 

224 
where "c\<in>carrier G" 

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

226 
by auto 

227 
thus "P" by (elim elim) 

228 
qed 

229 

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

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

232 
shows "a divides a" 

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

234 
apply (simp, simp add: carr) 

235 
done 

236 

237 
lemma (in monoid) divides_trans [trans]: 

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

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

240 
shows "a divides c" 

241 
using dvds[THEN dividesD] 

242 
by (blast intro: dividesI m_assoc acarr) 

243 

244 
lemma (in monoid) divides_mult_lI [intro]: 

245 
assumes ab: "a divides b" 

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

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

248 
using ab 

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

250 
apply (fast intro: dividesI) 

251 
done 

252 

253 
lemma (in monoid_cancel) divides_mult_l [simp]: 

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

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

256 
apply safe 

257 
apply (elim dividesE, intro dividesI, assumption) 

258 
apply (rule l_cancel[of c]) 

259 
apply (simp add: m_assoc carr)+ 

260 
apply (fast intro: divides_mult_lI carr) 

261 
done 

262 

263 
lemma (in comm_monoid) divides_mult_rI [intro]: 

264 
assumes ab: "a divides b" 

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

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

267 
using carr ab 

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

269 
apply (rule divides_mult_lI, assumption+) 

270 
done 

271 

272 
lemma (in comm_monoid_cancel) divides_mult_r [simp]: 

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

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

275 
using carr 

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

277 

278 
lemma (in monoid) divides_prod_r: 

279 
assumes ab: "a divides b" 

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

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

282 
using ab carr 

283 
by (fast intro: m_assoc) 

284 

285 
lemma (in comm_monoid) divides_prod_l: 

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

287 
and ab: "a divides b" 

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

289 
using ab carr 

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

291 
apply (fast intro: divides_prod_r) 

292 
done 

293 

294 
lemma (in monoid) unit_divides: 

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

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

297 
shows "u divides a" 

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

299 
from uunit acarr 

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

301 

302 
from uunit acarr 

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

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

305 
also from acarr 

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

307 
finally 

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

309 
qed 

310 

311 
lemma (in comm_monoid) divides_unit: 

312 
assumes udvd: "a divides u" 

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

314 
shows "a \<in> Units G" 

315 
using udvd carr 

316 
by (blast intro: unit_factor) 

317 

318 
lemma (in comm_monoid) Unit_eq_dividesone: 

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

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

321 
using ucarr 

322 
by (fast dest: divides_unit intro: unit_divides) 

323 

324 

325 
subsubsection {* Association *} 

326 

327 
lemma associatedI: 

328 
fixes G (structure) 

329 
assumes "a divides b" "b divides a" 

330 
shows "a \<sim> b" 

331 
using assms 

332 
by (simp add: associated_def) 

333 

334 
lemma (in monoid) associatedI2: 

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

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

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

338 
shows "a \<sim> b" 

339 
using uunit bcarr 

340 
unfolding a 

341 
apply (intro associatedI) 

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

343 
apply (simp add: m_assoc Units_closed Units_r_inv) 

344 
apply fast 

345 
done 

346 

347 
lemma (in monoid) associatedI2': 

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

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

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

351 
shows "a \<sim> b" 

352 
using assms by (intro associatedI2) 

353 

354 
lemma associatedD: 

355 
fixes G (structure) 

356 
assumes "a \<sim> b" 

357 
shows "a divides b" 

358 
using assms by (simp add: associated_def) 

359 

360 
lemma (in monoid_cancel) associatedD2: 

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

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

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

364 
using assoc 

365 
unfolding associated_def 

366 
proof clarify 

367 
assume "b divides a" 

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

369 
from this obtain u 

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

371 
by auto 

372 

373 
assume "a divides b" 

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

375 
from this obtain u' 

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

377 
by auto 

378 
note carr = carr ucarr u'carr 

379 

380 
from carr 

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

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

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

384 
also from carr 

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

386 
finally 

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

388 
with carr 

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

390 

391 
from carr 

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

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

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

395 
also from carr 

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

397 
finally 

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

399 
with carr 

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

401 

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

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

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

405 

406 
from ucarr this a 

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

408 
qed 

409 

410 
lemma associatedE: 

411 
fixes G (structure) 

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

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

414 
shows "P" 

415 
proof  

416 
from assoc 

417 
have "a divides b" "b divides a" 

418 
by (simp add: associated_def)+ 

419 
thus "P" by (elim e) 

420 
qed 

421 

422 
lemma (in monoid_cancel) associatedE2: 

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

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

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

426 
shows "P" 

427 
proof  

428 
from assoc and carr 

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

430 
from this obtain u 

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

432 
by auto 

433 
thus "P" by (elim e) 

434 
qed 

435 

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

437 
assumes "a \<in> carrier G" 

438 
shows "a \<sim> a" 

439 
using assms 

440 
by (fast intro: associatedI) 

441 

442 
lemma (in monoid) associated_sym [sym]: 

443 
assumes "a \<sim> b" 

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

445 
shows "b \<sim> a" 

446 
using assms 

447 
by (iprover intro: associatedI elim: associatedE) 

448 

449 
lemma (in monoid) associated_trans [trans]: 

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

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

452 
shows "a \<sim> c" 

453 
using assms 

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

455 

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

457 
"equivalence (division_rel G)" 

458 
apply unfold_locales 

459 
apply simp_all 

460 
apply (rule associated_sym, assumption+) 

461 
apply (iprover intro: associated_trans) 

462 
done 

463 

464 

465 
subsubsection {* Division and associativity *} 

466 

467 
lemma divides_antisym: 

468 
fixes G (structure) 

469 
assumes "a divides b" "b divides a" 

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

471 
shows "a \<sim> b" 

472 
using assms 

473 
by (fast intro: associatedI) 

474 

475 
lemma (in monoid) divides_cong_l [trans]: 

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

477 
and xdvdy: "x' divides y" 

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

479 
shows "x divides y" 

480 
proof  

481 
from xx' 

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

483 
also note xdvdy 

484 
finally 

485 
show "x divides y" by simp 

486 
qed 

487 

488 
lemma (in monoid) divides_cong_r [trans]: 

489 
assumes xdvdy: "x divides y" 

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

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

492 
shows "x divides y'" 

493 
proof  

494 
note xdvdy 

495 
also from yy' 

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

497 
finally 

498 
show "x divides y'" by simp 

499 
qed 

500 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

501 
lemma (in monoid) division_weak_partial_order [simp, intro!]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

502 
"weak_partial_order (division_rel G)" 
27701  503 
apply unfold_locales 
504 
apply simp_all 

505 
apply (simp add: associated_sym) 

506 
apply (blast intro: associated_trans) 

507 
apply (simp add: divides_antisym) 

508 
apply (blast intro: divides_trans) 

509 
apply (blast intro: divides_cong_l divides_cong_r associated_sym) 

510 
done 

511 

512 

513 
subsubsection {* Multiplication and associativity *} 

514 

515 
lemma (in monoid_cancel) mult_cong_r: 

516 
assumes "b \<sim> b'" 

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

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

519 
using assms 

520 
apply (elim associatedE2, intro associatedI2) 

521 
apply (auto intro: m_assoc[symmetric]) 

522 
done 

523 

524 
lemma (in comm_monoid_cancel) mult_cong_l: 

525 
assumes "a \<sim> a'" 

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

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

528 
using assms 

529 
apply (elim associatedE2, intro associatedI2) 

530 
apply assumption 

531 
apply (simp add: m_assoc Units_closed) 

532 
apply (simp add: m_comm Units_closed) 

533 
apply simp+ 

534 
done 

535 

536 
lemma (in monoid_cancel) assoc_l_cancel: 

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

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

539 
shows "b \<sim> b'" 

540 
using assms 

541 
apply (elim associatedE2, intro associatedI2) 

542 
apply assumption 

543 
apply (rule l_cancel[of a]) 

544 
apply (simp add: m_assoc Units_closed) 

545 
apply fast+ 

546 
done 

547 

548 
lemma (in comm_monoid_cancel) assoc_r_cancel: 

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

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

551 
shows "a \<sim> a'" 

552 
using assms 

553 
apply (elim associatedE2, intro associatedI2) 

554 
apply assumption 

555 
apply (rule r_cancel[of a b]) 

556 
apply (simp add: m_assoc Units_closed) 

557 
apply (simp add: m_comm Units_closed) 

558 
apply fast+ 

559 
done 

560 

561 

562 
subsubsection {* Units *} 

563 

564 
lemma (in monoid_cancel) assoc_unit_l [trans]: 

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

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

567 
shows "a \<in> Units G" 

568 
using assms 

569 
by (fast elim: associatedE2) 

570 

571 
lemma (in monoid_cancel) assoc_unit_r [trans]: 

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

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

574 
shows "b \<in> Units G" 

575 
using aunit bcarr associated_sym[OF asc] 

576 
by (blast intro: assoc_unit_l) 

577 

578 
lemma (in comm_monoid) Units_cong: 

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

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

581 
shows "b \<in> Units G" 

582 
using assms 

583 
by (blast intro: divides_unit elim: associatedE) 

584 

585 
lemma (in monoid) Units_assoc: 

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

587 
shows "a \<sim> b" 

588 
using units 

589 
by (fast intro: associatedI unit_divides) 

590 

591 
lemma (in monoid) Units_are_ones: 

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

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

594 
proof clarsimp 

595 
fix a 

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

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

598 
apply (rule associatedI) 

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

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

601 
done 

602 
next 

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

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

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

606 
qed 

607 

608 
lemma (in comm_monoid) Units_Lower: 

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

610 
apply (simp add: Units_def Lower_def) 

611 
apply (rule, rule) 

612 
apply clarsimp 

613 
apply (rule unit_divides) 

614 
apply (unfold Units_def, fast) 

615 
apply assumption 

616 
apply clarsimp 

617 
proof  

618 
fix x 

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

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

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

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

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

624 
from this obtain x' 

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

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

627 
by auto 

628 

629 
note xx' 

630 
also with xcarr x'carr 

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

632 
finally 

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

634 

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

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

637 
qed 

638 

639 

640 
subsubsection {* Proper factors *} 

641 

642 
lemma properfactorI: 

643 
fixes G (structure) 

644 
assumes "a divides b" 

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

646 
shows "properfactor G a b" 

647 
using assms 

648 
unfolding properfactor_def 

649 
by simp 

650 

651 
lemma properfactorI2: 

652 
fixes G (structure) 

653 
assumes advdb: "a divides b" 

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

655 
shows "properfactor G a b" 

656 
apply (rule properfactorI, rule advdb) 

657 
proof (rule ccontr, simp) 

658 
assume "b divides a" 

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

660 
with neq show "False" by fast 

661 
qed 

662 

663 
lemma (in comm_monoid_cancel) properfactorI3: 

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

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

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

667 
shows "properfactor G a p" 

668 
unfolding p 

669 
using carr 

670 
apply (intro properfactorI, fast) 

671 
proof (clarsimp, elim dividesE) 

672 
fix c 

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

674 
note [simp] = carr ccarr 

675 

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

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

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

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

680 

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

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

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

684 

685 
from ccarr linv[symmetric] rinv[symmetric] 

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

687 
with nunit 

688 
show "False" .. 

689 
qed 

690 

691 
lemma properfactorE: 

692 
fixes G (structure) 

693 
assumes pf: "properfactor G a b" 

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

695 
shows "P" 

696 
using pf 

697 
unfolding properfactor_def 

698 
by (fast intro: r) 

699 

700 
lemma properfactorE2: 

701 
fixes G (structure) 

702 
assumes pf: "properfactor G a b" 

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

704 
shows "P" 

705 
using pf 

706 
unfolding properfactor_def 

707 
by (fast elim: elim associatedE) 

708 

709 
lemma (in monoid) properfactor_unitE: 

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

711 
and pf: "properfactor G a u" 

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

713 
shows "P" 

714 
using pf unit_divides[OF uunit acarr] 

715 
by (fast elim: properfactorE) 

716 

717 

718 
lemma (in monoid) properfactor_divides: 

719 
assumes pf: "properfactor G a b" 

720 
shows "a divides b" 

721 
using pf 

722 
by (elim properfactorE) 

723 

724 
lemma (in monoid) properfactor_trans1 [trans]: 

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

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

727 
shows "properfactor G a c" 

728 
using dvds carr 

729 
apply (elim properfactorE, intro properfactorI) 

730 
apply (iprover intro: divides_trans)+ 

731 
done 

732 

733 
lemma (in monoid) properfactor_trans2 [trans]: 

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

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

736 
shows "properfactor G a c" 

737 
using dvds carr 

738 
apply (elim properfactorE, intro properfactorI) 

739 
apply (iprover intro: divides_trans)+ 

740 
done 

741 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

742 
lemma properfactor_lless: 
27701  743 
fixes G (structure) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

744 
shows "properfactor G = lless (division_rel G)" 
27701  745 
apply (rule ext) apply (rule ext) apply rule 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

746 
apply (fastsimp elim: properfactorE2 intro: weak_llessI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

747 
apply (fastsimp elim: weak_llessE intro: properfactorI2) 
27701  748 
done 
749 

750 
lemma (in monoid) properfactor_cong_l [trans]: 

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

752 
and pf: "properfactor G x y" 

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

754 
shows "properfactor G x' y" 

755 
using pf 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

756 
unfolding properfactor_lless 
27701  757 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

758 
interpret weak_partial_order ["division_rel G"] .. 
27701  759 
from x'x 
760 
have "x' .=\<^bsub>division_rel G\<^esub> x" by simp 

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

762 
finally 

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

764 
qed 

765 

766 
lemma (in monoid) properfactor_cong_r [trans]: 

767 
assumes pf: "properfactor G x y" 

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

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

770 
shows "properfactor G x y'" 

771 
using pf 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

772 
unfolding properfactor_lless 
27701  773 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27701
diff
changeset

774 
interpret weak_partial_order ["division_rel G"] .. 
27701  775 
assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" 
776 
also from yy' 

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

778 
finally 

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

780 
qed 

781 

782 
lemma (in monoid_cancel) properfactor_mult_lI [intro]: 

783 
assumes ab: "properfactor G a b" 

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

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

786 
using ab carr 

787 
by (fastsimp elim: properfactorE intro: properfactorI) 

788 

789 
lemma (in monoid_cancel) properfactor_mult_l [simp]: 

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

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

792 
using carr 

793 
by (fastsimp elim: properfactorE intro: properfactorI) 

794 

795 
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: 

796 
assumes ab: "properfactor G a b" 

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

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

799 
using ab carr 

800 
by (fastsimp elim: properfactorE intro: properfactorI) 

801 

802 
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: 

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

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

805 
using carr 

806 
by (fastsimp elim: properfactorE intro: properfactorI) 

807 

808 
lemma (in monoid) properfactor_prod_r: 

809 
assumes ab: "properfactor G a b" 

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

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

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

813 

814 
lemma (in comm_monoid) properfactor_prod_l: 

815 
assumes ab: "properfactor G a b" 

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

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

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

819 

820 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

821 
subsection {* Irreducible Elements and Primes *} 
27701  822 

823 
subsubsection {* Irreducible elements *} 

824 

825 
lemma irreducibleI: 

826 
fixes G (structure) 

827 
assumes "a \<notin> Units G" 

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

829 
shows "irreducible G a" 

830 
using assms 

831 
unfolding irreducible_def 

832 
by blast 

833 

834 
lemma irreducibleE: 

835 
fixes G (structure) 

836 
assumes irr: "irreducible G a" 

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

838 
shows "P" 

839 
using assms 

840 
unfolding irreducible_def 

841 
by blast 

842 

843 
lemma irreducibleD: 

844 
fixes G (structure) 

845 
assumes irr: "irreducible G a" 

846 
and pf: "properfactor G b a" 

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

848 
shows "b \<in> Units G" 

849 
using assms 

850 
by (fast elim: irreducibleE) 

851 

852 
lemma (in monoid_cancel) irreducible_cong [trans]: 

853 
assumes irred: "irreducible G a" 

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

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

856 
shows "irreducible G a'" 

857 
using assms 

858 
apply (elim irreducibleE, intro irreducibleI) 

859 
apply simp_all 

860 
proof clarify 

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

862 
also note aa'[symmetric] 

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

864 

865 
assume "a \<notin> Units G" 

866 
with aunit 

867 
show "False" by fast 

868 
next 

869 
fix b 

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

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

872 
assume "properfactor G b a'" 

873 
also note aa'[symmetric] 

874 
finally 

875 
have "properfactor G b a" by simp 

876 

877 
with bcarr 

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

879 
qed 

880 

881 

882 
lemma (in monoid) irreducible_prod_rI: 

883 
assumes airr: "irreducible G a" 

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

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

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

887 
using airr carr bunit 

888 
apply (elim irreducibleE, intro irreducibleI, clarify) 

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

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

891 
proof  

892 
fix c 

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

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

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

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

897 
finally 

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

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

900 
qed 

901 

902 
lemma (in comm_monoid) irreducible_prod_lI: 

903 
assumes birr: "irreducible G b" 

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

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

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

907 
apply (subst m_comm, simp+) 

908 
apply (intro irreducible_prod_rI assms) 

909 
done 

910 

911 
lemma (in comm_monoid_cancel) irreducible_prodE [elim]: 

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

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

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

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

916 
shows "P" 

917 
using irr 

918 
proof (elim irreducibleE) 

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

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

921 

922 
show "P" 

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

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

925 

926 
have "irreducible G b" 

927 
apply (rule irreducibleI) 

928 
proof (rule ccontr, simp) 

929 
assume "b \<in> Units G" 

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

931 
with abnunit show "False" .. 

932 
next 

933 
fix c 

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

935 
and "properfactor G c b" 

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

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

938 
qed 

939 

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

941 
next 

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

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

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

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

946 

947 
have "irreducible G a" 

948 
apply (rule irreducibleI) 

949 
proof (rule ccontr, simp) 

950 
assume "a \<in> Units G" 

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

952 
with abnunit show "False" .. 

953 
next 

954 
fix c 

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

956 
and "properfactor G c a" 

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

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

959 
qed 

960 

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

962 
qed 

963 
qed 

964 

965 

966 
subsubsection {* Prime elements *} 

967 

968 
lemma primeI: 

969 
fixes G (structure) 

970 
assumes "p \<notin> Units G" 

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

972 
shows "prime G p" 

973 
using assms 

974 
unfolding prime_def 

975 
by blast 

976 

977 
lemma primeE: 

978 
fixes G (structure) 

979 
assumes pprime: "prime G p" 

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

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

982 
shows "P" 

983 
using pprime 

984 
unfolding prime_def 

985 
by (blast dest: e) 

986 

987 
lemma (in comm_monoid_cancel) prime_divides: 

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

989 
and pprime: "prime G p" 

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

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

992 
using assms 

993 
by (blast elim: primeE) 

994 

995 
lemma (in monoid_cancel) prime_cong [trans]: 

996 
assumes pprime: "prime G p" 

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

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

999 
shows "prime G p'" 

1000 
using pprime 

1001 
apply (elim primeE, intro primeI) 

1002 
proof clarify 

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

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

1005 
also note pp'[symmetric] 

1006 
finally 

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

1008 
with pnunit 

1009 
show False .. 

1010 
next 

1011 
fix a b 

1012 
assume r[rule_format]: 

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

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

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

1016 

1017 
note pp' 

1018 
also note p'dvd 

1019 
finally 

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

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

1022 
moreover { 

1023 
note pp'[symmetric] 

1024 
also assume "p divides a" 

1025 
finally 

1026 
have "p' divides a" by simp 

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

1028 
} 

1029 
moreover { 

1030 
note pp'[symmetric] 

1031 
also assume "p divides b" 

1032 
finally 

1033 
have "p' divides b" by simp 

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

1035 
} 

1036 
ultimately 

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

1038 
qed 

1039 

1040 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset

1041 
subsection {* Factorization and Factorial Monoids *} 
27701  1042 

1043 
subsubsection {* Function definitions *} 

1044 

1045 
constdefs (structure G) 

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

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

1048 

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

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

1051 

1052 
abbreviation 

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

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

1055 

1056 
constdefs (structure G) 

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

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

1059 

1060 

1061 
locale factorial_monoid = comm_monoid_cancel + 

1062 
assumes factors_exist: 

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

1064 
and factors_unique: 

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

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

1067 

1068 

1069 
subsubsection {* Comparing lists of elements *} 

1070 

1071 
text {* Association on lists *} 

1072 

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

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

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

1076 
using assms 

1077 
by (induct as) simp+ 

1078 

1079 
lemma (in monoid) listassoc_sym [sym]: 

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

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

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

1083 
using assms 

1084 
proof (induct as arbitrary: bs, simp) 

1085 
case Cons 

1086 
thus ?case 

1087 
apply (induct bs, simp) 

1088 
apply clarsimp 

1089 
apply (iprover intro: associated_sym) 

1090 
done 

1091 
qed 

1092 

1093 
lemma (in monoid) listassoc_trans [trans]: 

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

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

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

1097 
using assms 

1098 
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) 

1099 
apply (rule associated_trans) 

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

1101 
apply (simp, simp) 

1102 
apply blast+ 

1103 
done 

1104 

1105 
lemma (in monoid_cancel) irrlist_listassoc_cong: 

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

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

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

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

1110 
using assms 

1111 
apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) 

1112 
apply (blast intro: irreducible_cong) 

1113 
done 

1114 

1115 

1116 
text {* Permutations *} 

1117 

1118 
lemma perm_map [intro]: 

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

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

1121 
using p 

1122 
by induct auto 

1123 

1124 
lemma perm_map_switch: 

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

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

1127 
using p m 

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

1129 

1130 
lemma (in monoid) perm_assoc_switch: 

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

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

1133 
using p a 

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

1135 
apply (clarsimp simp add: list_all2_Cons2, blast) 

1136 
apply (clarsimp simp add: list_all2_Cons2) 

1137 
apply blast 

1138 
apply blast 

1139 
done 

1140 

1141 
lemma (in monoid) perm_assoc_switch_r: 

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

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

1144 
using p a 

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

1146 
apply (clarsimp simp add: list_all2_Cons1, blast) 

1147 
apply (clarsimp simp add: list_all2_Cons1) 

1148 
apply blast 

1149 
apply blast 

1150 
done 

1151 

1152 
declare perm_sym [sym] 

1153 

1154 
lemma perm_setP: 

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

1156 
and as: "P (set as)" 

1157 
shows "P (set bs)" 

1158 
proof  

1159 
from perm 

1160 
have "multiset_of as = multiset_of bs" 

1161 
by (simp add: multiset_of_eq_perm) 

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

1163 
with as 

1164 
show "P (set bs)" by simp 

1165 
qed 

1166 

1167 
lemmas (in monoid) perm_closed = 

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

1169 

1170 
lemmas (in monoid) irrlist_perm_cong = 

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

1172 

1173 

1174 
text {* Essentially equal factorizations *} 

1175 

1176 
lemma (in monoid) essentially_equalI: 

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

1178 
shows "essentially_equal G fs1 fs2" 

1179 
using ex 

1180 
unfolding essentially_equal_def 

1181 
by fast 

1182 

1183 
lemma (in monoid) essentially_equalE: 

1184 
assumes ee: "essentially_equal G fs1 fs2" 

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

1186 
shows "P" 

1187 
using ee 

1188 
unfolding essentially_equal_def 

1189 
by (fast intro: e) 

1190 

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

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

1193 
shows "essentially_equal G as as" 

1194 
using carr 

1195 
by (fast intro: essentially_equalI) 

1196 

1197 
lemma (in monoid) ee_sym [sym]: 

1198 
assumes ee: "essentially_equal G as bs" 

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

1200 
shows "essentially_equal G bs as" 

1201 
using ee 

1202 
proof (elim essentially_equalE) 

1203 
fix fs 

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

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

1206 
from this obtain fs' 

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

1208 
by auto 

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

1210 
with a[symmetric] carr 

1211 
show ?thesis 

1212 
by (iprover intro: essentially_equalI perm_closed) 

1213 
qed 

1214 

1215 
lemma (in monoid) ee_trans [trans]: 

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

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

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

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

1220 
shows "essentially_equal G as cs" 

1221 
using ab bc 

1222 
proof (elim essentially_equalE) 

1223 
fix abs bcs 

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

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

1226 
from this obtain bs' 

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

1228 
by auto 

1229 

1230 
assume "as <~~> abs" 

1231 
with p 

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

1233 

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

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

1236 
note a 

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

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

1239 

1240 
with pp 

1241 
show ?thesis 

1242 
by (rule essentially_equalI) 

1243 
qed 

1244 

1245 

1246 
subsubsection {* Properties of lists of elements *} 

1247 

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

1249 

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

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

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

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

1254 

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

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

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

1258 
using assms 

1259 
apply (induct fs) 

1260 
apply simp 

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

1262 
apply (fast intro: dividesI) 

1263 
apply clarsimp 

1264 
apply (elim dividesE, intro dividesI) 

1265 
defer 1 

1266 
apply (simp add: m_comm) 

1267 
apply (simp add: m_assoc[symmetric]) 

1268 
apply (simp add: m_comm) 

1269 
apply simp 

1270 
done 

1271 

1272 
lemma (in comm_monoid_cancel) multlist_listassoc_cong: 

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

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

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

1276 
using assms 

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

1278 
case (Cons a as fs') 

1279 
thus ?case 

1280 
apply (induct fs', simp) 

1281 
proof clarsimp 

1282 
fix b bs 

1283 
assume "a \<sim> b" 

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

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

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

1287 
by (fast intro: mult_cong_l) 

1288 
also 

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

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

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

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

1293 
with ascarr bscarr bcarr 

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

1295 
by (fast intro: mult_cong_r) 

1296 
finally 

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

1298 
by (simp add: ascarr bscarr acarr bcarr) 

1299 
qed 

1300 
qed 

1301 

1302 
lemma (in comm_monoid) multlist_perm_cong: 

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

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

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

1306 
using prm ascarr 

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

1308 
proof clarsimp 

1309 
fix xs ys zs 

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

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

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

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

1314 
qed 

1315 

1316 
lemma (in comm_monoid_cancel) multlist_ee_cong: 

1317 
assumes "essentially_equal G fs fs'" 

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

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

1320 
using assms 

1321 
apply (elim essentially_equalE) 

1322 
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) 

1323 
done 

1324 

1325 

1326 
subsubsection {* Factorization in irreducible elements *} 

1327 

1328 
lemma wfactorsI: 

28599  1329 
fixes G (structure) 
27701  1330 
assumes "\<forall>f\<in>set fs. irreducible G f" 
1331 
and "foldr (op \<otimes>) fs \<one> \<sim> a" 

1332 
shows "wfactors G fs a" 

1333 
using assms 

1334 
unfolding wfactors_def 

1335 
by simp 

1336 

1337 
lemma wfactorsE: 

28599  1338 
fixes G (structure) 
27701  1339 
assumes wf: "wfactors G fs a" 
1340 
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P" 

1341 
shows "P" 

1342 
using wf 

1343 
unfolding wfactors_def 

1344 
by (fast dest: e) 

1345 

1346 
lemma (in monoid) factorsI: 

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

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

1349 
shows "factors G fs a" 

1350 
using assms 

1351 
unfolding factors_def 

1352 
by simp 

1353 

1354 
lemma factorsE: 

28599  1355 
fixes G (structure) 
27701  1356 
assumes f: "factors G fs a" 
1357 
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P" 

1358 
shows "P" 

1359 
using f 

1360 
unfolding factors_def 

1361 
by (simp add: e) 

1362 

1363 
lemma (in monoid) factors_wfactors: 

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

1365 
shows "wfactors G as a" 

1366 
using assms 

1367 
by (blast elim: factorsE intro: wfactorsI) 

1368 

1369 
lemma (in monoid) wfactors_factors: 

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

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

1372 
using assms 

1373 
by (blast elim: wfactorsE intro: factorsI) 

1374 

1375 
lemma (in monoid) factors_closed [dest]: 

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

1377 
shows "a \<in> carrier G" 

1378 
using assms 

1379 
by (elim factorsE, clarsimp) 

1380 

1381 
lemma (in monoid) nunit_factors: 

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

1383 
and fs: "factors G as a" 

1384 
shows "length as > 0" 

1385 
apply (insert fs, elim factorsE) 

1386 
proof (cases "length as = 0") 

1387 
assume "length as = 0" 

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

1389 

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

1391 
with fold 

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

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

1394 
with anunit 

1395 
have "False" by simp 

1396 
thus ?thesis .. 

1397 
qed simp 

1398 

1399 
lemma (in monoid) unit_wfactors [simp]: 

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

1401 
shows "wfactors G [] a" 

1402 
using aunit 

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

1404 

1405 
lemma (in comm_monoid_cancel) unit_wfactors_empty: 

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

1407 
and wf: "wfactors G fs a" 

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

1409 
shows "fs = []" 

1410 
proof (rule ccontr, cases fs, simp) 

1411 
fix f fs' 

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

1413 

1414 
from carr 

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

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

1417 
by (simp add: fs)+ 

1418 

1419 
from fs wf 

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

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

1422 

1423 
from fs wf 

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

1425 

1426 
note aunit 

1427 
also from fs wf 

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

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

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

1431 
finally 

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

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

1434 

1435 
with fnunit show "False" by simp 

1436 
qed 

1437 

1438 

1439 
text {* Comparing wfactors *} 

1440 

1441 
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l: 

1442 
assumes fact: "wfactors G fs a" 

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

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

1445 
shows "wfactors G fs' a" 

1446 
using fact 

1447 
apply (elim wfactorsE, intro wfactorsI) 

1448 
proof  

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

1450 
also note asc 

1451 
finally (irrlist_listassoc_cong) 

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

1453 
next 

1454 
from asc[symmetric] 

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

1456 
by (simp add: multlist_listassoc_cong carr) 

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

1458 
finally 

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

1460 
qed 

1461 

1462 
lemma (in comm_monoid) wfactors_perm_cong_l: 

1463 
assumes "wfactors G fs a" 

1464 
and "fs <~~> fs'" 

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

1466 
shows "wfactors G fs' a" 

1467 
using assms 

1468 
apply (elim wfactorsE, intro wfactorsI) 

1469 
apply (rule irrlist_perm_cong, assumption+) 

1470 
apply (simp add: multlist_perm_cong[symmetric]) 

1471 
done 

1472 
