src/HOL/Algebra/Group.thy
changeset 13854 91c9ab25fece
parent 13835 12b2ffbe543a
child 13936 d3671b878828
     1.1 --- a/src/HOL/Algebra/Group.thy	Mon Mar 10 16:21:06 2003 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Mar 10 17:25:34 2003 +0100
     1.3 @@ -20,14 +20,6 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -(* The following may be unnecessary. *)
     1.8 -text {*
     1.9 -  We write groups additively.  This simplifies notation for rings.
    1.10 -  All rings have an additive inverse, only fields have a
    1.11 -  multiplicative one.  This definitions reduces the need for
    1.12 -  qualifiers.
    1.13 -*}
    1.14 -
    1.15  record 'a semigroup =
    1.16    carrier :: "'a set"
    1.17    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    1.18 @@ -104,6 +96,14 @@
    1.19    then show "y \<otimes> x = z \<otimes> x" by simp
    1.20  qed
    1.21  
    1.22 +lemma (in group) inv_one [simp]:
    1.23 +  "inv \<one> = \<one>"
    1.24 +proof -
    1.25 +  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by simp
    1.26 +  moreover have "... = \<one>" by (simp add: r_inv)
    1.27 +  finally show ?thesis .
    1.28 +qed
    1.29 +
    1.30  lemma (in group) inv_inv [simp]:
    1.31    "x \<in> carrier G ==> inv (inv x) = x"
    1.32  proof -
    1.33 @@ -112,7 +112,7 @@
    1.34    with x show ?thesis by simp
    1.35  qed
    1.36  
    1.37 -lemma (in group) inv_mult:
    1.38 +lemma (in group) inv_mult_group:
    1.39    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
    1.40  proof -
    1.41    assume G: "x \<in> carrier G" "y \<in> carrier G"
    1.42 @@ -245,21 +245,21 @@
    1.43  
    1.44  constdefs
    1.45    DirProdSemigroup ::
    1.46 -    "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
    1.47 +    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
    1.48      => ('a \<times> 'b) semigroup"
    1.49      (infixr "\<times>\<^sub>s" 80)
    1.50    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
    1.51      mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
    1.52  
    1.53    DirProdMonoid ::
    1.54 -    "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a \<times> 'b) monoid"
    1.55 +    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
    1.56      (infixr "\<times>\<^sub>m" 80)
    1.57    "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
    1.58      mult = mult (G \<times>\<^sub>s H),
    1.59      one = (one G, one H) |)"
    1.60  
    1.61    DirProdGroup ::
    1.62 -    "[('a, 'c) group_scheme, ('b, 'd) group_scheme] => ('a \<times> 'b) group"
    1.63 +    "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
    1.64      (infixr "\<times>\<^sub>g" 80)
    1.65    "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>m H),
    1.66      mult = mult (G \<times>\<^sub>m H),
    1.67 @@ -409,4 +409,8 @@
    1.68  
    1.69  locale abelian_group = abelian_monoid + group
    1.70  
    1.71 +lemma (in abelian_group) inv_mult:
    1.72 +  "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
    1.73 +  by (simp add: ac inv_mult_group)
    1.74 +
    1.75  end