src/HOL/Algebra/Group.thy
author paulson
Wed May 26 11:43:50 2004 +0200 (2004-05-26)
changeset 14803 f7557773cc87
parent 14761 28b5eb4a867f
child 14852 fffab59e0050
permissions -rw-r--r--
more group isomorphisms
     1 (*
     2   Title:  HOL/Algebra/Group.thy
     3   Id:     $Id$
     4   Author: Clemens Ballarin, started 4 February 2003
     5 
     6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     7 *)
     8 
     9 header {* Groups *}
    10 
    11 theory Group = FuncSet + Lattice:
    12 
    13 
    14 section {* From Magmas to Groups *}
    15 
    16 text {*
    17   Definitions follow \cite{Jacobson:1985}; with the exception of
    18   \emph{magma} which, following Bourbaki, is a set together with a
    19   binary, closed operation.
    20 *}
    21 
    22 subsection {* Definitions *}
    23 
    24 record 'a semigroup = "'a partial_object" +
    25   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    26 
    27 record 'a monoid = "'a semigroup" +
    28   one :: 'a ("\<one>\<index>")
    29 
    30 constdefs (structure G)
    31   m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
    32   "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    33 
    34   Units :: "_ => 'a set"
    35   "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    36 
    37 consts
    38   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    39 
    40 defs (overloaded)
    41   nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
    42   int_pow_def: "pow G a z ==
    43     let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    44     in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
    45 
    46 locale magma = struct G +
    47   assumes m_closed [intro, simp]:
    48     "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    49 
    50 locale semigroup = magma +
    51   assumes m_assoc:
    52     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    53     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    54 
    55 locale monoid = semigroup +
    56   assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    57     and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    58     and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    59 
    60 lemma monoidI:
    61   includes struct G
    62   assumes m_closed:
    63       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    64     and one_closed: "\<one> \<in> carrier G"
    65     and m_assoc:
    66       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    67       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    68     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    69     and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
    70   shows "monoid G"
    71   by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    72     semigroup.intro monoid_axioms.intro
    73     intro: prems)
    74 
    75 lemma (in monoid) Units_closed [dest]:
    76   "x \<in> Units G ==> x \<in> carrier G"
    77   by (unfold Units_def) fast
    78 
    79 lemma (in monoid) inv_unique:
    80   assumes eq: "y \<otimes> x = \<one>"  "x \<otimes> y' = \<one>"
    81     and G: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
    82   shows "y = y'"
    83 proof -
    84   from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
    85   also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
    86   also from G eq have "... = y'" by simp
    87   finally show ?thesis .
    88 qed
    89 
    90 lemma (in monoid) Units_one_closed [intro, simp]:
    91   "\<one> \<in> Units G"
    92   by (unfold Units_def) auto
    93 
    94 lemma (in monoid) Units_inv_closed [intro, simp]:
    95   "x \<in> Units G ==> inv x \<in> carrier G"
    96   apply (unfold Units_def m_inv_def, auto)
    97   apply (rule theI2, fast)
    98    apply (fast intro: inv_unique, fast)
    99   done
   100 
   101 lemma (in monoid) Units_l_inv:
   102   "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   103   apply (unfold Units_def m_inv_def, auto)
   104   apply (rule theI2, fast)
   105    apply (fast intro: inv_unique, fast)
   106   done
   107 
   108 lemma (in monoid) Units_r_inv:
   109   "x \<in> Units G ==> x \<otimes> inv x = \<one>"
   110   apply (unfold Units_def m_inv_def, auto)
   111   apply (rule theI2, fast)
   112    apply (fast intro: inv_unique, fast)
   113   done
   114 
   115 lemma (in monoid) Units_inv_Units [intro, simp]:
   116   "x \<in> Units G ==> inv x \<in> Units G"
   117 proof -
   118   assume x: "x \<in> Units G"
   119   show "inv x \<in> Units G"
   120     by (auto simp add: Units_def
   121       intro: Units_l_inv Units_r_inv x Units_closed [OF x])
   122 qed
   123 
   124 lemma (in monoid) Units_l_cancel [simp]:
   125   "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
   126    (x \<otimes> y = x \<otimes> z) = (y = z)"
   127 proof
   128   assume eq: "x \<otimes> y = x \<otimes> z"
   129     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   130   then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
   131     by (simp add: m_assoc Units_closed)
   132   with G show "y = z" by (simp add: Units_l_inv)
   133 next
   134   assume eq: "y = z"
   135     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   136   then show "x \<otimes> y = x \<otimes> z" by simp
   137 qed
   138 
   139 lemma (in monoid) Units_inv_inv [simp]:
   140   "x \<in> Units G ==> inv (inv x) = x"
   141 proof -
   142   assume x: "x \<in> Units G"
   143   then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
   144     by (simp add: Units_l_inv Units_r_inv)
   145   with x show ?thesis by (simp add: Units_closed)
   146 qed
   147 
   148 lemma (in monoid) inv_inj_on_Units:
   149   "inj_on (m_inv G) (Units G)"
   150 proof (rule inj_onI)
   151   fix x y
   152   assume G: "x \<in> Units G"  "y \<in> Units G" and eq: "inv x = inv y"
   153   then have "inv (inv x) = inv (inv y)" by simp
   154   with G show "x = y" by simp
   155 qed
   156 
   157 lemma (in monoid) Units_inv_comm:
   158   assumes inv: "x \<otimes> y = \<one>"
   159     and G: "x \<in> Units G"  "y \<in> Units G"
   160   shows "y \<otimes> x = \<one>"
   161 proof -
   162   from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
   163   with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
   164 qed
   165 
   166 text {* Power *}
   167 
   168 lemma (in monoid) nat_pow_closed [intro, simp]:
   169   "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
   170   by (induct n) (simp_all add: nat_pow_def)
   171 
   172 lemma (in monoid) nat_pow_0 [simp]:
   173   "x (^) (0::nat) = \<one>"
   174   by (simp add: nat_pow_def)
   175 
   176 lemma (in monoid) nat_pow_Suc [simp]:
   177   "x (^) (Suc n) = x (^) n \<otimes> x"
   178   by (simp add: nat_pow_def)
   179 
   180 lemma (in monoid) nat_pow_one [simp]:
   181   "\<one> (^) (n::nat) = \<one>"
   182   by (induct n) simp_all
   183 
   184 lemma (in monoid) nat_pow_mult:
   185   "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
   186   by (induct m) (simp_all add: m_assoc [THEN sym])
   187 
   188 lemma (in monoid) nat_pow_pow:
   189   "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
   190   by (induct m) (simp, simp add: nat_pow_mult add_commute)
   191 
   192 text {*
   193   A group is a monoid all of whose elements are invertible.
   194 *}
   195 
   196 locale group = monoid +
   197   assumes Units: "carrier G <= Units G"
   198 
   199 
   200 lemma (in group) is_group: "group G"
   201   by (rule group.intro [OF prems]) 
   202 
   203 theorem groupI:
   204   includes struct G
   205   assumes m_closed [simp]:
   206       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   207     and one_closed [simp]: "\<one> \<in> carrier G"
   208     and m_assoc:
   209       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   210       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   211     and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   212     and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   213   shows "group G"
   214 proof -
   215   have l_cancel [simp]:
   216     "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   217     (x \<otimes> y = x \<otimes> z) = (y = z)"
   218   proof
   219     fix x y z
   220     assume eq: "x \<otimes> y = x \<otimes> z"
   221       and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   222     with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   223       and l_inv: "x_inv \<otimes> x = \<one>" by fast
   224     from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z"
   225       by (simp add: m_assoc)
   226     with G show "y = z" by (simp add: l_inv)
   227   next
   228     fix x y z
   229     assume eq: "y = z"
   230       and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   231     then show "x \<otimes> y = x \<otimes> z" by simp
   232   qed
   233   have r_one:
   234     "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
   235   proof -
   236     fix x
   237     assume x: "x \<in> carrier G"
   238     with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   239       and l_inv: "x_inv \<otimes> x = \<one>" by fast
   240     from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x"
   241       by (simp add: m_assoc [symmetric] l_inv)
   242     with x xG show "x \<otimes> \<one> = x" by simp
   243   qed
   244   have inv_ex:
   245     "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   246   proof -
   247     fix x
   248     assume x: "x \<in> carrier G"
   249     with l_inv_ex obtain y where y: "y \<in> carrier G"
   250       and l_inv: "y \<otimes> x = \<one>" by fast
   251     from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>"
   252       by (simp add: m_assoc [symmetric] l_inv r_one)
   253     with x y have r_inv: "x \<otimes> y = \<one>"
   254       by simp
   255     from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
   256       by (fast intro: l_inv r_inv)
   257   qed
   258   then have carrier_subset_Units: "carrier G <= Units G"
   259     by (unfold Units_def) fast
   260   show ?thesis
   261     by (fast intro!: group.intro magma.intro semigroup_axioms.intro
   262       semigroup.intro monoid_axioms.intro group_axioms.intro
   263       carrier_subset_Units intro: prems r_one)
   264 qed
   265 
   266 lemma (in monoid) monoid_groupI:
   267   assumes l_inv_ex:
   268     "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   269   shows "group G"
   270   by (rule groupI) (auto intro: m_assoc l_inv_ex)
   271 
   272 lemma (in group) Units_eq [simp]:
   273   "Units G = carrier G"
   274 proof
   275   show "Units G <= carrier G" by fast
   276 next
   277   show "carrier G <= Units G" by (rule Units)
   278 qed
   279 
   280 lemma (in group) inv_closed [intro, simp]:
   281   "x \<in> carrier G ==> inv x \<in> carrier G"
   282   using Units_inv_closed by simp
   283 
   284 lemma (in group) l_inv:
   285   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   286   using Units_l_inv by simp
   287 
   288 subsection {* Cancellation Laws and Basic Properties *}
   289 
   290 lemma (in group) l_cancel [simp]:
   291   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   292    (x \<otimes> y = x \<otimes> z) = (y = z)"
   293   using Units_l_inv by simp
   294 
   295 lemma (in group) r_inv:
   296   "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
   297 proof -
   298   assume x: "x \<in> carrier G"
   299   then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
   300     by (simp add: m_assoc [symmetric] l_inv)
   301   with x show ?thesis by (simp del: r_one)
   302 qed
   303 
   304 lemma (in group) r_cancel [simp]:
   305   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   306    (y \<otimes> x = z \<otimes> x) = (y = z)"
   307 proof
   308   assume eq: "y \<otimes> x = z \<otimes> x"
   309     and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   310   then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
   311     by (simp add: m_assoc [symmetric])
   312   with G show "y = z" by (simp add: r_inv)
   313 next
   314   assume eq: "y = z"
   315     and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   316   then show "y \<otimes> x = z \<otimes> x" by simp
   317 qed
   318 
   319 lemma (in group) inv_one [simp]:
   320   "inv \<one> = \<one>"
   321 proof -
   322   have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
   323   moreover have "... = \<one>" by (simp add: r_inv)
   324   finally show ?thesis .
   325 qed
   326 
   327 lemma (in group) inv_inv [simp]:
   328   "x \<in> carrier G ==> inv (inv x) = x"
   329   using Units_inv_inv by simp
   330 
   331 lemma (in group) inv_inj:
   332   "inj_on (m_inv G) (carrier G)"
   333   using inv_inj_on_Units by simp
   334 
   335 lemma (in group) inv_mult_group:
   336   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
   337 proof -
   338   assume G: "x \<in> carrier G"  "y \<in> carrier G"
   339   then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   340     by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   341   with G show ?thesis by simp
   342 qed
   343 
   344 lemma (in group) inv_comm:
   345   "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
   346   by (rule Units_inv_comm) auto
   347 
   348 lemma (in group) inv_equality:
   349      "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
   350 apply (simp add: m_inv_def)
   351 apply (rule the_equality)
   352  apply (simp add: inv_comm [of y x])
   353 apply (rule r_cancel [THEN iffD1], auto)
   354 done
   355 
   356 text {* Power *}
   357 
   358 lemma (in group) int_pow_def2:
   359   "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
   360   by (simp add: int_pow_def nat_pow_def Let_def)
   361 
   362 lemma (in group) int_pow_0 [simp]:
   363   "x (^) (0::int) = \<one>"
   364   by (simp add: int_pow_def2)
   365 
   366 lemma (in group) int_pow_one [simp]:
   367   "\<one> (^) (z::int) = \<one>"
   368   by (simp add: int_pow_def2)
   369 
   370 subsection {* Substructures *}
   371 
   372 locale submagma = var H + struct G +
   373   assumes subset [intro, simp]: "H \<subseteq> carrier G"
   374     and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   375 
   376 declare (in submagma) magma.intro [intro] semigroup.intro [intro]
   377   semigroup_axioms.intro [intro]
   378 
   379 lemma submagma_imp_subset:
   380   "submagma H G ==> H \<subseteq> carrier G"
   381   by (rule submagma.subset)
   382 
   383 lemma (in submagma) subsetD [dest, simp]:
   384   "x \<in> H ==> x \<in> carrier G"
   385   using subset by blast
   386 
   387 lemma (in submagma) magmaI [intro]:
   388   includes magma G
   389   shows "magma (G(| carrier := H |))"
   390   by rule simp
   391 
   392 lemma (in submagma) semigroup_axiomsI [intro]:
   393   includes semigroup G
   394   shows "semigroup_axioms (G(| carrier := H |))"
   395     by rule (simp add: m_assoc)
   396 
   397 lemma (in submagma) semigroupI [intro]:
   398   includes semigroup G
   399   shows "semigroup (G(| carrier := H |))"
   400   using prems by fast
   401 
   402 
   403 locale subgroup = submagma H G +
   404   assumes one_closed [intro, simp]: "\<one> \<in> H"
   405     and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   406 
   407 declare (in subgroup) group.intro [intro]
   408 
   409 lemma (in subgroup) group_axiomsI [intro]:
   410   includes group G
   411   shows "group_axioms (G(| carrier := H |))"
   412   by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
   413 
   414 lemma (in subgroup) groupI [intro]:
   415   includes group G
   416   shows "group (G(| carrier := H |))"
   417   by (rule groupI) (auto intro: m_assoc l_inv)
   418 
   419 text {*
   420   Since @{term H} is nonempty, it contains some element @{term x}.  Since
   421   it is closed under inverse, it contains @{text "inv x"}.  Since
   422   it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
   423 *}
   424 
   425 lemma (in group) one_in_subset:
   426   "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
   427    ==> \<one> \<in> H"
   428 by (force simp add: l_inv)
   429 
   430 text {* A characterization of subgroups: closed, non-empty subset. *}
   431 
   432 lemma (in group) subgroupI:
   433   assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   434     and inv: "!!a. a \<in> H ==> inv a \<in> H"
   435     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
   436   shows "subgroup H G"
   437 proof (rule subgroup.intro)
   438   from subset and mult show "submagma H G" by (rule submagma.intro)
   439 next
   440   have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   441   with inv show "subgroup_axioms H G"
   442     by (intro subgroup_axioms.intro) simp_all
   443 qed
   444 
   445 text {*
   446   Repeat facts of submagmas for subgroups.  Necessary???
   447 *}
   448 
   449 lemma (in subgroup) subset:
   450   "H \<subseteq> carrier G"
   451   ..
   452 
   453 lemma (in subgroup) m_closed:
   454   "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   455   ..
   456 
   457 declare magma.m_closed [simp]
   458 
   459 declare monoid.one_closed [iff] group.inv_closed [simp]
   460   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   461 
   462 lemma subgroup_nonempty:
   463   "~ subgroup {} G"
   464   by (blast dest: subgroup.one_closed)
   465 
   466 lemma (in subgroup) finite_imp_card_positive:
   467   "finite (carrier G) ==> 0 < card H"
   468 proof (rule classical)
   469   have sub: "subgroup H G" using prems by (rule subgroup.intro)
   470   assume fin: "finite (carrier G)"
   471     and zero: "~ 0 < card H"
   472   then have "finite H" by (blast intro: finite_subset dest: subset)
   473   with zero sub have "subgroup {} G" by simp
   474   with subgroup_nonempty show ?thesis by contradiction
   475 qed
   476 
   477 (*
   478 lemma (in monoid) Units_subgroup:
   479   "subgroup (Units G) G"
   480 *)
   481 
   482 subsection {* Direct Products *}
   483 
   484 constdefs (structure G and H)
   485   DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
   486   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   487     mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
   488 
   489   DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
   490   "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
   491 
   492 lemma DirProdSemigroup_magma:
   493   includes magma G + magma H
   494   shows "magma (G \<times>\<^sub>s H)"
   495   by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
   496 
   497 lemma DirProdSemigroup_semigroup_axioms:
   498   includes semigroup G + semigroup H
   499   shows "semigroup_axioms (G \<times>\<^sub>s H)"
   500   by (rule semigroup_axioms.intro)
   501     (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
   502 
   503 lemma DirProdSemigroup_semigroup:
   504   includes semigroup G + semigroup H
   505   shows "semigroup (G \<times>\<^sub>s H)"
   506   using prems
   507   by (fast intro: semigroup.intro
   508     DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
   509 
   510 lemma DirProdGroup_magma:
   511   includes magma G + magma H
   512   shows "magma (G \<times>\<^sub>g H)"
   513   by (rule magma.intro)
   514     (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   515 
   516 lemma DirProdGroup_semigroup_axioms:
   517   includes semigroup G + semigroup H
   518   shows "semigroup_axioms (G \<times>\<^sub>g H)"
   519   by (rule semigroup_axioms.intro)
   520     (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
   521       G.m_assoc H.m_assoc)
   522 
   523 lemma DirProdGroup_semigroup:
   524   includes semigroup G + semigroup H
   525   shows "semigroup (G \<times>\<^sub>g H)"
   526   using prems
   527   by (fast intro: semigroup.intro
   528     DirProdGroup_magma DirProdGroup_semigroup_axioms)
   529 
   530 text {* \dots\ and further lemmas for group \dots *}
   531 
   532 lemma DirProdGroup_group:
   533   includes group G + group H
   534   shows "group (G \<times>\<^sub>g H)"
   535   by (rule groupI)
   536     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   537       simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   538 
   539 lemma carrier_DirProdGroup [simp]:
   540      "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
   541   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   542 
   543 lemma one_DirProdGroup [simp]:
   544      "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
   545   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   546 
   547 lemma mult_DirProdGroup [simp]:
   548      "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   549   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   550 
   551 lemma inv_DirProdGroup [simp]:
   552   includes group G + group H
   553   assumes g: "g \<in> carrier G"
   554       and h: "h \<in> carrier H"
   555   shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   556   apply (rule group.inv_equality [OF DirProdGroup_group])
   557   apply (simp_all add: prems group_def group.l_inv)
   558   done
   559 
   560 subsection {* Isomorphisms *}
   561 
   562 constdefs (structure G and H)
   563   hom :: "_ => _ => ('a => 'b) set"
   564   "hom G H ==
   565     {h. h \<in> carrier G -> carrier H &
   566       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
   567 
   568 lemma (in semigroup) hom:
   569      "semigroup (| carrier = hom G G, mult = op o |)"
   570 proof (rule semigroup.intro)
   571   show "magma (| carrier = hom G G, mult = op o |)"
   572     by (rule magma.intro) (simp add: Pi_def hom_def)
   573 next
   574   show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
   575     by (rule semigroup_axioms.intro) (simp add: o_assoc)
   576 qed
   577 
   578 lemma hom_mult:
   579   "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
   580    ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
   581   by (simp add: hom_def)
   582 
   583 lemma hom_closed:
   584   "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
   585   by (auto simp add: hom_def funcset_mem)
   586 
   587 lemma (in group) hom_compose:
   588      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
   589 apply (auto simp add: hom_def funcset_compose) 
   590 apply (simp add: compose_def funcset_mem)
   591 done
   592 
   593 
   594 subsection {* Isomorphisms *}
   595 
   596 constdefs
   597   iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
   598   "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
   599 
   600 lemma iso_refl: "(%x. x) \<in> G \<cong> G"
   601 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
   602 
   603 lemma (in group) iso_sym:
   604      "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
   605 apply (simp add: iso_def bij_betw_Inv) 
   606 apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 
   607  prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 
   608 apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f) 
   609 done
   610 
   611 lemma (in group) iso_trans: 
   612      "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
   613 by (auto simp add: iso_def hom_compose bij_betw_compose)
   614 
   615 lemma DirProdGroup_commute_iso:
   616   shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
   617 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
   618 
   619 lemma DirProdGroup_assoc_iso:
   620   shows "(%(x,y,z). (x,(y,z))) \<in> (G \<times>\<^sub>g H \<times>\<^sub>g I) \<cong> (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
   621 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
   622 
   623 
   624 locale group_hom = group G + group H + var h +
   625   assumes homh: "h \<in> hom G H"
   626   notes hom_mult [simp] = hom_mult [OF homh]
   627     and hom_closed [simp] = hom_closed [OF homh]
   628 
   629 lemma (in group_hom) one_closed [simp]:
   630   "h \<one> \<in> carrier H"
   631   by simp
   632 
   633 lemma (in group_hom) hom_one [simp]:
   634   "h \<one> = \<one>\<^bsub>H\<^esub>"
   635 proof -
   636   have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
   637     by (simp add: hom_mult [symmetric] del: hom_mult)
   638   then show ?thesis by (simp del: r_one)
   639 qed
   640 
   641 lemma (in group_hom) inv_closed [simp]:
   642   "x \<in> carrier G ==> h (inv x) \<in> carrier H"
   643   by simp
   644 
   645 lemma (in group_hom) hom_inv [simp]:
   646   "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
   647 proof -
   648   assume x: "x \<in> carrier G"
   649   then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
   650     by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   651   also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
   652     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   653   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   654   with x show ?thesis by simp
   655 qed
   656 
   657 subsection {* Commutative Structures *}
   658 
   659 text {*
   660   Naming convention: multiplicative structures that are commutative
   661   are called \emph{commutative}, additive structures are called
   662   \emph{Abelian}.
   663 *}
   664 
   665 subsection {* Definition *}
   666 
   667 locale comm_semigroup = semigroup +
   668   assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   669 
   670 lemma (in comm_semigroup) m_lcomm:
   671   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   672    x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   673 proof -
   674   assume xyz: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   675   from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
   676   also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
   677   also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
   678   finally show ?thesis .
   679 qed
   680 
   681 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
   682 
   683 locale comm_monoid = comm_semigroup + monoid
   684 
   685 lemma comm_monoidI:
   686   includes struct G
   687   assumes m_closed:
   688       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   689     and one_closed: "\<one> \<in> carrier G"
   690     and m_assoc:
   691       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   692       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   693     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   694     and m_comm:
   695       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   696   shows "comm_monoid G"
   697   using l_one
   698   by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   699     comm_semigroup_axioms.intro monoid_axioms.intro
   700     intro: prems simp: m_closed one_closed m_comm)
   701 
   702 lemma (in monoid) monoid_comm_monoidI:
   703   assumes m_comm:
   704       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   705   shows "comm_monoid G"
   706   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   707 (*lemma (in comm_monoid) r_one [simp]:
   708   "x \<in> carrier G ==> x \<otimes> \<one> = x"
   709 proof -
   710   assume G: "x \<in> carrier G"
   711   then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
   712   also from G have "... = x" by simp
   713   finally show ?thesis .
   714 qed*)
   715 lemma (in comm_monoid) nat_pow_distr:
   716   "[| x \<in> carrier G; y \<in> carrier G |] ==>
   717   (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   718   by (induct n) (simp, simp add: m_ac)
   719 
   720 locale comm_group = comm_monoid + group
   721 
   722 lemma (in group) group_comm_groupI:
   723   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   724       x \<otimes> y = y \<otimes> x"
   725   shows "comm_group G"
   726   by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   727                   is_group prems)
   728 
   729 lemma comm_groupI:
   730   includes struct G
   731   assumes m_closed:
   732       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   733     and one_closed: "\<one> \<in> carrier G"
   734     and m_assoc:
   735       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   736       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   737     and m_comm:
   738       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   739     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   740     and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   741   shows "comm_group G"
   742   by (fast intro: group.group_comm_groupI groupI prems)
   743 
   744 lemma (in comm_group) inv_mult:
   745   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   746   by (simp add: m_ac inv_mult_group)
   747 
   748 subsection {* Lattice of subgroups of a group *}
   749 
   750 text_raw {* \label{sec:subgroup-lattice} *}
   751 
   752 theorem (in group) subgroups_partial_order:
   753   "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
   754   by (rule partial_order.intro) simp_all
   755 
   756 lemma (in group) subgroup_self:
   757   "subgroup (carrier G) G"
   758   by (rule subgroupI) auto
   759 
   760 lemma (in group) subgroup_imp_group:
   761   "subgroup H G ==> group (G(| carrier := H |))"
   762   using subgroup.groupI [OF _ group.intro] .
   763 
   764 lemma (in group) is_monoid [intro, simp]:
   765   "monoid G"
   766   by (rule monoid.intro)
   767 
   768 lemma (in group) subgroup_inv_equality:
   769   "[| subgroup H G; x \<in> H |] ==> m_inv (G (| carrier := H |)) x = inv x"
   770 apply (rule_tac inv_equality [THEN sym])
   771   apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+)
   772  apply (rule subsetD [OF subgroup.subset], assumption+)
   773 apply (rule subsetD [OF subgroup.subset], assumption)
   774 apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+)
   775 done
   776 
   777 theorem (in group) subgroups_Inter:
   778   assumes subgr: "(!!H. H \<in> A ==> subgroup H G)"
   779     and not_empty: "A ~= {}"
   780   shows "subgroup (\<Inter>A) G"
   781 proof (rule subgroupI)
   782   from subgr [THEN subgroup.subset] and not_empty
   783   show "\<Inter>A \<subseteq> carrier G" by blast
   784 next
   785   from subgr [THEN subgroup.one_closed]
   786   show "\<Inter>A ~= {}" by blast
   787 next
   788   fix x assume "x \<in> \<Inter>A"
   789   with subgr [THEN subgroup.m_inv_closed]
   790   show "inv x \<in> \<Inter>A" by blast
   791 next
   792   fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A"
   793   with subgr [THEN subgroup.m_closed]
   794   show "x \<otimes> y \<in> \<Inter>A" by blast
   795 qed
   796 
   797 theorem (in group) subgroups_complete_lattice:
   798   "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
   799     (is "complete_lattice ?L")
   800 proof (rule partial_order.complete_lattice_criterion1)
   801   show "partial_order ?L" by (rule subgroups_partial_order)
   802 next
   803   have "greatest ?L (carrier G) (carrier ?L)"
   804     by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
   805   then show "EX G. greatest ?L G (carrier ?L)" ..
   806 next
   807   fix A
   808   assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
   809   then have Int_subgroup: "subgroup (\<Inter>A) G"
   810     by (fastsimp intro: subgroups_Inter)
   811   have "greatest ?L (\<Inter>A) (Lower ?L A)"
   812     (is "greatest ?L ?Int _")
   813   proof (rule greatest_LowerI)
   814     fix H
   815     assume H: "H \<in> A"
   816     with L have subgroupH: "subgroup H G" by auto
   817     from subgroupH have submagmaH: "submagma H G" by (rule subgroup.axioms)
   818     from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
   819       by (rule subgroup_imp_group)
   820     from groupH have monoidH: "monoid ?H"
   821       by (rule group.is_monoid)
   822     from H have Int_subset: "?Int \<subseteq> H" by fastsimp
   823     then show "le ?L ?Int H" by simp
   824   next
   825     fix H
   826     assume H: "H \<in> Lower ?L A"
   827     with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest)
   828   next
   829     show "A \<subseteq> carrier ?L" by (rule L)
   830   next
   831     show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
   832   qed
   833   then show "EX I. greatest ?L I (Lower ?L A)" ..
   834 qed
   835 
   836 end