src/HOL/Algebra/Group.thy
author wenzelm
Sat May 01 22:05:05 2004 +0200 (2004-05-01)
changeset 14693 4deda204e1d8
parent 14651 02b8f3bcf7fe
child 14706 71590b7733b7
permissions -rw-r--r--
improved syntax;
     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:
    12 
    13 section {* From Magmas to Groups *}
    14 
    15 text {*
    16   Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    17   the exception of \emph{magma} which, following Bourbaki, is a set
    18   together with a binary, closed operation.
    19 *}
    20 
    21 subsection {* Definitions *}
    22 
    23 (* Object with a carrier set. *)
    24 
    25 record 'a partial_object =
    26   carrier :: "'a set"
    27 
    28 record 'a semigroup = "'a partial_object" +
    29   mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    30 
    31 record 'a monoid = "'a semigroup" +
    32   one :: 'a ("\<one>\<index>")
    33 
    34 constdefs (structure G)
    35   m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
    36   "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    37 
    38   Units :: "_ => 'a set"
    39   "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    40 
    41 consts
    42   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    43 
    44 defs (overloaded)
    45   nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
    46   int_pow_def: "pow G a z ==
    47     let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    48     in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
    49 
    50 locale magma = struct G +
    51   assumes m_closed [intro, simp]:
    52     "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    53 
    54 locale semigroup = magma +
    55   assumes m_assoc:
    56     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    57     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    58 
    59 locale monoid = semigroup +
    60   assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    61     and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    62     and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    63 
    64 lemma monoidI:
    65   includes struct G
    66   assumes m_closed:
    67       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
    68     and one_closed: "\<one> \<in> carrier G"
    69     and m_assoc:
    70       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    71       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    72     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
    73     and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
    74   shows "monoid G"
    75   by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    76     semigroup.intro monoid_axioms.intro
    77     intro: prems)
    78 
    79 lemma (in monoid) Units_closed [dest]:
    80   "x \<in> Units G ==> x \<in> carrier G"
    81   by (unfold Units_def) fast
    82 
    83 lemma (in monoid) inv_unique:
    84   assumes eq: "y \<otimes> x = \<one>"  "x \<otimes> y' = \<one>"
    85     and G: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
    86   shows "y = y'"
    87 proof -
    88   from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
    89   also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
    90   also from G eq have "... = y'" by simp
    91   finally show ?thesis .
    92 qed
    93 
    94 lemma (in monoid) Units_one_closed [intro, simp]:
    95   "\<one> \<in> Units G"
    96   by (unfold Units_def) auto
    97 
    98 lemma (in monoid) Units_inv_closed [intro, simp]:
    99   "x \<in> Units G ==> inv x \<in> carrier G"
   100   apply (unfold Units_def m_inv_def, auto)
   101   apply (rule theI2, fast)
   102    apply (fast intro: inv_unique, fast)
   103   done
   104 
   105 lemma (in monoid) Units_l_inv:
   106   "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   107   apply (unfold Units_def m_inv_def, auto)
   108   apply (rule theI2, fast)
   109    apply (fast intro: inv_unique, fast)
   110   done
   111 
   112 lemma (in monoid) Units_r_inv:
   113   "x \<in> Units G ==> x \<otimes> inv x = \<one>"
   114   apply (unfold Units_def m_inv_def, auto)
   115   apply (rule theI2, fast)
   116    apply (fast intro: inv_unique, fast)
   117   done
   118 
   119 lemma (in monoid) Units_inv_Units [intro, simp]:
   120   "x \<in> Units G ==> inv x \<in> Units G"
   121 proof -
   122   assume x: "x \<in> Units G"
   123   show "inv x \<in> Units G"
   124     by (auto simp add: Units_def
   125       intro: Units_l_inv Units_r_inv x Units_closed [OF x])
   126 qed
   127 
   128 lemma (in monoid) Units_l_cancel [simp]:
   129   "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
   130    (x \<otimes> y = x \<otimes> z) = (y = z)"
   131 proof
   132   assume eq: "x \<otimes> y = x \<otimes> z"
   133     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   134   then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
   135     by (simp add: m_assoc Units_closed)
   136   with G show "y = z" by (simp add: Units_l_inv)
   137 next
   138   assume eq: "y = z"
   139     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   140   then show "x \<otimes> y = x \<otimes> z" by simp
   141 qed
   142 
   143 lemma (in monoid) Units_inv_inv [simp]:
   144   "x \<in> Units G ==> inv (inv x) = x"
   145 proof -
   146   assume x: "x \<in> Units G"
   147   then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
   148     by (simp add: Units_l_inv Units_r_inv)
   149   with x show ?thesis by (simp add: Units_closed)
   150 qed
   151 
   152 lemma (in monoid) inv_inj_on_Units:
   153   "inj_on (m_inv G) (Units G)"
   154 proof (rule inj_onI)
   155   fix x y
   156   assume G: "x \<in> Units G"  "y \<in> Units G" and eq: "inv x = inv y"
   157   then have "inv (inv x) = inv (inv y)" by simp
   158   with G show "x = y" by simp
   159 qed
   160 
   161 lemma (in monoid) Units_inv_comm:
   162   assumes inv: "x \<otimes> y = \<one>"
   163     and G: "x \<in> Units G"  "y \<in> Units G"
   164   shows "y \<otimes> x = \<one>"
   165 proof -
   166   from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
   167   with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
   168 qed
   169 
   170 text {* Power *}
   171 
   172 lemma (in monoid) nat_pow_closed [intro, simp]:
   173   "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
   174   by (induct n) (simp_all add: nat_pow_def)
   175 
   176 lemma (in monoid) nat_pow_0 [simp]:
   177   "x (^) (0::nat) = \<one>"
   178   by (simp add: nat_pow_def)
   179 
   180 lemma (in monoid) nat_pow_Suc [simp]:
   181   "x (^) (Suc n) = x (^) n \<otimes> x"
   182   by (simp add: nat_pow_def)
   183 
   184 lemma (in monoid) nat_pow_one [simp]:
   185   "\<one> (^) (n::nat) = \<one>"
   186   by (induct n) simp_all
   187 
   188 lemma (in monoid) nat_pow_mult:
   189   "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
   190   by (induct m) (simp_all add: m_assoc [THEN sym])
   191 
   192 lemma (in monoid) nat_pow_pow:
   193   "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
   194   by (induct m) (simp, simp add: nat_pow_mult add_commute)
   195 
   196 text {*
   197   A group is a monoid all of whose elements are invertible.
   198 *}
   199 
   200 locale group = monoid +
   201   assumes Units: "carrier G <= Units G"
   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 alternative definition of submagma
   380 
   381 locale submagma = var H + struct G +
   382   assumes subset [intro, simp]: "carrier H \<subseteq> carrier G"
   383     and m_equal [simp]: "mult H = mult G"
   384     and m_closed [intro, simp]:
   385       "[| x \<in> carrier H; y \<in> carrier H |] ==> x \<otimes> y \<in> carrier H"
   386 *)
   387 
   388 lemma submagma_imp_subset:
   389   "submagma H G ==> H \<subseteq> carrier G"
   390   by (rule submagma.subset)
   391 
   392 lemma (in submagma) subsetD [dest, simp]:
   393   "x \<in> H ==> x \<in> carrier G"
   394   using subset by blast
   395 
   396 lemma (in submagma) magmaI [intro]:
   397   includes magma G
   398   shows "magma (G(| carrier := H |))"
   399   by rule simp
   400 
   401 lemma (in submagma) semigroup_axiomsI [intro]:
   402   includes semigroup G
   403   shows "semigroup_axioms (G(| carrier := H |))"
   404     by rule (simp add: m_assoc)
   405 
   406 lemma (in submagma) semigroupI [intro]:
   407   includes semigroup G
   408   shows "semigroup (G(| carrier := H |))"
   409   using prems by fast
   410 
   411 
   412 locale subgroup = submagma H G +
   413   assumes one_closed [intro, simp]: "\<one> \<in> H"
   414     and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   415 
   416 declare (in subgroup) group.intro [intro]
   417 
   418 lemma (in subgroup) group_axiomsI [intro]:
   419   includes group G
   420   shows "group_axioms (G(| carrier := H |))"
   421   by (rule group_axioms.intro) (auto intro: l_inv r_inv simp add: Units_def)
   422 
   423 lemma (in subgroup) groupI [intro]:
   424   includes group G
   425   shows "group (G(| carrier := H |))"
   426   by (rule groupI) (auto intro: m_assoc l_inv)
   427 
   428 text {*
   429   Since @{term H} is nonempty, it contains some element @{term x}.  Since
   430   it is closed under inverse, it contains @{text "inv x"}.  Since
   431   it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
   432 *}
   433 
   434 lemma (in group) one_in_subset:
   435   "[| 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 |]
   436    ==> \<one> \<in> H"
   437 by (force simp add: l_inv)
   438 
   439 text {* A characterization of subgroups: closed, non-empty subset. *}
   440 
   441 lemma (in group) subgroupI:
   442   assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   443     and inv: "!!a. a \<in> H ==> inv a \<in> H"
   444     and mult: "!!a b. [|a \<in> H; b \<in> H|] ==> a \<otimes> b \<in> H"
   445   shows "subgroup H G"
   446 proof (rule subgroup.intro)
   447   from subset and mult show "submagma H G" by (rule submagma.intro)
   448 next
   449   have "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems)
   450   with inv show "subgroup_axioms H G"
   451     by (intro subgroup_axioms.intro) simp_all
   452 qed
   453 
   454 text {*
   455   Repeat facts of submagmas for subgroups.  Necessary???
   456 *}
   457 
   458 lemma (in subgroup) subset:
   459   "H \<subseteq> carrier G"
   460   ..
   461 
   462 lemma (in subgroup) m_closed:
   463   "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   464   ..
   465 
   466 declare magma.m_closed [simp]
   467 
   468 declare monoid.one_closed [iff] group.inv_closed [simp]
   469   monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   470 
   471 lemma subgroup_nonempty:
   472   "~ subgroup {} G"
   473   by (blast dest: subgroup.one_closed)
   474 
   475 lemma (in subgroup) finite_imp_card_positive:
   476   "finite (carrier G) ==> 0 < card H"
   477 proof (rule classical)
   478   have sub: "subgroup H G" using prems by (rule subgroup.intro)
   479   assume fin: "finite (carrier G)"
   480     and zero: "~ 0 < card H"
   481   then have "finite H" by (blast intro: finite_subset dest: subset)
   482   with zero sub have "subgroup {} G" by simp
   483   with subgroup_nonempty show ?thesis by contradiction
   484 qed
   485 
   486 (*
   487 lemma (in monoid) Units_subgroup:
   488   "subgroup (Units G) G"
   489 *)
   490 
   491 subsection {* Direct Products *}
   492 
   493 constdefs (structure G and H)
   494   DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
   495   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   496     mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
   497 
   498   DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
   499   "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
   500 
   501 lemma DirProdSemigroup_magma:
   502   includes magma G + magma H
   503   shows "magma (G \<times>\<^sub>s H)"
   504   by (rule magma.intro) (auto simp add: DirProdSemigroup_def)
   505 
   506 lemma DirProdSemigroup_semigroup_axioms:
   507   includes semigroup G + semigroup H
   508   shows "semigroup_axioms (G \<times>\<^sub>s H)"
   509   by (rule semigroup_axioms.intro)
   510     (auto simp add: DirProdSemigroup_def G.m_assoc H.m_assoc)
   511 
   512 lemma DirProdSemigroup_semigroup:
   513   includes semigroup G + semigroup H
   514   shows "semigroup (G \<times>\<^sub>s H)"
   515   using prems
   516   by (fast intro: semigroup.intro
   517     DirProdSemigroup_magma DirProdSemigroup_semigroup_axioms)
   518 
   519 lemma DirProdGroup_magma:
   520   includes magma G + magma H
   521   shows "magma (G \<times>\<^sub>g H)"
   522   by (rule magma.intro)
   523     (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   524 
   525 lemma DirProdGroup_semigroup_axioms:
   526   includes semigroup G + semigroup H
   527   shows "semigroup_axioms (G \<times>\<^sub>g H)"
   528   by (rule semigroup_axioms.intro)
   529     (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
   530       G.m_assoc H.m_assoc)
   531 
   532 lemma DirProdGroup_semigroup:
   533   includes semigroup G + semigroup H
   534   shows "semigroup (G \<times>\<^sub>g H)"
   535   using prems
   536   by (fast intro: semigroup.intro
   537     DirProdGroup_magma DirProdGroup_semigroup_axioms)
   538 
   539 text {* \dots\ and further lemmas for group \dots *}
   540 
   541 lemma DirProdGroup_group:
   542   includes group G + group H
   543   shows "group (G \<times>\<^sub>g H)"
   544   by (rule groupI)
   545     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   546       simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   547 
   548 lemma carrier_DirProdGroup [simp]:
   549      "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
   550   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   551 
   552 lemma one_DirProdGroup [simp]:
   553      "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
   554   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   555 
   556 lemma mult_DirProdGroup [simp]:
   557      "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
   558   by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
   559 
   560 lemma inv_DirProdGroup [simp]:
   561   includes group G + group H
   562   assumes g: "g \<in> carrier G"
   563       and h: "h \<in> carrier H"
   564   shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
   565   apply (rule group.inv_equality [OF DirProdGroup_group])
   566   apply (simp_all add: prems group_def group.l_inv)
   567   done
   568 
   569 subsection {* Homomorphisms *}
   570 
   571 constdefs (structure G and H)
   572   hom :: "_ => _ => ('a => 'b) set"
   573   "hom G H ==
   574     {h. h \<in> carrier G -> carrier H &
   575       (\<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)}"
   576 
   577 lemma (in semigroup) hom:
   578   includes semigroup G
   579   shows "semigroup (| carrier = hom G G, mult = op o |)"
   580 proof (rule semigroup.intro)
   581   show "magma (| carrier = hom G G, mult = op o |)"
   582     by (rule magma.intro) (simp add: Pi_def hom_def)
   583 next
   584   show "semigroup_axioms (| carrier = hom G G, mult = op o |)"
   585     by (rule semigroup_axioms.intro) (simp add: o_assoc)
   586 qed
   587 
   588 lemma hom_mult:
   589   "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
   590    ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
   591   by (simp add: hom_def)
   592 
   593 lemma hom_closed:
   594   "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
   595   by (auto simp add: hom_def funcset_mem)
   596 
   597 lemma compose_hom:
   598      "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
   599       ==> compose (carrier G) h h' \<in> hom G G"
   600 apply (simp (no_asm_simp) add: hom_def)
   601 apply (intro conjI)
   602  apply (force simp add: funcset_compose hom_def)
   603 apply (simp add: compose_def group.axioms hom_mult funcset_mem)
   604 done
   605 
   606 locale group_hom = group G + group H + var h +
   607   assumes homh: "h \<in> hom G H"
   608   notes hom_mult [simp] = hom_mult [OF homh]
   609     and hom_closed [simp] = hom_closed [OF homh]
   610 
   611 lemma (in group_hom) one_closed [simp]:
   612   "h \<one> \<in> carrier H"
   613   by simp
   614 
   615 lemma (in group_hom) hom_one [simp]:
   616   "h \<one> = \<one>\<^bsub>H\<^esub>"
   617 proof -
   618   have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
   619     by (simp add: hom_mult [symmetric] del: hom_mult)
   620   then show ?thesis by (simp del: r_one)
   621 qed
   622 
   623 lemma (in group_hom) inv_closed [simp]:
   624   "x \<in> carrier G ==> h (inv x) \<in> carrier H"
   625   by simp
   626 
   627 lemma (in group_hom) hom_inv [simp]:
   628   "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
   629 proof -
   630   assume x: "x \<in> carrier G"
   631   then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
   632     by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
   633   also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
   634     by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
   635   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   636   with x show ?thesis by simp
   637 qed
   638 
   639 subsection {* Commutative Structures *}
   640 
   641 text {*
   642   Naming convention: multiplicative structures that are commutative
   643   are called \emph{commutative}, additive structures are called
   644   \emph{Abelian}.
   645 *}
   646 
   647 subsection {* Definition *}
   648 
   649 locale comm_semigroup = semigroup +
   650   assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   651 
   652 lemma (in comm_semigroup) m_lcomm:
   653   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   654    x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   655 proof -
   656   assume xyz: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   657   from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
   658   also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
   659   also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
   660   finally show ?thesis .
   661 qed
   662 
   663 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
   664 
   665 locale comm_monoid = comm_semigroup + monoid
   666 
   667 lemma comm_monoidI:
   668   includes struct G
   669   assumes m_closed:
   670       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   671     and one_closed: "\<one> \<in> carrier G"
   672     and m_assoc:
   673       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   674       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   675     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   676     and m_comm:
   677       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   678   shows "comm_monoid G"
   679   using l_one
   680   by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   681     comm_semigroup_axioms.intro monoid_axioms.intro
   682     intro: prems simp: m_closed one_closed m_comm)
   683 
   684 lemma (in monoid) monoid_comm_monoidI:
   685   assumes m_comm:
   686       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   687   shows "comm_monoid G"
   688   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   689 (*lemma (in comm_monoid) r_one [simp]:
   690   "x \<in> carrier G ==> x \<otimes> \<one> = x"
   691 proof -
   692   assume G: "x \<in> carrier G"
   693   then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
   694   also from G have "... = x" by simp
   695   finally show ?thesis .
   696 qed*)
   697 lemma (in comm_monoid) nat_pow_distr:
   698   "[| x \<in> carrier G; y \<in> carrier G |] ==>
   699   (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   700   by (induct n) (simp, simp add: m_ac)
   701 
   702 locale comm_group = comm_monoid + group
   703 
   704 lemma (in group) group_comm_groupI:
   705   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   706       x \<otimes> y = y \<otimes> x"
   707   shows "comm_group G"
   708   by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   709     group.axioms prems)
   710 
   711 lemma comm_groupI:
   712   includes struct G
   713   assumes m_closed:
   714       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
   715     and one_closed: "\<one> \<in> carrier G"
   716     and m_assoc:
   717       "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   718       (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   719     and m_comm:
   720       "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   721     and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
   722     and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
   723   shows "comm_group G"
   724   by (fast intro: group.group_comm_groupI groupI prems)
   725 
   726 lemma (in comm_group) inv_mult:
   727   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   728   by (simp add: m_ac inv_mult_group)
   729 
   730 end