src/HOL/Algebra/Coset.thy
 author wenzelm Thu Mar 26 20:08:55 2009 +0100 (2009-03-26) changeset 30729 461ee3e49ad3 parent 30198 922f944f03b2 child 31727 2621a957d417 permissions -rw-r--r--
interpretation/interpret: prefixes are mandatory by default;
1 (*  Title:      HOL/Algebra/Coset.thy
2     Author:     Florian Kammueller, with new proofs by L C Paulson, and
3                 Stephan Hohe
4 *)
6 theory Coset imports Group begin
9 section {*Cosets and Quotient Groups*}
11 constdefs (structure G)
12   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
13   "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
15   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
16   "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
18   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _"  80)
19   "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
21   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
22   "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
24   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _"  80)
25   "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
28 locale normal = subgroup + group +
29   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
31 abbreviation
32   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
33   "H \<lhd> G \<equiv> normal H G"
36 subsection {*Basic Properties of Cosets*}
38 lemma (in group) coset_mult_assoc:
39      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
40       ==> (M #> g) #> h = M #> (g \<otimes> h)"
41 by (force simp add: r_coset_def m_assoc)
43 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
44 by (force simp add: r_coset_def)
46 lemma (in group) coset_mult_inv1:
47      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
48          M \<subseteq> carrier G |] ==> M #> x = M #> y"
49 apply (erule subst [of concl: "%z. M #> x = z #> y"])
50 apply (simp add: coset_mult_assoc m_assoc)
51 done
53 lemma (in group) coset_mult_inv2:
54      "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
55       ==> M #> (x \<otimes> (inv y)) = M "
56 apply (simp add: coset_mult_assoc [symmetric])
57 apply (simp add: coset_mult_assoc)
58 done
60 lemma (in group) coset_join1:
61      "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
62 apply (erule subst)
63 apply (simp add: r_coset_def)
64 apply (blast intro: l_one subgroup.one_closed sym)
65 done
67 lemma (in group) solve_equation:
68     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
69 apply (rule bexI [of _ "y \<otimes> (inv x)"])
70 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
71                       subgroup.subset [THEN subsetD])
72 done
74 lemma (in group) repr_independence:
75      "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
76 by (auto simp add: r_coset_def m_assoc [symmetric]
77                    subgroup.subset [THEN subsetD]
78                    subgroup.m_closed solve_equation)
80 lemma (in group) coset_join2:
81      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
82   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
83 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
85 lemma (in monoid) r_coset_subset_G:
86      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
87 by (auto simp add: r_coset_def)
89 lemma (in group) rcosI:
90      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
91 by (auto simp add: r_coset_def)
93 lemma (in group) rcosetsI:
94      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
95 by (auto simp add: RCOSETS_def)
97 text{*Really needed?*}
98 lemma (in group) transpose_inv:
99      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
100       ==> (inv x) \<otimes> z = y"
101 by (force simp add: m_assoc [symmetric])
103 lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
104 apply (simp add: r_coset_def)
105 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
106                     subgroup.one_closed)
107 done
109 text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
110 lemma (in group) repr_independenceD:
111   assumes "subgroup H G"
112   assumes ycarr: "y \<in> carrier G"
113       and repr:  "H #> x = H #> y"
114   shows "y \<in> H #> x"
115 proof -
116   interpret subgroup H G by fact
117   show ?thesis  apply (subst repr)
118   apply (intro rcos_self)
119    apply (rule ycarr)
120    apply (rule is_subgroup)
121   done
122 qed
124 text {* Elements of a right coset are in the carrier *}
125 lemma (in subgroup) elemrcos_carrier:
126   assumes "group G"
127   assumes acarr: "a \<in> carrier G"
128     and a': "a' \<in> H #> a"
129   shows "a' \<in> carrier G"
130 proof -
131   interpret group G by fact
132   from subset and acarr
133   have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G)
134   from this and a'
135   show "a' \<in> carrier G"
136     by fast
137 qed
139 lemma (in subgroup) rcos_const:
140   assumes "group G"
141   assumes hH: "h \<in> H"
142   shows "H #> h = H"
143 proof -
144   interpret group G by fact
145   show ?thesis apply (unfold r_coset_def)
146     apply rule
147     apply rule
148     apply clarsimp
149     apply (intro subgroup.m_closed)
150     apply (rule is_subgroup)
151     apply assumption
152     apply (rule hH)
153     apply rule
154     apply simp
155   proof -
156     fix h'
157     assume h'H: "h' \<in> H"
158     note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier]
159     from carr
160     have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc)
161     from h'H hH
162     have "h' \<otimes> inv h \<in> H" by simp
163     from this and a
164     show "\<exists>x\<in>H. h' = x \<otimes> h" by fast
165   qed
166 qed
168 text {* Step one for lemma @{text "rcos_module"} *}
169 lemma (in subgroup) rcos_module_imp:
170   assumes "group G"
171   assumes xcarr: "x \<in> carrier G"
172       and x'cos: "x' \<in> H #> x"
173   shows "(x' \<otimes> inv x) \<in> H"
174 proof -
175   interpret group G by fact
176   from xcarr x'cos
177       have x'carr: "x' \<in> carrier G"
178       by (rule elemrcos_carrier[OF is_group])
179   from xcarr
180       have ixcarr: "inv x \<in> carrier G"
181       by simp
182   from x'cos
183       have "\<exists>h\<in>H. x' = h \<otimes> x"
184       unfolding r_coset_def
185       by fast
186   from this
187       obtain h
188         where hH: "h \<in> H"
189         and x': "x' = h \<otimes> x"
190       by auto
191   from hH and subset
192       have hcarr: "h \<in> carrier G" by fast
193   note carr = xcarr x'carr hcarr
194   from x' and carr
195       have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast
196   also from carr
197       have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc)
198   also from carr
199       have "\<dots> = h \<otimes> \<one>" by simp
200   also from carr
201       have "\<dots> = h" by simp
202   finally
203       have "x' \<otimes> (inv x) = h" by simp
204   from hH this
205       show "x' \<otimes> (inv x) \<in> H" by simp
206 qed
208 text {* Step two for lemma @{text "rcos_module"} *}
209 lemma (in subgroup) rcos_module_rev:
210   assumes "group G"
211   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
212       and xixH: "(x' \<otimes> inv x) \<in> H"
213   shows "x' \<in> H #> x"
214 proof -
215   interpret group G by fact
216   from xixH
217       have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast
218   from this
219       obtain h
220         where hH: "h \<in> H"
221         and hsym: "x' \<otimes> (inv x) = h"
222       by fast
223   from hH subset have hcarr: "h \<in> carrier G" by simp
224   note carr = carr hcarr
225   from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast
226   also from carr
227       have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
228   also from carr
229       have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
230   also from carr
231       have "\<dots> = x'" by simp
232   finally
233       have "h \<otimes> x = x'" by simp
234   from this[symmetric] and hH
235       show "x' \<in> H #> x"
236       unfolding r_coset_def
237       by fast
238 qed
240 text {* Module property of right cosets *}
241 lemma (in subgroup) rcos_module:
242   assumes "group G"
243   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
244   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
245 proof -
246   interpret group G by fact
247   show ?thesis proof  assume "x' \<in> H #> x"
248     from this and carr
249     show "x' \<otimes> inv x \<in> H"
250       by (intro rcos_module_imp[OF is_group])
251   next
252     assume "x' \<otimes> inv x \<in> H"
253     from this and carr
254     show "x' \<in> H #> x"
255       by (intro rcos_module_rev[OF is_group])
256   qed
257 qed
259 text {* Right cosets are subsets of the carrier. *}
260 lemma (in subgroup) rcosets_carrier:
261   assumes "group G"
262   assumes XH: "X \<in> rcosets H"
263   shows "X \<subseteq> carrier G"
264 proof -
265   interpret group G by fact
266   from XH have "\<exists>x\<in> carrier G. X = H #> x"
267       unfolding RCOSETS_def
268       by fast
269   from this
270       obtain x
271         where xcarr: "x\<in> carrier G"
272         and X: "X = H #> x"
273       by fast
274   from subset and xcarr
275       show "X \<subseteq> carrier G"
276       unfolding X
277       by (rule r_coset_subset_G)
278 qed
280 text {* Multiplication of general subsets *}
281 lemma (in monoid) set_mult_closed:
282   assumes Acarr: "A \<subseteq> carrier G"
283       and Bcarr: "B \<subseteq> carrier G"
284   shows "A <#> B \<subseteq> carrier G"
285 apply rule apply (simp add: set_mult_def, clarsimp)
286 proof -
287   fix a b
288   assume "a \<in> A"
289   from this and Acarr
290       have acarr: "a \<in> carrier G" by fast
292   assume "b \<in> B"
293   from this and Bcarr
294       have bcarr: "b \<in> carrier G" by fast
296   from acarr bcarr
297       show "a \<otimes> b \<in> carrier G" by (rule m_closed)
298 qed
300 lemma (in comm_group) mult_subgroups:
301   assumes subH: "subgroup H G"
302       and subK: "subgroup K G"
303   shows "subgroup (H <#> K) G"
304 apply (rule subgroup.intro)
305    apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK])
306   apply (simp add: set_mult_def) apply clarsimp defer 1
307   apply (simp add: set_mult_def) defer 1
308   apply (simp add: set_mult_def, clarsimp) defer 1
309 proof -
310   fix ha hb ka kb
311   assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K"
312   note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]]
313               kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]]
314   from carr
315       have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc)
316   also from carr
317       have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm)
318   also from carr
319       have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc)
320   finally
321       have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" .
323   from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH])
324   from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK])
326   from hH and kK and eq
327       show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast
328 next
329   have "\<one> = \<one> \<otimes> \<one>" by simp
330   from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this
331       show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast
332 next
333   fix h k
334   assume hH: "h \<in> H"
335      and kK: "k \<in> K"
337   from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]]
338       have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm)
340   from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this
341       show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast
342 qed
344 lemma (in subgroup) lcos_module_rev:
345   assumes "group G"
346   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
347       and xixH: "(inv x \<otimes> x') \<in> H"
348   shows "x' \<in> x <# H"
349 proof -
350   interpret group G by fact
351   from xixH
352       have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast
353   from this
354       obtain h
355         where hH: "h \<in> H"
356         and hsym: "(inv x) \<otimes> x' = h"
357       by fast
359   from hH subset have hcarr: "h \<in> carrier G" by simp
360   note carr = carr hcarr
361   from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast
362   also from carr
363       have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric])
364   also from carr
365       have "\<dots> = \<one> \<otimes> x'" by simp
366   also from carr
367       have "\<dots> = x'" by simp
368   finally
369       have "x \<otimes> h = x'" by simp
371   from this[symmetric] and hH
372       show "x' \<in> x <# H"
373       unfolding l_coset_def
374       by fast
375 qed
378 subsection {* Normal subgroups *}
380 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
381   by (simp add: normal_def subgroup_def)
383 lemma (in group) normalI:
384   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
385   by (simp add: normal_def normal_axioms_def prems)
387 lemma (in normal) inv_op_closed1:
388      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
389 apply (insert coset_eq)
390 apply (auto simp add: l_coset_def r_coset_def)
391 apply (drule bspec, assumption)
392 apply (drule equalityD1 [THEN subsetD], blast, clarify)
393 apply (simp add: m_assoc)
394 apply (simp add: m_assoc [symmetric])
395 done
397 lemma (in normal) inv_op_closed2:
398      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
399 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
400 apply (simp add: )
401 apply (blast intro: inv_op_closed1)
402 done
404 text{*Alternative characterization of normal subgroups*}
405 lemma (in group) normal_inv_iff:
406      "(N \<lhd> G) =
407       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
408       (is "_ = ?rhs")
409 proof
410   assume N: "N \<lhd> G"
411   show ?rhs
412     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
413 next
414   assume ?rhs
415   hence sg: "subgroup N G"
416     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
417   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
418   show "N \<lhd> G"
419   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
420     fix x
421     assume x: "x \<in> carrier G"
422     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
423     proof
424       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
425       proof clarify
426         fix n
427         assume n: "n \<in> N"
428         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
429         proof
430           from closed [of "inv x"]
431           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
432           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
433             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
434         qed
435       qed
436     next
437       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
438       proof clarify
439         fix n
440         assume n: "n \<in> N"
441         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
442         proof
443           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
444           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
445             by (simp add: x n m_assoc sb [THEN subsetD])
446         qed
447       qed
448     qed
449   qed
450 qed
453 subsection{*More Properties of Cosets*}
455 lemma (in group) lcos_m_assoc:
456      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
457       ==> g <# (h <# M) = (g \<otimes> h) <# M"
458 by (force simp add: l_coset_def m_assoc)
460 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
461 by (force simp add: l_coset_def)
463 lemma (in group) l_coset_subset_G:
464      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
465 by (auto simp add: l_coset_def subsetD)
467 lemma (in group) l_coset_swap:
468      "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
469 proof (simp add: l_coset_def)
470   assume "\<exists>h\<in>H. y = x \<otimes> h"
471     and x: "x \<in> carrier G"
472     and sb: "subgroup H G"
473   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
474   show "\<exists>h\<in>H. x = y \<otimes> h"
475   proof
476     show "x = y \<otimes> inv h'" using h' x sb
477       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
478     show "inv h' \<in> H" using h' sb
479       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
480   qed
481 qed
483 lemma (in group) l_coset_carrier:
484      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
485 by (auto simp add: l_coset_def m_assoc
486                    subgroup.subset [THEN subsetD] subgroup.m_closed)
488 lemma (in group) l_repr_imp_subset:
489   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
490   shows "y <# H \<subseteq> x <# H"
491 proof -
492   from y
493   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
494   thus ?thesis using x sb
495     by (auto simp add: l_coset_def m_assoc
496                        subgroup.subset [THEN subsetD] subgroup.m_closed)
497 qed
499 lemma (in group) l_repr_independence:
500   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
501   shows "x <# H = y <# H"
502 proof
503   show "x <# H \<subseteq> y <# H"
504     by (rule l_repr_imp_subset,
505         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
506   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
507 qed
509 lemma (in group) setmult_subset_G:
510      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
511 by (auto simp add: set_mult_def subsetD)
513 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
514 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
515 apply (rule_tac x = x in bexI)
516 apply (rule bexI [of _ "\<one>"])
517 apply (auto simp add: subgroup.m_closed subgroup.one_closed
518                       r_one subgroup.subset [THEN subsetD])
519 done
522 subsubsection {* Set of Inverses of an @{text r_coset}. *}
524 lemma (in normal) rcos_inv:
525   assumes x:     "x \<in> carrier G"
526   shows "set_inv (H #> x) = H #> (inv x)"
527 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
528   fix h
529   assume "h \<in> H"
530   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
531   proof
532     show "inv x \<otimes> inv h \<otimes> x \<in> H"
533       by (simp add: inv_op_closed1 prems)
534     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
535       by (simp add: prems m_assoc)
536   qed
537 next
538   fix h
539   assume "h \<in> H"
540   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
541   proof
542     show "x \<otimes> inv h \<otimes> inv x \<in> H"
543       by (simp add: inv_op_closed2 prems)
544     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
545       by (simp add: prems m_assoc [symmetric] inv_mult_group)
546   qed
547 qed
550 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
552 lemma (in group) setmult_rcos_assoc:
553      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
554       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
555 by (force simp add: r_coset_def set_mult_def m_assoc)
557 lemma (in group) rcos_assoc_lcos:
558      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
559       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
560 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
562 lemma (in normal) rcos_mult_step1:
563      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
564       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
565 by (simp add: setmult_rcos_assoc subset
566               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
568 lemma (in normal) rcos_mult_step2:
569      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
570       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
571 by (insert coset_eq, simp add: normal_def)
573 lemma (in normal) rcos_mult_step3:
574      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
575       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
576 by (simp add: setmult_rcos_assoc coset_mult_assoc
577               subgroup_mult_id normal.axioms subset prems)
579 lemma (in normal) rcos_sum:
580      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
581       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
582 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
584 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
585   -- {* generalizes @{text subgroup_mult_id} *}
586   by (auto simp add: RCOSETS_def subset
587         setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
590 subsubsection{*An Equivalence Relation*}
592 constdefs (structure G)
593   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
594                   ("rcong\<index> _")
595    "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
598 lemma (in subgroup) equiv_rcong:
599    assumes "group G"
600    shows "equiv (carrier G) (rcong H)"
601 proof -
602   interpret group G by fact
603   show ?thesis
604   proof (intro equiv.intro)
605     show "refl_on (carrier G) (rcong H)"
606       by (auto simp add: r_congruent_def refl_on_def)
607   next
608     show "sym (rcong H)"
609     proof (simp add: r_congruent_def sym_def, clarify)
610       fix x y
611       assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
612 	 and "inv x \<otimes> y \<in> H"
613       hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
614       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
615     qed
616   next
617     show "trans (rcong H)"
618     proof (simp add: r_congruent_def trans_def, clarify)
619       fix x y z
620       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
621 	 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
622       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
623       hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
624 	by (simp add: m_assoc del: r_inv Units_r_inv)
625       thus "inv x \<otimes> z \<in> H" by simp
626     qed
627   qed
628 qed
630 text{*Equivalence classes of @{text rcong} correspond to left cosets.
631   Was there a mistake in the definitions? I'd have expected them to
632   correspond to right cosets.*}
634 (* CB: This is correct, but subtle.
635    We call H #> a the right coset of a relative to H.  According to
636    Jacobson, this is what the majority of group theory literature does.
637    He then defines the notion of congruence relation ~ over monoids as
638    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
639    Our notion of right congruence induced by K: rcong K appears only in
640    the context where K is a normal subgroup.  Jacobson doesn't name it.
641    But in this context left and right cosets are identical.
642 *)
644 lemma (in subgroup) l_coset_eq_rcong:
645   assumes "group G"
646   assumes a: "a \<in> carrier G"
647   shows "a <# H = rcong H `` {a}"
648 proof -
649   interpret group G by fact
650   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
651 qed
653 subsubsection{*Two Distinct Right Cosets are Disjoint*}
655 lemma (in group) rcos_equation:
656   assumes "subgroup H G"
657   assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
658   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
659 proof -
660   interpret subgroup H G by fact
661   from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
662     apply (simp add: )
663     apply (simp add: m_assoc transpose_inv)
664     done
665 qed
667 lemma (in group) rcos_disjoint:
668   assumes "subgroup H G"
669   assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
670   shows "a \<inter> b = {}"
671 proof -
672   interpret subgroup H G by fact
673   from p show ?thesis apply (simp add: RCOSETS_def r_coset_def)
674     apply (blast intro: rcos_equation prems sym)
675     done
676 qed
678 subsection {* Further lemmas for @{text "r_congruent"} *}
680 text {* The relation is a congruence *}
682 lemma (in normal) congruent_rcong:
683   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
684 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
685   fix a b c
686   assume abrcong: "(a, b) \<in> rcong H"
687     and ccarr: "c \<in> carrier G"
689   from abrcong
690       have acarr: "a \<in> carrier G"
691         and bcarr: "b \<in> carrier G"
692         and abH: "inv a \<otimes> b \<in> H"
693       unfolding r_congruent_def
694       by fast+
696   note carr = acarr bcarr ccarr
698   from ccarr and abH
699       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
700   moreover
701       from carr and inv_closed
702       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)"
703       by (force cong: m_assoc)
704   moreover
705       from carr and inv_closed
706       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
707       by (simp add: inv_mult_group)
708   ultimately
709       have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
710   from carr and this
711      have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
712      by (simp add: lcos_module_rev[OF is_group])
713   from carr and this and is_subgroup
714      show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
715 next
716   fix a b c
717   assume abrcong: "(a, b) \<in> rcong H"
718     and ccarr: "c \<in> carrier G"
720   from ccarr have "c \<in> Units G" by (simp add: Units_eq)
721   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
723   from abrcong
724       have acarr: "a \<in> carrier G"
725        and bcarr: "b \<in> carrier G"
726        and abH: "inv a \<otimes> b \<in> H"
727       by (unfold r_congruent_def, fast+)
729   note carr = acarr bcarr ccarr
731   from carr and inv_closed
732      have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
733   also from carr and inv_closed
734       have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
735   also from carr and inv_closed
736       have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
737   also from carr and inv_closed
738       have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
739   finally
740       have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
741   from abH and this
742       have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
744   from carr and this
745      have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
746      by (simp add: lcos_module_rev[OF is_group])
747   from carr and this and is_subgroup
748      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
749 qed
752 subsection {*Order of a Group and Lagrange's Theorem*}
754 constdefs
755   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
756   "order S \<equiv> card (carrier S)"
758 lemma (in group) rcosets_part_G:
759   assumes "subgroup H G"
760   shows "\<Union>(rcosets H) = carrier G"
761 proof -
762   interpret subgroup H G by fact
763   show ?thesis
764     apply (rule equalityI)
765     apply (force simp add: RCOSETS_def r_coset_def)
766     apply (auto simp add: RCOSETS_def intro: rcos_self prems)
767     done
768 qed
770 lemma (in group) cosets_finite:
771      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
772 apply (auto simp add: RCOSETS_def)
773 apply (simp add: r_coset_subset_G [THEN finite_subset])
774 done
776 text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
777 lemma (in group) inj_on_f:
778     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
779 apply (rule inj_onI)
780 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
781  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
782 apply (simp add: subsetD)
783 done
785 lemma (in group) inj_on_g:
786     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
787 by (force simp add: inj_on_def subsetD)
789 lemma (in group) card_cosets_equal:
790      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
791       \<Longrightarrow> card c = card H"
792 apply (auto simp add: RCOSETS_def)
793 apply (rule card_bij_eq)
794      apply (rule inj_on_f, assumption+)
795     apply (force simp add: m_assoc subsetD r_coset_def)
796    apply (rule inj_on_g, assumption+)
797   apply (force simp add: m_assoc subsetD r_coset_def)
798  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
799  apply (simp add: r_coset_subset_G [THEN finite_subset])
800 apply (blast intro: finite_subset)
801 done
803 lemma (in group) rcosets_subset_PowG:
804      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
805 apply (simp add: RCOSETS_def)
806 apply (blast dest: r_coset_subset_G subgroup.subset)
807 done
810 theorem (in group) lagrange:
811      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
812       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
813 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
814 apply (subst mult_commute)
815 apply (rule card_partition)
816    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
817   apply (simp add: rcosets_part_G)
818  apply (simp add: card_cosets_equal subgroup.subset)
819 apply (simp add: rcos_disjoint)
820 done
823 subsection {*Quotient Groups: Factorization of a Group*}
825 constdefs
826   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
827      (infixl "Mod" 65)
828     --{*Actually defined for groups rather than monoids*}
829   "FactGroup G H \<equiv>
830     \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
832 lemma (in normal) setmult_closed:
833      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
834 by (auto simp add: rcos_sum RCOSETS_def)
836 lemma (in normal) setinv_closed:
837      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
838 by (auto simp add: rcos_inv RCOSETS_def)
840 lemma (in normal) rcosets_assoc:
841      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
842       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
843 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
845 lemma (in subgroup) subgroup_in_rcosets:
846   assumes "group G"
847   shows "H \<in> rcosets H"
848 proof -
849   interpret group G by fact
850   from _ subgroup_axioms have "H #> \<one> = H"
851     by (rule coset_join2) auto
852   then show ?thesis
853     by (auto simp add: RCOSETS_def)
854 qed
856 lemma (in normal) rcosets_inv_mult_group_eq:
857      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
858 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
860 theorem (in normal) factorgroup_is_group:
861   "group (G Mod H)"
862 apply (simp add: FactGroup_def)
863 apply (rule groupI)
864     apply (simp add: setmult_closed)
865    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
866   apply (simp add: restrictI setmult_closed rcosets_assoc)
867  apply (simp add: normal_imp_subgroup
868                   subgroup_in_rcosets rcosets_mult_eq)
869 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
870 done
872 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
873   by (simp add: FactGroup_def)
875 lemma (in normal) inv_FactGroup:
876      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
877 apply (rule group.inv_equality [OF factorgroup_is_group])
878 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
879 done
881 text{*The coset map is a homomorphism from @{term G} to the quotient group
882   @{term "G Mod H"}*}
883 lemma (in normal) r_coset_hom_Mod:
884   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
885   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
888 subsection{*The First Isomorphism Theorem*}
890 text{*The quotient by the kernel of a homomorphism is isomorphic to the
891   range of that homomorphism.*}
893 constdefs
894   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
895              ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
896     --{*the kernel of a homomorphism*}
897   "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
899 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
900 apply (rule subgroup.intro)
901 apply (auto simp add: kernel_def group.intro prems)
902 done
904 text{*The kernel of a homomorphism is a normal subgroup*}
905 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
906 apply (simp add: G.normal_inv_iff subgroup_kernel)
907 apply (simp add: kernel_def)
908 done
910 lemma (in group_hom) FactGroup_nonempty:
911   assumes X: "X \<in> carrier (G Mod kernel G H h)"
912   shows "X \<noteq> {}"
913 proof -
914   from X
915   obtain g where "g \<in> carrier G"
916              and "X = kernel G H h #> g"
917     by (auto simp add: FactGroup_def RCOSETS_def)
918   thus ?thesis
919    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
920 qed
923 lemma (in group_hom) FactGroup_contents_mem:
924   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
925   shows "contents (h`X) \<in> carrier H"
926 proof -
927   from X
928   obtain g where g: "g \<in> carrier G"
929              and "X = kernel G H h #> g"
930     by (auto simp add: FactGroup_def RCOSETS_def)
931   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
932   thus ?thesis by (auto simp add: g)
933 qed
935 lemma (in group_hom) FactGroup_hom:
936      "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
937 apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
938 proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
939   fix X and X'
940   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
941      and X': "X' \<in> carrier (G Mod kernel G H h)"
942   then
943   obtain g and g'
944            where "g \<in> carrier G" and "g' \<in> carrier G"
945              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
946     by (auto simp add: FactGroup_def RCOSETS_def)
947   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
948     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
949     by (force simp add: kernel_def r_coset_def image_def)+
950   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
951     by (auto dest!: FactGroup_nonempty
952              simp add: set_mult_def image_eq_UN
953                        subsetD [OF Xsub] subsetD [OF X'sub])
954   thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
955     by (simp add: all image_eq_UN FactGroup_nonempty X X')
956 qed
959 text{*Lemma for the following injectivity result*}
960 lemma (in group_hom) FactGroup_subset:
961      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
962       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
963 apply (clarsimp simp add: kernel_def r_coset_def image_def)
964 apply (rename_tac y)
965 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
966 apply (simp add: G.m_assoc)
967 done
969 lemma (in group_hom) FactGroup_inj_on:
970      "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
971 proof (simp add: inj_on_def, clarify)
972   fix X and X'
973   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
974      and X': "X' \<in> carrier (G Mod kernel G H h)"
975   then
976   obtain g and g'
977            where gX: "g \<in> carrier G"  "g' \<in> carrier G"
978               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
979     by (auto simp add: FactGroup_def RCOSETS_def)
980   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
981     by (force simp add: kernel_def r_coset_def image_def)+
982   assume "contents (h ` X) = contents (h ` X')"
983   hence h: "h g = h g'"
984     by (simp add: image_eq_UN all FactGroup_nonempty X X')
985   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
986 qed
988 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
989 homomorphism from the quotient group*}
990 lemma (in group_hom) FactGroup_onto:
991   assumes h: "h ` carrier G = carrier H"
992   shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
993 proof
994   show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
995     by (auto simp add: FactGroup_contents_mem)
996   show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
997   proof
998     fix y
999     assume y: "y \<in> carrier H"
1000     with h obtain g where g: "g \<in> carrier G" "h g = y"
1001       by (blast elim: equalityE)
1002     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
1003       by (auto simp add: y kernel_def r_coset_def)
1004     with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
1005       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
1006   qed
1007 qed
1010 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
1011  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
1012 theorem (in group_hom) FactGroup_iso:
1013   "h ` carrier G = carrier H
1014    \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
1015 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
1016               FactGroup_onto)
1019 end