src/HOL/Algebra/Group.thy
changeset 35850 dd2636f0f608
parent 35849 b5522b51cb1e
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 17:12:31 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 17:28:35 2010 +0100
     1.3 @@ -30,13 +30,19 @@
     1.4    where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
     1.5  
     1.6  consts
     1.7 -  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
     1.8 +  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a"  (infixr "'(^')\<index>" 75)
     1.9 +
    1.10 +overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
    1.11 +begin
    1.12 +  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
    1.13 +end
    1.14  
    1.15 -defs (overloaded)
    1.16 -  nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
    1.17 -  int_pow_def: "pow G a z ==
    1.18 -    let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    1.19 -    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
    1.20 +overloading int_pow == "pow :: [_, 'a, int] => 'a"
    1.21 +begin
    1.22 +  definition "int_pow G a z =
    1.23 +   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    1.24 +    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
    1.25 +end
    1.26  
    1.27  locale monoid =
    1.28    fixes G (structure)