src/HOL/Algebra/Group.thy
changeset 13949 0ce528cd6f19
parent 13944 9b34607cd83e
child 13975 c8e9a89883ce
     1.1 --- a/src/HOL/Algebra/Group.thy	Fri May 02 16:43:36 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Fri May 02 20:02:50 2003 +0200
     1.3 @@ -6,14 +6,14 @@
     1.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     1.5  *)
     1.6  
     1.7 -header {* Algebraic Structures up to Commutative Groups *}
     1.8 +header {* Groups *}
     1.9  
    1.10  theory Group = FuncSet:
    1.11  
    1.12 -axclass number < type
    1.13 +(* axclass number < type
    1.14  
    1.15  instance nat :: number ..
    1.16 -instance int :: number ..
    1.17 +instance int :: number .. *)
    1.18  
    1.19  section {* From Magmas to Groups *}
    1.20  
    1.21 @@ -416,12 +416,7 @@
    1.22      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
    1.23  
    1.24  declare (in subgroup) group.intro [intro]
    1.25 -(*
    1.26 -lemma (in subgroup) l_oneI [intro]:
    1.27 -  includes l_one G
    1.28 -  shows "l_one (G(| carrier := H |))"
    1.29 -  by rule simp_all
    1.30 -*)
    1.31 +
    1.32  lemma (in subgroup) group_axiomsI [intro]:
    1.33    includes group G
    1.34    shows "group_axioms (G(| carrier := H |))"
    1.35 @@ -511,15 +506,6 @@
    1.36    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
    1.37      mult = mult (G \<times>\<^sub>s H),
    1.38      one = (one G, one H) |)"
    1.39 -(*
    1.40 -  DirProdGroup ::
    1.41 -    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
    1.42 -    (infixr "\<times>\<^sub>g" 80)
    1.43 -  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    1.44 -    mult = mult (G \<times>\<^sub>m H),
    1.45 -    one = one (G \<times>\<^sub>m H),
    1.46 -    m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
    1.47 -*)
    1.48  
    1.49  lemma DirProdSemigroup_magma:
    1.50    includes magma G + magma H
    1.51 @@ -659,7 +645,7 @@
    1.52    with x show ?thesis by simp
    1.53  qed
    1.54  
    1.55 -section {* Commutative Structures *}
    1.56 +subsection {* Commutative Structures *}
    1.57  
    1.58  text {*
    1.59    Naming convention: multiplicative structures that are commutative