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