author  ballarin 
Thu, 27 Feb 2003 15:12:29 +0100  
changeset 13835  12b2ffbe543a 
parent 13817  7e031a968443 
child 13854  91c9ab25fece 
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 

9 
header {* Algebraic Structures up to Abelian Groups *} 

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 

13 
text {* 

14 
Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with 

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

16 
together with a binary, closed operation. 

17 
*} 

18 

19 
section {* From Magmas to Groups *} 

20 

21 
subsection {* Definitions *} 

22 

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

23 
(* The following may be unnecessary. *) 
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13817
diff
changeset

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

25 
We write groups additively. This simplifies notation for rings. 
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13817
diff
changeset

26 
All rings have an additive inverse, only fields have a 
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13817
diff
changeset

27 
multiplicative one. This definitions reduces the need for 
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13817
diff
changeset

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

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

30 

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

34 

13817  35 
record 'a monoid = "'a semigroup" + 
13813  36 
one :: 'a ("\<one>\<index>") 
13817  37 

38 
record 'a group = "'a monoid" + 

13813  39 
m_inv :: "'a => 'a" ("inv\<index> _" [81] 80) 
40 

41 
locale magma = struct G + 

42 
assumes m_closed [intro, simp]: 

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

44 

45 
locale semigroup = magma + 

46 
assumes m_assoc: 

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

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

49 

13817  50 
locale l_one = struct G + 
13813  51 
assumes one_closed [intro, simp]: "\<one> \<in> carrier G" 
52 
and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x" 

13817  53 

54 
locale group = semigroup + l_one + 

55 
assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G" 

13813  56 
and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>" 
57 

58 
subsection {* Cancellation Laws and Basic Properties *} 

59 

60 
lemma (in group) l_cancel [simp]: 

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

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

63 
proof 

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

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

66 
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc) 

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

68 
next 

69 
assume eq: "y = z" 

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

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

72 
qed 

73 

74 
lemma (in group) r_one [simp]: 

75 
"x \<in> carrier G ==> x \<otimes> \<one> = x" 

76 
proof  

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

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

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

80 
with x show ?thesis by simp 

81 
qed 

82 

83 
lemma (in group) r_inv: 

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

85 
proof  

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

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

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

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

90 
qed 

91 

92 
lemma (in group) r_cancel [simp]: 

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

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

95 
proof 

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

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

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

99 
by (simp add: m_assoc [symmetric]) 

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

101 
next 

102 
assume eq: "y = z" 

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

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

105 
qed 

106 

107 
lemma (in group) inv_inv [simp]: 

108 
"x \<in> carrier G ==> inv (inv x) = x" 

109 
proof  

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

111 
then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv) 

112 
with x show ?thesis by simp 

113 
qed 

114 

115 
lemma (in group) inv_mult: 

116 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" 

117 
proof  

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

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

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

121 
with G show ?thesis by simp 

122 
qed 

123 

124 
subsection {* Substructures *} 

125 

126 
locale submagma = var H + struct G + 

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

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

129 

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

131 

132 
(* 

133 
alternative definition of submagma 

134 

135 
locale submagma = var H + struct G + 

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

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

138 
and m_closed [intro, simp]: 

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

140 
*) 

141 

142 
lemma submagma_imp_subset: 

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

144 
by (rule submagma.subset) 

145 

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

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

148 
using subset by blast 

149 

150 
lemma (in submagma) magmaI [intro]: 

151 
includes magma G 

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

153 
by rule simp 

154 

155 
lemma (in submagma) semigroup_axiomsI [intro]: 

156 
includes semigroup G 

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

158 
by rule (simp add: m_assoc) 

159 

160 
lemma (in submagma) semigroupI [intro]: 

161 
includes semigroup G 

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

163 
using prems by fast 

164 

165 
locale subgroup = submagma H G + 

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

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

168 

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

170 

13817  171 
lemma (in subgroup) l_oneI [intro]: 
172 
includes l_one G 

173 
shows "l_one (G( carrier := H ))" 

174 
by rule simp_all 

175 

13813  176 
lemma (in subgroup) group_axiomsI [intro]: 
177 
includes group G 

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

179 
by rule (simp_all add: l_inv) 

180 

181 
lemma (in subgroup) groupI [intro]: 

182 
includes group G 

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

184 
using prems by fast 

185 

186 
text {* 

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

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

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

190 
*} 

191 

192 
lemma (in group) one_in_subset: 

193 
"[ 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 ] 

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

195 
by (force simp add: l_inv) 

196 

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

198 

199 
lemma (in group) subgroupI: 

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

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

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

203 
shows "subgroup H G" 

204 
proof 

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

206 
next 

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

208 
with inv show "subgroup_axioms H G" 

209 
by (intro subgroup_axioms.intro) simp_all 

210 
qed 

211 

212 
text {* 

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

214 
*} 

215 

216 
lemma (in subgroup) subset: 

217 
"H \<subseteq> carrier G" 

218 
.. 

219 

220 
lemma (in subgroup) m_closed: 

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

222 
.. 

223 

224 
declare magma.m_closed [simp] 

225 

13817  226 
declare l_one.one_closed [iff] group.inv_closed [simp] 
227 
l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp] 

13813  228 

229 
lemma subgroup_nonempty: 

230 
"~ subgroup {} G" 

231 
by (blast dest: subgroup.one_closed) 

232 

233 
lemma (in subgroup) finite_imp_card_positive: 

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

235 
proof (rule classical) 

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

237 
assume fin: "finite (carrier G)" 

238 
and zero: "~ 0 < card H" 

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

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

241 
with subgroup_nonempty show ?thesis by contradiction 

242 
qed 

243 

244 
subsection {* Direct Products *} 

245 

246 
constdefs 

13817  247 
DirProdSemigroup :: 
248 
"[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme] 

249 
=> ('a \<times> 'b) semigroup" 

250 
(infixr "\<times>\<^sub>s" 80) 

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

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

253 

254 
DirProdMonoid :: 

255 
"[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid" 

13813  256 
(infixr "\<times>\<^sub>m" 80) 
13817  257 
"G \<times>\<^sub>m H == ( carrier = carrier (G \<times>\<^sub>s H), 
258 
mult = mult (G \<times>\<^sub>s H), 

259 
one = (one G, one H) )" 

13813  260 

261 
DirProdGroup :: 

262 
"[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group" 

263 
(infixr "\<times>\<^sub>g" 80) 

264 
"G \<times>\<^sub>g H == ( carrier = carrier (G \<times>\<^sub>m H), 

265 
mult = mult (G \<times>\<^sub>m H), 

13817  266 
one = one (G \<times>\<^sub>m H), 
13813  267 
m_inv = (%(g, h). (m_inv G g, m_inv H h)) )" 
268 

13817  269 
lemma DirProdSemigroup_magma: 
13813  270 
includes magma G + magma H 
13817  271 
shows "magma (G \<times>\<^sub>s H)" 
272 
by rule (auto simp add: DirProdSemigroup_def) 

13813  273 

13817  274 
lemma DirProdSemigroup_semigroup_axioms: 
13813  275 
includes semigroup G + semigroup H 
13817  276 
shows "semigroup_axioms (G \<times>\<^sub>s H)" 
277 
by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc) 

13813  278 

13817  279 
lemma DirProdSemigroup_semigroup: 
13813  280 
includes semigroup G + semigroup H 
13817  281 
shows "semigroup (G \<times>\<^sub>s H)" 
13813  282 
using prems 
283 
by (fast intro: semigroup.intro 

13817  284 
DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms) 
13813  285 

286 
lemma DirProdGroup_magma: 

287 
includes magma G + magma H 

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

13817  289 
by rule 
290 
(auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def) 

13813  291 

292 
lemma DirProdGroup_semigroup_axioms: 

293 
includes semigroup G + semigroup H 

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

295 
by rule 

13817  296 
(auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def 
297 
G.m_assoc H.m_assoc) 

13813  298 

299 
lemma DirProdGroup_semigroup: 

300 
includes semigroup G + semigroup H 

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

302 
using prems 

303 
by (fast intro: semigroup.intro 

304 
DirProdGroup_magma DirProdGroup_semigroup_axioms) 

305 

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

307 

13817  308 
lemma DirProdGroup_group: 
13813  309 
includes group G + group H 
310 
shows "group (G \<times>\<^sub>g H)" 

311 
by rule 

13817  312 
(auto intro: magma.intro l_one.intro 
313 
semigroup_axioms.intro group_axioms.intro 

314 
simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def 

13813  315 
G.m_assoc H.m_assoc G.l_inv H.l_inv) 
316 

317 
subsection {* Homomorphisms *} 

318 

319 
constdefs 

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

13813  322 
"hom G H == 
323 
{h. h \<in> carrier G > carrier H & 

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

325 

326 
lemma (in semigroup) hom: 

327 
includes semigroup G 

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

329 
proof 

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

331 
by rule (simp add: Pi_def hom_def) 

332 
next 

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

334 
by rule (simp add: o_assoc) 

335 
qed 

336 

337 
lemma hom_mult: 

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

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

340 
by (simp add: hom_def) 

341 

342 
lemma hom_closed: 

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

344 
by (auto simp add: hom_def funcset_mem) 

345 

346 
locale group_hom = group G + group H + var h + 

347 
assumes homh: "h \<in> hom G H" 

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

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

350 

351 
lemma (in group_hom) one_closed [simp]: 

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

353 
by simp 

354 

355 
lemma (in group_hom) hom_one [simp]: 

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

357 
proof  

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

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

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

361 
qed 

362 

363 
lemma (in group_hom) inv_closed [simp]: 

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

365 
by simp 

366 

367 
lemma (in group_hom) hom_inv [simp]: 

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

369 
proof  

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

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

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

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

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

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

376 
with x show ?thesis by simp 

377 
qed 

378 

379 
section {* Abelian Structures *} 

380 

381 
subsection {* Definition *} 

382 

383 
locale abelian_semigroup = semigroup + 

384 
assumes m_comm: "[ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x" 

385 

386 
lemma (in abelian_semigroup) m_lcomm: 

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

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

389 
proof  

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

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

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

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

394 
finally show ?thesis . 

395 
qed 

396 

397 
lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm 

398 

13817  399 
locale abelian_monoid = abelian_semigroup + l_one 
400 

401 
lemma (in abelian_monoid) l_one [simp]: 

402 
"x \<in> carrier G ==> x \<otimes> \<one> = x" 

403 
proof  

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

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

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

407 
finally show ?thesis . 

408 
qed 

409 

410 
locale abelian_group = abelian_monoid + group 

411 

13813  412 
end 