src/HOL/Algebra/Coset.thy
 author ballarin Tue Jun 20 15:53:44 2006 +0200 (2006-06-20) changeset 19931 fb32b43e7f80 parent 19380 b808efaa5828 child 20318 0e0ea63fe768 permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
```     1 (*  Title:      HOL/Algebra/Coset.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Florian Kammueller, with new proofs by L C Paulson
```
```     4 *)
```
```     5
```
```     6 header{*Cosets and Quotient Groups*}
```
```     7
```
```     8 theory Coset imports Group Exponent begin
```
```     9
```
```    10 constdefs (structure G)
```
```    11   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
```
```    12   "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
```
```    13
```
```    14   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
```
```    15   "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
```
```    16
```
```    17   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
```
```    18   "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
```
```    19
```
```    20   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
```
```    21   "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
```
```    22
```
```    23   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
```
```    24   "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
```
```    25
```
```    26
```
```    27 locale normal = subgroup + group +
```
```    28   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
```
```    29
```
```    30 abbreviation
```
```    31   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60)
```
```    32   "H \<lhd> G \<equiv> normal H G"
```
```    33
```
```    34
```
```    35 subsection {*Basic Properties of Cosets*}
```
```    36
```
```    37 lemma (in group) coset_mult_assoc:
```
```    38      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
```
```    39       ==> (M #> g) #> h = M #> (g \<otimes> h)"
```
```    40 by (force simp add: r_coset_def m_assoc)
```
```    41
```
```    42 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
```
```    43 by (force simp add: r_coset_def)
```
```    44
```
```    45 lemma (in group) coset_mult_inv1:
```
```    46      "[| M #> (x \<otimes> (inv y)) = M;  x \<in> carrier G ; y \<in> carrier G;
```
```    47          M \<subseteq> carrier G |] ==> M #> x = M #> y"
```
```    48 apply (erule subst [of concl: "%z. M #> x = z #> y"])
```
```    49 apply (simp add: coset_mult_assoc m_assoc)
```
```    50 done
```
```    51
```
```    52 lemma (in group) coset_mult_inv2:
```
```    53      "[| M #> x = M #> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
```
```    54       ==> M #> (x \<otimes> (inv y)) = M "
```
```    55 apply (simp add: coset_mult_assoc [symmetric])
```
```    56 apply (simp add: coset_mult_assoc)
```
```    57 done
```
```    58
```
```    59 lemma (in group) coset_join1:
```
```    60      "[| H #> x = H;  x \<in> carrier G;  subgroup H G |] ==> x \<in> H"
```
```    61 apply (erule subst)
```
```    62 apply (simp add: r_coset_def)
```
```    63 apply (blast intro: l_one subgroup.one_closed sym)
```
```    64 done
```
```    65
```
```    66 lemma (in group) solve_equation:
```
```    67     "\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x"
```
```    68 apply (rule bexI [of _ "y \<otimes> (inv x)"])
```
```    69 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
```
```    70                       subgroup.subset [THEN subsetD])
```
```    71 done
```
```    72
```
```    73 lemma (in group) repr_independence:
```
```    74      "\<lbrakk>y \<in> H #> x;  x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y"
```
```    75 by (auto simp add: r_coset_def m_assoc [symmetric]
```
```    76                    subgroup.subset [THEN subsetD]
```
```    77                    subgroup.m_closed solve_equation)
```
```    78
```
```    79 lemma (in group) coset_join2:
```
```    80      "\<lbrakk>x \<in> carrier G;  subgroup H G;  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
```
```    81   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
```
```    82 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
```
```    83
```
```    84 lemma (in group) r_coset_subset_G:
```
```    85      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H #> x \<subseteq> carrier G"
```
```    86 by (auto simp add: r_coset_def)
```
```    87
```
```    88 lemma (in group) rcosI:
```
```    89      "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x"
```
```    90 by (auto simp add: r_coset_def)
```
```    91
```
```    92 lemma (in group) rcosetsI:
```
```    93      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
```
```    94 by (auto simp add: RCOSETS_def)
```
```    95
```
```    96 text{*Really needed?*}
```
```    97 lemma (in group) transpose_inv:
```
```    98      "[| x \<otimes> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
```
```    99       ==> (inv x) \<otimes> z = y"
```
```   100 by (force simp add: m_assoc [symmetric])
```
```   101
```
```   102 lemma (in group) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x"
```
```   103 apply (simp add: r_coset_def)
```
```   104 apply (blast intro: sym l_one subgroup.subset [THEN subsetD]
```
```   105                     subgroup.one_closed)
```
```   106 done
```
```   107
```
```   108
```
```   109 subsection {* Normal subgroups *}
```
```   110
```
```   111 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
```
```   112   by (simp add: normal_def subgroup_def)
```
```   113
```
```   114 lemma (in group) normalI:
```
```   115   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
```
```   116   by (simp add: normal_def normal_axioms_def prems)
```
```   117
```
```   118 lemma (in normal) inv_op_closed1:
```
```   119      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H"
```
```   120 apply (insert coset_eq)
```
```   121 apply (auto simp add: l_coset_def r_coset_def)
```
```   122 apply (drule bspec, assumption)
```
```   123 apply (drule equalityD1 [THEN subsetD], blast, clarify)
```
```   124 apply (simp add: m_assoc)
```
```   125 apply (simp add: m_assoc [symmetric])
```
```   126 done
```
```   127
```
```   128 lemma (in normal) inv_op_closed2:
```
```   129      "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
```
```   130 apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
```
```   131 apply (simp add: );
```
```   132 apply (blast intro: inv_op_closed1)
```
```   133 done
```
```   134
```
```   135 text{*Alternative characterization of normal subgroups*}
```
```   136 lemma (in group) normal_inv_iff:
```
```   137      "(N \<lhd> G) =
```
```   138       (subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
```
```   139       (is "_ = ?rhs")
```
```   140 proof
```
```   141   assume N: "N \<lhd> G"
```
```   142   show ?rhs
```
```   143     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)
```
```   144 next
```
```   145   assume ?rhs
```
```   146   hence sg: "subgroup N G"
```
```   147     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
```
```   148   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset)
```
```   149   show "N \<lhd> G"
```
```   150   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
```
```   151     fix x
```
```   152     assume x: "x \<in> carrier G"
```
```   153     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
```
```   154     proof
```
```   155       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   156       proof clarify
```
```   157         fix n
```
```   158         assume n: "n \<in> N"
```
```   159         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
```
```   160         proof
```
```   161           from closed [of "inv x"]
```
```   162           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
```
```   163           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
```
```   164             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
```
```   165         qed
```
```   166       qed
```
```   167     next
```
```   168       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   169       proof clarify
```
```   170         fix n
```
```   171         assume n: "n \<in> N"
```
```   172         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
```
```   173         proof
```
```   174           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
```
```   175           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
```
```   176             by (simp add: x n m_assoc sb [THEN subsetD])
```
```   177         qed
```
```   178       qed
```
```   179     qed
```
```   180   qed
```
```   181 qed
```
```   182
```
```   183
```
```   184 subsection{*More Properties of Cosets*}
```
```   185
```
```   186 lemma (in group) lcos_m_assoc:
```
```   187      "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
```
```   188       ==> g <# (h <# M) = (g \<otimes> h) <# M"
```
```   189 by (force simp add: l_coset_def m_assoc)
```
```   190
```
```   191 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M"
```
```   192 by (force simp add: l_coset_def)
```
```   193
```
```   194 lemma (in group) l_coset_subset_G:
```
```   195      "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <# H \<subseteq> carrier G"
```
```   196 by (auto simp add: l_coset_def subsetD)
```
```   197
```
```   198 lemma (in group) l_coset_swap:
```
```   199      "\<lbrakk>y \<in> x <# H;  x \<in> carrier G;  subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H"
```
```   200 proof (simp add: l_coset_def)
```
```   201   assume "\<exists>h\<in>H. y = x \<otimes> h"
```
```   202     and x: "x \<in> carrier G"
```
```   203     and sb: "subgroup H G"
```
```   204   then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast
```
```   205   show "\<exists>h\<in>H. x = y \<otimes> h"
```
```   206   proof
```
```   207     show "x = y \<otimes> inv h'" using h' x sb
```
```   208       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
```
```   209     show "inv h' \<in> H" using h' sb
```
```   210       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
```
```   211   qed
```
```   212 qed
```
```   213
```
```   214 lemma (in group) l_coset_carrier:
```
```   215      "[| y \<in> x <# H;  x \<in> carrier G;  subgroup H G |] ==> y \<in> carrier G"
```
```   216 by (auto simp add: l_coset_def m_assoc
```
```   217                    subgroup.subset [THEN subsetD] subgroup.m_closed)
```
```   218
```
```   219 lemma (in group) l_repr_imp_subset:
```
```   220   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
```
```   221   shows "y <# H \<subseteq> x <# H"
```
```   222 proof -
```
```   223   from y
```
```   224   obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def)
```
```   225   thus ?thesis using x sb
```
```   226     by (auto simp add: l_coset_def m_assoc
```
```   227                        subgroup.subset [THEN subsetD] subgroup.m_closed)
```
```   228 qed
```
```   229
```
```   230 lemma (in group) l_repr_independence:
```
```   231   assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G"
```
```   232   shows "x <# H = y <# H"
```
```   233 proof
```
```   234   show "x <# H \<subseteq> y <# H"
```
```   235     by (rule l_repr_imp_subset,
```
```   236         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
```
```   237   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
```
```   238 qed
```
```   239
```
```   240 lemma (in group) setmult_subset_G:
```
```   241      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G"
```
```   242 by (auto simp add: set_mult_def subsetD)
```
```   243
```
```   244 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
```
```   245 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
```
```   246 apply (rule_tac x = x in bexI)
```
```   247 apply (rule bexI [of _ "\<one>"])
```
```   248 apply (auto simp add: subgroup.m_closed subgroup.one_closed
```
```   249                       r_one subgroup.subset [THEN subsetD])
```
```   250 done
```
```   251
```
```   252
```
```   253 subsubsection {* Set of inverses of an @{text r_coset}. *}
```
```   254
```
```   255 lemma (in normal) rcos_inv:
```
```   256   assumes x:     "x \<in> carrier G"
```
```   257   shows "set_inv (H #> x) = H #> (inv x)"
```
```   258 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
```
```   259   fix h
```
```   260   assume "h \<in> H"
```
```   261   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
```
```   262   proof
```
```   263     show "inv x \<otimes> inv h \<otimes> x \<in> H"
```
```   264       by (simp add: inv_op_closed1 prems)
```
```   265     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
```
```   266       by (simp add: prems m_assoc)
```
```   267   qed
```
```   268 next
```
```   269   fix h
```
```   270   assume "h \<in> H"
```
```   271   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
```
```   272   proof
```
```   273     show "x \<otimes> inv h \<otimes> inv x \<in> H"
```
```   274       by (simp add: inv_op_closed2 prems)
```
```   275     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
```
```   276       by (simp add: prems m_assoc [symmetric] inv_mult_group)
```
```   277   qed
```
```   278 qed
```
```   279
```
```   280
```
```   281 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
```
```   282
```
```   283 lemma (in group) setmult_rcos_assoc:
```
```   284      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
```
```   285       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
```
```   286 by (force simp add: r_coset_def set_mult_def m_assoc)
```
```   287
```
```   288 lemma (in group) rcos_assoc_lcos:
```
```   289      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
```
```   290       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
```
```   291 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
```
```   292
```
```   293 lemma (in normal) rcos_mult_step1:
```
```   294      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   295       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
```
```   296 by (simp add: setmult_rcos_assoc subset
```
```   297               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
```
```   298
```
```   299 lemma (in normal) rcos_mult_step2:
```
```   300      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   301       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
```
```   302 by (insert coset_eq, simp add: normal_def)
```
```   303
```
```   304 lemma (in normal) rcos_mult_step3:
```
```   305      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   306       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
```
```   307 by (simp add: setmult_rcos_assoc coset_mult_assoc
```
```   308               subgroup_mult_id normal.axioms subset prems)
```
```   309
```
```   310 lemma (in normal) rcos_sum:
```
```   311      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
```
```   312       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
```
```   313 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
```
```   314
```
```   315 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
```
```   316   -- {* generalizes @{text subgroup_mult_id} *}
```
```   317   by (auto simp add: RCOSETS_def subset
```
```   318         setmult_rcos_assoc subgroup_mult_id normal.axioms prems)
```
```   319
```
```   320
```
```   321 subsubsection{*An Equivalence Relation*}
```
```   322
```
```   323 constdefs (structure G)
```
```   324   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
```
```   325                   ("rcong\<index> _")
```
```   326    "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
```
```   327
```
```   328
```
```   329 lemma (in subgroup) equiv_rcong:
```
```   330    includes group G
```
```   331    shows "equiv (carrier G) (rcong H)"
```
```   332 proof (intro equiv.intro)
```
```   333   show "refl (carrier G) (rcong H)"
```
```   334     by (auto simp add: r_congruent_def refl_def)
```
```   335 next
```
```   336   show "sym (rcong H)"
```
```   337   proof (simp add: r_congruent_def sym_def, clarify)
```
```   338     fix x y
```
```   339     assume [simp]: "x \<in> carrier G" "y \<in> carrier G"
```
```   340        and "inv x \<otimes> y \<in> H"
```
```   341     hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed)
```
```   342     thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
```
```   343   qed
```
```   344 next
```
```   345   show "trans (rcong H)"
```
```   346   proof (simp add: r_congruent_def trans_def, clarify)
```
```   347     fix x y z
```
```   348     assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
```
```   349        and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
```
```   350     hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
```
```   351     hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv)
```
```   352     thus "inv x \<otimes> z \<in> H" by simp
```
```   353   qed
```
```   354 qed
```
```   355
```
```   356 text{*Equivalence classes of @{text rcong} correspond to left cosets.
```
```   357   Was there a mistake in the definitions? I'd have expected them to
```
```   358   correspond to right cosets.*}
```
```   359
```
```   360 (* CB: This is correct, but subtle.
```
```   361    We call H #> a the right coset of a relative to H.  According to
```
```   362    Jacobson, this is what the majority of group theory literature does.
```
```   363    He then defines the notion of congruence relation ~ over monoids as
```
```   364    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
```
```   365    Our notion of right congruence induced by K: rcong K appears only in
```
```   366    the context where K is a normal subgroup.  Jacobson doesn't name it.
```
```   367    But in this context left and right cosets are identical.
```
```   368 *)
```
```   369
```
```   370 lemma (in subgroup) l_coset_eq_rcong:
```
```   371   includes group G
```
```   372   assumes a: "a \<in> carrier G"
```
```   373   shows "a <# H = rcong H `` {a}"
```
```   374 by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a )
```
```   375
```
```   376
```
```   377 subsubsection{*Two distinct right cosets are disjoint*}
```
```   378
```
```   379 lemma (in group) rcos_equation:
```
```   380   includes subgroup H G
```
```   381   shows
```
```   382      "\<lbrakk>ha \<otimes> a = h \<otimes> b; a \<in> carrier G;  b \<in> carrier G;
```
```   383         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
```
```   384       \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
```
```   385 apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
```
```   386 apply (simp add: );
```
```   387 apply (simp add: m_assoc transpose_inv)
```
```   388 done
```
```   389
```
```   390 lemma (in group) rcos_disjoint:
```
```   391   includes subgroup H G
```
```   392   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
```
```   393 apply (simp add: RCOSETS_def r_coset_def)
```
```   394 apply (blast intro: rcos_equation prems sym)
```
```   395 done
```
```   396
```
```   397
```
```   398 subsection {*Order of a Group and Lagrange's Theorem*}
```
```   399
```
```   400 constdefs
```
```   401   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
```
```   402   "order S \<equiv> card (carrier S)"
```
```   403
```
```   404 lemma (in group) rcos_self:
```
```   405   includes subgroup
```
```   406   shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
```
```   407 apply (simp add: r_coset_def)
```
```   408 apply (rule_tac x="\<one>" in bexI)
```
```   409 apply (auto simp add: );
```
```   410 done
```
```   411
```
```   412 lemma (in group) rcosets_part_G:
```
```   413   includes subgroup
```
```   414   shows "\<Union>(rcosets H) = carrier G"
```
```   415 apply (rule equalityI)
```
```   416  apply (force simp add: RCOSETS_def r_coset_def)
```
```   417 apply (auto simp add: RCOSETS_def intro: rcos_self prems)
```
```   418 done
```
```   419
```
```   420 lemma (in group) cosets_finite:
```
```   421      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
```
```   422 apply (auto simp add: RCOSETS_def)
```
```   423 apply (simp add: r_coset_subset_G [THEN finite_subset])
```
```   424 done
```
```   425
```
```   426 text{*The next two lemmas support the proof of @{text card_cosets_equal}.*}
```
```   427 lemma (in group) inj_on_f:
```
```   428     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
```
```   429 apply (rule inj_onI)
```
```   430 apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G")
```
```   431  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
```
```   432 apply (simp add: subsetD)
```
```   433 done
```
```   434
```
```   435 lemma (in group) inj_on_g:
```
```   436     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
```
```   437 by (force simp add: inj_on_def subsetD)
```
```   438
```
```   439 lemma (in group) card_cosets_equal:
```
```   440      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
```
```   441       \<Longrightarrow> card c = card H"
```
```   442 apply (auto simp add: RCOSETS_def)
```
```   443 apply (rule card_bij_eq)
```
```   444      apply (rule inj_on_f, assumption+)
```
```   445     apply (force simp add: m_assoc subsetD r_coset_def)
```
```   446    apply (rule inj_on_g, assumption+)
```
```   447   apply (force simp add: m_assoc subsetD r_coset_def)
```
```   448  txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*}
```
```   449  apply (simp add: r_coset_subset_G [THEN finite_subset])
```
```   450 apply (blast intro: finite_subset)
```
```   451 done
```
```   452
```
```   453 lemma (in group) rcosets_subset_PowG:
```
```   454      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
```
```   455 apply (simp add: RCOSETS_def)
```
```   456 apply (blast dest: r_coset_subset_G subgroup.subset)
```
```   457 done
```
```   458
```
```   459
```
```   460 theorem (in group) lagrange:
```
```   461      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
```
```   462       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
```
```   463 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
```
```   464 apply (subst mult_commute)
```
```   465 apply (rule card_partition)
```
```   466    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
```
```   467   apply (simp add: rcosets_part_G)
```
```   468  apply (simp add: card_cosets_equal subgroup.subset)
```
```   469 apply (simp add: rcos_disjoint)
```
```   470 done
```
```   471
```
```   472
```
```   473 subsection {*Quotient Groups: Factorization of a Group*}
```
```   474
```
```   475 constdefs
```
```   476   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid"
```
```   477      (infixl "Mod" 65)
```
```   478     --{*Actually defined for groups rather than monoids*}
```
```   479   "FactGroup G H \<equiv>
```
```   480     \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
```
```   481
```
```   482 lemma (in normal) setmult_closed:
```
```   483      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
```
```   484 by (auto simp add: rcos_sum RCOSETS_def)
```
```   485
```
```   486 lemma (in normal) setinv_closed:
```
```   487      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
```
```   488 by (auto simp add: rcos_inv RCOSETS_def)
```
```   489
```
```   490 lemma (in normal) rcosets_assoc:
```
```   491      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
```
```   492       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
```
```   493 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
```
```   494
```
```   495 lemma (in subgroup) subgroup_in_rcosets:
```
```   496   includes group G
```
```   497   shows "H \<in> rcosets H"
```
```   498 proof -
```
```   499   have "H #> \<one> = H"
```
```   500     by (rule coset_join2, auto)
```
```   501   then show ?thesis
```
```   502     by (auto simp add: RCOSETS_def)
```
```   503 qed
```
```   504
```
```   505 lemma (in normal) rcosets_inv_mult_group_eq:
```
```   506      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
```
```   507 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems)
```
```   508
```
```   509 theorem (in normal) factorgroup_is_group:
```
```   510   "group (G Mod H)"
```
```   511 apply (simp add: FactGroup_def)
```
```   512 apply (rule groupI)
```
```   513     apply (simp add: setmult_closed)
```
```   514    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
```
```   515   apply (simp add: restrictI setmult_closed rcosets_assoc)
```
```   516  apply (simp add: normal_imp_subgroup
```
```   517                   subgroup_in_rcosets rcosets_mult_eq)
```
```   518 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
```
```   519 done
```
```   520
```
```   521 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
```
```   522   by (simp add: FactGroup_def)
```
```   523
```
```   524 lemma (in normal) inv_FactGroup:
```
```   525      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
```
```   526 apply (rule group.inv_equality [OF factorgroup_is_group])
```
```   527 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
```
```   528 done
```
```   529
```
```   530 text{*The coset map is a homomorphism from @{term G} to the quotient group
```
```   531   @{term "G Mod H"}*}
```
```   532 lemma (in normal) r_coset_hom_Mod:
```
```   533   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
```
```   534   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
```
```   535
```
```   536
```
```   537 subsection{*The First Isomorphism Theorem*}
```
```   538
```
```   539 text{*The quotient by the kernel of a homomorphism is isomorphic to the
```
```   540   range of that homomorphism.*}
```
```   541
```
```   542 constdefs
```
```   543   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
```
```   544              ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
```
```   545     --{*the kernel of a homomorphism*}
```
```   546   "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
```
```   547
```
```   548 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
```
```   549 apply (rule subgroup.intro)
```
```   550 apply (auto simp add: kernel_def group.intro prems)
```
```   551 done
```
```   552
```
```   553 text{*The kernel of a homomorphism is a normal subgroup*}
```
```   554 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
```
```   555 apply (simp add: G.normal_inv_iff subgroup_kernel)
```
```   556 apply (simp add: kernel_def)
```
```   557 done
```
```   558
```
```   559 lemma (in group_hom) FactGroup_nonempty:
```
```   560   assumes X: "X \<in> carrier (G Mod kernel G H h)"
```
```   561   shows "X \<noteq> {}"
```
```   562 proof -
```
```   563   from X
```
```   564   obtain g where "g \<in> carrier G"
```
```   565              and "X = kernel G H h #> g"
```
```   566     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   567   thus ?thesis
```
```   568    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
```
```   569 qed
```
```   570
```
```   571
```
```   572 lemma (in group_hom) FactGroup_contents_mem:
```
```   573   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
```
```   574   shows "contents (h`X) \<in> carrier H"
```
```   575 proof -
```
```   576   from X
```
```   577   obtain g where g: "g \<in> carrier G"
```
```   578              and "X = kernel G H h #> g"
```
```   579     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   580   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
```
```   581   thus ?thesis by (auto simp add: g)
```
```   582 qed
```
```   583
```
```   584 lemma (in group_hom) FactGroup_hom:
```
```   585      "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
```
```   586 apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
```
```   587 proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
```
```   588   fix X and X'
```
```   589   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```   590      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```   591   then
```
```   592   obtain g and g'
```
```   593            where "g \<in> carrier G" and "g' \<in> carrier G"
```
```   594              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
```
```   595     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   596   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```   597     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
```
```   598     by (force simp add: kernel_def r_coset_def image_def)+
```
```   599   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
```
```   600     by (auto dest!: FactGroup_nonempty
```
```   601              simp add: set_mult_def image_eq_UN
```
```   602                        subsetD [OF Xsub] subsetD [OF X'sub])
```
```   603   thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
```
```   604     by (simp add: all image_eq_UN FactGroup_nonempty X X')
```
```   605 qed
```
```   606
```
```   607
```
```   608 text{*Lemma for the following injectivity result*}
```
```   609 lemma (in group_hom) FactGroup_subset:
```
```   610      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
```
```   611       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
```
```   612 apply (clarsimp simp add: kernel_def r_coset_def image_def);
```
```   613 apply (rename_tac y)
```
```   614 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
```
```   615 apply (simp add: G.m_assoc);
```
```   616 done
```
```   617
```
```   618 lemma (in group_hom) FactGroup_inj_on:
```
```   619      "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
```
```   620 proof (simp add: inj_on_def, clarify)
```
```   621   fix X and X'
```
```   622   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
```
```   623      and X': "X' \<in> carrier (G Mod kernel G H h)"
```
```   624   then
```
```   625   obtain g and g'
```
```   626            where gX: "g \<in> carrier G"  "g' \<in> carrier G"
```
```   627               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
```
```   628     by (auto simp add: FactGroup_def RCOSETS_def)
```
```   629   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
```
```   630     by (force simp add: kernel_def r_coset_def image_def)+
```
```   631   assume "contents (h ` X) = contents (h ` X')"
```
```   632   hence h: "h g = h g'"
```
```   633     by (simp add: image_eq_UN all FactGroup_nonempty X X')
```
```   634   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
```
```   635 qed
```
```   636
```
```   637 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
```
```   638 homomorphism from the quotient group*}
```
```   639 lemma (in group_hom) FactGroup_onto:
```
```   640   assumes h: "h ` carrier G = carrier H"
```
```   641   shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
```
```   642 proof
```
```   643   show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
```
```   644     by (auto simp add: FactGroup_contents_mem)
```
```   645   show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
```
```   646   proof
```
```   647     fix y
```
```   648     assume y: "y \<in> carrier H"
```
```   649     with h obtain g where g: "g \<in> carrier G" "h g = y"
```
```   650       by (blast elim: equalityE);
```
```   651     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
```
```   652       by (auto simp add: y kernel_def r_coset_def)
```
```   653     with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
```
```   654       by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
```
```   655   qed
```
```   656 qed
```
```   657
```
```   658
```
```   659 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
```
```   660  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
```
```   661 theorem (in group_hom) FactGroup_iso:
```
```   662   "h ` carrier G = carrier H
```
```   663    \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
```
```   664 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
```
```   665               FactGroup_onto)
```
```   666
```
```   667
```
```   668 end
```