src/HOL/Algebra/Group.thy
changeset 14651 02b8f3bcf7fe
parent 14551 2cb6ff394bfb
child 14693 4deda204e1d8
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu Apr 22 11:00:22 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu Apr 22 11:01:34 2004 +0200
     1.3 @@ -31,14 +31,12 @@
     1.4  record 'a monoid = "'a semigroup" +
     1.5    one :: 'a ("\<one>\<index>")
     1.6  
     1.7 -constdefs
     1.8 -  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
     1.9 -  "m_inv G x == (THE y. y \<in> carrier G &
    1.10 -                  mult G x y = one G & mult G y x = one G)"
    1.11 +constdefs (structure G)
    1.12 +  m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
    1.13 +  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    1.14  
    1.15 -  Units :: "('a, 'm) monoid_scheme => 'a set"
    1.16 -  "Units G == {y. y \<in> carrier G &
    1.17 -                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
    1.18 +  Units :: "_ => 'a set"
    1.19 +  "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    1.20  
    1.21  consts
    1.22    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    1.23 @@ -492,20 +490,13 @@
    1.24  
    1.25  subsection {* Direct Products *}
    1.26  
    1.27 -constdefs
    1.28 -  DirProdSemigroup ::
    1.29 -    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
    1.30 -    => ('a \<times> 'b) semigroup"
    1.31 -    (infixr "\<times>\<^sub>s" 80)
    1.32 +constdefs (structure G and H)
    1.33 +  DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
    1.34    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    1.35 -    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    1.36 +    mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
    1.37  
    1.38 -  DirProdGroup ::
    1.39 -    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
    1.40 -    (infixr "\<times>\<^sub>g" 80)
    1.41 -  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
    1.42 -    mult = mult (G \<times>\<^sub>s H),
    1.43 -    one = (one G, one H) |)"
    1.44 +  DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
    1.45 +  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
    1.46  
    1.47  lemma DirProdSemigroup_magma:
    1.48    includes magma G + magma H
    1.49 @@ -529,13 +520,13 @@
    1.50    includes magma G + magma H
    1.51    shows "magma (G \<times>\<^sub>g H)"
    1.52    by (rule magma.intro)
    1.53 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
    1.54 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    1.55  
    1.56  lemma DirProdGroup_semigroup_axioms:
    1.57    includes semigroup G + semigroup H
    1.58    shows "semigroup_axioms (G \<times>\<^sub>g H)"
    1.59    by (rule semigroup_axioms.intro)
    1.60 -    (auto simp add: DirProdGroup_def DirProdSemigroup_def
    1.61 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
    1.62        G.m_assoc H.m_assoc)
    1.63  
    1.64  lemma DirProdGroup_semigroup:
    1.65 @@ -545,26 +536,26 @@
    1.66    by (fast intro: semigroup.intro
    1.67      DirProdGroup_magma DirProdGroup_semigroup_axioms)
    1.68  
    1.69 -(* ... and further lemmas for group ... *)
    1.70 +text {* \dots\ and further lemmas for group \dots *}
    1.71  
    1.72  lemma DirProdGroup_group:
    1.73    includes group G + group H
    1.74    shows "group (G \<times>\<^sub>g H)"
    1.75    by (rule groupI)
    1.76      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
    1.77 -      simp add: DirProdGroup_def DirProdSemigroup_def)
    1.78 +      simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    1.79  
    1.80  lemma carrier_DirProdGroup [simp]:
    1.81       "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
    1.82 -  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.83 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    1.84  
    1.85  lemma one_DirProdGroup [simp]:
    1.86       "one (G \<times>\<^sub>g H) = (one G, one H)"
    1.87 -  by (simp add: DirProdGroup_def DirProdSemigroup_def);
    1.88 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    1.89  
    1.90  lemma mult_DirProdGroup [simp]:
    1.91       "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
    1.92 -  by (simp add: DirProdGroup_def DirProdSemigroup_def)
    1.93 +  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
    1.94  
    1.95  lemma inv_DirProdGroup [simp]:
    1.96    includes group G + group H
    1.97 @@ -577,12 +568,11 @@
    1.98  
    1.99  subsection {* Homomorphisms *}
   1.100  
   1.101 -constdefs
   1.102 -  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
   1.103 -    => ('a => 'b)set"
   1.104 +constdefs (structure G and H)
   1.105 +  hom :: "_ => _ => ('a => 'b) set"
   1.106    "hom G H ==
   1.107      {h. h \<in> carrier G -> carrier H &
   1.108 -      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
   1.109 +      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
   1.110  
   1.111  lemma (in semigroup) hom:
   1.112    includes semigroup G