src/HOL/Algebra/Group.thy
changeset 13936 d3671b878828
parent 13854 91c9ab25fece
child 13940 c67798653056
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Apr 29 12:36:49 2003 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Apr 30 10:01:35 2003 +0200
     1.3 @@ -6,18 +6,23 @@
     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 Abelian Groups *}
     1.8 +header {* Algebraic Structures up to Commutative Groups *}
     1.9  
    1.10  theory Group = FuncSet:
    1.11  
    1.12 +axclass number < type
    1.13 +
    1.14 +instance nat :: number ..
    1.15 +instance int :: number ..
    1.16 +
    1.17 +section {* From Magmas to Groups *}
    1.18 +
    1.19  text {*
    1.20    Definitions follow Jacobson, Basic Algebra I, Freeman, 1985; with
    1.21    the exception of \emph{magma} which, following Bourbaki, is a set
    1.22    together with a binary, closed operation.
    1.23  *}
    1.24  
    1.25 -section {* From Magmas to Groups *}
    1.26 -
    1.27  subsection {* Definitions *}
    1.28  
    1.29  record 'a semigroup =
    1.30 @@ -27,8 +32,23 @@
    1.31  record 'a monoid = "'a semigroup" +
    1.32    one :: 'a ("\<one>\<index>")
    1.33  
    1.34 -record 'a group = "'a monoid" +
    1.35 -  m_inv :: "'a => 'a" ("inv\<index> _" [81] 80)
    1.36 +constdefs
    1.37 +  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
    1.38 +  "m_inv G x == (THE y. y \<in> carrier G &
    1.39 +                  mult G x y = one G & mult G y x = one G)"
    1.40 +
    1.41 +  Units :: "('a, 'm) monoid_scheme => 'a set"
    1.42 +  "Units G == {y. y \<in> carrier G &
    1.43 +                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
    1.44 +
    1.45 +consts
    1.46 +  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    1.47 +
    1.48 +defs (overloaded)
    1.49 +  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
    1.50 +  int_pow_def: "pow G a z ==
    1.51 +    let p = nat_rec (one G) (%u b. mult G b a)
    1.52 +    in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
    1.53  
    1.54  locale magma = struct G +
    1.55    assumes m_closed [intro, simp]:
    1.56 @@ -37,32 +57,237 @@
    1.57  locale semigroup = magma +
    1.58    assumes m_assoc:
    1.59      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.60 -     (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.61 +    (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    1.62  
    1.63 -locale l_one = struct G +
    1.64 +locale monoid = semigroup +
    1.65    assumes one_closed [intro, simp]: "\<one> \<in> carrier G"
    1.66      and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x"
    1.67 +    and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
    1.68  
    1.69 -locale group = semigroup + l_one +
    1.70 -  assumes inv_closed [intro, simp]: "x \<in> carrier G ==> inv x \<in> carrier G"
    1.71 -    and l_inv: "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    1.72 +lemma monoidI:
    1.73 +  assumes m_closed:
    1.74 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
    1.75 +    and one_closed: "one G \<in> carrier G"
    1.76 +    and m_assoc:
    1.77 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.78 +      mult G (mult G x y) z = mult G x (mult G y z)"
    1.79 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
    1.80 +    and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
    1.81 +  shows "monoid G"
    1.82 +  by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
    1.83 +    semigroup.intro monoid_axioms.intro
    1.84 +    intro: prems)
    1.85 +
    1.86 +lemma (in monoid) Units_closed [dest]:
    1.87 +  "x \<in> Units G ==> x \<in> carrier G"
    1.88 +  by (unfold Units_def) fast
    1.89 +
    1.90 +lemma (in monoid) inv_unique:
    1.91 +  assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
    1.92 +    and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
    1.93 +  shows "y = y'"
    1.94 +proof -
    1.95 +  from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
    1.96 +  also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc)
    1.97 +  also from G eq have "... = y'" by simp
    1.98 +  finally show ?thesis .
    1.99 +qed
   1.100 +
   1.101 +lemma (in monoid) Units_inv_closed [intro, simp]:
   1.102 +  "x \<in> Units G ==> inv x \<in> carrier G"
   1.103 +  apply (unfold Units_def m_inv_def)
   1.104 +  apply auto
   1.105 +  apply (rule theI2, fast)
   1.106 +   apply (fast intro: inv_unique)
   1.107 +  apply fast
   1.108 +  done
   1.109 +
   1.110 +lemma (in monoid) Units_l_inv:
   1.111 +  "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   1.112 +  apply (unfold Units_def m_inv_def)
   1.113 +  apply auto
   1.114 +  apply (rule theI2, fast)
   1.115 +   apply (fast intro: inv_unique)
   1.116 +  apply fast
   1.117 +  done
   1.118 +
   1.119 +lemma (in monoid) Units_r_inv:
   1.120 +  "x \<in> Units G ==> x \<otimes> inv x = \<one>"
   1.121 +  apply (unfold Units_def m_inv_def)
   1.122 +  apply auto
   1.123 +  apply (rule theI2, fast)
   1.124 +   apply (fast intro: inv_unique)
   1.125 +  apply fast
   1.126 +  done
   1.127 +
   1.128 +lemma (in monoid) Units_inv_Units [intro, simp]:
   1.129 +  "x \<in> Units G ==> inv x \<in> Units G"
   1.130 +proof -
   1.131 +  assume x: "x \<in> Units G"
   1.132 +  show "inv x \<in> Units G"
   1.133 +    by (auto simp add: Units_def
   1.134 +      intro: Units_l_inv Units_r_inv x Units_closed [OF x])
   1.135 +qed
   1.136 +
   1.137 +lemma (in monoid) Units_l_cancel [simp]:
   1.138 +  "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.139 +   (x \<otimes> y = x \<otimes> z) = (y = z)"
   1.140 +proof
   1.141 +  assume eq: "x \<otimes> y = x \<otimes> z"
   1.142 +    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
   1.143 +  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
   1.144 +    by (simp add: m_assoc Units_closed)
   1.145 +  with G show "y = z" by (simp add: Units_l_inv)
   1.146 +next
   1.147 +  assume eq: "y = z"
   1.148 +    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
   1.149 +  then show "x \<otimes> y = x \<otimes> z" by simp
   1.150 +qed
   1.151 +
   1.152 +lemma (in monoid) Units_inv_inv [simp]:
   1.153 +  "x \<in> Units G ==> inv (inv x) = x"
   1.154 +proof -
   1.155 +  assume x: "x \<in> Units G"
   1.156 +  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
   1.157 +    by (simp add: Units_l_inv Units_r_inv)
   1.158 +  with x show ?thesis by (simp add: Units_closed)
   1.159 +qed
   1.160 +
   1.161 +lemma (in monoid) inv_inj_on_Units:
   1.162 +  "inj_on (m_inv G) (Units G)"
   1.163 +proof (rule inj_onI)
   1.164 +  fix x y
   1.165 +  assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
   1.166 +  then have "inv (inv x) = inv (inv y)" by simp
   1.167 +  with G show "x = y" by simp
   1.168 +qed
   1.169 +
   1.170 +text {* Power *}
   1.171 +
   1.172 +lemma (in monoid) nat_pow_closed [intro, simp]:
   1.173 +  "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
   1.174 +  by (induct n) (simp_all add: nat_pow_def)
   1.175 +
   1.176 +lemma (in monoid) nat_pow_0 [simp]:
   1.177 +  "x (^) (0::nat) = \<one>"
   1.178 +  by (simp add: nat_pow_def)
   1.179 +
   1.180 +lemma (in monoid) nat_pow_Suc [simp]:
   1.181 +  "x (^) (Suc n) = x (^) n \<otimes> x"
   1.182 +  by (simp add: nat_pow_def)
   1.183 +
   1.184 +lemma (in monoid) nat_pow_one [simp]:
   1.185 +  "\<one> (^) (n::nat) = \<one>"
   1.186 +  by (induct n) simp_all
   1.187 +
   1.188 +lemma (in monoid) nat_pow_mult:
   1.189 +  "x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)"
   1.190 +  by (induct m) (simp_all add: m_assoc [THEN sym])
   1.191 +
   1.192 +lemma (in monoid) nat_pow_pow:
   1.193 +  "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
   1.194 +  by (induct m) (simp, simp add: nat_pow_mult add_commute)
   1.195 +
   1.196 +text {*
   1.197 +  A group is a monoid all of whose elements are invertible.
   1.198 +*}
   1.199 +
   1.200 +locale group = monoid +
   1.201 +  assumes Units: "carrier G <= Units G"
   1.202 +
   1.203 +theorem groupI:
   1.204 +  assumes m_closed [simp]:
   1.205 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   1.206 +    and one_closed [simp]: "one G \<in> carrier G"
   1.207 +    and m_assoc:
   1.208 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.209 +      mult G (mult G x y) z = mult G x (mult G y z)"
   1.210 +    and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   1.211 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   1.212 +  shows "group G"
   1.213 +proof -
   1.214 +  have l_cancel [simp]:
   1.215 +    "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.216 +    (mult G x y = mult G x z) = (y = z)"
   1.217 +  proof
   1.218 +    fix x y z
   1.219 +    assume eq: "mult G x y = mult G x z"
   1.220 +      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.221 +    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   1.222 +      and l_inv: "mult G x_inv x = one G" by fast
   1.223 +    from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
   1.224 +      by (simp add: m_assoc)
   1.225 +    with G show "y = z" by (simp add: l_inv)
   1.226 +  next
   1.227 +    fix x y z
   1.228 +    assume eq: "y = z"
   1.229 +      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.230 +    then show "mult G x y = mult G x z" by simp
   1.231 +  qed
   1.232 +  have r_one:
   1.233 +    "!!x. x \<in> carrier G ==> mult G x (one G) = x"
   1.234 +  proof -
   1.235 +    fix x
   1.236 +    assume x: "x \<in> carrier G"
   1.237 +    with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
   1.238 +      and l_inv: "mult G x_inv x = one G" by fast
   1.239 +    from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
   1.240 +      by (simp add: m_assoc [symmetric] l_inv)
   1.241 +    with x xG show "mult G x (one G) = x" by simp 
   1.242 +  qed
   1.243 +  have inv_ex:
   1.244 +    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
   1.245 +      mult G x y = one G"
   1.246 +  proof -
   1.247 +    fix x
   1.248 +    assume x: "x \<in> carrier G"
   1.249 +    with l_inv_ex obtain y where y: "y \<in> carrier G"
   1.250 +      and l_inv: "mult G y x = one G" by fast
   1.251 +    from x y have "mult G y (mult G x y) = mult G y (one G)"
   1.252 +      by (simp add: m_assoc [symmetric] l_inv r_one)
   1.253 +    with x y have r_inv: "mult G x y = one G"
   1.254 +      by simp
   1.255 +    from x y show "EX y : carrier G. mult G y x = one G &
   1.256 +      mult G x y = one G"
   1.257 +      by (fast intro: l_inv r_inv)
   1.258 +  qed
   1.259 +  then have carrier_subset_Units: "carrier G <= Units G"
   1.260 +    by (unfold Units_def) fast
   1.261 +  show ?thesis
   1.262 +    by (fast intro!: group.intro magma.intro semigroup_axioms.intro
   1.263 +      semigroup.intro monoid_axioms.intro group_axioms.intro
   1.264 +      carrier_subset_Units intro: prems r_one)
   1.265 +qed
   1.266 +
   1.267 +lemma (in monoid) monoid_groupI:
   1.268 +  assumes l_inv_ex:
   1.269 +    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   1.270 +  shows "group G"
   1.271 +  by (rule groupI) (auto intro: m_assoc l_inv_ex)
   1.272 +
   1.273 +lemma (in group) Units_eq [simp]:
   1.274 +  "Units G = carrier G"
   1.275 +proof
   1.276 +  show "Units G <= carrier G" by fast
   1.277 +next
   1.278 +  show "carrier G <= Units G" by (rule Units)
   1.279 +qed
   1.280 +
   1.281 +lemma (in group) inv_closed [intro, simp]:
   1.282 +  "x \<in> carrier G ==> inv x \<in> carrier G"
   1.283 +  using Units_inv_closed by simp
   1.284 +
   1.285 +lemma (in group) l_inv:
   1.286 +  "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
   1.287 +  using Units_l_inv by simp
   1.288  
   1.289  subsection {* Cancellation Laws and Basic Properties *}
   1.290  
   1.291  lemma (in group) l_cancel [simp]:
   1.292    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.293     (x \<otimes> y = x \<otimes> z) = (y = z)"
   1.294 -proof
   1.295 -  assume eq: "x \<otimes> y = x \<otimes> z"
   1.296 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.297 -  then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" by (simp add: m_assoc)
   1.298 -  with G show "y = z" by (simp add: l_inv)
   1.299 -next
   1.300 -  assume eq: "y = z"
   1.301 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   1.302 -  then show "x \<otimes> y = x \<otimes> z" by simp
   1.303 -qed
   1.304 -
   1.305 +  using Units_l_inv by simp
   1.306 +(*
   1.307  lemma (in group) r_one [simp]:  
   1.308    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   1.309  proof -
   1.310 @@ -71,7 +296,7 @@
   1.311      by (simp add: m_assoc [symmetric] l_inv)
   1.312    with x show ?thesis by simp 
   1.313  qed
   1.314 -
   1.315 +*)
   1.316  lemma (in group) r_inv:
   1.317    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
   1.318  proof -
   1.319 @@ -106,11 +331,11 @@
   1.320  
   1.321  lemma (in group) inv_inv [simp]:
   1.322    "x \<in> carrier G ==> inv (inv x) = x"
   1.323 -proof -
   1.324 -  assume x: "x \<in> carrier G"
   1.325 -  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by (simp add: l_inv r_inv)
   1.326 -  with x show ?thesis by simp
   1.327 -qed
   1.328 +  using Units_inv_inv by simp
   1.329 +
   1.330 +lemma (in group) inv_inj:
   1.331 +  "inj_on (m_inv G) (carrier G)"
   1.332 +  using inv_inj_on_Units by simp
   1.333  
   1.334  lemma (in group) inv_mult_group:
   1.335    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
   1.336 @@ -121,6 +346,20 @@
   1.337    with G show ?thesis by simp
   1.338  qed
   1.339  
   1.340 +text {* Power *}
   1.341 +
   1.342 +lemma (in group) int_pow_def2:
   1.343 +  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
   1.344 +  by (simp add: int_pow_def nat_pow_def Let_def)
   1.345 +
   1.346 +lemma (in group) int_pow_0 [simp]:
   1.347 +  "x (^) (0::int) = \<one>"
   1.348 +  by (simp add: int_pow_def2)
   1.349 +
   1.350 +lemma (in group) int_pow_one [simp]:
   1.351 +  "\<one> (^) (z::int) = \<one>"
   1.352 +  by (simp add: int_pow_def2)
   1.353 +
   1.354  subsection {* Substructures *}
   1.355  
   1.356  locale submagma = var H + struct G +
   1.357 @@ -128,7 +367,7 @@
   1.358      and m_closed [intro, simp]: "[| x \<in> H; y \<in> H |] ==> x \<otimes> y \<in> H"
   1.359  
   1.360  declare (in submagma) magma.intro [intro] semigroup.intro [intro]
   1.361 -
   1.362 +  semigroup_axioms.intro [intro]
   1.363  (*
   1.364  alternative definition of submagma
   1.365  
   1.366 @@ -167,21 +406,21 @@
   1.367      and m_inv_closed [intro, simp]: "x \<in> H ==> inv x \<in> H"
   1.368  
   1.369  declare (in subgroup) group.intro [intro]
   1.370 -
   1.371 +(*
   1.372  lemma (in subgroup) l_oneI [intro]:
   1.373    includes l_one G
   1.374    shows "l_one (G(| carrier := H |))"
   1.375    by rule simp_all
   1.376 -
   1.377 +*)
   1.378  lemma (in subgroup) group_axiomsI [intro]:
   1.379    includes group G
   1.380    shows "group_axioms (G(| carrier := H |))"
   1.381 -  by rule (simp_all add: l_inv)
   1.382 +  by rule (auto intro: l_inv r_inv simp add: Units_def)
   1.383  
   1.384  lemma (in subgroup) groupI [intro]:
   1.385    includes group G
   1.386    shows "group (G(| carrier := H |))"
   1.387 -  using prems by fast
   1.388 +  by (rule groupI) (auto intro: m_assoc l_inv)
   1.389  
   1.390  text {*
   1.391    Since @{term H} is nonempty, it contains some element @{term x}.  Since
   1.392 @@ -223,8 +462,8 @@
   1.393  
   1.394  declare magma.m_closed [simp]
   1.395  
   1.396 -declare l_one.one_closed [iff] group.inv_closed [simp]
   1.397 -  l_one.l_one [simp] group.r_one [simp] group.inv_inv [simp]
   1.398 +declare monoid.one_closed [iff] group.inv_closed [simp]
   1.399 +  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]
   1.400  
   1.401  lemma subgroup_nonempty:
   1.402    "~ subgroup {} G"
   1.403 @@ -241,6 +480,11 @@
   1.404    with subgroup_nonempty show ?thesis by contradiction
   1.405  qed
   1.406  
   1.407 +(*
   1.408 +lemma (in monoid) Units_subgroup:
   1.409 +  "subgroup (Units G) G"
   1.410 +*)
   1.411 +
   1.412  subsection {* Direct Products *}
   1.413  
   1.414  constdefs
   1.415 @@ -251,13 +495,13 @@
   1.416    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
   1.417      mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
   1.418  
   1.419 -  DirProdMonoid ::
   1.420 +  DirProdGroup ::
   1.421      "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
   1.422 -    (infixr "\<times>\<^sub>m" 80)
   1.423 -  "G \<times>\<^sub>m H == (| carrier = carrier (G \<times>\<^sub>s H),
   1.424 +    (infixr "\<times>\<^sub>g" 80)
   1.425 +  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
   1.426      mult = mult (G \<times>\<^sub>s H),
   1.427      one = (one G, one H) |)"
   1.428 -
   1.429 +(*
   1.430    DirProdGroup ::
   1.431      "[('a, 'm) group_scheme, ('b, 'n) group_scheme] => ('a \<times> 'b) group"
   1.432      (infixr "\<times>\<^sub>g" 80)
   1.433 @@ -265,6 +509,7 @@
   1.434      mult = mult (G \<times>\<^sub>m H),
   1.435      one = one (G \<times>\<^sub>m H),
   1.436      m_inv = (%(g, h). (m_inv G g, m_inv H h)) |)"
   1.437 +*)
   1.438  
   1.439  lemma DirProdSemigroup_magma:
   1.440    includes magma G + magma H
   1.441 @@ -287,13 +532,13 @@
   1.442    includes magma G + magma H
   1.443    shows "magma (G \<times>\<^sub>g H)"
   1.444    by rule
   1.445 -    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def)
   1.446 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
   1.447  
   1.448  lemma DirProdGroup_semigroup_axioms:
   1.449    includes semigroup G + semigroup H
   1.450    shows "semigroup_axioms (G \<times>\<^sub>g H)"
   1.451    by rule
   1.452 -    (auto simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   1.453 +    (auto simp add: DirProdGroup_def DirProdSemigroup_def
   1.454        G.m_assoc H.m_assoc)
   1.455  
   1.456  lemma DirProdGroup_semigroup:
   1.457 @@ -308,11 +553,9 @@
   1.458  lemma DirProdGroup_group:
   1.459    includes group G + group H
   1.460    shows "group (G \<times>\<^sub>g H)"
   1.461 -by rule
   1.462 -  (auto intro: magma.intro l_one.intro
   1.463 -      semigroup_axioms.intro group_axioms.intro
   1.464 -    simp add: DirProdGroup_def DirProdMonoid_def DirProdSemigroup_def
   1.465 -      G.m_assoc H.m_assoc G.l_inv H.l_inv)
   1.466 +  by (rule groupI)
   1.467 +    (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
   1.468 +      simp add: DirProdGroup_def DirProdSemigroup_def)
   1.469  
   1.470  subsection {* Homomorphisms *}
   1.471  
   1.472 @@ -376,14 +619,20 @@
   1.473    with x show ?thesis by simp
   1.474  qed
   1.475  
   1.476 -section {* Abelian Structures *}
   1.477 +section {* Commutative Structures *}
   1.478 +
   1.479 +text {*
   1.480 +  Naming convention: multiplicative structures that are commutative
   1.481 +  are called \emph{commutative}, additive structures are called
   1.482 +  \emph{Abelian}.
   1.483 +*}
   1.484  
   1.485  subsection {* Definition *}
   1.486  
   1.487 -locale abelian_semigroup = semigroup +
   1.488 +locale comm_semigroup = semigroup +
   1.489    assumes m_comm: "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
   1.490  
   1.491 -lemma (in abelian_semigroup) m_lcomm:
   1.492 +lemma (in comm_semigroup) m_lcomm:
   1.493    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.494     x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   1.495  proof -
   1.496 @@ -394,11 +643,33 @@
   1.497    finally show ?thesis .
   1.498  qed
   1.499  
   1.500 -lemmas (in abelian_semigroup) ac = m_assoc m_comm m_lcomm
   1.501 +lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm
   1.502 +
   1.503 +locale comm_monoid = comm_semigroup + monoid
   1.504  
   1.505 -locale abelian_monoid = abelian_semigroup + l_one
   1.506 +lemma comm_monoidI:
   1.507 +  assumes m_closed:
   1.508 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   1.509 +    and one_closed: "one G \<in> carrier G"
   1.510 +    and m_assoc:
   1.511 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.512 +      mult G (mult G x y) z = mult G x (mult G y z)"
   1.513 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   1.514 +    and m_comm:
   1.515 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.516 +  shows "comm_monoid G"
   1.517 +  using l_one
   1.518 +  by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
   1.519 +    comm_semigroup_axioms.intro monoid_axioms.intro
   1.520 +    intro: prems simp: m_closed one_closed m_comm)
   1.521  
   1.522 -lemma (in abelian_monoid) l_one [simp]:
   1.523 +lemma (in monoid) monoid_comm_monoidI:
   1.524 +  assumes m_comm:
   1.525 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.526 +  shows "comm_monoid G"
   1.527 +  by (rule comm_monoidI) (auto intro: m_assoc m_comm)
   1.528 +(*
   1.529 +lemma (in comm_monoid) r_one [simp]:
   1.530    "x \<in> carrier G ==> x \<otimes> \<one> = x"
   1.531  proof -
   1.532    assume G: "x \<in> carrier G"
   1.533 @@ -406,11 +677,38 @@
   1.534    also from G have "... = x" by simp
   1.535    finally show ?thesis .
   1.536  qed
   1.537 +*)
   1.538  
   1.539 -locale abelian_group = abelian_monoid + group
   1.540 +lemma (in comm_monoid) nat_pow_distr:
   1.541 +  "[| x \<in> carrier G; y \<in> carrier G |] ==>
   1.542 +  (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
   1.543 +  by (induct n) (simp, simp add: m_ac)
   1.544 +
   1.545 +locale comm_group = comm_monoid + group
   1.546 +
   1.547 +lemma (in group) group_comm_groupI:
   1.548 +  assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
   1.549 +      mult G x y = mult G y x"
   1.550 +  shows "comm_group G"
   1.551 +  by (fast intro: comm_group.intro comm_semigroup_axioms.intro
   1.552 +    group.axioms prems)
   1.553  
   1.554 -lemma (in abelian_group) inv_mult:
   1.555 +lemma comm_groupI:
   1.556 +  assumes m_closed:
   1.557 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
   1.558 +    and one_closed: "one G \<in> carrier G"
   1.559 +    and m_assoc:
   1.560 +      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
   1.561 +      mult G (mult G x y) z = mult G x (mult G y z)"
   1.562 +    and m_comm:
   1.563 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
   1.564 +    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
   1.565 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
   1.566 +  shows "comm_group G"
   1.567 +  by (fast intro: group.group_comm_groupI groupI prems)
   1.568 +
   1.569 +lemma (in comm_group) inv_mult:
   1.570    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
   1.571 -  by (simp add: ac inv_mult_group)
   1.572 +  by (simp add: m_ac inv_mult_group)
   1.573  
   1.574  end