src/HOL/Power.thy
changeset 30730 4d3565f2cb0e
parent 30516 68b4a06cbd5c
child 30960 fec1a04b7220
     1.1 --- a/src/HOL/Power.thy	Wed Mar 25 14:47:08 2009 +0100
     1.2 +++ b/src/HOL/Power.thy	Thu Mar 26 14:10:48 2009 +0000
     1.3 @@ -186,6 +186,10 @@
     1.4  apply (auto simp add: abs_mult)
     1.5  done
     1.6  
     1.7 +lemma abs_power_minus [simp]:
     1.8 +  fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)"
     1.9 +  by (simp add: abs_minus_cancel power_abs) 
    1.10 +
    1.11  lemma zero_less_power_abs_iff [simp,noatp]:
    1.12       "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
    1.13  proof (induct "n")