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