author  ballarin 
Wed, 10 Dec 2003 14:29:05 +0100  
changeset 14286  0ae66ffb9784 
parent 14254  342634f38451 
child 14551  2cb6ff394bfb 
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 

13936  13 
section {* From Magmas to Groups *} 
14 

13813  15 
text {* 
16 
Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with 

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

18 
together with a binary, closed operation. 

19 
*} 

20 

21 
subsection {* Definitions *} 

22 

14286
0ae66ffb9784
New structure "partial_object" as common root for lattices and magmas.
ballarin
parents:
14254
diff
changeset

23 
(* Object with a carrier set. *) 
0ae66ffb9784
New structure "partial_object" as common root for lattices and magmas.
ballarin
parents:
14254
diff
changeset

24 

0ae66ffb9784
New structure "partial_object" as common root for lattices and magmas.
ballarin
parents:
14254
diff
changeset

25 
record 'a partial_object = 
13813  26 
carrier :: "'a set" 
14286
0ae66ffb9784
New structure "partial_object" as common root for lattices and magmas.
ballarin
parents:
14254
diff
changeset

27 

0ae66ffb9784
New structure "partial_object" as common root for lattices and magmas.
ballarin
parents:
14254
diff
changeset

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

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

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

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

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

38 

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

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

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

42 

43 
consts 

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

45 

46 
defs (overloaded) 

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

48 
int_pow_def: "pow G a z == 

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

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

13813  51 

52 
locale magma = struct G + 

53 
assumes m_closed [intro, simp]: 

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

55 

56 
locale semigroup = magma + 

57 
assumes m_assoc: 

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

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

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

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

13936  66 
lemma monoidI: 
67 
assumes m_closed: 

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

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

70 
and m_assoc: 

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

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

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

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

75 
shows "monoid G" 

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

77 
semigroup.intro monoid_axioms.intro 

78 
intro: prems) 

79 

80 
lemma (in monoid) Units_closed [dest]: 

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

82 
by (unfold Units_def) fast 

83 

84 
lemma (in monoid) inv_unique: 

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

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

87 
shows "y = y'" 

88 
proof  

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

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

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

92 
finally show ?thesis . 

93 
qed 

94 

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

97 
by (unfold Units_def) auto 

98 

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

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

106 
lemma (in monoid) Units_l_inv: 

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

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

113 
lemma (in monoid) Units_r_inv: 

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

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

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

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

122 
proof  

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

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

125 
by (auto simp add: Units_def 

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

127 
qed 

128 

129 
lemma (in monoid) Units_l_cancel [simp]: 

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

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

132 
proof 

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

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

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

136 
by (simp add: m_assoc Units_closed) 

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

138 
next 

139 
assume eq: "y = z" 

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

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

142 
qed 

143 

144 
lemma (in monoid) Units_inv_inv [simp]: 

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

146 
proof  

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

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

149 
by (simp add: Units_l_inv Units_r_inv) 

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

151 
qed 

152 

153 
lemma (in monoid) inv_inj_on_Units: 

154 
"inj_on (m_inv G) (Units G)" 

155 
proof (rule inj_onI) 

156 
fix x y 

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

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

159 
with G show "x = y" by simp 

160 
qed 

161 

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

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

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

166 
proof  

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

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

169 
qed 

170 

13936  171 
text {* Power *} 
172 

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

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

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

176 

177 
lemma (in monoid) nat_pow_0 [simp]: 

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

179 
by (simp add: nat_pow_def) 

180 

181 
lemma (in monoid) nat_pow_Suc [simp]: 

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

183 
by (simp add: nat_pow_def) 

184 

185 
lemma (in monoid) nat_pow_one [simp]: 

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

187 
by (induct n) simp_all 

188 

189 
lemma (in monoid) nat_pow_mult: 

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

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

192 

193 
lemma (in monoid) nat_pow_pow: 

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

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

196 

197 
text {* 

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

199 
*} 

200 

201 
locale group = monoid + 

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

203 

204 
theorem groupI: 

205 
assumes m_closed [simp]: 

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

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

208 
and m_assoc: 

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

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

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

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

213 
shows "group G" 

214 
proof  

215 
have l_cancel [simp]: 

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

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

218 
proof 

219 
fix x y z 

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

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

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

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

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

225 
by (simp add: m_assoc) 

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

227 
next 

228 
fix x y z 

229 
assume eq: "y = z" 

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

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

232 
qed 

233 
have r_one: 

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

235 
proof  

236 
fix x 

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

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

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

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

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

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

243 
qed 

244 
have inv_ex: 

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

246 
mult G x y = one G" 

247 
proof  

248 
fix x 

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

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

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

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

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

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

255 
by simp 

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

257 
mult G x y = one G" 

258 
by (fast intro: l_inv r_inv) 

259 
qed 

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

261 
by (unfold Units_def) fast 

262 
show ?thesis 

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

264 
semigroup.intro monoid_axioms.intro group_axioms.intro 

265 
carrier_subset_Units intro: prems r_one) 

266 
qed 

267 

268 
lemma (in monoid) monoid_groupI: 

269 
assumes l_inv_ex: 

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

271 
shows "group G" 

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

273 

274 
lemma (in group) Units_eq [simp]: 

275 
"Units G = carrier G" 

276 
proof 

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

278 
next 

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

280 
qed 

281 

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

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

284 
using Units_inv_closed by simp 

285 

286 
lemma (in group) l_inv: 

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

288 
using Units_l_inv by simp 

13813  289 

290 
subsection {* Cancellation Laws and Basic Properties *} 

291 

292 
lemma (in group) l_cancel [simp]: 

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

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

13936  295 
using Units_l_inv by simp 
13940  296 

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

299 
proof  

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

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

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

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

304 
qed 

305 

306 
lemma (in group) r_cancel [simp]: 

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

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

309 
proof 

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

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

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

313 
by (simp add: m_assoc [symmetric]) 

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

315 
next 

316 
assume eq: "y = z" 

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

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

319 
qed 

320 

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

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

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

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

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

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

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

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

328 

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

13936  331 
using Units_inv_inv by simp 
332 

333 
lemma (in group) inv_inj: 

334 
"inj_on (m_inv G) (carrier G)" 

335 
using inv_inj_on_Units by simp 

13813  336 

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

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

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

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

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

343 
with G show ?thesis by simp 

344 
qed 

345 

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

348 
by (rule Units_inv_comm) auto 

349 

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

353 
apply (rule the_equality) 

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

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

356 
done 

357 

13936  358 
text {* Power *} 
359 

360 
lemma (in group) int_pow_def2: 

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

362 
by (simp add: int_pow_def nat_pow_def Let_def) 

363 

364 
lemma (in group) int_pow_0 [simp]: 

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

366 
by (simp add: int_pow_def2) 

367 

368 
lemma (in group) int_pow_one [simp]: 

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

370 
by (simp add: int_pow_def2) 

371 

13813  372 
subsection {* Substructures *} 
373 

374 
locale submagma = var H + struct G + 

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

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

377 

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

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

382 

383 
locale submagma = var H + struct G + 

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

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

386 
and m_closed [intro, simp]: 

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

388 
*) 

389 

390 
lemma submagma_imp_subset: 

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

392 
by (rule submagma.subset) 

393 

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

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

396 
using subset by blast 

397 

398 
lemma (in submagma) magmaI [intro]: 

399 
includes magma G 

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

401 
by rule simp 

402 

403 
lemma (in submagma) semigroup_axiomsI [intro]: 

404 
includes semigroup G 

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

406 
by rule (simp add: m_assoc) 

407 

408 
lemma (in submagma) semigroupI [intro]: 

409 
includes semigroup G 

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

411 
using prems by fast 

412 

413 
locale subgroup = submagma H G + 

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

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

416 

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

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

418 

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

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

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

422 
by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def) 
13813  423 

424 
lemma (in subgroup) groupI [intro]: 

425 
includes group G 

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

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

429 
text {* 

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

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

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

433 
*} 

434 

435 
lemma (in group) one_in_subset: 

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

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

438 
by (force simp add: l_inv) 

439 

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

441 

442 
lemma (in group) subgroupI: 

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

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

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

446 
shows "subgroup H G" 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

447 
proof (rule subgroup.intro) 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

448 
from subset and mult show "submagma H G" by (rule submagma.intro) 
13813  449 
next 
450 
have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems) 

451 
with inv show "subgroup_axioms H G" 

452 
by (intro subgroup_axioms.intro) simp_all 

453 
qed 

454 

455 
text {* 

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

457 
*} 

458 

459 
lemma (in subgroup) subset: 

460 
"H \<subseteq> carrier G" 

461 
.. 

462 

463 
lemma (in subgroup) m_closed: 

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

465 
.. 

466 

467 
declare magma.m_closed [simp] 

468 

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

13813  471 

472 
lemma subgroup_nonempty: 

473 
"~ subgroup {} G" 

474 
by (blast dest: subgroup.one_closed) 

475 

476 
lemma (in subgroup) finite_imp_card_positive: 

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

478 
proof (rule classical) 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

479 
have sub: "subgroup H G" using prems by (rule subgroup.intro) 
13813  480 
assume fin: "finite (carrier G)" 
481 
and zero: "~ 0 < card H" 

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

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

484 
with subgroup_nonempty show ?thesis by contradiction 

485 
qed 

486 

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

489 
"subgroup (Units G) G" 

490 
*) 

491 

13813  492 
subsection {* Direct Products *} 
493 

494 
constdefs 

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

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

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

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

501 

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

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

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

13813  508 

13817  509 
lemma DirProdSemigroup_magma: 
13813  510 
includes magma G + magma H 
13817  511 
shows "magma (G \<times>\<^sub>s H)" 
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

512 
by (rule magma.intro) (auto simp add: DirProdSemigroup_def) 
13813  513 

13817  514 
lemma DirProdSemigroup_semigroup_axioms: 
13813  515 
includes semigroup G + semigroup H 
13817  516 
shows "semigroup_axioms (G \<times>\<^sub>s H)" 
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

517 
by (rule semigroup_axioms.intro) 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

518 
(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)" 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

530 
by (rule magma.intro) 
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)" 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

536 
by (rule semigroup_axioms.intro) 
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 )" 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

589 
proof (rule semigroup.intro) 
13813  590 
show "magma ( carrier = hom G G, mult = op o )" 
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

591 
by (rule magma.intro) (simp add: Pi_def hom_def) 
13813  592 
next 
593 
show "semigroup_axioms ( carrier = hom G G, mult = op o )" 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13975
diff
changeset

594 
by (rule semigroup_axioms.intro) (simp add: o_assoc) 
13813  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 