src/HOL/Algebra/Group.thy
 changeset 14693 4deda204e1d8 parent 14651 02b8f3bcf7fe child 14706 71590b7733b7
```     1.1 --- a/src/HOL/Algebra/Group.thy	Sat May 01 22:04:14 2004 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Sat May 01 22:05:05 2004 +0200
1.3 @@ -42,10 +42,10 @@
1.4    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
1.5
1.7 -  nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n"
1.8 +  nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
1.9    int_pow_def: "pow G a z ==
1.10 -    let p = nat_rec (one G) (%u b. mult G b a)
1.11 -    in if neg z then m_inv G (p (nat (-z))) else p (nat z)"
1.12 +    let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
1.13 +    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
1.14
1.15  locale magma = struct G +
1.16    assumes m_closed [intro, simp]:
1.17 @@ -62,14 +62,15 @@
1.18      and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x"
1.19
1.20  lemma monoidI:
1.21 +  includes struct G
1.22    assumes m_closed:
1.23 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
1.24 -    and one_closed: "one G \<in> carrier G"
1.25 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
1.26 +    and one_closed: "\<one> \<in> carrier G"
1.27      and m_assoc:
1.28        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.29 -      mult G (mult G x y) z = mult G x (mult G y z)"
1.30 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
1.31 -    and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x"
1.32 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.33 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.34 +    and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
1.35    shows "monoid G"
1.36    by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro
1.37      semigroup.intro monoid_axioms.intro
1.38 @@ -80,8 +81,8 @@
1.39    by (unfold Units_def) fast
1.40
1.41  lemma (in monoid) inv_unique:
1.42 -  assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
1.43 -    and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
1.44 +  assumes eq: "y \<otimes> x = \<one>"  "x \<otimes> y' = \<one>"
1.45 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
1.46    shows "y = y'"
1.47  proof -
1.48    from G eq have "y = y \<otimes> (x \<otimes> y')" by simp
1.49 @@ -129,13 +130,13 @@
1.50     (x \<otimes> y = x \<otimes> z) = (y = z)"
1.51  proof
1.52    assume eq: "x \<otimes> y = x \<otimes> z"
1.53 -    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
1.54 +    and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
1.55    then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
1.56      by (simp add: m_assoc Units_closed)
1.57    with G show "y = z" by (simp add: Units_l_inv)
1.58  next
1.59    assume eq: "y = z"
1.60 -    and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
1.61 +    and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
1.62    then show "x \<otimes> y = x \<otimes> z" by simp
1.63  qed
1.64
1.65 @@ -152,14 +153,14 @@
1.66    "inj_on (m_inv G) (Units G)"
1.67  proof (rule inj_onI)
1.68    fix x y
1.69 -  assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y"
1.70 +  assume G: "x \<in> Units G"  "y \<in> Units G" and eq: "inv x = inv y"
1.71    then have "inv (inv x) = inv (inv y)" by simp
1.72    with G show "x = y" by simp
1.73  qed
1.74
1.75  lemma (in monoid) Units_inv_comm:
1.76    assumes inv: "x \<otimes> y = \<one>"
1.77 -    and G: "x \<in> Units G" "y \<in> Units G"
1.78 +    and G: "x \<in> Units G"  "y \<in> Units G"
1.79    shows "y \<otimes> x = \<one>"
1.80  proof -
1.81    from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
1.82 @@ -200,59 +201,58 @@
1.83    assumes Units: "carrier G <= Units G"
1.84
1.85  theorem groupI:
1.86 +  includes struct G
1.87    assumes m_closed [simp]:
1.88 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
1.89 -    and one_closed [simp]: "one G \<in> carrier G"
1.90 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
1.91 +    and one_closed [simp]: "\<one> \<in> carrier G"
1.92      and m_assoc:
1.93        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.94 -      mult G (mult G x y) z = mult G x (mult G y z)"
1.95 -    and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
1.96 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
1.97 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.98 +    and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.99 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
1.100    shows "group G"
1.101  proof -
1.102    have l_cancel [simp]:
1.103      "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.104 -    (mult G x y = mult G x z) = (y = z)"
1.105 +    (x \<otimes> y = x \<otimes> z) = (y = z)"
1.106    proof
1.107      fix x y z
1.108 -    assume eq: "mult G x y = mult G x z"
1.109 -      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.110 +    assume eq: "x \<otimes> y = x \<otimes> z"
1.111 +      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
1.112      with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
1.113 -      and l_inv: "mult G x_inv x = one G" by fast
1.114 -    from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z"
1.115 +      and l_inv: "x_inv \<otimes> x = \<one>" by fast
1.116 +    from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z"
1.118      with G show "y = z" by (simp add: l_inv)
1.119    next
1.120      fix x y z
1.121      assume eq: "y = z"
1.122 -      and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.123 -    then show "mult G x y = mult G x z" by simp
1.124 +      and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
1.125 +    then show "x \<otimes> y = x \<otimes> z" by simp
1.126    qed
1.127    have r_one:
1.128 -    "!!x. x \<in> carrier G ==> mult G x (one G) = x"
1.129 +    "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x"
1.130    proof -
1.131      fix x
1.132      assume x: "x \<in> carrier G"
1.133      with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G"
1.134 -      and l_inv: "mult G x_inv x = one G" by fast
1.135 -    from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x"
1.136 +      and l_inv: "x_inv \<otimes> x = \<one>" by fast
1.137 +    from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x"
1.138        by (simp add: m_assoc [symmetric] l_inv)
1.139 -    with x xG show "mult G x (one G) = x" by simp
1.140 +    with x xG show "x \<otimes> \<one> = x" by simp
1.141    qed
1.142    have inv_ex:
1.143 -    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G &
1.144 -      mult G x y = one G"
1.145 +    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
1.146    proof -
1.147      fix x
1.148      assume x: "x \<in> carrier G"
1.149      with l_inv_ex obtain y where y: "y \<in> carrier G"
1.150 -      and l_inv: "mult G y x = one G" by fast
1.151 -    from x y have "mult G y (mult G x y) = mult G y (one G)"
1.152 +      and l_inv: "y \<otimes> x = \<one>" by fast
1.153 +    from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>"
1.154        by (simp add: m_assoc [symmetric] l_inv r_one)
1.155 -    with x y have r_inv: "mult G x y = one G"
1.156 +    with x y have r_inv: "x \<otimes> y = \<one>"
1.157        by simp
1.158 -    from x y show "EX y : carrier G. mult G y x = one G &
1.159 -      mult G x y = one G"
1.160 +    from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>"
1.161        by (fast intro: l_inv r_inv)
1.162    qed
1.163    then have carrier_subset_Units: "carrier G <= Units G"
1.164 @@ -265,7 +265,7 @@
1.165
1.166  lemma (in monoid) monoid_groupI:
1.167    assumes l_inv_ex:
1.168 -    "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
1.169 +    "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
1.170    shows "group G"
1.171    by (rule groupI) (auto intro: m_assoc l_inv_ex)
1.172
1.173 @@ -306,13 +306,13 @@
1.174     (y \<otimes> x = z \<otimes> x) = (y = z)"
1.175  proof
1.176    assume eq: "y \<otimes> x = z \<otimes> x"
1.177 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.178 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
1.179    then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
1.180      by (simp add: m_assoc [symmetric])
1.181    with G show "y = z" by (simp add: r_inv)
1.182  next
1.183    assume eq: "y = z"
1.184 -    and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.185 +    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
1.186    then show "y \<otimes> x = z \<otimes> x" by simp
1.187  qed
1.188
1.189 @@ -335,7 +335,7 @@
1.190  lemma (in group) inv_mult_group:
1.191    "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
1.192  proof -
1.193 -  assume G: "x \<in> carrier G" "y \<in> carrier G"
1.194 +  assume G: "x \<in> carrier G"  "y \<in> carrier G"
1.195    then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
1.197    with G show ?thesis by simp
1.198 @@ -343,14 +343,14 @@
1.199
1.200  lemma (in group) inv_comm:
1.201    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
1.202 -  by (rule Units_inv_comm) auto
1.203 +  by (rule Units_inv_comm) auto
1.204
1.205  lemma (in group) inv_equality:
1.206       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
1.208  apply (rule the_equality)
1.209 - apply (simp add: inv_comm [of y x])
1.210 -apply (rule r_cancel [THEN iffD1], auto)
1.211 + apply (simp add: inv_comm [of y x])
1.212 +apply (rule r_cancel [THEN iffD1], auto)
1.213  done
1.214
1.215  text {* Power *}
1.216 @@ -493,10 +493,10 @@
1.217  constdefs (structure G and H)
1.218    DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
1.219    "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
1.220 -    mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
1.221 +    mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)"
1.222
1.223    DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
1.224 -  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
1.225 +  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)"
1.226
1.227  lemma DirProdSemigroup_magma:
1.228    includes magma G + magma H
1.229 @@ -550,18 +550,18 @@
1.230    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
1.231
1.232  lemma one_DirProdGroup [simp]:
1.233 -     "one (G \<times>\<^sub>g H) = (one G, one H)"
1.234 +     "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)"
1.235    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
1.236
1.237  lemma mult_DirProdGroup [simp]:
1.238 -     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
1.239 +     "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')"
1.240    by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
1.241
1.242  lemma inv_DirProdGroup [simp]:
1.243    includes group G + group H
1.244    assumes g: "g \<in> carrier G"
1.245        and h: "h \<in> carrier H"
1.246 -  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
1.247 +  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
1.248    apply (rule group.inv_equality [OF DirProdGroup_group])
1.249    apply (simp_all add: prems group_def group.l_inv)
1.250    done
1.251 @@ -572,7 +572,7 @@
1.252    hom :: "_ => _ => ('a => 'b) set"
1.253    "hom G H ==
1.254      {h. h \<in> carrier G -> carrier H &
1.255 -      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
1.256 +      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
1.257
1.258  lemma (in semigroup) hom:
1.259    includes semigroup G
1.260 @@ -586,9 +586,9 @@
1.261  qed
1.262
1.263  lemma hom_mult:
1.264 -  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
1.265 -   ==> h (mult G x y) = mult H (h x) (h y)"
1.266 -  by (simp add: hom_def)
1.267 +  "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |]
1.268 +   ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
1.269 +  by (simp add: hom_def)
1.270
1.271  lemma hom_closed:
1.272    "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H"
1.273 @@ -598,9 +598,9 @@
1.274       "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|]
1.275        ==> compose (carrier G) h h' \<in> hom G G"
1.276  apply (simp (no_asm_simp) add: hom_def)
1.277 -apply (intro conjI)
1.278 +apply (intro conjI)
1.279   apply (force simp add: funcset_compose hom_def)
1.280 -apply (simp add: compose_def group.axioms hom_mult funcset_mem)
1.281 +apply (simp add: compose_def group.axioms hom_mult funcset_mem)
1.282  done
1.283
1.284  locale group_hom = group G + group H + var h +
1.285 @@ -613,9 +613,9 @@
1.286    by simp
1.287
1.288  lemma (in group_hom) hom_one [simp]:
1.289 -  "h \<one> = \<one>\<^sub>2"
1.290 +  "h \<one> = \<one>\<^bsub>H\<^esub>"
1.291  proof -
1.292 -  have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>"
1.293 +  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
1.294      by (simp add: hom_mult [symmetric] del: hom_mult)
1.295    then show ?thesis by (simp del: r_one)
1.296  qed
1.297 @@ -625,14 +625,14 @@
1.298    by simp
1.299
1.300  lemma (in group_hom) hom_inv [simp]:
1.301 -  "x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)"
1.302 +  "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)"
1.303  proof -
1.304    assume x: "x \<in> carrier G"
1.305 -  then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2"
1.306 +  then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>"
1.307      by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult)
1.308 -  also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)"
1.309 +  also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
1.310      by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult)
1.311 -  finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" .
1.312 +  finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
1.313    with x show ?thesis by simp
1.314  qed
1.315
1.316 @@ -653,7 +653,7 @@
1.317    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.318     x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
1.319  proof -
1.320 -  assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.321 +  assume xyz: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
1.322    from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc)
1.323    also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm)
1.324    also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc)
1.325 @@ -665,15 +665,16 @@
1.326  locale comm_monoid = comm_semigroup + monoid
1.327
1.328  lemma comm_monoidI:
1.329 +  includes struct G
1.330    assumes m_closed:
1.331 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
1.332 -    and one_closed: "one G \<in> carrier G"
1.333 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
1.334 +    and one_closed: "\<one> \<in> carrier G"
1.335      and m_assoc:
1.336        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.337 -      mult G (mult G x y) z = mult G x (mult G y z)"
1.338 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
1.339 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.340 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.341      and m_comm:
1.342 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
1.343 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
1.344    shows "comm_monoid G"
1.345    using l_one
1.346    by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro
1.347 @@ -682,20 +683,17 @@
1.348
1.349  lemma (in monoid) monoid_comm_monoidI:
1.350    assumes m_comm:
1.351 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
1.352 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
1.353    shows "comm_monoid G"
1.354    by (rule comm_monoidI) (auto intro: m_assoc m_comm)
1.355 -(*
1.356 -lemma (in comm_monoid) r_one [simp]:
1.357 +(*lemma (in comm_monoid) r_one [simp]:
1.358    "x \<in> carrier G ==> x \<otimes> \<one> = x"
1.359  proof -
1.360    assume G: "x \<in> carrier G"
1.361    then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
1.362    also from G have "... = x" by simp
1.363    finally show ?thesis .
1.364 -qed
1.365 -*)
1.366 -
1.367 +qed*)
1.368  lemma (in comm_monoid) nat_pow_distr:
1.369    "[| x \<in> carrier G; y \<in> carrier G |] ==>
1.370    (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n"
1.371 @@ -705,22 +703,23 @@
1.372
1.373  lemma (in group) group_comm_groupI:
1.374    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
1.375 -      mult G x y = mult G y x"
1.376 +      x \<otimes> y = y \<otimes> x"
1.377    shows "comm_group G"
1.378    by (fast intro: comm_group.intro comm_semigroup_axioms.intro
1.379      group.axioms prems)
1.380
1.381  lemma comm_groupI:
1.382 +  includes struct G
1.383    assumes m_closed:
1.384 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G"
1.385 -    and one_closed: "one G \<in> carrier G"
1.386 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G"
1.387 +    and one_closed: "\<one> \<in> carrier G"
1.388      and m_assoc:
1.389        "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.390 -      mult G (mult G x y) z = mult G x (mult G y z)"
1.391 +      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
1.392      and m_comm:
1.393 -      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x"
1.394 -    and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x"
1.395 -    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G"
1.396 +      "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x"
1.397 +    and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x"
1.398 +    and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>"
1.399    shows "comm_group G"
1.400    by (fast intro: group.group_comm_groupI groupI prems)
1.401
```