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)
```