src/ZF/ex/Group.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14891 f2e9f7d813af
child 19931 fb32b43e7f80
permissions -rw-r--r--
migrated theory headers to new format
     1 (* Title:  ZF/ex/Group.thy
     2   Id:     $Id$
     3 
     4 *)
     5 
     6 header {* Groups *}
     7 
     8 theory Group imports Main begin
     9 
    10 text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
    11 Markus Wenzel.*}
    12 
    13 
    14 subsection {* Monoids *}
    15 
    16 (*First, we must simulate a record declaration:
    17 record monoid = 
    18   carrier :: i
    19   mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)
    20   one :: i ("\<one>\<index>")
    21 *)
    22 
    23 constdefs
    24   carrier :: "i => i"
    25    "carrier(M) == fst(M)"
    26 
    27   mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70)
    28    "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
    29 
    30   one :: "i => i" ("\<one>\<index>")
    31    "one(M) == fst(snd(snd(M)))"
    32 
    33   update_carrier :: "[i,i] => i"
    34    "update_carrier(M,A) == <A,snd(M)>"
    35 
    36 constdefs (structure G)
    37   m_inv :: "i => i => i" ("inv\<index> _" [81] 80)
    38   "inv x == (THE y. y \<in> carrier(G) & y \<cdot> x = \<one> & x \<cdot> y = \<one>)"
    39 
    40 locale monoid = struct G +
    41   assumes m_closed [intro, simp]:
    42          "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
    43       and m_assoc:
    44          "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
    45           \<Longrightarrow> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
    46       and one_closed [intro, simp]: "\<one> \<in> carrier(G)"
    47       and l_one [simp]: "x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
    48       and r_one [simp]: "x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
    49 
    50 text{*Simulating the record*}
    51 lemma carrier_eq [simp]: "carrier(<A,Z>) = A"
    52   by (simp add: carrier_def)
    53 
    54 lemma mult_eq [simp]: "mmult(<A,M,Z>, x, y) = M ` <x,y>"
    55   by (simp add: mmult_def)
    56 
    57 lemma one_eq [simp]: "one(<A,M,I,Z>) = I"
    58   by (simp add: one_def)
    59 
    60 lemma update_carrier_eq [simp]: "update_carrier(<A,Z>,B) = <B,Z>"
    61   by (simp add: update_carrier_def)
    62 
    63 lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
    64 by (simp add: update_carrier_def) 
    65 
    66 lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
    67 by (simp add: update_carrier_def mmult_def) 
    68 
    69 lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
    70 by (simp add: update_carrier_def one_def) 
    71 
    72 
    73 lemma (in monoid) inv_unique:
    74   assumes eq: "y \<cdot> x = \<one>"  "x \<cdot> y' = \<one>"
    75     and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "y' \<in> carrier(G)"
    76   shows "y = y'"
    77 proof -
    78   from G eq have "y = y \<cdot> (x \<cdot> y')" by simp
    79   also from G have "... = (y \<cdot> x) \<cdot> y'" by (simp add: m_assoc)
    80   also from G eq have "... = y'" by simp
    81   finally show ?thesis .
    82 qed
    83 
    84 text {*
    85   A group is a monoid all of whose elements are invertible.
    86 *}
    87 
    88 locale group = monoid +
    89   assumes inv_ex:
    90      "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
    91 
    92 lemma (in group) is_group [simp]: "group(G)"
    93   by (rule group.intro [OF prems]) 
    94 
    95 theorem groupI:
    96   includes struct G
    97   assumes m_closed [simp]:
    98       "\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
    99     and one_closed [simp]: "\<one> \<in> carrier(G)"
   100     and m_assoc:
   101       "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
   102       (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   103     and l_one [simp]: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"
   104     and l_inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one>"
   105   shows "group(G)"
   106 proof -
   107   have l_cancel [simp]:
   108     "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
   109     (x \<cdot> y = x \<cdot> z) <-> (y = z)"
   110   proof
   111     fix x y z
   112     assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
   113     { 
   114       assume eq: "x \<cdot> y = x \<cdot> z"
   115       with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
   116 	and l_inv: "x_inv \<cdot> x = \<one>" by fast
   117       from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z"
   118 	by (simp add: m_assoc)
   119       with G show "y = z" by (simp add: l_inv)
   120     next
   121       assume eq: "y = z"
   122       with G show "x \<cdot> y = x \<cdot> z" by simp
   123     }
   124   qed
   125   have r_one:
   126     "\<And>x. x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"
   127   proof -
   128     fix x
   129     assume x: "x \<in> carrier(G)"
   130     with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"
   131       and l_inv: "x_inv \<cdot> x = \<one>" by fast
   132     from x xG have "x_inv \<cdot> (x \<cdot> \<one>) = x_inv \<cdot> x"
   133       by (simp add: m_assoc [symmetric] l_inv)
   134     with x xG show "x \<cdot> \<one> = x" by simp
   135   qed
   136   have inv_ex:
   137     "!!x. x \<in> carrier(G) ==> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
   138   proof -
   139     fix x
   140     assume x: "x \<in> carrier(G)"
   141     with l_inv_ex obtain y where y: "y \<in> carrier(G)"
   142       and l_inv: "y \<cdot> x = \<one>" by fast
   143     from x y have "y \<cdot> (x \<cdot> y) = y \<cdot> \<one>"
   144       by (simp add: m_assoc [symmetric] l_inv r_one)
   145     with x y have r_inv: "x \<cdot> y = \<one>"
   146       by simp
   147     from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
   148       by (fast intro: l_inv r_inv)
   149   qed
   150   show ?thesis
   151     by (blast intro: group.intro monoid.intro group_axioms.intro 
   152                      prems r_one inv_ex)
   153 qed
   154 
   155 lemma (in group) inv [simp]:
   156   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>"
   157   apply (frule inv_ex) 
   158   apply (unfold Bex_def m_inv_def)
   159   apply (erule exE) 
   160   apply (rule theI)
   161   apply (rule ex1I, assumption)
   162    apply (blast intro: inv_unique)
   163   done
   164 
   165 lemma (in group) inv_closed [intro!]:
   166   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G)"
   167   by simp
   168 
   169 lemma (in group) l_inv:
   170   "x \<in> carrier(G) \<Longrightarrow> inv x \<cdot> x = \<one>"
   171   by simp
   172 
   173 lemma (in group) r_inv:
   174   "x \<in> carrier(G) \<Longrightarrow> x \<cdot> inv x = \<one>"
   175   by simp
   176 
   177 
   178 subsection {* Cancellation Laws and Basic Properties *}
   179 
   180 lemma (in group) l_cancel [simp]:
   181   assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
   182   shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
   183 proof
   184   assume eq: "x \<cdot> y = x \<cdot> z"
   185   hence  "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
   186     by (simp only: m_assoc inv_closed prems)
   187   thus "y = z" by simp
   188 next
   189   assume eq: "y = z"
   190   then show "x \<cdot> y = x \<cdot> z" by simp
   191 qed
   192 
   193 lemma (in group) r_cancel [simp]:
   194   assumes [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
   195   shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
   196 proof
   197   assume eq: "y \<cdot> x = z \<cdot> x"
   198   then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
   199     by (simp only: m_assoc [symmetric] inv_closed prems)
   200   thus "y = z" by simp
   201 next
   202   assume eq: "y = z"
   203   thus  "y \<cdot> x = z \<cdot> x" by simp
   204 qed
   205 
   206 lemma (in group) inv_comm:
   207   assumes inv: "x \<cdot> y = \<one>"
   208       and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
   209   shows "y \<cdot> x = \<one>"
   210 proof -
   211   from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)
   212   with G show ?thesis by (simp del: r_one add: m_assoc)
   213 qed
   214 
   215 lemma (in group) inv_equality:
   216      "\<lbrakk>y \<cdot> x = \<one>; x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv x = y"
   217 apply (simp add: m_inv_def)
   218 apply (rule the_equality)
   219  apply (simp add: inv_comm [of y x])
   220 apply (rule r_cancel [THEN iffD1], auto)
   221 done
   222 
   223 lemma (in group) inv_one [simp]:
   224   "inv \<one> = \<one>"
   225   by (auto intro: inv_equality) 
   226 
   227 lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x"
   228   by (auto intro: inv_equality) 
   229 
   230 text{*This proof is by cancellation*}
   231 lemma (in group) inv_mult_group:
   232   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x"
   233 proof -
   234   assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"
   235   then have "inv (x \<cdot> y) \<cdot> (x \<cdot> y) = (inv y \<cdot> inv x) \<cdot> (x \<cdot> y)"
   236     by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   237   with G show ?thesis by (simp_all del: inv add: inv_closed)
   238 qed
   239 
   240 
   241 subsection {* Substructures *}
   242 
   243 locale subgroup = var H + struct G + 
   244   assumes subset: "H \<subseteq> carrier(G)"
   245     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
   246     and  one_closed [simp]: "\<one> \<in> H"
   247     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
   248 
   249 
   250 lemma (in subgroup) mem_carrier [simp]:
   251   "x \<in> H \<Longrightarrow> x \<in> carrier(G)"
   252   using subset by blast
   253 
   254 
   255 lemma subgroup_imp_subset:
   256   "subgroup(H,G) \<Longrightarrow> H \<subseteq> carrier(G)"
   257   by (rule subgroup.subset)
   258 
   259 lemma (in subgroup) group_axiomsI [intro]:
   260   includes group G
   261   shows "group_axioms (update_carrier(G,H))"
   262 by (force intro: group_axioms.intro l_inv r_inv) 
   263 
   264 lemma (in subgroup) is_group [intro]:
   265   includes group G
   266   shows "group (update_carrier(G,H))"
   267   by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
   268 
   269 text {*
   270   Since @{term H} is nonempty, it contains some element @{term x}.  Since
   271   it is closed under inverse, it contains @{text "inv x"}.  Since
   272   it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
   273 *}
   274 
   275 text {*
   276   Since @{term H} is nonempty, it contains some element @{term x}.  Since
   277   it is closed under inverse, it contains @{text "inv x"}.  Since
   278   it is closed under product, it contains @{text "x \<cdot> inv x = \<one>"}.
   279 *}
   280 
   281 lemma (in group) one_in_subset:
   282   "\<lbrakk>H \<subseteq> carrier(G); H \<noteq> 0; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<cdot> b \<in> H\<rbrakk>
   283    \<Longrightarrow> \<one> \<in> H"
   284 by (force simp add: l_inv)
   285 
   286 text {* A characterization of subgroups: closed, non-empty subset. *}
   287 
   288 declare monoid.one_closed [simp] group.inv_closed [simp]
   289   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   290 
   291 lemma subgroup_nonempty:
   292   "~ subgroup(0,G)"
   293   by (blast dest: subgroup.one_closed)
   294 
   295 
   296 subsection {* Direct Products *}
   297 
   298 constdefs
   299   DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80)
   300   "G \<Otimes> H == <carrier(G) \<times> carrier(H),
   301               (\<lambda><<g,h>, <g', h'>>
   302                    \<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).
   303                 <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>),
   304               <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>, 0>"
   305 
   306 lemma DirProdGroup_group:
   307   includes group G + group H
   308   shows "group (G \<Otimes> H)"
   309 by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
   310           simp add: DirProdGroup_def)
   311 
   312 lemma carrier_DirProdGroup [simp]:
   313      "carrier (G \<Otimes> H) = carrier(G) \<times> carrier(H)"
   314   by (simp add: DirProdGroup_def)
   315 
   316 lemma one_DirProdGroup [simp]:
   317      "\<one>\<^bsub>G \<Otimes> H\<^esub> = <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>"
   318   by (simp add: DirProdGroup_def)
   319 
   320 lemma mult_DirProdGroup [simp]:
   321      "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
   322       ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
   323 by (simp add: DirProdGroup_def)
   324 
   325 lemma inv_DirProdGroup [simp]:
   326   includes group G + group H
   327   assumes g: "g \<in> carrier(G)"
   328       and h: "h \<in> carrier(H)"
   329   shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"
   330   apply (rule group.inv_equality [OF DirProdGroup_group])
   331   apply (simp_all add: prems group_def group.l_inv)
   332   done
   333 
   334 subsection {* Isomorphisms *}
   335 
   336 constdefs
   337   hom :: "[i,i] => i"
   338   "hom(G,H) ==
   339     {h \<in> carrier(G) -> carrier(H).
   340       (\<forall>x \<in> carrier(G). \<forall>y \<in> carrier(G). h ` (x \<cdot>\<^bsub>G\<^esub> y) = (h ` x) \<cdot>\<^bsub>H\<^esub> (h ` y))}"
   341 
   342 lemma hom_mult:
   343   "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   344    \<Longrightarrow> h ` (x \<cdot>\<^bsub>G\<^esub> y) = h ` x \<cdot>\<^bsub>H\<^esub> h ` y"
   345   by (simp add: hom_def)
   346 
   347 lemma hom_closed:
   348   "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h ` x \<in> carrier(H)"
   349   by (auto simp add: hom_def)
   350 
   351 lemma (in group) hom_compose:
   352      "\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)"
   353 by (force simp add: hom_def comp_fun) 
   354 
   355 lemma hom_is_fun:
   356   "h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)"
   357   by (simp add: hom_def)
   358 
   359 
   360 subsection {* Isomorphisms *}
   361 
   362 constdefs
   363   iso :: "[i,i] => i"  (infixr "\<cong>" 60)
   364   "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
   365 
   366 lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
   367 by (simp add: iso_def hom_def id_type id_bij) 
   368 
   369 
   370 lemma (in group) iso_sym:
   371      "h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G"
   372 apply (simp add: iso_def bij_converse_bij, clarify) 
   373 apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)") 
   374  prefer 2 apply (simp add: bij_converse_bij bij_is_fun) 
   375 apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"] 
   376             simp add: hom_def bij_is_inj right_inverse_bij); 
   377 done
   378 
   379 lemma (in group) iso_trans: 
   380      "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
   381 by (auto simp add: iso_def hom_compose comp_bij)
   382 
   383 lemma DirProdGroup_commute_iso:
   384   includes group G + group H
   385   shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
   386 by (auto simp add: iso_def hom_def inj_def surj_def bij_def) 
   387 
   388 lemma DirProdGroup_assoc_iso:
   389   includes group G + group H + group I
   390   shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
   391           \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
   392 by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
   393 
   394 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   395   @term{H}, with a homomorphism @{term h} between them*}
   396 locale group_hom = group G + group H + var h +
   397   assumes homh: "h \<in> hom(G,H)"
   398   notes hom_mult [simp] = hom_mult [OF homh]
   399     and hom_closed [simp] = hom_closed [OF homh]
   400     and hom_is_fun [simp] = hom_is_fun [OF homh]
   401 
   402 lemma (in group_hom) one_closed [simp]:
   403   "h ` \<one> \<in> carrier(H)"
   404   by simp
   405 
   406 lemma (in group_hom) hom_one [simp]:
   407   "h ` \<one> = \<one>\<^bsub>H\<^esub>"
   408 proof -
   409   have "h ` \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h ` \<one>) \<cdot>\<^bsub>H\<^esub> (h ` \<one>)"
   410     by (simp add: hom_mult [symmetric] del: hom_mult)
   411   then show ?thesis by (simp del: r_one)
   412 qed
   413 
   414 lemma (in group_hom) inv_closed [simp]:
   415   "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) \<in> carrier(H)"
   416   by simp
   417 
   418 lemma (in group_hom) hom_inv [simp]:
   419   "x \<in> carrier(G) \<Longrightarrow> h ` (inv x) = inv\<^bsub>H\<^esub> (h ` x)"
   420 proof -
   421   assume x: "x \<in> carrier(G)"
   422   then have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = \<one>\<^bsub>H\<^esub>"
   423     by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   424   also from x have "... = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)"
   425     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   426   finally have "h ` x \<cdot>\<^bsub>H\<^esub> h ` (inv x) = h ` x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h ` x)" .
   427   with x show ?thesis by (simp del: inv add: is_group)
   428 qed
   429 
   430 subsection {* Commutative Structures *}
   431 
   432 text {*
   433   Naming convention: multiplicative structures that are commutative
   434   are called \emph{commutative}, additive structures are called
   435   \emph{Abelian}.
   436 *}
   437 
   438 subsection {* Definition *}
   439 
   440 locale comm_monoid = monoid +
   441   assumes m_comm: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x"
   442 
   443 lemma (in comm_monoid) m_lcomm:
   444   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
   445    x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   446 proof -
   447   assume xyz: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
   448   from xyz have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by (simp add: m_assoc)
   449   also from xyz have "... = (y \<cdot> x) \<cdot> z" by (simp add: m_comm)
   450   also from xyz have "... = y \<cdot> (x \<cdot> z)" by (simp add: m_assoc)
   451   finally show ?thesis .
   452 qed
   453 
   454 lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm
   455 
   456 locale comm_group = comm_monoid + group
   457 
   458 lemma (in comm_group) inv_mult:
   459   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y"
   460   by (simp add: m_ac inv_mult_group)
   461 
   462 
   463 lemma (in group) subgroup_self: "subgroup (carrier(G),G)"
   464 by (simp add: subgroup_def prems) 
   465 
   466 lemma (in group) subgroup_imp_group:
   467   "subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"
   468 by (simp add: subgroup.is_group)
   469 
   470 lemma (in group) subgroupI:
   471   assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"
   472     and inv: "!!a. a \<in> H ==> inv a \<in> H"
   473     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"
   474   shows "subgroup(H,G)"
   475 proof (simp add: subgroup_def prems)
   476   show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   477 qed
   478 
   479 
   480 subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
   481 
   482 constdefs
   483   BijGroup :: "i=>i"
   484   "BijGroup(S) ==
   485     <bij(S,S),
   486      \<lambda><g,f> \<in> bij(S,S) \<times> bij(S,S). g O f,
   487      id(S), 0>"
   488 
   489 
   490 subsection {*Bijections Form a Group *}
   491 
   492 theorem group_BijGroup: "group(BijGroup(S))"
   493 apply (simp add: BijGroup_def)
   494 apply (rule groupI) 
   495     apply (simp_all add: id_bij comp_bij comp_assoc) 
   496  apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)
   497 apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)
   498 done
   499 
   500 
   501 subsection{*Automorphisms Form a Group*}
   502 
   503 lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f) ` x \<in> S" 
   504 by (blast intro: apply_funtype bij_is_fun bij_converse_bij)
   505 
   506 lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)"
   507 apply (rule group.inv_equality)
   508 apply (rule group_BijGroup)
   509 apply (simp_all add: BijGroup_def bij_converse_bij 
   510           left_comp_inverse [OF bij_is_inj]) 
   511 done
   512 
   513 lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))"
   514 by (simp add: iso_def)
   515 
   516 
   517 constdefs
   518   auto :: "i=>i"
   519   "auto(G) == iso(G,G)"
   520 
   521   AutoGroup :: "i=>i"
   522   "AutoGroup(G) == update_carrier(BijGroup(carrier(G)), auto(G))"
   523 
   524 
   525 lemma (in group) id_in_auto: "id(carrier(G)) \<in> auto(G)"
   526   by (simp add: iso_refl auto_def)
   527 
   528 lemma (in group) subgroup_auto:
   529       "subgroup (auto(G)) (BijGroup (carrier(G)))"
   530 proof (rule subgroup.intro)
   531   show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))"
   532     by (auto simp add: auto_def BijGroup_def iso_def)
   533 next
   534   fix x y
   535   assume "x \<in> auto(G)" "y \<in> auto(G)" 
   536   thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)"
   537     by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun 
   538                        group.hom_compose comp_bij)
   539 next
   540   show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add:  BijGroup_def id_in_auto)
   541 next
   542   fix x 
   543   assume "x \<in> auto(G)" 
   544   thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)"
   545     by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym) 
   546 qed
   547 
   548 theorem (in group) AutoGroup: "group (AutoGroup(G))"
   549 by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)
   550 
   551 
   552 
   553 subsection{*Cosets and Quotient Groups*}
   554 
   555 constdefs (structure G)
   556   r_coset  :: "[i,i,i] => i"    (infixl "#>\<index>" 60)
   557    "H #> a == \<Union>h\<in>H. {h \<cdot> a}"
   558 
   559   l_coset  :: "[i,i,i] => i"    (infixl "<#\<index>" 60)
   560    "a <# H == \<Union>h\<in>H. {a \<cdot> h}"
   561 
   562   RCOSETS  :: "[i,i] => i"          ("rcosets\<index> _" [81] 80)
   563    "rcosets H == \<Union>a\<in>carrier(G). {H #> a}"
   564 
   565   set_mult :: "[i,i,i] => i"    (infixl "<#>\<index>" 60)
   566    "H <#> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot> k}"
   567 
   568   SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80)
   569    "set_inv H == \<Union>h\<in>H. {inv h}"
   570 
   571 
   572 locale normal = subgroup + group +
   573   assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
   574 
   575 
   576 syntax
   577   "@normal" :: "[i,i] => i"  (infixl "\<lhd>" 60)
   578 
   579 translations
   580   "H \<lhd> G" == "normal(H,G)"
   581 
   582 
   583 subsection {*Basic Properties of Cosets*}
   584 
   585 lemma (in group) coset_mult_assoc:
   586      "\<lbrakk>M \<subseteq> carrier(G); g \<in> carrier(G); h \<in> carrier(G)\<rbrakk>
   587       \<Longrightarrow> (M #> g) #> h = M #> (g \<cdot> h)"
   588 by (force simp add: r_coset_def m_assoc)
   589 
   590 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier(G) \<Longrightarrow> M #> \<one> = M"
   591 by (force simp add: r_coset_def)
   592 
   593 lemma (in group) solve_equation:
   594     "\<lbrakk>subgroup(H,G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<cdot> x"
   595 apply (rule bexI [of _ "y \<cdot> (inv x)"])
   596 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc
   597                       subgroup.subset [THEN subsetD])
   598 done
   599 
   600 lemma (in group) repr_independence:
   601      "\<lbrakk>y \<in> H #> x;  x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> H #> x = H #> y"
   602 by (auto simp add: r_coset_def m_assoc [symmetric]
   603                    subgroup.subset [THEN subsetD]
   604                    subgroup.m_closed solve_equation)
   605 
   606 lemma (in group) coset_join2:
   607      "\<lbrakk>x \<in> carrier(G);  subgroup(H,G);  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"
   608   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}
   609 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
   610 
   611 lemma (in group) r_coset_subset_G:
   612      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier(G)"
   613 by (auto simp add: r_coset_def)
   614 
   615 lemma (in group) rcosI:
   616      "\<lbrakk>h \<in> H; H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h \<cdot> x \<in> H #> x"
   617 by (auto simp add: r_coset_def)
   618 
   619 lemma (in group) rcosetsI:
   620      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
   621 by (auto simp add: RCOSETS_def)
   622 
   623 
   624 text{*Really needed?*}
   625 lemma (in group) transpose_inv:
   626      "\<lbrakk>x \<cdot> y = z;  x \<in> carrier(G);  y \<in> carrier(G);  z \<in> carrier(G)\<rbrakk>
   627       \<Longrightarrow> (inv x) \<cdot> z = y"
   628 by (force simp add: m_assoc [symmetric])
   629 
   630 
   631 
   632 subsection {* Normal subgroups *}
   633 
   634 lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)"
   635   by (simp add: normal_def subgroup_def)
   636 
   637 lemma (in group) normalI: 
   638   "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   639 apply (simp add: normal_def normal_axioms_def, auto) 
   640   by (blast intro: prems)
   641 
   642 lemma (in normal) inv_op_closed1:
   643      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"
   644 apply (insert coset_eq) 
   645 apply (auto simp add: l_coset_def r_coset_def)
   646 apply (drule bspec, assumption)
   647 apply (drule equalityD1 [THEN subsetD], blast, clarify)
   648 apply (simp add: m_assoc)
   649 apply (simp add: m_assoc [symmetric])
   650 done
   651 
   652 lemma (in normal) inv_op_closed2:
   653      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H"
   654 apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H") 
   655 apply simp 
   656 apply (blast intro: inv_op_closed1) 
   657 done
   658 
   659 text{*Alternative characterization of normal subgroups*}
   660 lemma (in group) normal_inv_iff:
   661      "(N \<lhd> G) <->
   662       (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
   663       (is "_ <-> ?rhs")
   664 proof
   665   assume N: "N \<lhd> G"
   666   show ?rhs
   667     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   668 next
   669   assume ?rhs
   670   hence sg: "subgroup(N,G)" 
   671     and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto
   672   hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset) 
   673   show "N \<lhd> G"
   674   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   675     fix x
   676     assume x: "x \<in> carrier(G)"
   677     show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})"
   678     proof
   679       show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})"
   680       proof clarify
   681         fix n
   682         assume n: "n \<in> N" 
   683         show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})"
   684         proof (rule UN_I) 
   685           from closed [of "inv x"]
   686           show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n)
   687           show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}"
   688             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
   689         qed
   690       qed
   691     next
   692       show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})"
   693       proof clarify
   694         fix n
   695         assume n: "n \<in> N" 
   696         show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})"
   697         proof (rule UN_I) 
   698           show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed)
   699           show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}"
   700             by (simp add: x n m_assoc sb [THEN subsetD])
   701         qed
   702       qed
   703     qed
   704   qed
   705 qed
   706 
   707 
   708 subsection{*More Properties of Cosets*}
   709 
   710 lemma (in group) l_coset_subset_G:
   711      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier(G)"
   712 by (auto simp add: l_coset_def subsetD)
   713 
   714 lemma (in group) l_coset_swap:
   715      "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> x \<in> y <# H"
   716 proof (simp add: l_coset_def)
   717   assume "\<exists>h\<in>H. y = x \<cdot> h"
   718     and x: "x \<in> carrier(G)"
   719     and sb: "subgroup(H,G)"
   720   then obtain h' where h': "h' \<in> H & x \<cdot> h' = y" by blast
   721   show "\<exists>h\<in>H. x = y \<cdot> h"
   722   proof
   723     show "x = y \<cdot> inv h'" using h' x sb
   724       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])
   725     show "inv h' \<in> H" using h' sb
   726       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)
   727   qed
   728 qed
   729 
   730 lemma (in group) l_coset_carrier:
   731      "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> y \<in> carrier(G)"
   732 by (auto simp add: l_coset_def m_assoc
   733                    subgroup.subset [THEN subsetD] subgroup.m_closed)
   734 
   735 lemma (in group) l_repr_imp_subset:
   736   assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
   737   shows "y <# H \<subseteq> x <# H"
   738 proof -
   739   from y
   740   obtain h' where "h' \<in> H" "x \<cdot> h' = y" by (auto simp add: l_coset_def)
   741   thus ?thesis using x sb
   742     by (auto simp add: l_coset_def m_assoc
   743                        subgroup.subset [THEN subsetD] subgroup.m_closed)
   744 qed
   745 
   746 lemma (in group) l_repr_independence:
   747   assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"
   748   shows "x <# H = y <# H"
   749 proof
   750   show "x <# H \<subseteq> y <# H"
   751     by (rule l_repr_imp_subset,
   752         (blast intro: l_coset_swap l_coset_carrier y x sb)+)
   753   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])
   754 qed
   755 
   756 lemma (in group) setmult_subset_G:
   757      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)"
   758 by (auto simp add: set_mult_def subsetD)
   759 
   760 lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H"
   761 apply (rule equalityI) 
   762 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
   763 apply (rule_tac x = x in bexI)
   764 apply (rule bexI [of _ "\<one>"])
   765 apply (auto simp add: subgroup.m_closed subgroup.one_closed
   766                       r_one subgroup.subset [THEN subsetD])
   767 done
   768 
   769 
   770 subsubsection {* Set of inverses of an @{text r_coset}. *}
   771 
   772 lemma (in normal) rcos_inv:
   773   assumes x:     "x \<in> carrier(G)"
   774   shows "set_inv (H #> x) = H #> (inv x)" 
   775 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI)
   776   fix h
   777   assume "h \<in> H"
   778   show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"
   779   proof (rule UN_I)
   780     show "inv x \<cdot> inv h \<cdot> x \<in> H"
   781       by (simp add: inv_op_closed1 prems)
   782     show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"
   783       by (simp add: prems m_assoc)
   784   qed
   785 next
   786   fix h
   787   assume "h \<in> H"
   788   show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"
   789   proof (rule UN_I)
   790     show "x \<cdot> inv h \<cdot> inv x \<in> H"
   791       by (simp add: inv_op_closed2 prems)
   792     show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"
   793       by (simp add: prems m_assoc [symmetric] inv_mult_group)
   794   qed
   795 qed
   796 
   797 
   798 
   799 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
   800 
   801 lemma (in group) setmult_rcos_assoc:
   802      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
   803       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"
   804 by (force simp add: r_coset_def set_mult_def m_assoc)
   805 
   806 lemma (in group) rcos_assoc_lcos:
   807      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>
   808       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"
   809 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)
   810 
   811 lemma (in normal) rcos_mult_step1:
   812      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   813       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   814 by (simp add: setmult_rcos_assoc subset
   815               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)
   816 
   817 lemma (in normal) rcos_mult_step2:
   818      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   819       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   820 by (insert coset_eq, simp add: normal_def)
   821 
   822 lemma (in normal) rcos_mult_step3:
   823      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   824       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"
   825 by (simp add: setmult_rcos_assoc coset_mult_assoc
   826               subgroup_mult_id subset prems)
   827 
   828 lemma (in normal) rcos_sum:
   829      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>
   830       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<cdot> y)"
   831 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   832 
   833 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   834   -- {* generalizes @{text subgroup_mult_id} *}
   835   by (auto simp add: RCOSETS_def subset
   836         setmult_rcos_assoc subgroup_mult_id prems)
   837 
   838 
   839 subsubsection{*Two distinct right cosets are disjoint*}
   840 
   841 constdefs (structure G)
   842   r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60)
   843    "rcong H == {<x,y> \<in> carrier(G) * carrier(G). inv x \<cdot> y \<in> H}"
   844 
   845 
   846 lemma (in subgroup) equiv_rcong:
   847    includes group G
   848    shows "equiv (carrier(G), rcong H)"
   849 proof (simp add: equiv_def, intro conjI)
   850   show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
   851     by (auto simp add: r_congruent_def) 
   852 next
   853   show "refl (carrier(G), rcong H)"
   854     by (auto simp add: r_congruent_def refl_def) 
   855 next
   856   show "sym (rcong H)"
   857   proof (simp add: r_congruent_def sym_def, clarify)
   858     fix x y
   859     assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" 
   860        and "inv x \<cdot> y \<in> H"
   861     hence "inv (inv x \<cdot> y) \<in> H" by (simp add: m_inv_closed) 
   862     thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)
   863   qed
   864 next
   865   show "trans (rcong H)"
   866   proof (simp add: r_congruent_def trans_def, clarify)
   867     fix x y z
   868     assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
   869        and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H"
   870     hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp
   871     hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv) 
   872     thus "inv x \<cdot> z \<in> H" by simp
   873   qed
   874 qed
   875 
   876 text{*Equivalence classes of @{text rcong} correspond to left cosets.
   877   Was there a mistake in the definitions? I'd have expected them to
   878   correspond to right cosets.*}
   879 lemma (in subgroup) l_coset_eq_rcong:
   880   includes group G
   881   assumes a: "a \<in> carrier(G)"
   882   shows "a <# H = (rcong H) `` {a}" 
   883 by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
   884                 Collect_image_eq) 
   885 
   886 
   887 lemma (in group) rcos_equation:
   888   includes subgroup H G
   889   shows
   890      "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);  
   891         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   892       \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})"
   893 apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
   894 apply (simp add: m_assoc transpose_inv)
   895 done
   896 
   897 
   898 lemma (in group) rcos_disjoint:
   899   includes subgroup H G
   900   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0"
   901 apply (simp add: RCOSETS_def r_coset_def)
   902 apply (blast intro: rcos_equation prems sym)
   903 done
   904 
   905 
   906 subsection {*Order of a Group and Lagrange's Theorem*}
   907 
   908 constdefs
   909   order :: "i => i"
   910   "order(S) == |carrier(S)|"
   911 
   912 lemma (in group) rcos_self:
   913   includes subgroup
   914   shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x"
   915 apply (simp add: r_coset_def)
   916 apply (rule_tac x="\<one>" in bexI, auto) 
   917 done
   918 
   919 lemma (in group) rcosets_part_G:
   920   includes subgroup
   921   shows "\<Union>(rcosets H) = carrier(G)"
   922 apply (rule equalityI)
   923  apply (force simp add: RCOSETS_def r_coset_def)
   924 apply (auto simp add: RCOSETS_def intro: rcos_self prems)
   925 done
   926 
   927 lemma (in group) cosets_finite:
   928      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier(G);  Finite (carrier(G))\<rbrakk> \<Longrightarrow> Finite(c)"
   929 apply (auto simp add: RCOSETS_def)
   930 apply (simp add: r_coset_subset_G [THEN subset_Finite])
   931 done
   932 
   933 text{*More general than the HOL version, which also requires @{term G} to
   934       be finite.*}
   935 lemma (in group) card_cosets_equal:
   936   assumes H:   "H \<subseteq> carrier(G)"
   937   shows "c \<in> rcosets H \<Longrightarrow> |c| = |H|"
   938 proof (simp add: RCOSETS_def, clarify)
   939   fix a
   940   assume a: "a \<in> carrier(G)"
   941   show "|H #> a| = |H|"
   942   proof (rule eqpollI [THEN cardinal_cong])
   943     show "H #> a \<lesssim> H"
   944     proof (simp add: lepoll_def, intro exI) 
   945       show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)"
   946         by (auto intro: lam_type 
   947                  simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)
   948     qed
   949     show "H \<lesssim> H #> a"
   950     proof (simp add: lepoll_def, intro exI) 
   951       show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)"
   952         by (auto intro: lam_type 
   953                  simp add: inj_def r_coset_def  subsetD [OF H] a)
   954     qed
   955   qed
   956 qed
   957 
   958 
   959 lemma (in group) rcosets_subset_PowG:
   960      "subgroup(H,G) \<Longrightarrow> rcosets H \<subseteq> Pow(carrier(G))"
   961 apply (simp add: RCOSETS_def)
   962 apply (blast dest: r_coset_subset_G subgroup.subset)
   963 done
   964 
   965 theorem (in group) lagrange:
   966      "\<lbrakk>Finite(carrier(G)); subgroup(H,G)\<rbrakk>
   967       \<Longrightarrow> |rcosets H| #* |H| = order(G)"
   968 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   969 apply (subst mult_commute)
   970 apply (rule card_partition)
   971    apply (simp add: rcosets_subset_PowG [THEN subset_Finite])
   972   apply (simp add: rcosets_part_G)
   973  apply (simp add: card_cosets_equal [OF subgroup.subset])
   974 apply (simp add: rcos_disjoint)
   975 done
   976 
   977 
   978 subsection {*Quotient Groups: Factorization of a Group*}
   979 
   980 constdefs (structure G)
   981   FactGroup :: "[i,i] => i" (infixl "Mod" 65)
   982     --{*Actually defined for groups rather than monoids*}
   983   "G Mod H == 
   984      <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#> K2, H, 0>"
   985 
   986 lemma (in normal) setmult_closed:
   987      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   988 by (auto simp add: rcos_sum RCOSETS_def)
   989 
   990 lemma (in normal) setinv_closed:
   991      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
   992 by (auto simp add: rcos_inv RCOSETS_def)
   993 
   994 lemma (in normal) rcosets_assoc:
   995      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   996       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   997 by (auto simp add: RCOSETS_def rcos_sum m_assoc)
   998 
   999 lemma (in subgroup) subgroup_in_rcosets:
  1000   includes group G
  1001   shows "H \<in> rcosets H"
  1002 proof -
  1003   have "H #> \<one> = H"
  1004     by (rule coset_join2, auto)
  1005   then show ?thesis
  1006     by (auto simp add: RCOSETS_def intro: sym)
  1007 qed
  1008 
  1009 lemma (in normal) rcosets_inv_mult_group_eq:
  1010      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
  1011 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset prems)
  1012 
  1013 theorem (in normal) factorgroup_is_group:
  1014   "group (G Mod H)"
  1015 apply (simp add: FactGroup_def)
  1016 apply (rule groupI)
  1017     apply (simp add: setmult_closed)
  1018    apply (simp add: normal_imp_subgroup subgroup_in_rcosets)
  1019   apply (simp add: setmult_closed rcosets_assoc)
  1020  apply (simp add: normal_imp_subgroup
  1021                   subgroup_in_rcosets rcosets_mult_eq)
  1022 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
  1023 done
  1024 
  1025 lemma (in normal) inv_FactGroup:
  1026      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
  1027 apply (rule group.inv_equality [OF factorgroup_is_group]) 
  1028 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
  1029 done
  1030 
  1031 text{*The coset map is a homomorphism from @{term G} to the quotient group
  1032   @{term "G Mod H"}*}
  1033 lemma (in normal) r_coset_hom_Mod:
  1034   "(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)"
  1035 by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type) 
  1036 
  1037 
  1038 subsection{*The First Isomorphism Theorem*}
  1039 
  1040 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
  1041   range of that homomorphism.*}
  1042 
  1043 constdefs
  1044   kernel :: "[i,i,i] => i" 
  1045     --{*the kernel of a homomorphism*}
  1046   "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
  1047 
  1048 lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
  1049 apply (rule subgroup.intro) 
  1050 apply (auto simp add: kernel_def group.intro prems) 
  1051 done
  1052 
  1053 text{*The kernel of a homomorphism is a normal subgroup*}
  1054 lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G"
  1055 apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
  1056 apply (simp add: kernel_def)  
  1057 done
  1058 
  1059 lemma (in group_hom) FactGroup_nonempty:
  1060   assumes X: "X \<in> carrier (G Mod kernel(G,H,h))"
  1061   shows "X \<noteq> 0"
  1062 proof -
  1063   from X
  1064   obtain g where "g \<in> carrier(G)" 
  1065              and "X = kernel(G,H,h) #> g"
  1066     by (auto simp add: FactGroup_def RCOSETS_def)
  1067   thus ?thesis 
  1068    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
  1069 qed
  1070 
  1071 
  1072 lemma (in group_hom) FactGroup_contents_mem:
  1073   assumes X: "X \<in> carrier (G Mod (kernel(G,H,h)))"
  1074   shows "contents (h``X) \<in> carrier(H)"
  1075 proof -
  1076   from X
  1077   obtain g where g: "g \<in> carrier(G)" 
  1078              and "X = kernel(G,H,h) #> g"
  1079     by (auto simp add: FactGroup_def RCOSETS_def)
  1080   hence "h `` X = {h ` g}"
  1081     by (auto simp add: kernel_def r_coset_def image_UN 
  1082                        image_eq_UN [OF hom_is_fun] g)
  1083   thus ?thesis by (auto simp add: g)
  1084 qed
  1085 
  1086 lemma mult_FactGroup:
  1087      "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
  1088       ==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
  1089 by (simp add: FactGroup_def) 
  1090 
  1091 lemma (in normal) FactGroup_m_closed:
  1092      "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|] 
  1093       ==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)"
  1094 by (simp add: FactGroup_def setmult_closed) 
  1095 
  1096 lemma (in group_hom) FactGroup_hom:
  1097      "(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (h``X))
  1098       \<in> hom (G Mod (kernel(G,H,h)), H)" 
  1099 proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)  
  1100   fix X and X'
  1101   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
  1102      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
  1103   then
  1104   obtain g and g'
  1105            where "g \<in> carrier(G)" and "g' \<in> carrier(G)" 
  1106              and "X = kernel(G,H,h) #> g" and "X' = kernel(G,H,h) #> g'"
  1107     by (auto simp add: FactGroup_def RCOSETS_def)
  1108   hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'" 
  1109     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
  1110     by (force simp add: kernel_def r_coset_def image_def)+
  1111   hence "h `` (X <#> X') = {h ` g \<cdot>\<^bsub>H\<^esub> h ` g'}" using X X'
  1112     by (auto dest!: FactGroup_nonempty
  1113              simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN
  1114                        subsetD [OF Xsub] subsetD [OF X'sub]) 
  1115   thus "contents (h `` (X <#> X')) = contents (h `` X) \<cdot>\<^bsub>H\<^esub> contents (h `` X')"
  1116     by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
  1117                   X X' Xsub X'sub)
  1118 qed
  1119 
  1120 
  1121 text{*Lemma for the following injectivity result*}
  1122 lemma (in group_hom) FactGroup_subset:
  1123      "\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h ` g = h ` g'\<rbrakk>
  1124       \<Longrightarrow>  kernel(G,H,h) #> g \<subseteq> kernel(G,H,h) #> g'"
  1125 apply (clarsimp simp add: kernel_def r_coset_def image_def)
  1126 apply (rename_tac y)  
  1127 apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI) 
  1128 apply (simp_all add: G.m_assoc) 
  1129 done
  1130 
  1131 lemma (in group_hom) FactGroup_inj:
  1132      "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
  1133       \<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))"
  1134 proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify) 
  1135   fix X and X'
  1136   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"
  1137      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"
  1138   then
  1139   obtain g and g'
  1140            where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)" 
  1141               "X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'"
  1142     by (auto simp add: FactGroup_def RCOSETS_def)
  1143   hence all: "\<forall>x\<in>X. h ` x = h ` g" "\<forall>x\<in>X'. h ` x = h ` g'"
  1144     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"
  1145     by (force simp add: kernel_def r_coset_def image_def)+
  1146   assume "contents (h `` X) = contents (h `` X')"
  1147   hence h: "h ` g = h ` g'"
  1148     by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty 
  1149                   X X' Xsub X'sub)
  1150   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
  1151 qed
  1152 
  1153 
  1154 lemma (in group_hom) kernel_rcoset_subset:
  1155   assumes g: "g \<in> carrier(G)"
  1156   shows "kernel(G,H,h) #> g \<subseteq> carrier (G)"
  1157     by (auto simp add: g kernel_def r_coset_def) 
  1158 
  1159 
  1160 
  1161 text{*If the homomorphism @{term h} is onto @{term H}, then so is the
  1162 homomorphism from the quotient group*}
  1163 lemma (in group_hom) FactGroup_surj:
  1164   assumes h: "h \<in> surj(carrier(G), carrier(H))"
  1165   shows "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h `` X))
  1166          \<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))"
  1167 proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)
  1168   fix y
  1169   assume y: "y \<in> carrier(H)"
  1170   with h obtain g where g: "g \<in> carrier(G)" "h ` g = y"
  1171     by (auto simp add: surj_def) 
  1172   hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h ` x}) = {y}" 
  1173     by (auto simp add: y kernel_def r_coset_def) 
  1174   with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h `` x) = y"
  1175         --{*The witness is @{term "kernel(G,H,h) #> g"}*}
  1176     by (force simp add: FactGroup_def RCOSETS_def 
  1177            image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)
  1178 qed
  1179 
  1180 
  1181 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
  1182  quotient group @{term "G Mod (kernel(G,H,h))"} is isomorphic to @{term H}.*}
  1183 theorem (in group_hom) FactGroup_iso:
  1184   "h \<in> surj(carrier(G), carrier(H))
  1185    \<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h``X)) \<in> (G Mod (kernel(G,H,h))) \<cong> H"
  1186 by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)
  1187  
  1188 end