author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 32960  69916a850301 
child 35272  c283ae736bea 
permissions  rwrr 
27701  1 
(* 
2 
Title: Divisibility in monoids and rings 

3 
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

4 

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

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

8 
theory Divisibility 

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

9 
imports Permutation Coset Group 
27701  10 
begin 
11 

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

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

13 

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

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

16 
locale monoid_cancel = monoid + 

17 
assumes l_cancel: 

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

19 
and r_cancel: 

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

21 

22 
lemma (in monoid) monoid_cancelI: 

23 
assumes l_cancel: 

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

25 
and r_cancel: 

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

27 
shows "monoid_cancel G" 

28823  28 
proof qed fact+ 
27701  29 

30 
lemma (in monoid_cancel) is_monoid_cancel: 

31 
"monoid_cancel G" 

28823  32 
.. 
27701  33 

29237  34 
sublocale group \<subseteq> monoid_cancel 
28823  35 
proof qed simp+ 
27701  36 

37 

38 
locale comm_monoid_cancel = monoid_cancel + comm_monoid 

39 

40 
lemma comm_monoid_cancelI: 

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

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

45 
shows "comm_monoid_cancel G" 

28599  46 
proof  
29237  47 
interpret comm_monoid G by fact 
28599  48 
show "comm_monoid_cancel G" 
49 
apply unfold_locales 

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

51 
apply (iprover intro: cancel) 

52 
apply (simp add: m_comm) 

53 
apply (iprover intro: cancel) 

54 
done 

55 
qed 

27701  56 

57 
lemma (in comm_monoid_cancel) is_comm_monoid_cancel: 

58 
"comm_monoid_cancel G" 

28823  59 
by intro_locales 
27701  60 

29237  61 
sublocale comm_group \<subseteq> comm_monoid_cancel 
28823  62 
.. 
27701  63 

64 

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

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

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

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

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

70 
unfolding Units_def 

71 
using assms 

72 
apply safe 

73 
apply fast 

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

75 
apply (simp add: m_assoc Units_closed) 

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

77 
apply (simp add: m_assoc Units_closed) 

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

79 
apply fast 

80 
done 

81 

82 
lemma (in monoid) prod_unit_l: 

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

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

85 
shows "b \<in> Units G" 

86 
proof  

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

88 

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

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

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

92 

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

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

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

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

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

98 
by (simp add: m_assoc del: Units_l_inv) 

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

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

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

102 

103 
from c li ri 

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

105 
qed 

106 

107 
lemma (in monoid) prod_unit_r: 

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

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

110 
shows "a \<in> Units G" 

111 
proof  

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

113 

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

115 
by (simp add: m_assoc del: Units_r_inv) 

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

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

118 

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

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

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

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

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

124 
by (simp add: m_assoc del: Units_l_inv) 

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

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

127 

128 
from c li ri 

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

130 
qed 

131 

132 
lemma (in comm_monoid) unit_factor: 

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

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

135 
shows "a \<in> Units G" 

136 
using abunit[simplified Units_def] 

137 
proof clarsimp 

138 
fix i 

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

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

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

142 

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

144 

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

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

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

148 
also note li 

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

150 

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

152 
also note ri 

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

154 

155 
from carr' li' ri' 

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

157 
qed 

158 

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

159 
subsection {* Divisibility and Association *} 
27701  160 

161 
subsubsection {* Function definitions *} 

162 

163 
constdefs (structure G) 

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

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

166 

167 
constdefs (structure G) 

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

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

170 

171 
abbreviation 

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

173 

174 
constdefs (structure G) 

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

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

177 

178 
constdefs (structure G) 

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

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

181 

182 
constdefs (structure G) 

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

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

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

186 

187 

188 

189 
subsubsection {* Divisibility *} 

190 

191 
lemma dividesI: 

192 
fixes G (structure) 

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

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

195 
shows "a divides b" 

196 
unfolding factor_def 

197 
using assms by fast 

198 

199 
lemma dividesI' [intro]: 

200 
fixes G (structure) 

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

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

203 
shows "a divides b" 

204 
using assms 

205 
by (fast intro: dividesI) 

206 

207 
lemma dividesD: 

208 
fixes G (structure) 

209 
assumes "a divides b" 

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

211 
using assms 

212 
unfolding factor_def 

213 
by fast 

214 

215 
lemma dividesE [elim]: 

216 
fixes G (structure) 

217 
assumes d: "a divides b" 

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

219 
shows "P" 

220 
proof  

221 
from dividesD[OF d] 

222 
obtain c 

223 
where "c\<in>carrier G" 

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

225 
by auto 

226 
thus "P" by (elim elim) 

227 
qed 

228 

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

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

231 
shows "a divides a" 

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

233 
apply (simp, simp add: carr) 

234 
done 

235 

236 
lemma (in monoid) divides_trans [trans]: 

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

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

239 
shows "a divides c" 

240 
using dvds[THEN dividesD] 

241 
by (blast intro: dividesI m_assoc acarr) 

242 

243 
lemma (in monoid) divides_mult_lI [intro]: 

244 
assumes ab: "a divides b" 

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

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

247 
using ab 

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

249 
apply (fast intro: dividesI) 

250 
done 

251 

252 
lemma (in monoid_cancel) divides_mult_l [simp]: 

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

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

255 
apply safe 

256 
apply (elim dividesE, intro dividesI, assumption) 

257 
apply (rule l_cancel[of c]) 

258 
apply (simp add: m_assoc carr)+ 

259 
apply (fast intro: divides_mult_lI carr) 

260 
done 

261 

262 
lemma (in comm_monoid) divides_mult_rI [intro]: 

263 
assumes ab: "a divides b" 

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

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

266 
using carr ab 

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

268 
apply (rule divides_mult_lI, assumption+) 

269 
done 

270 

271 
lemma (in comm_monoid_cancel) divides_mult_r [simp]: 

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

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

274 
using carr 

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

276 

277 
lemma (in monoid) divides_prod_r: 

278 
assumes ab: "a divides b" 

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

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

281 
using ab carr 

282 
by (fast intro: m_assoc) 

283 

284 
lemma (in comm_monoid) divides_prod_l: 

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

286 
and ab: "a divides b" 

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

288 
using ab carr 

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

290 
apply (fast intro: divides_prod_r) 

291 
done 

292 

293 
lemma (in monoid) unit_divides: 

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

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

296 
shows "u divides a" 

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

298 
from uunit acarr 

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

300 

301 
from uunit acarr 

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

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

304 
also from acarr 

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

306 
finally 

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

308 
qed 

309 

310 
lemma (in comm_monoid) divides_unit: 

311 
assumes udvd: "a divides u" 

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

313 
shows "a \<in> Units G" 

314 
using udvd carr 

315 
by (blast intro: unit_factor) 

316 

317 
lemma (in comm_monoid) Unit_eq_dividesone: 

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

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

320 
using ucarr 

321 
by (fast dest: divides_unit intro: unit_divides) 

322 

323 

324 
subsubsection {* Association *} 

325 

326 
lemma associatedI: 

327 
fixes G (structure) 

328 
assumes "a divides b" "b divides a" 

329 
shows "a \<sim> b" 

330 
using assms 

331 
by (simp add: associated_def) 

332 

333 
lemma (in monoid) associatedI2: 

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

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

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

337 
shows "a \<sim> b" 

338 
using uunit bcarr 

339 
unfolding a 

340 
apply (intro associatedI) 

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

342 
apply (simp add: m_assoc Units_closed Units_r_inv) 

343 
apply fast 

344 
done 

345 

346 
lemma (in monoid) associatedI2': 

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

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

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

350 
shows "a \<sim> b" 

351 
using assms by (intro associatedI2) 

352 

353 
lemma associatedD: 

354 
fixes G (structure) 

355 
assumes "a \<sim> b" 

356 
shows "a divides b" 

357 
using assms by (simp add: associated_def) 

358 

359 
lemma (in monoid_cancel) associatedD2: 

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

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

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

363 
using assoc 

364 
unfolding associated_def 

365 
proof clarify 

366 
assume "b divides a" 

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

368 
from this obtain u 

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

370 
by auto 

371 

372 
assume "a divides b" 

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

374 
from this obtain u' 

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

376 
by auto 

377 
note carr = carr ucarr u'carr 

378 

379 
from carr 

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

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

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

383 
also from carr 

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

385 
finally 

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

387 
with carr 

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

389 

390 
from carr 

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

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

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

394 
also from carr 

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

396 
finally 

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

398 
with carr 

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

400 

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

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

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

404 

405 
from ucarr this a 

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

407 
qed 

408 

409 
lemma associatedE: 

410 
fixes G (structure) 

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

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

413 
shows "P" 

414 
proof  

415 
from assoc 

416 
have "a divides b" "b divides a" 

417 
by (simp add: associated_def)+ 

418 
thus "P" by (elim e) 

419 
qed 

420 

421 
lemma (in monoid_cancel) associatedE2: 

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

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

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

425 
shows "P" 

426 
proof  

427 
from assoc and carr 

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

429 
from this obtain u 

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

431 
by auto 

432 
thus "P" by (elim e) 

433 
qed 

434 

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

436 
assumes "a \<in> carrier G" 

437 
shows "a \<sim> a" 

438 
using assms 

439 
by (fast intro: associatedI) 

440 

441 
lemma (in monoid) associated_sym [sym]: 

442 
assumes "a \<sim> b" 

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

444 
shows "b \<sim> a" 

445 
using assms 

446 
by (iprover intro: associatedI elim: associatedE) 

447 

448 
lemma (in monoid) associated_trans [trans]: 

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

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

451 
shows "a \<sim> c" 

452 
using assms 

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

454 

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

456 
"equivalence (division_rel G)" 

457 
apply unfold_locales 

458 
apply simp_all 

459 
apply (rule associated_sym, assumption+) 

460 
apply (iprover intro: associated_trans) 

461 
done 

462 

463 

464 
subsubsection {* Division and associativity *} 

465 

466 
lemma divides_antisym: 

467 
fixes G (structure) 

468 
assumes "a divides b" "b divides a" 

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

470 
shows "a \<sim> b" 

471 
using assms 

472 
by (fast intro: associatedI) 

473 

474 
lemma (in monoid) divides_cong_l [trans]: 

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

476 
and xdvdy: "x' divides y" 

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

478 
shows "x divides y" 

479 
proof  

480 
from xx' 

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

482 
also note xdvdy 

483 
finally 

484 
show "x divides y" by simp 

485 
qed 

486 

487 
lemma (in monoid) divides_cong_r [trans]: 

488 
assumes xdvdy: "x divides y" 

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

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

491 
shows "x divides y'" 

492 
proof  

493 
note xdvdy 

494 
also from yy' 

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

496 
finally 

497 
show "x divides y'" by simp 

498 
qed 

499 

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

500 
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

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

504 
apply (simp add: associated_sym) 

505 
apply (blast intro: associated_trans) 

506 
apply (simp add: divides_antisym) 

507 
apply (blast intro: divides_trans) 

508 
apply (blast intro: divides_cong_l divides_cong_r associated_sym) 

509 
done 

510 

511 

512 
subsubsection {* Multiplication and associativity *} 

513 

514 
lemma (in monoid_cancel) mult_cong_r: 

515 
assumes "b \<sim> b'" 

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

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

518 
using assms 

519 
apply (elim associatedE2, intro associatedI2) 

520 
apply (auto intro: m_assoc[symmetric]) 

521 
done 

522 

523 
lemma (in comm_monoid_cancel) mult_cong_l: 

524 
assumes "a \<sim> a'" 

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

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

527 
using assms 

528 
apply (elim associatedE2, intro associatedI2) 

529 
apply assumption 

530 
apply (simp add: m_assoc Units_closed) 

531 
apply (simp add: m_comm Units_closed) 

532 
apply simp+ 

533 
done 

534 

535 
lemma (in monoid_cancel) assoc_l_cancel: 

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

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

538 
shows "b \<sim> b'" 

539 
using assms 

540 
apply (elim associatedE2, intro associatedI2) 

541 
apply assumption 

542 
apply (rule l_cancel[of a]) 

543 
apply (simp add: m_assoc Units_closed) 

544 
apply fast+ 

545 
done 

546 

547 
lemma (in comm_monoid_cancel) assoc_r_cancel: 

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

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

550 
shows "a \<sim> a'" 

551 
using assms 

552 
apply (elim associatedE2, intro associatedI2) 

553 
apply assumption 

554 
apply (rule r_cancel[of a b]) 

555 
apply (simp add: m_assoc Units_closed) 

556 
apply (simp add: m_comm Units_closed) 

557 
apply fast+ 

558 
done 

559 

560 

561 
subsubsection {* Units *} 

562 

563 
lemma (in monoid_cancel) assoc_unit_l [trans]: 

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

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

566 
shows "a \<in> Units G" 

567 
using assms 

568 
by (fast elim: associatedE2) 

569 

570 
lemma (in monoid_cancel) assoc_unit_r [trans]: 

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 aunit bcarr associated_sym[OF asc] 

575 
by (blast intro: assoc_unit_l) 

576 

577 
lemma (in comm_monoid) Units_cong: 

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

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

580 
shows "b \<in> Units G" 

581 
using assms 

582 
by (blast intro: divides_unit elim: associatedE) 

583 

584 
lemma (in monoid) Units_assoc: 

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

586 
shows "a \<sim> b" 

587 
using units 

588 
by (fast intro: associatedI unit_divides) 

589 

590 
lemma (in monoid) Units_are_ones: 

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

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

593 
proof clarsimp 

594 
fix a 

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

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

597 
apply (rule associatedI) 

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

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

600 
done 

601 
next 

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

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

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

605 
qed 

606 

607 
lemma (in comm_monoid) Units_Lower: 

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

609 
apply (simp add: Units_def Lower_def) 

610 
apply (rule, rule) 

611 
apply clarsimp 

612 
apply (rule unit_divides) 

613 
apply (unfold Units_def, fast) 

614 
apply assumption 

615 
apply clarsimp 

616 
proof  

617 
fix x 

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

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

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

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

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

623 
from this obtain x' 

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

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

626 
by auto 

627 

628 
note xx' 

629 
also with xcarr x'carr 

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

631 
finally 

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

633 

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

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

636 
qed 

637 

638 

639 
subsubsection {* Proper factors *} 

640 

641 
lemma properfactorI: 

642 
fixes G (structure) 

643 
assumes "a divides b" 

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

645 
shows "properfactor G a b" 

646 
using assms 

647 
unfolding properfactor_def 

648 
by simp 

649 

650 
lemma properfactorI2: 

651 
fixes G (structure) 

652 
assumes advdb: "a divides b" 

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

654 
shows "properfactor G a b" 

655 
apply (rule properfactorI, rule advdb) 

656 
proof (rule ccontr, simp) 

657 
assume "b divides a" 

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

659 
with neq show "False" by fast 

660 
qed 

661 

662 
lemma (in comm_monoid_cancel) properfactorI3: 

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

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

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

666 
shows "properfactor G a p" 

667 
unfolding p 

668 
using carr 

669 
apply (intro properfactorI, fast) 

670 
proof (clarsimp, elim dividesE) 

671 
fix c 

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

673 
note [simp] = carr ccarr 

674 

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

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

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

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

679 

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

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

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

683 

684 
from ccarr linv[symmetric] rinv[symmetric] 

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

686 
with nunit 

687 
show "False" .. 

688 
qed 

689 

690 
lemma properfactorE: 

691 
fixes G (structure) 

692 
assumes pf: "properfactor G a b" 

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

694 
shows "P" 

695 
using pf 

696 
unfolding properfactor_def 

697 
by (fast intro: r) 

698 

699 
lemma properfactorE2: 

700 
fixes G (structure) 

701 
assumes pf: "properfactor G a b" 

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

703 
shows "P" 

704 
using pf 

705 
unfolding properfactor_def 

706 
by (fast elim: elim associatedE) 

707 

708 
lemma (in monoid) properfactor_unitE: 

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

710 
and pf: "properfactor G a u" 

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

712 
shows "P" 

713 
using pf unit_divides[OF uunit acarr] 

714 
by (fast elim: properfactorE) 

715 

716 

717 
lemma (in monoid) properfactor_divides: 

718 
assumes pf: "properfactor G a b" 

719 
shows "a divides b" 

720 
using pf 

721 
by (elim properfactorE) 

722 

723 
lemma (in monoid) properfactor_trans1 [trans]: 

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

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

726 
shows "properfactor G a c" 

727 
using dvds carr 

728 
apply (elim properfactorE, intro properfactorI) 

729 
apply (iprover intro: divides_trans)+ 

730 
done 

731 

732 
lemma (in monoid) properfactor_trans2 [trans]: 

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

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

735 
shows "properfactor G a c" 

736 
using dvds carr 

737 
apply (elim properfactorE, intro properfactorI) 

738 
apply (iprover intro: divides_trans)+ 

739 
done 

740 

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

741 
lemma properfactor_lless: 
27701  742 
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

743 
shows "properfactor G = lless (division_rel G)" 
27701  744 
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

745 
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

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

749 
lemma (in monoid) properfactor_cong_l [trans]: 

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

751 
and pf: "properfactor G x y" 

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

753 
shows "properfactor G x' y" 

754 
using pf 

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

755 
unfolding properfactor_lless 
27701  756 
proof  
29237  757 
interpret weak_partial_order "division_rel G" .. 
27701  758 
from x'x 
759 
have "x' .=\<^bsub>division_rel G\<^esub> x" by simp 

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

761 
finally 

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

763 
qed 

764 

765 
lemma (in monoid) properfactor_cong_r [trans]: 

766 
assumes pf: "properfactor G x y" 

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

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

769 
shows "properfactor G x y'" 

770 
using pf 

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

771 
unfolding properfactor_lless 
27701  772 
proof  
29237  773 
interpret weak_partial_order "division_rel G" .. 
27701  774 
assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" 
775 
also from yy' 

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

777 
finally 

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

779 
qed 

780 

781 
lemma (in monoid_cancel) properfactor_mult_lI [intro]: 

782 
assumes ab: "properfactor G a b" 

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

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

785 
using ab carr 

786 
by (fastsimp elim: properfactorE intro: properfactorI) 

787 

788 
lemma (in monoid_cancel) properfactor_mult_l [simp]: 

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

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

791 
using carr 

792 
by (fastsimp elim: properfactorE intro: properfactorI) 

793 

794 
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]: 

795 
assumes ab: "properfactor G a b" 

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

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

798 
using ab carr 

799 
by (fastsimp elim: properfactorE intro: properfactorI) 

800 

801 
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]: 

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

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

804 
using carr 

805 
by (fastsimp elim: properfactorE intro: properfactorI) 

806 

807 
lemma (in monoid) properfactor_prod_r: 

808 
assumes ab: "properfactor G a b" 

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

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

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

812 

813 
lemma (in comm_monoid) properfactor_prod_l: 

814 
assumes ab: "properfactor G a b" 

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

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

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

818 

819 

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

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

822 
subsubsection {* Irreducible elements *} 

823 

824 
lemma irreducibleI: 

825 
fixes G (structure) 

826 
assumes "a \<notin> Units G" 

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

828 
shows "irreducible G a" 

829 
using assms 

830 
unfolding irreducible_def 

831 
by blast 

832 

833 
lemma irreducibleE: 

834 
fixes G (structure) 

835 
assumes irr: "irreducible G a" 

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

837 
shows "P" 

838 
using assms 

839 
unfolding irreducible_def 

840 
by blast 

841 

842 
lemma irreducibleD: 

843 
fixes G (structure) 

844 
assumes irr: "irreducible G a" 

845 
and pf: "properfactor G b a" 

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

847 
shows "b \<in> Units G" 

848 
using assms 

849 
by (fast elim: irreducibleE) 

850 

851 
lemma (in monoid_cancel) irreducible_cong [trans]: 

852 
assumes irred: "irreducible G a" 

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

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

855 
shows "irreducible G a'" 

856 
using assms 

857 
apply (elim irreducibleE, intro irreducibleI) 

858 
apply simp_all 

859 
proof clarify 

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

861 
also note aa'[symmetric] 

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

863 

864 
assume "a \<notin> Units G" 

865 
with aunit 

866 
show "False" by fast 

867 
next 

868 
fix b 

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

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

871 
assume "properfactor G b a'" 

872 
also note aa'[symmetric] 

873 
finally 

874 
have "properfactor G b a" by simp 

875 

876 
with bcarr 

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

878 
qed 

879 

880 

881 
lemma (in monoid) irreducible_prod_rI: 

882 
assumes airr: "irreducible G a" 

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

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

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

886 
using airr carr bunit 

887 
apply (elim irreducibleE, intro irreducibleI, clarify) 

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

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

890 
proof  

891 
fix c 

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

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

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

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

896 
finally 

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

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

899 
qed 

900 

901 
lemma (in comm_monoid) irreducible_prod_lI: 

902 
assumes birr: "irreducible G b" 

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

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

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

906 
apply (subst m_comm, simp+) 

907 
apply (intro irreducible_prod_rI assms) 

908 
done 

909 

910 
lemma (in comm_monoid_cancel) irreducible_prodE [elim]: 

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

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

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

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

915 
shows "P" 

916 
using irr 

917 
proof (elim irreducibleE) 

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

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

920 

921 
show "P" 

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

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

924 

925 
have "irreducible G b" 

926 
apply (rule irreducibleI) 

927 
proof (rule ccontr, simp) 

928 
assume "b \<in> Units G" 

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

930 
with abnunit show "False" .. 

931 
next 

932 
fix c 

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

934 
and "properfactor G c b" 

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

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

937 
qed 

938 

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

940 
next 

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

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

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

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

945 

946 
have "irreducible G a" 

947 
apply (rule irreducibleI) 

948 
proof (rule ccontr, simp) 

949 
assume "a \<in> Units G" 

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

951 
with abnunit show "False" .. 

952 
next 

953 
fix c 

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

955 
and "properfactor G c a" 

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

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

958 
qed 

959 

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

961 
qed 

962 
qed 

963 

964 

965 
subsubsection {* Prime elements *} 

966 

967 
lemma primeI: 

968 
fixes G (structure) 

969 
assumes "p \<notin> Units G" 

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

971 
shows "prime G p" 

972 
using assms 

973 
unfolding prime_def 

974 
by blast 

975 

976 
lemma primeE: 

977 
fixes G (structure) 

978 
assumes pprime: "prime G p" 

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

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

981 
shows "P" 

982 
using pprime 

983 
unfolding prime_def 

984 
by (blast dest: e) 

985 

986 
lemma (in comm_monoid_cancel) prime_divides: 

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

988 
and pprime: "prime G p" 

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

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

991 
using assms 

992 
by (blast elim: primeE) 

993 

994 
lemma (in monoid_cancel) prime_cong [trans]: 

995 
assumes pprime: "prime G p" 

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

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

998 
shows "prime G p'" 

999 
using pprime 

1000 
apply (elim primeE, intro primeI) 

1001 
proof clarify 

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

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

1004 
also note pp'[symmetric] 

1005 
finally 

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

1007 
with pnunit 

1008 
show False .. 

1009 
next 

1010 
fix a b 

1011 
assume r[rule_format]: 

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

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

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

1015 

1016 
note pp' 

1017 
also note p'dvd 

1018 
finally 

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

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

1021 
moreover { 

1022 
note pp'[symmetric] 

1023 
also assume "p divides a" 

1024 
finally 

1025 
have "p' divides a" by simp 

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

1027 
} 

1028 
moreover { 

1029 
note pp'[symmetric] 

1030 
also assume "p divides b" 

1031 
finally 

1032 
have "p' divides b" by simp 

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

1034 
} 

1035 
ultimately 

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

1037 
qed 

1038 

1039 

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

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

1042 
subsubsection {* Function definitions *} 

1043 

1044 
constdefs (structure G) 

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

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

1047 

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

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

1050 

1051 
abbreviation 

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

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

1054 

1055 
constdefs (structure G) 

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

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

1058 

1059 

1060 
locale factorial_monoid = comm_monoid_cancel + 

1061 
assumes factors_exist: 

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

1063 
and factors_unique: 

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

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

1066 

1067 

1068 
subsubsection {* Comparing lists of elements *} 

1069 

1070 
text {* Association on lists *} 

1071 

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

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

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

1075 
using assms 

1076 
by (induct as) simp+ 

1077 

1078 
lemma (in monoid) listassoc_sym [sym]: 

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

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

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

1082 
using assms 

1083 
proof (induct as arbitrary: bs, simp) 

1084 
case Cons 

1085 
thus ?case 

1086 
apply (induct bs, simp) 

1087 
apply clarsimp 

1088 
apply (iprover intro: associated_sym) 

1089 
done 

1090 
qed 

1091 

1092 
lemma (in monoid) listassoc_trans [trans]: 

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

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

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

1096 
using assms 

1097 
apply (simp add: list_all2_conv_all_nth set_conv_nth, safe) 

1098 
apply (rule associated_trans) 

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

1100 
apply (simp, simp) 

1101 
apply blast+ 

1102 
done 

1103 

1104 
lemma (in monoid_cancel) irrlist_listassoc_cong: 

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

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

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

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

1109 
using assms 

1110 
apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth) 

1111 
apply (blast intro: irreducible_cong) 

1112 
done 

1113 

1114 

1115 
text {* Permutations *} 

1116 

1117 
lemma perm_map [intro]: 

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

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

1120 
using p 

1121 
by induct auto 

1122 

1123 
lemma perm_map_switch: 

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

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

1126 
using p m 

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

1128 

1129 
lemma (in monoid) perm_assoc_switch: 

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

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

1132 
using p a 

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

1134 
apply (clarsimp simp add: list_all2_Cons2, blast) 

1135 
apply (clarsimp simp add: list_all2_Cons2) 

1136 
apply blast 

1137 
apply blast 

1138 
done 

1139 

1140 
lemma (in monoid) perm_assoc_switch_r: 

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

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

1143 
using p a 

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

1145 
apply (clarsimp simp add: list_all2_Cons1, blast) 

1146 
apply (clarsimp simp add: list_all2_Cons1) 

1147 
apply blast 

1148 
apply blast 

1149 
done 

1150 

1151 
declare perm_sym [sym] 

1152 

1153 
lemma perm_setP: 

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

1155 
and as: "P (set as)" 

1156 
shows "P (set bs)" 

1157 
proof  

1158 
from perm 

1159 
have "multiset_of as = multiset_of bs" 

1160 
by (simp add: multiset_of_eq_perm) 

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

1162 
with as 

1163 
show "P (set bs)" by simp 

1164 
qed 

1165 

1166 
lemmas (in monoid) perm_closed = 

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

1168 

1169 
lemmas (in monoid) irrlist_perm_cong = 

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

1171 

1172 

1173 
text {* Essentially equal factorizations *} 

1174 

1175 
lemma (in monoid) essentially_equalI: 

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

1177 
shows "essentially_equal G fs1 fs2" 

1178 
using ex 

1179 
unfolding essentially_equal_def 

1180 
by fast 

1181 

1182 
lemma (in monoid) essentially_equalE: 

1183 
assumes ee: "essentially_equal G fs1 fs2" 

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

1185 
shows "P" 

1186 
using ee 

1187 
unfolding essentially_equal_def 

1188 
by (fast intro: e) 

1189 

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

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

1192 
shows "essentially_equal G as as" 

1193 
using carr 

1194 
by (fast intro: essentially_equalI) 

1195 

1196 
lemma (in monoid) ee_sym [sym]: 

1197 
assumes ee: "essentially_equal G as bs" 

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

1199 
shows "essentially_equal G bs as" 

1200 
using ee 

1201 
proof (elim essentially_equalE) 

1202 
fix fs 

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

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

1205 
from this obtain fs' 

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

1207 
by auto 

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

1209 
with a[symmetric] carr 

1210 
show ?thesis 

1211 
by (iprover intro: essentially_equalI perm_closed) 

1212 
qed 

1213 

1214 
lemma (in monoid) ee_trans [trans]: 

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

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

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

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

1219 
shows "essentially_equal G as cs" 

1220 
using ab bc 

1221 
proof (elim essentially_equalE) 

1222 
fix abs bcs 

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

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

1225 
from this obtain bs' 

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

1227 
by auto 

1228 

1229 
assume "as <~~> abs" 

1230 
with p 

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

1232 

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

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

1235 
note a 

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

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

1238 

1239 
with pp 

1240 
show ?thesis 

1241 
by (rule essentially_equalI) 

1242 
qed 

1243 

1244 

1245 
subsubsection {* Properties of lists of elements *} 

1246 

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

1248 

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

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

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

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

1253 

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

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

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

1257 
using assms 

1258 
apply (induct fs) 

1259 
apply simp 

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

1261 
apply (fast intro: dividesI) 

1262 
apply clarsimp 

1263 
apply (elim dividesE, intro dividesI) 

1264 
defer 1 

1265 
apply (simp add: m_comm) 

1266 
apply (simp add: m_assoc[symmetric]) 

1267 
apply (simp add: m_comm) 

1268 
apply simp 

1269 
done 

1270 

1271 
lemma (in comm_monoid_cancel) multlist_listassoc_cong: 

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

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

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

1275 
using assms 

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

1277 
case (Cons a as fs') 

1278 
thus ?case 

1279 
apply (induct fs', simp) 

1280 
proof clarsimp 

1281 
fix b bs 

1282 
assume "a \<sim> b" 

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

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

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

1286 
by (fast intro: mult_cong_l) 

1287 
also 

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

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

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

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

1292 
with ascarr bscarr bcarr 

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

1294 
by (fast intro: mult_cong_r) 

1295 
finally 

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

1297 
by (simp add: ascarr bscarr acarr bcarr) 

1298 
qed 

1299 
qed 

1300 

1301 
lemma (in comm_monoid) multlist_perm_cong: 

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

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

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

1305 
using prm ascarr 

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

1307 
proof clarsimp 

1308 
fix xs ys zs 

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

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

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

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

1313 
qed 

1314 

1315 
lemma (in comm_monoid_cancel) multlist_ee_cong: 

1316 
assumes "essentially_equal G fs fs'" 

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

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

1319 
using assms 

1320 
apply (elim essentially_equalE) 

1321 
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed) 

1322 
done 

1323 

1324 

1325 
subsubsection {* Factorization in irreducible elements *} 

1326 

1327 
lemma wfactorsI: 

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

1331 
shows "wfactors G fs a" 

1332 
using assms 

1333 
unfolding wfactors_def 

1334 
by simp 

1335 

1336 
lemma wfactorsE: 

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

1340 
shows "P" 

1341 
using wf 

1342 
unfolding wfactors_def 

1343 
by (fast dest: e) 

1344 

1345 
lemma (in monoid) factorsI: 

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

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

1348 
shows "factors G fs a" 

1349 
using assms 

1350 
unfolding factors_def 

1351 
by simp 

1352 

1353 
lemma factorsE: 

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

1357 
shows "P" 

1358 
using f 

1359 
unfolding factors_def 

1360 
by (simp add: e) 

1361 

1362 
lemma (in monoid) factors_wfactors: 

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

1364 
shows "wfactors G as a" 

1365 
using assms 

1366 
by (blast elim: factorsE intro: wfactorsI) 

1367 

1368 
lemma (in monoid) wfactors_factors: 

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

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

1371 
using assms 

1372 
by (blast elim: wfactorsE intro: factorsI) 

1373 

1374 
lemma (in monoid) factors_closed [dest]: 

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

1376 
shows "a \<in> carrier G" 

1377 
using assms 

1378 
by (elim factorsE, clarsimp) 

1379 

1380 
lemma (in monoid) nunit_factors: 

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

1382 
and fs: "factors G as a" 

1383 
shows "length as > 0" 

1384 
apply (insert fs, elim factorsE) 

1385 
proof (cases "length as = 0") 

1386 
assume "length as = 0" 

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

1388 

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

1390 
with fold 

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

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

1393 
with anunit 

1394 
have "False" by simp 

1395 
thus ?thesis .. 

1396 
qed simp 

1397 

1398 
lemma (in monoid) unit_wfactors [simp]: 

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

1400 
shows "wfactors G [] a" 

1401 
using aunit 

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

1403 

1404 
lemma (in comm_monoid_cancel) unit_wfactors_empty: 

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

1406 
and wf: "wfactors G fs a" 

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

1408 
shows "fs = []" 

1409 
proof (rule ccontr, cases fs, simp) 

1410 
fix f fs' 

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

1412 

1413 
from carr 

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

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

1416 
by (simp add: fs)+ 

1417 

1418 
from fs wf 

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

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

1421 

1422 
from fs wf 

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

1424 

1425 
note aunit 

1426 
also from fs wf 

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

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

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

1430 
finally 

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

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

1433 

1434 
with fnunit show "False" by simp 

1435 
qed 

1436 

1437 

1438 
text {* Comparing wfactors *} 

1439 

1440 
lemma (in comm_monoid_cancel) wfactors_listassoc_cong_l: 

1441 
assumes fact: "wfactors G fs a" 

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

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

1444 
shows "wfactors G fs' a" 

1445 
using fact 

1446 
apply (elim wfactorsE, intro wfactorsI) 

1447 
proof  

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

1449 
also note asc 

1450 
finally (irrlist_listassoc_cong) 

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

1452 
next 

1453 
from asc[symmetric] 

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

1455 
by (simp add: multlist_listassoc_cong carr) 

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

1457 
finally 

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

1459 
qed 

1460 

1461 
lemma (in comm_monoid) wfactors_perm_cong_l: 

1462 
assumes "wfactors G fs a" 

1463 
and "fs <~~> fs'" 

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

1465 
shows "wfactors G fs' a" 

1466 
using assms 

1467 
apply (elim wfactorsE, intro wfactorsI) 

1468 
apply (rule irrlist_perm_cong, assumption+) 

1469 
apply (simp add: multlist_perm_cong[symmetric]) 

1470 