src/HOL/Algebra/Group.thy
 changeset 20318 0e0ea63fe768 parent 19984 29bb4659f80a child 21041 60e418260b4d
equal inserted replaced
20317:6e070b33e72b 20318:0e0ea63fe768
     4   Author: Clemens Ballarin, started 4 February 2003
     4   Author: Clemens Ballarin, started 4 February 2003
     5
     5
     6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     6 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     7 *)
     7 *)
     8
     8
    11 theory Group imports FuncSet Lattice begin
     9 theory Group imports FuncSet Lattice begin
    12
    10
    13
    11
    14 section {* Monoids and Groups *}
    12 section {* Monoids and Groups *}

    13

    14 subsection {* Definitions *}
    15
    15
    16 text {*
    16 text {*
    17   Definitions follow \cite{Jacobson:1985}.
    17   Definitions follow \cite{Jacobson:1985}.
    18 *}
    18 *}
    21
    19
    22 record 'a monoid =  "'a partial_object" +
    20 record 'a monoid =  "'a partial_object" +
    23   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
    21   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
    24   one     :: 'a ("\<one>\<index>")
    22   one     :: 'a ("\<one>\<index>")
    25
    23
   289
   287
   290 lemma (in group) l_inv [simp]:
   288 lemma (in group) l_inv [simp]:
   291   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   289   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   292   using Units_l_inv by simp
   290   using Units_l_inv by simp
   293
   291

   292
   294 subsection {* Cancellation Laws and Basic Properties *}
   293 subsection {* Cancellation Laws and Basic Properties *}
   295
   294
   296 lemma (in group) l_cancel [simp]:
   295 lemma (in group) l_cancel [simp]:
   297   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   296   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   298    (x \<otimes> y = x \<otimes> z) = (y = z)"
   297    (x \<otimes> y = x \<otimes> z) = (y = z)"
   371
   370
   372 lemma (in group) int_pow_one [simp]:
   371 lemma (in group) int_pow_one [simp]:
   373   "\<one> (^) (z::int) = \<one>"
   372   "\<one> (^) (z::int) = \<one>"
   374   by (simp add: int_pow_def2)
   373   by (simp add: int_pow_def2)
   375
   374

   375
   376 subsection {* Subgroups *}
   376 subsection {* Subgroups *}
   377
   377
   378 locale subgroup =
   378 locale subgroup =
   379   fixes H and G (structure)
   379   fixes H and G (structure)
   380   assumes subset: "H \<subseteq> carrier G"
   380   assumes subset: "H \<subseteq> carrier G"
   381     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
   381     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
   382     and  one_closed [simp]: "\<one> \<in> H"
   382     and one_closed [simp]: "\<one> \<in> H"
   383     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
   383     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"

   384

   385 lemma (in subgroup) is_subgroup:

   386   "subgroup H G" .
   384
   387
   385 declare (in subgroup) group.intro [intro]
   388 declare (in subgroup) group.intro [intro]
   386
   389
   387 lemma (in subgroup) mem_carrier [simp]:
   390 lemma (in subgroup) mem_carrier [simp]:
   388   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   391   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   437
   440
   438 (*
   441 (*
   439 lemma (in monoid) Units_subgroup:
   442 lemma (in monoid) Units_subgroup:
   440   "subgroup (Units G) G"
   443   "subgroup (Units G) G"
   441 *)
   444 *)

   445
   442
   446
   443 subsection {* Direct Products *}
   447 subsection {* Direct Products *}
   444
   448
   445 constdefs
   449 constdefs
   446   DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid"  (infixr "\<times>\<times>" 80)
   450   DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid"  (infixr "\<times>\<times>" 80)
   522      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
   526      "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
   523 apply (auto simp add: hom_def funcset_compose)
   527 apply (auto simp add: hom_def funcset_compose)
   524 apply (simp add: compose_def funcset_mem)
   528 apply (simp add: compose_def funcset_mem)
   525 done
   529 done
   526
   530
   530 constdefs
   531 constdefs
   531   iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
   532   iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
   532   "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
   533   "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
   533
   534
   534 lemma iso_refl: "(%x. x) \<in> G \<cong> G"
   535 lemma iso_refl: "(%x. x) \<in> G \<cong> G"
   588     by (simp add: hom_mult [symmetric] del: hom_mult)
   589     by (simp add: hom_mult [symmetric] del: hom_mult)
   589   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   590   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
   590   with x show ?thesis by (simp del: H.r_inv)
   591   with x show ?thesis by (simp del: H.r_inv)
   591 qed
   592 qed
   592
   593

   594
   593 subsection {* Commutative Structures *}
   595 subsection {* Commutative Structures *}
   594
   596
   595 text {*
   597 text {*
   596   Naming convention: multiplicative structures that are commutative
   598   Naming convention: multiplicative structures that are commutative
   597   are called \emph{commutative}, additive structures are called
   599   are called \emph{commutative}, additive structures are called
   598   \emph{Abelian}.
   600   \emph{Abelian}.
   599 *}
   601 *}
   602
   602
   603 locale comm_monoid = monoid +
   603 locale comm_monoid = monoid +
   604   assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
   604   assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
   605
   605
   606 lemma (in comm_monoid) m_lcomm:
   606 lemma (in comm_monoid) m_lcomm:
   677
   677
   678 lemma (in comm_group) inv_mult:
   678 lemma (in comm_group) inv_mult:
   679   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   679   "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   680   by (simp add: m_ac inv_mult_group)
   680   by (simp add: m_ac inv_mult_group)
   681
   681
   682 subsection {* Lattice of subgroups of a group *}
   682

   683 subsection {* The Lattice of Subgroups of a Group *}
   683
   684
   684 text_raw {* \label{sec:subgroup-lattice} *}
   685 text_raw {* \label{sec:subgroup-lattice} *}
   685
   686
   686 theorem (in group) subgroups_partial_order:
   687 theorem (in group) subgroups_partial_order:
   687   "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
   688   "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"