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
```