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