avoid using constant Int.neg
authorhuffman
Tue Feb 21 10:30:57 2012 +0100 (2012-02-21)
changeset 4655969a273fcd53a
parent 46558 fdb84c40e074
child 46560 8e252a608765
avoid using constant Int.neg
src/HOL/Algebra/Group.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Feb 21 09:17:53 2012 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Feb 21 10:30:57 2012 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  begin
     1.5    definition "int_pow G a z =
     1.6     (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
     1.7 -    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
     1.8 +    in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
     1.9  end
    1.10  
    1.11  locale monoid =
    1.12 @@ -391,7 +391,7 @@
    1.13  text {* Power *}
    1.14  
    1.15  lemma (in group) int_pow_def2:
    1.16 -  "a (^) (z::int) = (if neg z then inv (a (^) (nat (-z))) else a (^) (nat z))"
    1.17 +  "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
    1.18    by (simp add: int_pow_def nat_pow_def Let_def)
    1.19  
    1.20  lemma (in group) int_pow_0 [simp]: