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.6  defs (overloaded)
     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.117        by (simp add: m_assoc)
   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.196      by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv)
   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.207  apply (simp add: m_inv_def)
   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