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