src/ZF/ex/Group.thy
 author paulson Tue Mar 06 15:15:49 2012 +0000 (2012-03-06) changeset 46820 c656222c4dc1 parent 41524 4d2f9a1c24c7 child 46822 95f1e700b712 permissions -rw-r--r--
mathematical symbols instead of ASCII
     1 (*  Title:      ZF/ex/Group.thy *)

     2

     3 header {* Groups *}

     4

     5 theory Group imports Main begin

     6

     7 text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and

     8 Markus Wenzel.*}

     9

    10

    11 subsection {* Monoids *}

    12

    13 (*First, we must simulate a record declaration:

    14 record monoid =

    15   carrier :: i

    16   mult :: "[i,i] => i" (infixl "\<cdot>\<index>" 70)

    17   one :: i ("\<one>\<index>")

    18 *)

    19

    20 definition

    21   carrier :: "i => i" where

    22   "carrier(M) == fst(M)"

    23

    24 definition

    25   mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where

    26   "mmult(M,x,y) == fst(snd(M))  <x,y>"

    27

    28 definition

    29   one :: "i => i" ("\<one>\<index>") where

    30   "one(M) == fst(snd(snd(M)))"

    31

    32 definition

    33   update_carrier :: "[i,i] => i" where

    34   "update_carrier(M,A) == <A,snd(M)>"

    35

    36 definition

    37   m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where

    38   "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"

    39

    40 locale monoid = fixes G (structure)

    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)" by (rule group_axioms)

    93

    94 theorem groupI:

    95   fixes G (structure)

    96   assumes m_closed [simp]:

    97       "\<And>x y. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"

    98     and one_closed [simp]: "\<one> \<in> carrier(G)"

    99     and m_assoc:

   100       "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>

   101       (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"

   102     and l_one [simp]: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<one> \<cdot> x = x"

   103     and l_inv_ex: "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one>"

   104   shows "group(G)"

   105 proof -

   106   have l_cancel [simp]:

   107     "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>

   108     (x \<cdot> y = x \<cdot> z) <-> (y = z)"

   109   proof

   110     fix x y z

   111     assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"

   112     {

   113       assume eq: "x \<cdot> y = x \<cdot> z"

   114       with G l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"

   115         and l_inv: "x_inv \<cdot> x = \<one>" by fast

   116       from G eq xG have "(x_inv \<cdot> x) \<cdot> y = (x_inv \<cdot> x) \<cdot> z"

   117         by (simp add: m_assoc)

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

   119     next

   120       assume eq: "y = z"

   121       with G show "x \<cdot> y = x \<cdot> z" by simp

   122     }

   123   qed

   124   have r_one:

   125     "\<And>x. x \<in> carrier(G) \<Longrightarrow> x \<cdot> \<one> = x"

   126   proof -

   127     fix x

   128     assume x: "x \<in> carrier(G)"

   129     with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier(G)"

   130       and l_inv: "x_inv \<cdot> x = \<one>" by fast

   131     from x xG have "x_inv \<cdot> (x \<cdot> \<one>) = x_inv \<cdot> x"

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

   133     with x xG show "x \<cdot> \<one> = x" by simp

   134   qed

   135   have inv_ex:

   136     "!!x. x \<in> carrier(G) ==> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"

   137   proof -

   138     fix x

   139     assume x: "x \<in> carrier(G)"

   140     with l_inv_ex obtain y where y: "y \<in> carrier(G)"

   141       and l_inv: "y \<cdot> x = \<one>" by fast

   142     from x y have "y \<cdot> (x \<cdot> y) = y \<cdot> \<one>"

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

   144     with x y have r_inv: "x \<cdot> y = \<one>"

   145       by simp

   146     from x y show "\<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"

   147       by (fast intro: l_inv r_inv)

   148   qed

   149   show ?thesis

   150     by (blast intro: group.intro monoid.intro group_axioms.intro

   151                      assms r_one inv_ex)

   152 qed

   153

   154 lemma (in group) inv [simp]:

   155   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) & inv x \<cdot> x = \<one> & x \<cdot> inv x = \<one>"

   156   apply (frule inv_ex)

   157   apply (unfold Bex_def m_inv_def)

   158   apply (erule exE)

   159   apply (rule theI)

   160   apply (rule ex1I, assumption)

   161    apply (blast intro: inv_unique)

   162   done

   163

   164 lemma (in group) inv_closed [intro!]:

   165   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G)"

   166   by simp

   167

   168 lemma (in group) l_inv:

   169   "x \<in> carrier(G) \<Longrightarrow> inv x \<cdot> x = \<one>"

   170   by simp

   171

   172 lemma (in group) r_inv:

   173   "x \<in> carrier(G) \<Longrightarrow> x \<cdot> inv x = \<one>"

   174   by simp

   175

   176

   177 subsection {* Cancellation Laws and Basic Properties *}

   178

   179 lemma (in group) l_cancel [simp]:

   180   assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"

   181   shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"

   182 proof

   183   assume eq: "x \<cdot> y = x \<cdot> z"

   184   hence  "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"

   185     by (simp only: m_assoc inv_closed assms)

   186   thus "y = z" by (simp add: assms)

   187 next

   188   assume eq: "y = z"

   189   then show "x \<cdot> y = x \<cdot> z" by simp

   190 qed

   191

   192 lemma (in group) r_cancel [simp]:

   193   assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"

   194   shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"

   195 proof

   196   assume eq: "y \<cdot> x = z \<cdot> x"

   197   then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"

   198     by (simp only: m_assoc [symmetric] inv_closed assms)

   199   thus "y = z" by (simp add: assms)

   200 next

   201   assume eq: "y = z"

   202   thus  "y \<cdot> x = z \<cdot> x" by simp

   203 qed

   204

   205 lemma (in group) inv_comm:

   206   assumes inv: "x \<cdot> y = \<one>"

   207       and G: "x \<in> carrier(G)"  "y \<in> carrier(G)"

   208   shows "y \<cdot> x = \<one>"

   209 proof -

   210   from G have "x \<cdot> y \<cdot> x = x \<cdot> \<one>" by (auto simp add: inv)

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

   212 qed

   213

   214 lemma (in group) inv_equality:

   215      "\<lbrakk>y \<cdot> x = \<one>; x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv x = y"

   216 apply (simp add: m_inv_def)

   217 apply (rule the_equality)

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

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

   220 done

   221

   222 lemma (in group) inv_one [simp]:

   223   "inv \<one> = \<one>"

   224   by (auto intro: inv_equality)

   225

   226 lemma (in group) inv_inv [simp]: "x \<in> carrier(G) \<Longrightarrow> inv (inv x) = x"

   227   by (auto intro: inv_equality)

   228

   229 text{*This proof is by cancellation*}

   230 lemma (in group) inv_mult_group:

   231   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv y \<cdot> inv x"

   232 proof -

   233   assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"

   234   then have "inv (x \<cdot> y) \<cdot> (x \<cdot> y) = (inv y \<cdot> inv x) \<cdot> (x \<cdot> y)"

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

   236   with G show ?thesis by (simp_all del: inv add: inv_closed)

   237 qed

   238

   239

   240 subsection {* Substructures *}

   241

   242 locale subgroup = fixes H and G (structure)

   243   assumes subset: "H \<subseteq> carrier(G)"

   244     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"

   245     and  one_closed [simp]: "\<one> \<in> H"

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

   247

   248

   249 lemma (in subgroup) mem_carrier [simp]:

   250   "x \<in> H \<Longrightarrow> x \<in> carrier(G)"

   251   using subset by blast

   252

   253

   254 lemma subgroup_imp_subset:

   255   "subgroup(H,G) \<Longrightarrow> H \<subseteq> carrier(G)"

   256   by (rule subgroup.subset)

   257

   258 lemma (in subgroup) group_axiomsI [intro]:

   259   assumes "group(G)"

   260   shows "group_axioms (update_carrier(G,H))"

   261 proof -

   262   interpret group G by fact

   263   show ?thesis by (force intro: group_axioms.intro l_inv r_inv)

   264 qed

   265

   266 lemma (in subgroup) is_group [intro]:

   267   assumes "group(G)"

   268   shows "group (update_carrier(G,H))"

   269 proof -

   270   interpret group G by fact

   271   show ?thesis

   272   by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)

   273 qed

   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 text {*

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

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

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

   285 *}

   286

   287 lemma (in group) one_in_subset:

   288   "\<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>

   289    \<Longrightarrow> \<one> \<in> H"

   290 by (force simp add: l_inv)

   291

   292 text {* A characterization of subgroups: closed, non-empty subset. *}

   293

   294 declare monoid.one_closed [simp] group.inv_closed [simp]

   295   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]

   296

   297 lemma subgroup_nonempty:

   298   "~ subgroup(0,G)"

   299   by (blast dest: subgroup.one_closed)

   300

   301

   302 subsection {* Direct Products *}

   303

   304 definition

   305   DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80) where

   306   "G \<Otimes> H == <carrier(G) \<times> carrier(H),

   307               (\<lambda><<g,h>, <g', h'>>

   308                    \<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).

   309                 <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>),

   310               <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>, 0>"

   311

   312 lemma DirProdGroup_group:

   313   assumes "group(G)" and "group(H)"

   314   shows "group (G \<Otimes> H)"

   315 proof -

   316   interpret G: group G by fact

   317   interpret H: group H by fact

   318   show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv

   319           simp add: DirProdGroup_def)

   320 qed

   321

   322 lemma carrier_DirProdGroup [simp]:

   323      "carrier (G \<Otimes> H) = carrier(G) \<times> carrier(H)"

   324   by (simp add: DirProdGroup_def)

   325

   326 lemma one_DirProdGroup [simp]:

   327      "\<one>\<^bsub>G \<Otimes> H\<^esub> = <\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>>"

   328   by (simp add: DirProdGroup_def)

   329

   330 lemma mult_DirProdGroup [simp]:

   331      "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]

   332       ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"

   333   by (simp add: DirProdGroup_def)

   334

   335 lemma inv_DirProdGroup [simp]:

   336   assumes "group(G)" and "group(H)"

   337   assumes g: "g \<in> carrier(G)"

   338       and h: "h \<in> carrier(H)"

   339   shows "inv \<^bsub>G \<Otimes> H\<^esub> <g, h> = <inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h>"

   340   apply (rule group.inv_equality [OF DirProdGroup_group])

   341   apply (simp_all add: assms group.l_inv)

   342   done

   343

   344 subsection {* Isomorphisms *}

   345

   346 definition

   347   hom :: "[i,i] => i" where

   348   "hom(G,H) ==

   349     {h \<in> carrier(G) -> carrier(H).

   350       (\<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))}"

   351

   352 lemma hom_mult:

   353   "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>

   354    \<Longrightarrow> h  (x \<cdot>\<^bsub>G\<^esub> y) = h  x \<cdot>\<^bsub>H\<^esub> h  y"

   355   by (simp add: hom_def)

   356

   357 lemma hom_closed:

   358   "\<lbrakk>h \<in> hom(G,H); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h  x \<in> carrier(H)"

   359   by (auto simp add: hom_def)

   360

   361 lemma (in group) hom_compose:

   362      "\<lbrakk>h \<in> hom(G,H); i \<in> hom(H,I)\<rbrakk> \<Longrightarrow> i O h \<in> hom(G,I)"

   363 by (force simp add: hom_def comp_fun)

   364

   365 lemma hom_is_fun:

   366   "h \<in> hom(G,H) \<Longrightarrow> h \<in> carrier(G) -> carrier(H)"

   367   by (simp add: hom_def)

   368

   369

   370 subsection {* Isomorphisms *}

   371

   372 definition

   373   iso :: "[i,i] => i"  (infixr "\<cong>" 60) where

   374   "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"

   375

   376 lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"

   377   by (simp add: iso_def hom_def id_type id_bij)

   378

   379

   380 lemma (in group) iso_sym:

   381      "h \<in> G \<cong> H \<Longrightarrow> converse(h) \<in> H \<cong> G"

   382 apply (simp add: iso_def bij_converse_bij, clarify)

   383 apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)")

   384  prefer 2 apply (simp add: bij_converse_bij bij_is_fun)

   385 apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]

   386             simp add: hom_def bij_is_inj right_inverse_bij);

   387 done

   388

   389 lemma (in group) iso_trans:

   390      "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"

   391   by (auto simp add: iso_def hom_compose comp_bij)

   392

   393 lemma DirProdGroup_commute_iso:

   394   assumes "group(G)" and "group(H)"

   395   shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"

   396 proof -

   397   interpret group G by fact

   398   interpret group H by fact

   399   show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)

   400 qed

   401

   402 lemma DirProdGroup_assoc_iso:

   403   assumes "group(G)" and "group(H)" and "group(I)"

   404   shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)

   405           \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"

   406 proof -

   407   interpret group G by fact

   408   interpret group H by fact

   409   interpret group I by fact

   410   show ?thesis

   411     by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)

   412 qed

   413

   414 text{*Basis for homomorphism proofs: we assume two groups @{term G} and

   415   @{term H}, with a homomorphism @{term h} between them*}

   416 locale group_hom = G: group G + H: group H

   417   for G (structure) and H (structure) and h +

   418   assumes homh: "h \<in> hom(G,H)"

   419   notes hom_mult [simp] = hom_mult [OF homh]

   420     and hom_closed [simp] = hom_closed [OF homh]

   421     and hom_is_fun [simp] = hom_is_fun [OF homh]

   422

   423 lemma (in group_hom) one_closed [simp]:

   424   "h  \<one> \<in> carrier(H)"

   425   by simp

   426

   427 lemma (in group_hom) hom_one [simp]:

   428   "h  \<one> = \<one>\<^bsub>H\<^esub>"

   429 proof -

   430   have "h  \<one> \<cdot>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = (h  \<one>) \<cdot>\<^bsub>H\<^esub> (h  \<one>)"

   431     by (simp add: hom_mult [symmetric] del: hom_mult)

   432   then show ?thesis by (simp del: r_one)

   433 qed

   434

   435 lemma (in group_hom) inv_closed [simp]:

   436   "x \<in> carrier(G) \<Longrightarrow> h  (inv x) \<in> carrier(H)"

   437   by simp

   438

   439 lemma (in group_hom) hom_inv [simp]:

   440   "x \<in> carrier(G) \<Longrightarrow> h  (inv x) = inv\<^bsub>H\<^esub> (h  x)"

   441 proof -

   442   assume x: "x \<in> carrier(G)"

   443   then have "h  x \<cdot>\<^bsub>H\<^esub> h  (inv x) = \<one>\<^bsub>H\<^esub>"

   444     by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)

   445   also from x have "... = h  x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h  x)"

   446     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)

   447   finally have "h  x \<cdot>\<^bsub>H\<^esub> h  (inv x) = h  x \<cdot>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h  x)" .

   448   with x show ?thesis by (simp del: inv)

   449 qed

   450

   451 subsection {* Commutative Structures *}

   452

   453 text {*

   454   Naming convention: multiplicative structures that are commutative

   455   are called \emph{commutative}, additive structures are called

   456   \emph{Abelian}.

   457 *}

   458

   459 subsection {* Definition *}

   460

   461 locale comm_monoid = monoid +

   462   assumes m_comm: "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y = y \<cdot> x"

   463

   464 lemma (in comm_monoid) m_lcomm:

   465   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>

   466    x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"

   467 proof -

   468   assume xyz: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"

   469   from xyz have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by (simp add: m_assoc)

   470   also from xyz have "... = (y \<cdot> x) \<cdot> z" by (simp add: m_comm)

   471   also from xyz have "... = y \<cdot> (x \<cdot> z)" by (simp add: m_assoc)

   472   finally show ?thesis .

   473 qed

   474

   475 lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm

   476

   477 locale comm_group = comm_monoid + group

   478

   479 lemma (in comm_group) inv_mult:

   480   "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> inv (x \<cdot> y) = inv x \<cdot> inv y"

   481   by (simp add: m_ac inv_mult_group)

   482

   483

   484 lemma (in group) subgroup_self: "subgroup (carrier(G),G)"

   485 by (simp add: subgroup_def)

   486

   487 lemma (in group) subgroup_imp_group:

   488   "subgroup(H,G) \<Longrightarrow> group (update_carrier(G,H))"

   489 by (simp add: subgroup.is_group)

   490

   491 lemma (in group) subgroupI:

   492   assumes subset: "H \<subseteq> carrier(G)" and non_empty: "H \<noteq> 0"

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

   494     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<cdot> b \<in> H"

   495   shows "subgroup(H,G)"

   496 proof (simp add: subgroup_def assms)

   497   show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: assms)

   498 qed

   499

   500

   501 subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}

   502

   503 definition

   504   BijGroup :: "i=>i" where

   505   "BijGroup(S) ==

   506     <bij(S,S),

   507      \<lambda><g,f> \<in> bij(S,S) \<times> bij(S,S). g O f,

   508      id(S), 0>"

   509

   510

   511 subsection {*Bijections Form a Group *}

   512

   513 theorem group_BijGroup: "group(BijGroup(S))"

   514 apply (simp add: BijGroup_def)

   515 apply (rule groupI)

   516     apply (simp_all add: id_bij comp_bij comp_assoc)

   517  apply (simp add: id_bij bij_is_fun left_comp_id [of _ S S] fun_is_rel)

   518 apply (blast intro: left_comp_inverse bij_is_inj bij_converse_bij)

   519 done

   520

   521

   522 subsection{*Automorphisms Form a Group*}

   523

   524 lemma Bij_Inv_mem: "\<lbrakk>f \<in> bij(S,S);  x \<in> S\<rbrakk> \<Longrightarrow> converse(f)  x \<in> S"

   525 by (blast intro: apply_funtype bij_is_fun bij_converse_bij)

   526

   527 lemma inv_BijGroup: "f \<in> bij(S,S) \<Longrightarrow> m_inv (BijGroup(S), f) = converse(f)"

   528 apply (rule group.inv_equality)

   529 apply (rule group_BijGroup)

   530 apply (simp_all add: BijGroup_def bij_converse_bij

   531           left_comp_inverse [OF bij_is_inj])

   532 done

   533

   534 lemma iso_is_bij: "h \<in> G \<cong> H ==> h \<in> bij(carrier(G), carrier(H))"

   535 by (simp add: iso_def)

   536

   537

   538 definition

   539   auto :: "i=>i" where

   540   "auto(G) == iso(G,G)"

   541

   542 definition

   543   AutoGroup :: "i=>i" where

   544   "AutoGroup(G) == update_carrier(BijGroup(carrier(G)), auto(G))"

   545

   546

   547 lemma (in group) id_in_auto: "id(carrier(G)) \<in> auto(G)"

   548   by (simp add: iso_refl auto_def)

   549

   550 lemma (in group) subgroup_auto:

   551       "subgroup (auto(G)) (BijGroup (carrier(G)))"

   552 proof (rule subgroup.intro)

   553   show "auto(G) \<subseteq> carrier (BijGroup (carrier(G)))"

   554     by (auto simp add: auto_def BijGroup_def iso_def)

   555 next

   556   fix x y

   557   assume "x \<in> auto(G)" "y \<in> auto(G)"

   558   thus "x \<cdot>\<^bsub>BijGroup (carrier(G))\<^esub> y \<in> auto(G)"

   559     by (auto simp add: BijGroup_def auto_def iso_def bij_is_fun

   560                        group.hom_compose comp_bij)

   561 next

   562   show "\<one>\<^bsub>BijGroup (carrier(G))\<^esub> \<in> auto(G)" by (simp add:  BijGroup_def id_in_auto)

   563 next

   564   fix x

   565   assume "x \<in> auto(G)"

   566   thus "inv\<^bsub>BijGroup (carrier(G))\<^esub> x \<in> auto(G)"

   567     by (simp add: auto_def inv_BijGroup iso_is_bij iso_sym)

   568 qed

   569

   570 theorem (in group) AutoGroup: "group (AutoGroup(G))"

   571 by (simp add: AutoGroup_def subgroup.is_group subgroup_auto group_BijGroup)

   572

   573

   574

   575 subsection{*Cosets and Quotient Groups*}

   576

   577 definition

   578   r_coset  :: "[i,i,i] => i"  (infixl "#>\<index>" 60) where

   579   "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"

   580

   581 definition

   582   l_coset  :: "[i,i,i] => i"  (infixl "<#\<index>" 60) where

   583   "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"

   584

   585 definition

   586   RCOSETS  :: "[i,i] => i"  ("rcosets\<index> _" [81] 80) where

   587   "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"

   588

   589 definition

   590   set_mult :: "[i,i,i] => i"  (infixl "<#>\<index>" 60) where

   591   "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"

   592

   593 definition

   594   SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80) where

   595   "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"

   596

   597

   598 locale normal = subgroup + group +

   599   assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"

   600

   601 notation

   602   normal  (infixl "\<lhd>" 60)

   603

   604

   605 subsection {*Basic Properties of Cosets*}

   606

   607 lemma (in group) coset_mult_assoc:

   608      "\<lbrakk>M \<subseteq> carrier(G); g \<in> carrier(G); h \<in> carrier(G)\<rbrakk>

   609       \<Longrightarrow> (M #> g) #> h = M #> (g \<cdot> h)"

   610 by (force simp add: r_coset_def m_assoc)

   611

   612 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier(G) \<Longrightarrow> M #> \<one> = M"

   613 by (force simp add: r_coset_def)

   614

   615 lemma (in group) solve_equation:

   616     "\<lbrakk>subgroup(H,G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<cdot> x"

   617 apply (rule bexI [of _ "y \<cdot> (inv x)"])

   618 apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc

   619                       subgroup.subset [THEN subsetD])

   620 done

   621

   622 lemma (in group) repr_independence:

   623      "\<lbrakk>y \<in> H #> x;  x \<in> carrier(G); subgroup(H,G)\<rbrakk> \<Longrightarrow> H #> x = H #> y"

   624 by (auto simp add: r_coset_def m_assoc [symmetric]

   625                    subgroup.subset [THEN subsetD]

   626                    subgroup.m_closed solve_equation)

   627

   628 lemma (in group) coset_join2:

   629      "\<lbrakk>x \<in> carrier(G);  subgroup(H,G);  x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H"

   630   --{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*}

   631 by (force simp add: subgroup.m_closed r_coset_def solve_equation)

   632

   633 lemma (in group) r_coset_subset_G:

   634      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier(G)"

   635 by (auto simp add: r_coset_def)

   636

   637 lemma (in group) rcosI:

   638      "\<lbrakk>h \<in> H; H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> h \<cdot> x \<in> H #> x"

   639 by (auto simp add: r_coset_def)

   640

   641 lemma (in group) rcosetsI:

   642      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"

   643 by (auto simp add: RCOSETS_def)

   644

   645

   646 text{*Really needed?*}

   647 lemma (in group) transpose_inv:

   648      "\<lbrakk>x \<cdot> y = z;  x \<in> carrier(G);  y \<in> carrier(G);  z \<in> carrier(G)\<rbrakk>

   649       \<Longrightarrow> (inv x) \<cdot> z = y"

   650 by (force simp add: m_assoc [symmetric])

   651

   652

   653

   654 subsection {* Normal subgroups *}

   655

   656 lemma normal_imp_subgroup: "H \<lhd> G ==> subgroup(H,G)"

   657   by (simp add: normal_def subgroup_def)

   658

   659 lemma (in group) normalI:

   660   "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";

   661   by (simp add: normal_def normal_axioms_def)

   662

   663 lemma (in normal) inv_op_closed1:

   664      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<cdot> h \<cdot> x \<in> H"

   665 apply (insert coset_eq)

   666 apply (auto simp add: l_coset_def r_coset_def)

   667 apply (drule bspec, assumption)

   668 apply (drule equalityD1 [THEN subsetD], blast, clarify)

   669 apply (simp add: m_assoc)

   670 apply (simp add: m_assoc [symmetric])

   671 done

   672

   673 lemma (in normal) inv_op_closed2:

   674      "\<lbrakk>x \<in> carrier(G); h \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> h \<cdot> (inv x) \<in> H"

   675 apply (subgoal_tac "inv (inv x) \<cdot> h \<cdot> (inv x) \<in> H")

   676 apply simp

   677 apply (blast intro: inv_op_closed1)

   678 done

   679

   680 text{*Alternative characterization of normal subgroups*}

   681 lemma (in group) normal_inv_iff:

   682      "(N \<lhd> G) <->

   683       (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"

   684       (is "_ <-> ?rhs")

   685 proof

   686   assume N: "N \<lhd> G"

   687   show ?rhs

   688     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup)

   689 next

   690   assume ?rhs

   691   hence sg: "subgroup(N,G)"

   692     and closed: "\<And>x. x\<in>carrier(G) \<Longrightarrow> \<forall>h\<in>N. x \<cdot> h \<cdot> inv x \<in> N" by auto

   693   hence sb: "N \<subseteq> carrier(G)" by (simp add: subgroup.subset)

   694   show "N \<lhd> G"

   695   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)

   696     fix x

   697     assume x: "x \<in> carrier(G)"

   698     show "(\<Union>h\<in>N. {h \<cdot> x}) = (\<Union>h\<in>N. {x \<cdot> h})"

   699     proof

   700       show "(\<Union>h\<in>N. {h \<cdot> x}) \<subseteq> (\<Union>h\<in>N. {x \<cdot> h})"

   701       proof clarify

   702         fix n

   703         assume n: "n \<in> N"

   704         show "n \<cdot> x \<in> (\<Union>h\<in>N. {x \<cdot> h})"

   705         proof (rule UN_I)

   706           from closed [of "inv x"]

   707           show "inv x \<cdot> n \<cdot> x \<in> N" by (simp add: x n)

   708           show "n \<cdot> x \<in> {x \<cdot> (inv x \<cdot> n \<cdot> x)}"

   709             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])

   710         qed

   711       qed

   712     next

   713       show "(\<Union>h\<in>N. {x \<cdot> h}) \<subseteq> (\<Union>h\<in>N. {h \<cdot> x})"

   714       proof clarify

   715         fix n

   716         assume n: "n \<in> N"

   717         show "x \<cdot> n \<in> (\<Union>h\<in>N. {h \<cdot> x})"

   718         proof (rule UN_I)

   719           show "x \<cdot> n \<cdot> inv x \<in> N" by (simp add: x n closed)

   720           show "x \<cdot> n \<in> {x \<cdot> n \<cdot> inv x \<cdot> x}"

   721             by (simp add: x n m_assoc sb [THEN subsetD])

   722         qed

   723       qed

   724     qed

   725   qed

   726 qed

   727

   728

   729 subsection{*More Properties of Cosets*}

   730

   731 lemma (in group) l_coset_subset_G:

   732      "\<lbrakk>H \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier(G)"

   733 by (auto simp add: l_coset_def subsetD)

   734

   735 lemma (in group) l_coset_swap:

   736      "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> x \<in> y <# H"

   737 proof (simp add: l_coset_def)

   738   assume "\<exists>h\<in>H. y = x \<cdot> h"

   739     and x: "x \<in> carrier(G)"

   740     and sb: "subgroup(H,G)"

   741   then obtain h' where h': "h' \<in> H & x \<cdot> h' = y" by blast

   742   show "\<exists>h\<in>H. x = y \<cdot> h"

   743   proof

   744     show "x = y \<cdot> inv h'" using h' x sb

   745       by (auto simp add: m_assoc subgroup.subset [THEN subsetD])

   746     show "inv h' \<in> H" using h' sb

   747       by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed)

   748   qed

   749 qed

   750

   751 lemma (in group) l_coset_carrier:

   752      "\<lbrakk>y \<in> x <# H;  x \<in> carrier(G);  subgroup(H,G)\<rbrakk> \<Longrightarrow> y \<in> carrier(G)"

   753 by (auto simp add: l_coset_def m_assoc

   754                    subgroup.subset [THEN subsetD] subgroup.m_closed)

   755

   756 lemma (in group) l_repr_imp_subset:

   757   assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"

   758   shows "y <# H \<subseteq> x <# H"

   759 proof -

   760   from y

   761   obtain h' where "h' \<in> H" "x \<cdot> h' = y" by (auto simp add: l_coset_def)

   762   thus ?thesis using x sb

   763     by (auto simp add: l_coset_def m_assoc

   764                        subgroup.subset [THEN subsetD] subgroup.m_closed)

   765 qed

   766

   767 lemma (in group) l_repr_independence:

   768   assumes y: "y \<in> x <# H" and x: "x \<in> carrier(G)" and sb: "subgroup(H,G)"

   769   shows "x <# H = y <# H"

   770 proof

   771   show "x <# H \<subseteq> y <# H"

   772     by (rule l_repr_imp_subset,

   773         (blast intro: l_coset_swap l_coset_carrier y x sb)+)

   774   show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb])

   775 qed

   776

   777 lemma (in group) setmult_subset_G:

   778      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G)\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier(G)"

   779 by (auto simp add: set_mult_def subsetD)

   780

   781 lemma (in group) subgroup_mult_id: "subgroup(H,G) \<Longrightarrow> H <#> H = H"

   782 apply (rule equalityI)

   783 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)

   784 apply (rule_tac x = x in bexI)

   785 apply (rule bexI [of _ "\<one>"])

   786 apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])

   787 done

   788

   789

   790 subsubsection {* Set of inverses of an @{text r_coset}. *}

   791

   792 lemma (in normal) rcos_inv:

   793   assumes x:     "x \<in> carrier(G)"

   794   shows "set_inv (H #> x) = H #> (inv x)"

   795 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe intro!: equalityI)

   796   fix h

   797   assume h: "h \<in> H"

   798   {

   799     show "inv x \<cdot> inv h \<in> (\<Union>j\<in>H. {j \<cdot> inv x})"

   800     proof (rule UN_I)

   801       show "inv x \<cdot> inv h \<cdot> x \<in> H"

   802         by (simp add: inv_op_closed1 h x)

   803       show "inv x \<cdot> inv h \<in> {inv x \<cdot> inv h \<cdot> x \<cdot> inv x}"

   804         by (simp add: h x m_assoc)

   805     qed

   806   next

   807     show "h \<cdot> inv x \<in> (\<Union>j\<in>H. {inv x \<cdot> inv j})"

   808     proof (rule UN_I)

   809       show "x \<cdot> inv h \<cdot> inv x \<in> H"

   810         by (simp add: inv_op_closed2 h x)

   811       show "h \<cdot> inv x \<in> {inv x \<cdot> inv (x \<cdot> inv h \<cdot> inv x)}"

   812         by (simp add: h x m_assoc [symmetric] inv_mult_group)

   813     qed

   814   }

   815 qed

   816

   817

   818

   819 subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}

   820

   821 lemma (in group) setmult_rcos_assoc:

   822      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>

   823       \<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x"

   824 by (force simp add: r_coset_def set_mult_def m_assoc)

   825

   826 lemma (in group) rcos_assoc_lcos:

   827      "\<lbrakk>H \<subseteq> carrier(G); K \<subseteq> carrier(G); x \<in> carrier(G)\<rbrakk>

   828       \<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)"

   829 by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc)

   830

   831 lemma (in normal) rcos_mult_step1:

   832      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>

   833       \<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"

   834 by (simp add: setmult_rcos_assoc subset

   835               r_coset_subset_G l_coset_subset_G rcos_assoc_lcos)

   836

   837 lemma (in normal) rcos_mult_step2:

   838      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>

   839       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"

   840 by (insert coset_eq, simp add: normal_def)

   841

   842 lemma (in normal) rcos_mult_step3:

   843      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>

   844       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<cdot> y)"

   845   by (simp add: setmult_rcos_assoc coset_mult_assoc

   846               subgroup_mult_id subset normal_axioms normal.axioms)

   847

   848 lemma (in normal) rcos_sum:

   849      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk>

   850       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<cdot> y)"

   851 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)

   852

   853 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"

   854   -- {* generalizes @{text subgroup_mult_id} *}

   855   by (auto simp add: RCOSETS_def subset

   856         setmult_rcos_assoc subgroup_mult_id normal_axioms normal.axioms)

   857

   858

   859 subsubsection{*Two distinct right cosets are disjoint*}

   860

   861 definition

   862   r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where

   863   "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"

   864

   865

   866 lemma (in subgroup) equiv_rcong:

   867    assumes "group(G)"

   868    shows "equiv (carrier(G), rcong H)"

   869 proof -

   870   interpret group G by fact

   871   show ?thesis proof (simp add: equiv_def, intro conjI)

   872     show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"

   873       by (auto simp add: r_congruent_def)

   874   next

   875     show "refl (carrier(G), rcong H)"

   876       by (auto simp add: r_congruent_def refl_def)

   877   next

   878     show "sym (rcong H)"

   879     proof (simp add: r_congruent_def sym_def, clarify)

   880       fix x y

   881       assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)"

   882         and "inv x \<cdot> y \<in> H"

   883       hence "inv (inv x \<cdot> y) \<in> H" by simp

   884       thus "inv y \<cdot> x \<in> H" by (simp add: inv_mult_group)

   885     qed

   886   next

   887     show "trans (rcong H)"

   888     proof (simp add: r_congruent_def trans_def, clarify)

   889       fix x y z

   890       assume [simp]: "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"

   891         and "inv x \<cdot> y \<in> H" and "inv y \<cdot> z \<in> H"

   892       hence "(inv x \<cdot> y) \<cdot> (inv y \<cdot> z) \<in> H" by simp

   893       hence "inv x \<cdot> (y \<cdot> inv y) \<cdot> z \<in> H" by (simp add: m_assoc del: inv)

   894       thus "inv x \<cdot> z \<in> H" by simp

   895     qed

   896   qed

   897 qed

   898

   899 text{*Equivalence classes of @{text rcong} correspond to left cosets.

   900   Was there a mistake in the definitions? I'd have expected them to

   901   correspond to right cosets.*}

   902 lemma (in subgroup) l_coset_eq_rcong:

   903   assumes "group(G)"

   904   assumes a: "a \<in> carrier(G)"

   905   shows "a <# H = (rcong H)  {a}"

   906 proof -

   907   interpret group G by fact

   908   show ?thesis

   909     by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a

   910       Collect_image_eq)

   911 qed

   912

   913 lemma (in group) rcos_equation:

   914   assumes "subgroup(H, G)"

   915   shows

   916      "\<lbrakk>ha \<cdot> a = h \<cdot> b; a \<in> carrier(G);  b \<in> carrier(G);

   917         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>

   918       \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")

   919 proof -

   920   interpret subgroup H G by fact

   921   show "PROP ?P"

   922     apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)

   923     apply (simp add: m_assoc transpose_inv)

   924     done

   925 qed

   926

   927 lemma (in group) rcos_disjoint:

   928   assumes "subgroup(H, G)"

   929   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")

   930 proof -

   931   interpret subgroup H G by fact

   932   show "PROP ?P"

   933     apply (simp add: RCOSETS_def r_coset_def)

   934     apply (blast intro: rcos_equation assms sym)

   935     done

   936 qed

   937

   938

   939 subsection {*Order of a Group and Lagrange's Theorem*}

   940

   941 definition

   942   order :: "i => i" where

   943   "order(S) == |carrier(S)|"

   944

   945 lemma (in group) rcos_self:

   946   assumes "subgroup(H, G)"

   947   shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")

   948 proof -

   949   interpret subgroup H G by fact

   950   show "PROP ?P"

   951     apply (simp add: r_coset_def)

   952     apply (rule_tac x="\<one>" in bexI) apply (auto)

   953     done

   954 qed

   955

   956 lemma (in group) rcosets_part_G:

   957   assumes "subgroup(H, G)"

   958   shows "\<Union>(rcosets H) = carrier(G)"

   959 proof -

   960   interpret subgroup H G by fact

   961   show ?thesis

   962     apply (rule equalityI)

   963     apply (force simp add: RCOSETS_def r_coset_def)

   964     apply (auto simp add: RCOSETS_def intro: rcos_self assms)

   965     done

   966 qed

   967

   968 lemma (in group) cosets_finite:

   969      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier(G);  Finite (carrier(G))\<rbrakk> \<Longrightarrow> Finite(c)"

   970 apply (auto simp add: RCOSETS_def)

   971 apply (simp add: r_coset_subset_G [THEN subset_Finite])

   972 done

   973

   974 text{*More general than the HOL version, which also requires @{term G} to

   975       be finite.*}

   976 lemma (in group) card_cosets_equal:

   977   assumes H:   "H \<subseteq> carrier(G)"

   978   shows "c \<in> rcosets H \<Longrightarrow> |c| = |H|"

   979 proof (simp add: RCOSETS_def, clarify)

   980   fix a

   981   assume a: "a \<in> carrier(G)"

   982   show "|H #> a| = |H|"

   983   proof (rule eqpollI [THEN cardinal_cong])

   984     show "H #> a \<lesssim> H"

   985     proof (simp add: lepoll_def, intro exI)

   986       show "(\<lambda>y \<in> H#>a. y \<cdot> inv a) \<in> inj(H #> a, H)"

   987         by (auto intro: lam_type

   988                  simp add: inj_def r_coset_def m_assoc subsetD [OF H] a)

   989     qed

   990     show "H \<lesssim> H #> a"

   991     proof (simp add: lepoll_def, intro exI)

   992       show "(\<lambda>y\<in> H. y \<cdot> a) \<in> inj(H, H #> a)"

   993         by (auto intro: lam_type

   994                  simp add: inj_def r_coset_def  subsetD [OF H] a)

   995     qed

   996   qed

   997 qed

   998

   999

  1000 lemma (in group) rcosets_subset_PowG:

  1001      "subgroup(H,G) \<Longrightarrow> rcosets H \<subseteq> Pow(carrier(G))"

  1002 apply (simp add: RCOSETS_def)

  1003 apply (blast dest: r_coset_subset_G subgroup.subset)

  1004 done

  1005

  1006 theorem (in group) lagrange:

  1007      "\<lbrakk>Finite(carrier(G)); subgroup(H,G)\<rbrakk>

  1008       \<Longrightarrow> |rcosets H| #* |H| = order(G)"

  1009 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])

  1010 apply (subst mult_commute)

  1011 apply (rule card_partition)

  1012    apply (simp add: rcosets_subset_PowG [THEN subset_Finite])

  1013   apply (simp add: rcosets_part_G)

  1014  apply (simp add: card_cosets_equal [OF subgroup.subset])

  1015 apply (simp add: rcos_disjoint)

  1016 done

  1017

  1018

  1019 subsection {*Quotient Groups: Factorization of a Group*}

  1020

  1021 definition

  1022   FactGroup :: "[i,i] => i" (infixl "Mod" 65) where

  1023     --{*Actually defined for groups rather than monoids*}

  1024   "G Mod H ==

  1025      <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"

  1026

  1027 lemma (in normal) setmult_closed:

  1028      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"

  1029 by (auto simp add: rcos_sum RCOSETS_def)

  1030

  1031 lemma (in normal) setinv_closed:

  1032      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"

  1033 by (auto simp add: rcos_inv RCOSETS_def)

  1034

  1035 lemma (in normal) rcosets_assoc:

  1036      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>

  1037       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"

  1038 by (auto simp add: RCOSETS_def rcos_sum m_assoc)

  1039

  1040 lemma (in subgroup) subgroup_in_rcosets:

  1041   assumes "group(G)"

  1042   shows "H \<in> rcosets H"

  1043 proof -

  1044   interpret group G by fact

  1045   have "H #> \<one> = H"

  1046     using _ subgroup_axioms by (rule coset_join2) simp_all

  1047   then show ?thesis

  1048     by (auto simp add: RCOSETS_def intro: sym)

  1049 qed

  1050

  1051 lemma (in normal) rcosets_inv_mult_group_eq:

  1052      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"

  1053 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal_axioms normal.axioms)

  1054

  1055 theorem (in normal) factorgroup_is_group:

  1056   "group (G Mod H)"

  1057 apply (simp add: FactGroup_def)

  1058 apply (rule groupI)

  1059     apply (simp add: setmult_closed)

  1060    apply (simp add: normal_imp_subgroup subgroup_in_rcosets)

  1061   apply (simp add: setmult_closed rcosets_assoc)

  1062  apply (simp add: normal_imp_subgroup

  1063                   subgroup_in_rcosets rcosets_mult_eq)

  1064 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)

  1065 done

  1066

  1067 lemma (in normal) inv_FactGroup:

  1068      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"

  1069 apply (rule group.inv_equality [OF factorgroup_is_group])

  1070 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)

  1071 done

  1072

  1073 text{*The coset map is a homomorphism from @{term G} to the quotient group

  1074   @{term "G Mod H"}*}

  1075 lemma (in normal) r_coset_hom_Mod:

  1076   "(\<lambda>a \<in> carrier(G). H #> a) \<in> hom(G, G Mod H)"

  1077 by (auto simp add: FactGroup_def RCOSETS_def hom_def rcos_sum intro: lam_type)

  1078

  1079

  1080 subsection{*The First Isomorphism Theorem*}

  1081

  1082 text{*The quotient by the kernel of a homomorphism is isomorphic to the

  1083   range of that homomorphism.*}

  1084

  1085 definition

  1086   kernel :: "[i,i,i] => i" where

  1087     --{*the kernel of a homomorphism*}

  1088   "kernel(G,H,h) == {x \<in> carrier(G). h  x = \<one>\<^bsub>H\<^esub>}";

  1089

  1090 lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"

  1091 apply (rule subgroup.intro)

  1092 apply (auto simp add: kernel_def group.intro)

  1093 done

  1094

  1095 text{*The kernel of a homomorphism is a normal subgroup*}

  1096 lemma (in group_hom) normal_kernel: "(kernel(G,H,h)) \<lhd> G"

  1097 apply (simp add: group.normal_inv_iff subgroup_kernel group.intro)

  1098 apply (simp add: kernel_def)

  1099 done

  1100

  1101 lemma (in group_hom) FactGroup_nonempty:

  1102   assumes X: "X \<in> carrier (G Mod kernel(G,H,h))"

  1103   shows "X \<noteq> 0"

  1104 proof -

  1105   from X

  1106   obtain g where "g \<in> carrier(G)"

  1107              and "X = kernel(G,H,h) #> g"

  1108     by (auto simp add: FactGroup_def RCOSETS_def)

  1109   thus ?thesis

  1110    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)

  1111 qed

  1112

  1113

  1114 lemma (in group_hom) FactGroup_contents_mem:

  1115   assumes X: "X \<in> carrier (G Mod (kernel(G,H,h)))"

  1116   shows "contents (hX) \<in> carrier(H)"

  1117 proof -

  1118   from X

  1119   obtain g where g: "g \<in> carrier(G)"

  1120              and "X = kernel(G,H,h) #> g"

  1121     by (auto simp add: FactGroup_def RCOSETS_def)

  1122   hence "h  X = {h  g}"

  1123     by (auto simp add: kernel_def r_coset_def image_UN

  1124                        image_eq_UN [OF hom_is_fun] g)

  1125   thus ?thesis by (auto simp add: g)

  1126 qed

  1127

  1128 lemma mult_FactGroup:

  1129      "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|]

  1130       ==> X \<cdot>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"

  1131 by (simp add: FactGroup_def)

  1132

  1133 lemma (in normal) FactGroup_m_closed:

  1134      "[|X \<in> carrier(G Mod H); X' \<in> carrier(G Mod H)|]

  1135       ==> X <#>\<^bsub>G\<^esub> X' \<in> carrier(G Mod H)"

  1136 by (simp add: FactGroup_def setmult_closed)

  1137

  1138 lemma (in group_hom) FactGroup_hom:

  1139      "(\<lambda>X \<in> carrier(G Mod (kernel(G,H,h))). contents (hX))

  1140       \<in> hom (G Mod (kernel(G,H,h)), H)"

  1141 proof (simp add: hom_def FactGroup_contents_mem lam_type mult_FactGroup normal.FactGroup_m_closed [OF normal_kernel], intro ballI)

  1142   fix X and X'

  1143   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"

  1144      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"

  1145   then

  1146   obtain g and g'

  1147            where "g \<in> carrier(G)" and "g' \<in> carrier(G)"

  1148              and "X = kernel(G,H,h) #> g" and "X' = kernel(G,H,h) #> g'"

  1149     by (auto simp add: FactGroup_def RCOSETS_def)

  1150   hence all: "\<forall>x\<in>X. h  x = h  g" "\<forall>x\<in>X'. h  x = h  g'"

  1151     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"

  1152     by (force simp add: kernel_def r_coset_def image_def)+

  1153   hence "h  (X <#> X') = {h  g \<cdot>\<^bsub>H\<^esub> h  g'}" using X X'

  1154     by (auto dest!: FactGroup_nonempty

  1155              simp add: set_mult_def image_eq_UN [OF hom_is_fun] image_UN

  1156                        subsetD [OF Xsub] subsetD [OF X'sub])

  1157   thus "contents (h  (X <#> X')) = contents (h  X) \<cdot>\<^bsub>H\<^esub> contents (h  X')"

  1158     by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty

  1159                   X X' Xsub X'sub)

  1160 qed

  1161

  1162

  1163 text{*Lemma for the following injectivity result*}

  1164 lemma (in group_hom) FactGroup_subset:

  1165      "\<lbrakk>g \<in> carrier(G); g' \<in> carrier(G); h  g = h  g'\<rbrakk>

  1166       \<Longrightarrow>  kernel(G,H,h) #> g \<subseteq> kernel(G,H,h) #> g'"

  1167 apply (clarsimp simp add: kernel_def r_coset_def image_def)

  1168 apply (rename_tac y)

  1169 apply (rule_tac x="y \<cdot> g \<cdot> inv g'" in bexI)

  1170 apply (simp_all add: G.m_assoc)

  1171 done

  1172

  1173 lemma (in group_hom) FactGroup_inj:

  1174      "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h  X))

  1175       \<in> inj(carrier (G Mod kernel(G,H,h)), carrier(H))"

  1176 proof (simp add: inj_def FactGroup_contents_mem lam_type, clarify)

  1177   fix X and X'

  1178   assume X:  "X  \<in> carrier (G Mod kernel(G,H,h))"

  1179      and X': "X' \<in> carrier (G Mod kernel(G,H,h))"

  1180   then

  1181   obtain g and g'

  1182            where gX: "g \<in> carrier(G)"  "g' \<in> carrier(G)"

  1183               "X = kernel(G,H,h) #> g" "X' = kernel(G,H,h) #> g'"

  1184     by (auto simp add: FactGroup_def RCOSETS_def)

  1185   hence all: "\<forall>x\<in>X. h  x = h  g" "\<forall>x\<in>X'. h  x = h  g'"

  1186     and Xsub: "X \<subseteq> carrier(G)" and X'sub: "X' \<subseteq> carrier(G)"

  1187     by (force simp add: kernel_def r_coset_def image_def)+

  1188   assume "contents (h  X) = contents (h  X')"

  1189   hence h: "h  g = h  g'"

  1190     by (simp add: all image_eq_UN [OF hom_is_fun] FactGroup_nonempty

  1191                   X X' Xsub X'sub)

  1192   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)

  1193 qed

  1194

  1195

  1196 lemma (in group_hom) kernel_rcoset_subset:

  1197   assumes g: "g \<in> carrier(G)"

  1198   shows "kernel(G,H,h) #> g \<subseteq> carrier (G)"

  1199     by (auto simp add: g kernel_def r_coset_def)

  1200

  1201

  1202

  1203 text{*If the homomorphism @{term h} is onto @{term H}, then so is the

  1204 homomorphism from the quotient group*}

  1205 lemma (in group_hom) FactGroup_surj:

  1206   assumes h: "h \<in> surj(carrier(G), carrier(H))"

  1207   shows "(\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (h  X))

  1208          \<in> surj(carrier (G Mod kernel(G,H,h)), carrier(H))"

  1209 proof (simp add: surj_def FactGroup_contents_mem lam_type, clarify)

  1210   fix y

  1211   assume y: "y \<in> carrier(H)"

  1212   with h obtain g where g: "g \<in> carrier(G)" "h  g = y"

  1213     by (auto simp add: surj_def)

  1214   hence "(\<Union>x\<in>kernel(G,H,h) #> g. {h  x}) = {y}"

  1215     by (auto simp add: y kernel_def r_coset_def)

  1216   with g show "\<exists>x\<in>carrier(G Mod kernel(G, H, h)). contents(h  x) = y"

  1217         --{*The witness is @{term "kernel(G,H,h) #> g"}*}

  1218     by (force simp add: FactGroup_def RCOSETS_def

  1219            image_eq_UN [OF hom_is_fun] kernel_rcoset_subset)

  1220 qed

  1221

  1222

  1223 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the

  1224  quotient group @{term "G Mod (kernel(G,H,h))"} is isomorphic to @{term H}.*}

  1225 theorem (in group_hom) FactGroup_iso:

  1226   "h \<in> surj(carrier(G), carrier(H))

  1227    \<Longrightarrow> (\<lambda>X\<in>carrier (G Mod kernel(G,H,h)). contents (hX)) \<in> (G Mod (kernel(G,H,h))) \<cong> H"

  1228 by (simp add: iso_def FactGroup_hom FactGroup_inj bij_def FactGroup_surj)

  1229

  1230 end