author  ballarin 
Fri, 02 May 2003 20:02:50 +0200  
changeset 13949  0ce528cd6f19 
parent 13944  9b34607cd83e 
child 13975  c8e9a89883ce 
permissions  rwrr 
13813  1 
(* 
2 
Title: HOL/Algebra/Group.thy 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 4 February 2003 

5 

6 
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. 

7 
*) 

8 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

9 
header {* Groups *} 
13813  10 

13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13817
diff
changeset

11 
theory Group = FuncSet: 
13813  12 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

13 
(* axclass number < type 
13936  14 

15 
instance nat :: number .. 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

16 
instance int :: number .. *) 
13936  17 

18 
section {* From Magmas to Groups *} 

19 

13813  20 
text {* 
21 
Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with 

22 
the exception of \emph{magma} which, following Bourbaki, is a set 

23 
together with a binary, closed operation. 

24 
*} 

25 

26 
subsection {* Definitions *} 

27 

13817  28 
record 'a semigroup = 
13813  29 
carrier :: "'a set" 
30 
mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70) 

31 

13817  32 
record 'a monoid = "'a semigroup" + 
13813  33 
one :: 'a ("\<one>\<index>") 
13817  34 

13936  35 
constdefs 
36 
m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80) 

37 
"m_inv G x == (THE y. y \<in> carrier G & 

38 
mult G x y = one G & mult G y x = one G)" 

39 

40 
Units :: "('a, 'm) monoid_scheme => 'a set" 

41 
"Units G == {y. y \<in> carrier G & 

42 
(EX x : carrier G. mult G x y = one G & mult G y x = one G)}" 

43 

44 
consts 

45 
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) 

46 

47 
defs (overloaded) 

48 
nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n" 

49 
int_pow_def: "pow G a z == 

50 
let p = nat_rec (one G) (%u b. mult G b a) 

51 
in if neg z then m_inv G (p (nat (z))) else p (nat z)" 

13813  52 

53 
locale magma = struct G + 

54 
assumes m_closed [intro, simp]: 

55 
"[ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G" 

56 

57 
locale semigroup = magma + 

58 
assumes m_assoc: 

59 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

13936  60 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 
13813  61 

13936  62 
locale monoid = semigroup + 
13813  63 
assumes one_closed [intro, simp]: "\<one> \<in> carrier G" 
64 
and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x" 

13936  65 
and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x" 
13817  66 

13936  67 
lemma monoidI: 
68 
assumes m_closed: 

69 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y \<in> carrier G" 

70 
and one_closed: "one G \<in> carrier G" 

71 
and m_assoc: 

72 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

73 
mult G (mult G x y) z = mult G x (mult G y z)" 

74 
and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" 

75 
and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x" 

76 
shows "monoid G" 

77 
by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro 

78 
semigroup.intro monoid_axioms.intro 

79 
intro: prems) 

80 

81 
lemma (in monoid) Units_closed [dest]: 

82 
"x \<in> Units G ==> x \<in> carrier G" 

83 
by (unfold Units_def) fast 

84 

85 
lemma (in monoid) inv_unique: 

86 
assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" 

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

88 
shows "y = y'" 

89 
proof  

90 
from G eq have "y = y \<otimes> (x \<otimes> y')" by simp 

91 
also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc) 

92 
also from G eq have "... = y'" by simp 

93 
finally show ?thesis . 

94 
qed 

95 

13940  96 
lemma (in monoid) Units_one_closed [intro, simp]: 
97 
"\<one> \<in> Units G" 

98 
by (unfold Units_def) auto 

99 

13936  100 
lemma (in monoid) Units_inv_closed [intro, simp]: 
101 
"x \<in> Units G ==> inv x \<in> carrier G" 

13943  102 
apply (unfold Units_def m_inv_def, auto) 
13936  103 
apply (rule theI2, fast) 
13943  104 
apply (fast intro: inv_unique, fast) 
13936  105 
done 
106 

107 
lemma (in monoid) Units_l_inv: 

108 
"x \<in> Units G ==> inv x \<otimes> x = \<one>" 

13943  109 
apply (unfold Units_def m_inv_def, auto) 
13936  110 
apply (rule theI2, fast) 
13943  111 
apply (fast intro: inv_unique, fast) 
13936  112 
done 
113 

114 
lemma (in monoid) Units_r_inv: 

115 
"x \<in> Units G ==> x \<otimes> inv x = \<one>" 

13943  116 
apply (unfold Units_def m_inv_def, auto) 
13936  117 
apply (rule theI2, fast) 
13943  118 
apply (fast intro: inv_unique, fast) 
13936  119 
done 
120 

121 
lemma (in monoid) Units_inv_Units [intro, simp]: 

122 
"x \<in> Units G ==> inv x \<in> Units G" 

123 
proof  

124 
assume x: "x \<in> Units G" 

125 
show "inv x \<in> Units G" 

126 
by (auto simp add: Units_def 

127 
intro: Units_l_inv Units_r_inv x Units_closed [OF x]) 

128 
qed 

129 

130 
lemma (in monoid) Units_l_cancel [simp]: 

131 
"[ x \<in> Units G; y \<in> carrier G; z \<in> carrier G ] ==> 

132 
(x \<otimes> y = x \<otimes> z) = (y = z)" 

133 
proof 

134 
assume eq: "x \<otimes> y = x \<otimes> z" 

135 
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" 

136 
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" 

137 
by (simp add: m_assoc Units_closed) 

138 
with G show "y = z" by (simp add: Units_l_inv) 

139 
next 

140 
assume eq: "y = z" 

141 
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" 

142 
then show "x \<otimes> y = x \<otimes> z" by simp 

143 
qed 

144 

145 
lemma (in monoid) Units_inv_inv [simp]: 

146 
"x \<in> Units G ==> inv (inv x) = x" 

147 
proof  

148 
assume x: "x \<in> Units G" 

149 
then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" 

150 
by (simp add: Units_l_inv Units_r_inv) 

151 
with x show ?thesis by (simp add: Units_closed) 

152 
qed 

153 

154 
lemma (in monoid) inv_inj_on_Units: 

155 
"inj_on (m_inv G) (Units G)" 

156 
proof (rule inj_onI) 

157 
fix x y 

158 
assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y" 

159 
then have "inv (inv x) = inv (inv y)" by simp 

160 
with G show "x = y" by simp 

161 
qed 

162 

13940  163 
lemma (in monoid) Units_inv_comm: 
164 
assumes inv: "x \<otimes> y = \<one>" 

165 
and G: "x \<in> Units G" "y \<in> Units G" 

166 
shows "y \<otimes> x = \<one>" 

167 
proof  

168 
from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed) 

169 
with G show ?thesis by (simp del: r_one add: m_assoc Units_closed) 

170 
qed 

171 

13936  172 
text {* Power *} 
173 

174 
lemma (in monoid) nat_pow_closed [intro, simp]: 

175 
"x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G" 

176 
by (induct n) (simp_all add: nat_pow_def) 

177 

178 
lemma (in monoid) nat_pow_0 [simp]: 

179 
"x (^) (0::nat) = \<one>" 

180 
by (simp add: nat_pow_def) 

181 

182 
lemma (in monoid) nat_pow_Suc [simp]: 

183 
"x (^) (Suc n) = x (^) n \<otimes> x" 

184 
by (simp add: nat_pow_def) 

185 

186 
lemma (in monoid) nat_pow_one [simp]: 

187 
"\<one> (^) (n::nat) = \<one>" 

188 
by (induct n) simp_all 

189 

190 
lemma (in monoid) nat_pow_mult: 

191 
"x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)" 

192 
by (induct m) (simp_all add: m_assoc [THEN sym]) 

193 

194 
lemma (in monoid) nat_pow_pow: 

195 
"x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)" 

196 
by (induct m) (simp, simp add: nat_pow_mult add_commute) 

197 

198 
text {* 

199 
A group is a monoid all of whose elements are invertible. 

200 
*} 

201 

202 
locale group = monoid + 

203 
assumes Units: "carrier G <= Units G" 

204 

205 
theorem groupI: 

206 
assumes m_closed [simp]: 

207 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y \<in> carrier G" 

208 
and one_closed [simp]: "one G \<in> carrier G" 

209 
and m_assoc: 

210 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

211 
mult G (mult G x y) z = mult G x (mult G y z)" 

212 
and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x" 

213 
and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G" 

214 
shows "group G" 

215 
proof  

216 
have l_cancel [simp]: 

217 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

218 
(mult G x y = mult G x z) = (y = z)" 

219 
proof 

220 
fix x y z 

221 
assume eq: "mult G x y = mult G x z" 

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

223 
with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" 

224 
and l_inv: "mult G x_inv x = one G" by fast 

225 
from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z" 

226 
by (simp add: m_assoc) 

227 
with G show "y = z" by (simp add: l_inv) 

228 
next 

229 
fix x y z 

230 
assume eq: "y = z" 

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

232 
then show "mult G x y = mult G x z" by simp 

233 
qed 

234 
have r_one: 

235 
"!!x. x \<in> carrier G ==> mult G x (one G) = x" 

236 
proof  

237 
fix x 

238 
assume x: "x \<in> carrier G" 

239 
with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" 

240 
and l_inv: "mult G x_inv x = one G" by fast 

241 
from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x" 

242 
by (simp add: m_assoc [symmetric] l_inv) 

243 
with x xG show "mult G x (one G) = x" by simp 

244 
qed 

245 
have inv_ex: 

246 
"!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G & 

247 
mult G x y = one G" 

248 
proof  

249 
fix x 

250 
assume x: "x \<in> carrier G" 

251 
with l_inv_ex obtain y where y: "y \<in> carrier G" 

252 
and l_inv: "mult G y x = one G" by fast 

253 
from x y have "mult G y (mult G x y) = mult G y (one G)" 

254 
by (simp add: m_assoc [symmetric] l_inv r_one) 

255 
with x y have r_inv: "mult G x y = one G" 

256 
by simp 

257 
from x y show "EX y : carrier G. mult G y x = one G & 

258 
mult G x y = one G" 

259 
by (fast intro: l_inv r_inv) 

260 
qed 

261 
then have carrier_subset_Units: "carrier G <= Units G" 

262 
by (unfold Units_def) fast 

263 
show ?thesis 

264 
by (fast intro!: group.intro magma.intro semigroup_axioms.intro 

265 
semigroup.intro monoid_axioms.intro group_axioms.intro 

266 
carrier_subset_Units intro: prems r_one) 

267 
qed 

268 

269 
lemma (in monoid) monoid_groupI: 

270 
assumes l_inv_ex: 

271 
"!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G" 

272 
shows "group G" 

273 
by (rule groupI) (auto intro: m_assoc l_inv_ex) 

274 

275 
lemma (in group) Units_eq [simp]: 

276 
"Units G = carrier G" 

277 
proof 

278 
show "Units G <= carrier G" by fast 

279 
next 

280 
show "carrier G <= Units G" by (rule Units) 

281 
qed 

282 

283 
lemma (in group) inv_closed [intro, simp]: 

284 
"x \<in> carrier G ==> inv x \<in> carrier G" 

285 
using Units_inv_closed by simp 

286 

287 
lemma (in group) l_inv: 

288 
"x \<in> carrier G ==> inv x \<otimes> x = \<one>" 

289 
using Units_l_inv by simp 

13813  290 

291 
subsection {* Cancellation Laws and Basic Properties *} 

292 

293 
lemma (in group) l_cancel [simp]: 

294 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

295 
(x \<otimes> y = x \<otimes> z) = (y = z)" 

13936  296 
using Units_l_inv by simp 
13940  297 

13813  298 
lemma (in group) r_inv: 
299 
"x \<in> carrier G ==> x \<otimes> inv x = \<one>" 

300 
proof  

301 
assume x: "x \<in> carrier G" 

302 
then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>" 

303 
by (simp add: m_assoc [symmetric] l_inv) 

304 
with x show ?thesis by (simp del: r_one) 

305 
qed 

306 

307 
lemma (in group) r_cancel [simp]: 

308 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

309 
(y \<otimes> x = z \<otimes> x) = (y = z)" 

310 
proof 

311 
assume eq: "y \<otimes> x = z \<otimes> x" 

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

313 
then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)" 

314 
by (simp add: m_assoc [symmetric]) 

315 
with G show "y = z" by (simp add: r_inv) 

316 
next 

317 
assume eq: "y = z" 

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

319 
then show "y \<otimes> x = z \<otimes> x" by simp 

320 
qed 

321 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

322 
lemma (in group) inv_one [simp]: 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

323 
"inv \<one> = \<one>" 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

324 
proof  
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

325 
have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

326 
moreover have "... = \<one>" by (simp add: r_inv) 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

327 
finally show ?thesis . 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

328 
qed 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

329 

13813  330 
lemma (in group) inv_inv [simp]: 
331 
"x \<in> carrier G ==> inv (inv x) = x" 

13936  332 
using Units_inv_inv by simp 
333 

334 
lemma (in group) inv_inj: 

335 
"inj_on (m_inv G) (carrier G)" 

336 
using inv_inj_on_Units by simp 

13813  337 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

338 
lemma (in group) inv_mult_group: 
13813  339 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" 
340 
proof  

341 
assume G: "x \<in> carrier G" "y \<in> carrier G" 

342 
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)" 

343 
by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv) 

344 
with G show ?thesis by simp 

345 
qed 

346 

13940  347 
lemma (in group) inv_comm: 
348 
"[ x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G ] ==> y \<otimes> x = \<one>" 

349 
by (rule Units_inv_comm) auto 

350 

13944  351 
lemma (in group) inv_equality: 
13943  352 
"[y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G] ==> inv x = y" 
353 
apply (simp add: m_inv_def) 

354 
apply (rule the_equality) 

355 
apply (simp add: inv_comm [of y x]) 

356 
apply (rule r_cancel [THEN iffD1], auto) 

357 
done 

358 

13936  359 
text {* Power *} 
360 

361 
lemma (in group) int_pow_def2: 

362 
"a (^) (z::int) = (if neg z then inv (a (^) (nat (z))) else a (^) (nat z))" 

363 
by (simp add: int_pow_def nat_pow_def Let_def) 

364 

365 
lemma (in group) int_pow_0 [simp]: 

366 
"x (^) (0::int) = \<one>" 

367 
by (simp add: int_pow_def2) 

368 

369 
lemma (in group) int_pow_one [simp]: 

370 
"\<one> (^) (z::int) = \<one>" 

371 
by (simp add: int_pow_def2) 

372 

13813  373 
subsection {* Substructures *} 
374 

375 
locale submagma = var H + struct G + 

376 
assumes subset [intro, simp]: "H \<subseteq> carrier G" 

377 
and m_closed [intro, simp]: "[ x \<in> H; y \<in> H ] ==> x \<otimes> y \<in> H" 

378 

379 
declare (in submagma) magma.intro [intro] semigroup.intro [intro] 

13936  380 
semigroup_axioms.intro [intro] 
13813  381 
(* 
382 
alternative definition of submagma 

383 

384 
locale submagma = var H + struct G + 

385 
assumes subset [intro, simp]: "carrier H \<subseteq> carrier G" 

386 
and m_equal [simp]: "mult H = mult G" 

387 
and m_closed [intro, simp]: 

388 
"[ x \<in> carrier H; y \<in> carrier H ] ==> x \<otimes> y \<in> carrier H" 

389 
*) 

390 

391 
lemma submagma_imp_subset: 

392 
"submagma H G ==> H \<subseteq> carrier G" 

393 
by (rule submagma.subset) 

394 

395 
lemma (in submagma) subsetD [dest, simp]: 

396 
"x \<in> H ==> x \<in> carrier G" 

397 
using subset by blast 

398 

399 
lemma (in submagma) magmaI [intro]: 

400 
includes magma G 

401 
shows "magma (G( carrier := H ))" 

402 
by rule simp 

403 

404 
lemma (in submagma) semigroup_axiomsI [intro]: 

405 
includes semigroup G 

406 
shows "semigroup_axioms (G( carrier := H ))" 

407 
by rule (simp add: m_assoc) 

408 

409 
lemma (in submagma) semigroupI [intro]: 

410 
includes semigroup G 

411 
shows "semigroup (G( carrier := H ))" 

412 
using prems by fast 

413 

414 
locale subgroup = submagma H G + 

415 
assumes one_closed [intro, simp]: "\<one> \<in> H" 

416 
and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H" 

417 

418 
declare (in subgroup) group.intro [intro] 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

419 

13813  420 
lemma (in subgroup) group_axiomsI [intro]: 
421 
includes group G 

422 
shows "group_axioms (G( carrier := H ))" 

13936  423 
by rule (auto intro: l_inv r_inv simp add: Units_def) 
13813  424 

425 
lemma (in subgroup) groupI [intro]: 

426 
includes group G 

427 
shows "group (G( carrier := H ))" 

13936  428 
by (rule groupI) (auto intro: m_assoc l_inv) 
13813  429 

430 
text {* 

431 
Since @{term H} is nonempty, it contains some element @{term x}. Since 

432 
it is closed under inverse, it contains @{text "inv x"}. Since 

433 
it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}. 

434 
*} 

435 

436 
lemma (in group) one_in_subset: 

437 
"[ H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H ] 

438 
==> \<one> \<in> H" 

439 
by (force simp add: l_inv) 

440 

441 
text {* A characterization of subgroups: closed, nonempty subset. *} 

442 

443 
lemma (in group) subgroupI: 

444 
assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}" 

445 
and inv: "!!a. a \<in> H ==> inv a \<in> H" 

446 
and mult: "!!a b. [a \<in> H; b \<in> H] ==> a \<otimes> b \<in> H" 

447 
shows "subgroup H G" 

448 
proof 

449 
from subset and mult show "submagma H G" .. 

450 
next 

451 
have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems) 

452 
with inv show "subgroup_axioms H G" 

453 
by (intro subgroup_axioms.intro) simp_all 

454 
qed 

455 

456 
text {* 

457 
Repeat facts of submagmas for subgroups. Necessary??? 

458 
*} 

459 

460 
lemma (in subgroup) subset: 

461 
"H \<subseteq> carrier G" 

462 
.. 

463 

464 
lemma (in subgroup) m_closed: 

465 
"[ x \<in> H; y \<in> H ] ==> x \<otimes> y \<in> H" 

466 
.. 

467 

468 
declare magma.m_closed [simp] 

469 

13936  470 
declare monoid.one_closed [iff] group.inv_closed [simp] 
471 
monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] 

13813  472 

473 
lemma subgroup_nonempty: 

474 
"~ subgroup {} G" 

475 
by (blast dest: subgroup.one_closed) 

476 

477 
lemma (in subgroup) finite_imp_card_positive: 

478 
"finite (carrier G) ==> 0 < card H" 

479 
proof (rule classical) 

480 
have sub: "subgroup H G" using prems .. 

481 
assume fin: "finite (carrier G)" 

482 
and zero: "~ 0 < card H" 

483 
then have "finite H" by (blast intro: finite_subset dest: subset) 

484 
with zero sub have "subgroup {} G" by simp 

485 
with subgroup_nonempty show ?thesis by contradiction 

486 
qed 

487 

13936  488 
(* 
489 
lemma (in monoid) Units_subgroup: 

490 
"subgroup (Units G) G" 

491 
*) 

492 

13813  493 
subsection {* Direct Products *} 
494 

495 
constdefs 

13817  496 
DirProdSemigroup :: 
13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

497 
"[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme] 
13817  498 
=> ('a \<times> 'b) semigroup" 
499 
(infixr "\<times>\<^sub>s" 80) 

500 
"G \<times>\<^sub>s H == ( carrier = carrier G \<times> carrier H, 

501 
mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) )" 

502 

13936  503 
DirProdGroup :: 
13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

504 
"[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid" 
13936  505 
(infixr "\<times>\<^sub>g" 80) 
506 
"G \<times>\<^sub>g H == ( carrier = carrier (G \<times>\<^sub>s H), 

13817  507 
mult = mult (G \<times>\<^sub>s H), 
508 
one = (one G, one H) )" 

13813  509 

13817  510 
lemma DirProdSemigroup_magma: 
13813  511 
includes magma G + magma H 
13817  512 
shows "magma (G \<times>\<^sub>s H)" 
513 
by rule (auto simp add: DirProdSemigroup_def) 

13813  514 

13817  515 
lemma DirProdSemigroup_semigroup_axioms: 
13813  516 
includes semigroup G + semigroup H 
13817  517 
shows "semigroup_axioms (G \<times>\<^sub>s H)" 
518 
by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc) 

13813  519 

13817  520 
lemma DirProdSemigroup_semigroup: 
13813  521 
includes semigroup G + semigroup H 
13817  522 
shows "semigroup (G \<times>\<^sub>s H)" 
13813  523 
using prems 
524 
by (fast intro: semigroup.intro 

13817  525 
DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms) 
13813  526 

527 
lemma DirProdGroup_magma: 

528 
includes magma G + magma H 

529 
shows "magma (G \<times>\<^sub>g H)" 

13817  530 
by rule 
13936  531 
(auto simp add: DirProdGroup_def DirProdSemigroup_def) 
13813  532 

533 
lemma DirProdGroup_semigroup_axioms: 

534 
includes semigroup G + semigroup H 

535 
shows "semigroup_axioms (G \<times>\<^sub>g H)" 

536 
by rule 

13936  537 
(auto simp add: DirProdGroup_def DirProdSemigroup_def 
13817  538 
G.m_assoc H.m_assoc) 
13813  539 

540 
lemma DirProdGroup_semigroup: 

541 
includes semigroup G + semigroup H 

542 
shows "semigroup (G \<times>\<^sub>g H)" 

543 
using prems 

544 
by (fast intro: semigroup.intro 

545 
DirProdGroup_magma DirProdGroup_semigroup_axioms) 

546 

547 
(* ... and further lemmas for group ... *) 

548 

13817  549 
lemma DirProdGroup_group: 
13813  550 
includes group G + group H 
551 
shows "group (G \<times>\<^sub>g H)" 

13936  552 
by (rule groupI) 
553 
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv 

554 
simp add: DirProdGroup_def DirProdSemigroup_def) 

13813  555 

13944  556 
lemma carrier_DirProdGroup [simp]: 
557 
"carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H" 

558 
by (simp add: DirProdGroup_def DirProdSemigroup_def) 

559 

560 
lemma one_DirProdGroup [simp]: 

561 
"one (G \<times>\<^sub>g H) = (one G, one H)" 

562 
by (simp add: DirProdGroup_def DirProdSemigroup_def); 

563 

564 
lemma mult_DirProdGroup [simp]: 

565 
"mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')" 

566 
by (simp add: DirProdGroup_def DirProdSemigroup_def) 

567 

568 
lemma inv_DirProdGroup [simp]: 

569 
includes group G + group H 

570 
assumes g: "g \<in> carrier G" 

571 
and h: "h \<in> carrier H" 

572 
shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)" 

573 
apply (rule group.inv_equality [OF DirProdGroup_group]) 

574 
apply (simp_all add: prems group_def group.l_inv) 

575 
done 

576 

13813  577 
subsection {* Homomorphisms *} 
578 

579 
constdefs 

13817  580 
hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme] 
581 
=> ('a => 'b)set" 

13813  582 
"hom G H == 
583 
{h. h \<in> carrier G > carrier H & 

584 
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}" 

585 

586 
lemma (in semigroup) hom: 

587 
includes semigroup G 

588 
shows "semigroup ( carrier = hom G G, mult = op o )" 

589 
proof 

590 
show "magma ( carrier = hom G G, mult = op o )" 

591 
by rule (simp add: Pi_def hom_def) 

592 
next 

593 
show "semigroup_axioms ( carrier = hom G G, mult = op o )" 

594 
by rule (simp add: o_assoc) 

595 
qed 

596 

597 
lemma hom_mult: 

598 
"[ h \<in> hom G H; x \<in> carrier G; y \<in> carrier G ] 

599 
==> h (mult G x y) = mult H (h x) (h y)" 

600 
by (simp add: hom_def) 

601 

602 
lemma hom_closed: 

603 
"[ h \<in> hom G H; x \<in> carrier G ] ==> h x \<in> carrier H" 

604 
by (auto simp add: hom_def funcset_mem) 

605 

13943  606 
lemma compose_hom: 
607 
"[group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G > carrier G] 

608 
==> compose (carrier G) h h' \<in> hom G G" 

609 
apply (simp (no_asm_simp) add: hom_def) 

610 
apply (intro conjI) 

611 
apply (force simp add: funcset_compose hom_def) 

612 
apply (simp add: compose_def group.axioms hom_mult funcset_mem) 

613 
done 

614 

13813  615 
locale group_hom = group G + group H + var h + 
616 
assumes homh: "h \<in> hom G H" 

617 
notes hom_mult [simp] = hom_mult [OF homh] 

618 
and hom_closed [simp] = hom_closed [OF homh] 

619 

620 
lemma (in group_hom) one_closed [simp]: 

621 
"h \<one> \<in> carrier H" 

622 
by simp 

623 

624 
lemma (in group_hom) hom_one [simp]: 

625 
"h \<one> = \<one>\<^sub>2" 

626 
proof  

627 
have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>" 

628 
by (simp add: hom_mult [symmetric] del: hom_mult) 

629 
then show ?thesis by (simp del: r_one) 

630 
qed 

631 

632 
lemma (in group_hom) inv_closed [simp]: 

633 
"x \<in> carrier G ==> h (inv x) \<in> carrier H" 

634 
by simp 

635 

636 
lemma (in group_hom) hom_inv [simp]: 

637 
"x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)" 

638 
proof  

639 
assume x: "x \<in> carrier G" 

640 
then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2" 

641 
by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult) 

642 
also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" 

643 
by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult) 

644 
finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" . 

645 
with x show ?thesis by simp 

646 
qed 

647 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

648 
subsection {* Commutative Structures *} 
13936  649 

650 
text {* 

651 
Naming convention: multiplicative structures that are commutative 

652 
are called \emph{commutative}, additive structures are called 

653 
\emph{Abelian}. 

654 
*} 

13813  655 

656 
subsection {* Definition *} 

657 

13936  658 
locale comm_semigroup = semigroup + 
13813  659 
assumes m_comm: "[ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x" 
660 

13936  661 
lemma (in comm_semigroup) m_lcomm: 
13813  662 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 
663 
x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)" 

664 
proof  

665 
assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 

666 
from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc) 

667 
also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm) 

668 
also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc) 

669 
finally show ?thesis . 

670 
qed 

671 

13936  672 
lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm 
673 

674 
locale comm_monoid = comm_semigroup + monoid 

13813  675 

13936  676 
lemma comm_monoidI: 
677 
assumes m_closed: 

678 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y \<in> carrier G" 

679 
and one_closed: "one G \<in> carrier G" 

680 
and m_assoc: 

681 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

682 
mult G (mult G x y) z = mult G x (mult G y z)" 

683 
and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" 

684 
and m_comm: 

685 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y = mult G y x" 

686 
shows "comm_monoid G" 

687 
using l_one 

688 
by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro 

689 
comm_semigroup_axioms.intro monoid_axioms.intro 

690 
intro: prems simp: m_closed one_closed m_comm) 

13817  691 

13936  692 
lemma (in monoid) monoid_comm_monoidI: 
693 
assumes m_comm: 

694 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y = mult G y x" 

695 
shows "comm_monoid G" 

696 
by (rule comm_monoidI) (auto intro: m_assoc m_comm) 

697 
(* 

698 
lemma (in comm_monoid) r_one [simp]: 

13817  699 
"x \<in> carrier G ==> x \<otimes> \<one> = x" 
700 
proof  

701 
assume G: "x \<in> carrier G" 

702 
then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm) 

703 
also from G have "... = x" by simp 

704 
finally show ?thesis . 

705 
qed 

13936  706 
*) 
13817  707 

13936  708 
lemma (in comm_monoid) nat_pow_distr: 
709 
"[ x \<in> carrier G; y \<in> carrier G ] ==> 

710 
(x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n" 

711 
by (induct n) (simp, simp add: m_ac) 

712 

713 
locale comm_group = comm_monoid + group 

714 

715 
lemma (in group) group_comm_groupI: 

716 
assumes m_comm: "!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> 

717 
mult G x y = mult G y x" 

718 
shows "comm_group G" 

719 
by (fast intro: comm_group.intro comm_semigroup_axioms.intro 

720 
group.axioms prems) 

13817  721 

13936  722 
lemma comm_groupI: 
723 
assumes m_closed: 

724 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y \<in> carrier G" 

725 
and one_closed: "one G \<in> carrier G" 

726 
and m_assoc: 

727 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

728 
mult G (mult G x y) z = mult G x (mult G y z)" 

729 
and m_comm: 

730 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> mult G x y = mult G y x" 

731 
and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" 

732 
and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G" 

733 
shows "comm_group G" 

734 
by (fast intro: group.group_comm_groupI groupI prems) 

735 

736 
lemma (in comm_group) inv_mult: 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

737 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" 
13936  738 
by (simp add: m_ac inv_mult_group) 
13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

739 

13813  740 
end 