src/HOL/Algebra/Group.thy
 author paulson Thu May 01 10:29:44 2003 +0200 (2003-05-01) changeset 13943 83d842ccd4aa parent 13940 c67798653056 child 13944 9b34607cd83e permissions -rw-r--r--
moving Bij.thy from GroupTheory to Algebra
1 (*
2   Title:  HOL/Algebra/Group.thy
3   Id:     $Id$
4   Author: Clemens Ballarin, started 4 February 2003
6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
7 *)
9 header {* Algebraic Structures up to Commutative Groups *}
11 theory Group = FuncSet:
13 axclass number < type
15 instance nat :: number ..
16 instance int :: number ..
18 section {* From Magmas to Groups *}
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 *}
26 subsection {* Definitions *}
28 record 'a semigroup =
29   carrier :: "'a set"
30   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
32 record 'a monoid = "'a semigroup" +
33   one :: 'a ("\<one>\<index>")
35 constdefs
36   m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _"  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)"
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)}"
44 consts
45   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
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)"
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"
57 locale semigroup = magma +
58   assumes m_assoc:
59     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
60     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
62 locale monoid = semigroup +
63   assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
64     and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
65     and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
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)
81 lemma (in monoid) Units_closed [dest]:
82   "x \<in> Units G ==> x \<in> carrier G"
83   by (unfold Units_def) fast
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
96 lemma (in monoid) Units_one_closed [intro, simp]:
97   "\<one> \<in> Units G"
98   by (unfold Units_def) auto
100 lemma (in monoid) Units_inv_closed [intro, simp]:
101   "x \<in> Units G ==> inv x \<in> carrier G"
102   apply (unfold Units_def m_inv_def, auto)
103   apply (rule theI2, fast)
104    apply (fast intro: inv_unique, fast)
105   done
107 lemma (in monoid) Units_l_inv:
108   "x \<in> Units G ==> inv x \<otimes> x = \<one>"
109   apply (unfold Units_def m_inv_def, auto)
110   apply (rule theI2, fast)
111    apply (fast intro: inv_unique, fast)
112   done
114 lemma (in monoid) Units_r_inv:
115   "x \<in> Units G ==> x \<otimes> inv x = \<one>"
116   apply (unfold Units_def m_inv_def, auto)
117   apply (rule theI2, fast)
118    apply (fast intro: inv_unique, fast)
119   done
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
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
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
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
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
172 text {* Power *}
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)
178 lemma (in monoid) nat_pow_0 [simp]:
179   "x (^) (0::nat) = \<one>"
180   by (simp add: nat_pow_def)
182 lemma (in monoid) nat_pow_Suc [simp]:
183   "x (^) (Suc n) = x (^) n \<otimes> x"
184   by (simp add: nat_pow_def)
186 lemma (in monoid) nat_pow_one [simp]:
187   "\<one> (^) (n::nat) = \<one>"
188   by (induct n) simp_all
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])
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)
198 text {*
199   A group is a monoid all of whose elements are invertible.
200 *}
202 locale group = monoid +
203   assumes Units: "carrier G <= Units G"
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
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)
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
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
287 lemma (in group) l_inv:
288   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
289   using Units_l_inv by simp
291 subsection {* Cancellation Laws and Basic Properties *}
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)"
296   using Units_l_inv by simp
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
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
322 lemma (in group) inv_one [simp]:
323   "inv \<one> = \<one>"
324 proof -
325   have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
326   moreover have "... = \<one>" by (simp add: r_inv)
327   finally show ?thesis .
328 qed
330 lemma (in group) inv_inv [simp]:
331   "x \<in> carrier G ==> inv (inv x) = x"
332   using Units_inv_inv by simp
334 lemma (in group) inv_inj:
335   "inj_on (m_inv G) (carrier G)"
336   using inv_inj_on_Units by simp
338 lemma (in group) inv_mult_group:
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
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
351 lemma (in group) m_inv_equality:
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
359 text {* Power *}
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)
365 lemma (in group) int_pow_0 [simp]:
366   "x (^) (0::int) = \<one>"
367   by (simp add: int_pow_def2)
369 lemma (in group) int_pow_one [simp]:
370   "\<one> (^) (z::int) = \<one>"
371   by (simp add: int_pow_def2)
373 subsection {* Substructures *}
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"
379 declare (in submagma) magma.intro [intro] semigroup.intro [intro]
380   semigroup_axioms.intro [intro]
381 (*
382 alternative definition of submagma
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 *)
391 lemma submagma_imp_subset:
392   "submagma H G ==> H \<subseteq> carrier G"
393   by (rule submagma.subset)
395 lemma (in submagma) subsetD [dest, simp]:
396   "x \<in> H ==> x \<in> carrier G"
397   using subset by blast
399 lemma (in submagma) magmaI [intro]:
400   includes magma G
401   shows "magma (G(| carrier := H |))"
402   by rule simp
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)
409 lemma (in submagma) semigroupI [intro]:
410   includes semigroup G
411   shows "semigroup (G(| carrier := H |))"
412   using prems by fast
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"
418 declare (in subgroup) group.intro [intro]
419 (*
420 lemma (in subgroup) l_oneI [intro]:
421   includes l_one G
422   shows "l_one (G(| carrier := H |))"
423   by rule simp_all
424 *)
425 lemma (in subgroup) group_axiomsI [intro]:
426   includes group G
427   shows "group_axioms (G(| carrier := H |))"
428   by rule (auto intro: l_inv r_inv simp add: Units_def)
430 lemma (in subgroup) groupI [intro]:
431   includes group G
432   shows "group (G(| carrier := H |))"
433   by (rule groupI) (auto intro: m_assoc l_inv)
435 text {*
436   Since @{term H} is nonempty, it contains some element @{term x}.  Since
437   it is closed under inverse, it contains @{text "inv x"}.  Since
438   it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
439 *}
441 lemma (in group) one_in_subset:
442   "[| 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 |]
443    ==> \<one> \<in> H"
444 by (force simp add: l_inv)
446 text {* A characterization of subgroups: closed, non-empty subset. *}
448 lemma (in group) subgroupI:
449   assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
450     and inv: "!!a. a \<in> H ==> inv a \<in> H"
451     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
452   shows "subgroup H G"
453 proof
454   from subset and mult show "submagma H G" ..
455 next
456   have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
457   with inv show "subgroup_axioms H G"
458     by (intro subgroup_axioms.intro) simp_all
459 qed
461 text {*
462   Repeat facts of submagmas for subgroups.  Necessary???
463 *}
465 lemma (in subgroup) subset:
466   "H \<subseteq> carrier G"
467   ..
469 lemma (in subgroup) m_closed:
470   "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
471   ..
473 declare magma.m_closed [simp]
475 declare monoid.one_closed [iff] group.inv_closed [simp]
476   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
478 lemma subgroup_nonempty:
479   "~ subgroup {} G"
480   by (blast dest: subgroup.one_closed)
482 lemma (in subgroup) finite_imp_card_positive:
483   "finite (carrier G) ==> 0 < card H"
484 proof (rule classical)
485   have sub: "subgroup H G" using prems ..
486   assume fin: "finite (carrier G)"
487     and zero: "~ 0 < card H"
488   then have "finite H" by (blast intro: finite_subset dest: subset)
489   with zero sub have "subgroup {} G" by simp
490   with subgroup_nonempty show ?thesis by contradiction
491 qed
493 (*
494 lemma (in monoid) Units_subgroup:
495   "subgroup (Units G) G"
496 *)
498 subsection {* Direct Products *}
500 constdefs
501   DirProdSemigroup ::
502     "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
503     => ('a \<times> 'b) semigroup"
504     (infixr "\<times>\<^sub>s" 80)
505   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
506     mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
508   DirProdGroup ::
509     "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
510     (infixr "\<times>\<^sub>g" 80)
511   "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
512     mult = mult (G \<times>\<^sub>s H),
513     one = (one G, one H) |)"
514 (*
515   DirProdGroup ::
516     "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
517     (infixr "\<times>\<^sub>g" 80)
518   "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
519     mult = mult (G \<times>\<^sub>m H),
520     one = one (G \<times>\<^sub>m H),
521     m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
522 *)
524 lemma DirProdSemigroup_magma:
525   includes magma G + magma H
526   shows "magma (G \<times>\<^sub>s H)"
527   by rule (auto simp add: DirProdSemigroup_def)
529 lemma DirProdSemigroup_semigroup_axioms:
530   includes semigroup G + semigroup H
531   shows "semigroup_axioms (G \<times>\<^sub>s H)"
532   by rule (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
534 lemma DirProdSemigroup_semigroup:
535   includes semigroup G + semigroup H
536   shows "semigroup (G \<times>\<^sub>s H)"
537   using prems
538   by (fast intro: semigroup.intro
539     DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
541 lemma DirProdGroup_magma:
542   includes magma G + magma H
543   shows "magma (G \<times>\<^sub>g H)"
544   by rule
545     (auto simp add: DirProdGroup_def DirProdSemigroup_def)
547 lemma DirProdGroup_semigroup_axioms:
548   includes semigroup G + semigroup H
549   shows "semigroup_axioms (G \<times>\<^sub>g H)"
550   by rule
551     (auto simp add: DirProdGroup_def DirProdSemigroup_def
552       G.m_assoc H.m_assoc)
554 lemma DirProdGroup_semigroup:
555   includes semigroup G + semigroup H
556   shows "semigroup (G \<times>\<^sub>g H)"
557   using prems
558   by (fast intro: semigroup.intro
559     DirProdGroup_magma DirProdGroup_semigroup_axioms)
561 (* ... and further lemmas for group ... *)
563 lemma DirProdGroup_group:
564   includes group G + group H
565   shows "group (G \<times>\<^sub>g H)"
566   by (rule groupI)
567     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
568       simp add: DirProdGroup_def DirProdSemigroup_def)
570 subsection {* Homomorphisms *}
572 constdefs
573   hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
574     => ('a => 'b)set"
575   "hom G H ==
576     {h. h \<in> carrier G -> carrier H &
577       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
579 lemma (in semigroup) hom:
580   includes semigroup G
581   shows "semigroup (| carrier = hom G G, mult = op o |)"
582 proof
583   show "magma (| carrier = hom G G, mult = op o |)"
584     by rule (simp add: Pi_def hom_def)
585 next
586   show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
587     by rule (simp add: o_assoc)
588 qed
590 lemma hom_mult:
591   "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
592    ==> h (mult G x y) = mult H (h x) (h y)"
593   by (simp add: hom_def)
595 lemma hom_closed:
596   "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
597   by (auto simp add: hom_def funcset_mem)
599 lemma compose_hom:
600      "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
601       ==> compose (carrier G) h h' \<in> hom G G"
602 apply (simp (no_asm_simp) add: hom_def)
603 apply (intro conjI)
604  apply (force simp add: funcset_compose hom_def)
605 apply (simp add: compose_def group.axioms hom_mult funcset_mem)
606 done
608 locale group_hom = group G + group H + var h +
609   assumes homh: "h \<in> hom G H"
610   notes hom_mult [simp] = hom_mult [OF homh]
611     and hom_closed [simp] = hom_closed [OF homh]
613 lemma (in group_hom) one_closed [simp]:
614   "h \<one> \<in> carrier H"
615   by simp
617 lemma (in group_hom) hom_one [simp]:
618   "h \<one> = \<one>\<^sub>2"
619 proof -
620   have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>"
621     by (simp add: hom_mult [symmetric] del: hom_mult)
622   then show ?thesis by (simp del: r_one)
623 qed
625 lemma (in group_hom) inv_closed [simp]:
626   "x \<in> carrier G ==> h (inv x) \<in> carrier H"
627   by simp
629 lemma (in group_hom) hom_inv [simp]:
630   "x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)"
631 proof -
632   assume x: "x \<in> carrier G"
633   then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2"
634     by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
635   also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)"
636     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
637   finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" .
638   with x show ?thesis by simp
639 qed
641 section {* Commutative Structures *}
643 text {*
644   Naming convention: multiplicative structures that are commutative
645   are called \emph{commutative}, additive structures are called
646   \emph{Abelian}.
647 *}
649 subsection {* Definition *}
651 locale comm_semigroup = semigroup +
652   assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
654 lemma (in comm_semigroup) m_lcomm:
655   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
656    x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
657 proof -
658   assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
659   from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
660   also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
661   also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
662   finally show ?thesis .
663 qed
665 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
667 locale comm_monoid = comm_semigroup + monoid
669 lemma comm_monoidI:
670   assumes m_closed:
671       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
672     and one_closed: "one G \<in> carrier G"
673     and m_assoc:
674       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
675       mult G (mult G x y) z = mult G x (mult G y z)"
676     and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
677     and m_comm:
678       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
679   shows "comm_monoid G"
680   using l_one
681   by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
682     comm_semigroup_axioms.intro monoid_axioms.intro
683     intro: prems simp: m_closed one_closed m_comm)
685 lemma (in monoid) monoid_comm_monoidI:
686   assumes m_comm:
687       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
688   shows "comm_monoid G"
689   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
690 (*
691 lemma (in comm_monoid) r_one [simp]:
692   "x \<in> carrier G ==> x \<otimes> \<one> = x"
693 proof -
694   assume G: "x \<in> carrier G"
695   then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
696   also from G have "... = x" by simp
697   finally show ?thesis .
698 qed
699 *)
701 lemma (in comm_monoid) nat_pow_distr:
702   "[| x \<in> carrier G; y \<in> carrier G |] ==>
703   (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
704   by (induct n) (simp, simp add: m_ac)
706 locale comm_group = comm_monoid + group
708 lemma (in group) group_comm_groupI:
709   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
710       mult G x y = mult G y x"
711   shows "comm_group G"
712   by (fast intro: comm_group.intro comm_semigroup_axioms.intro
713     group.axioms prems)
715 lemma comm_groupI:
716   assumes m_closed:
717       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
718     and one_closed: "one G \<in> carrier G"
719     and m_assoc:
720       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
721       mult G (mult G x y) z = mult G x (mult G y z)"
722     and m_comm:
723       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
724     and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
725     and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
726   shows "comm_group G"
727   by (fast intro: group.group_comm_groupI groupI prems)
729 lemma (in comm_group) inv_mult:
730   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
731   by (simp add: m_ac inv_mult_group)
733 end