src/HOL/Power.thy
changeset 28131 3130d7b3149d
parent 25874 14819a95cf75
child 29608 564ea783ace8
     1.1 --- a/src/HOL/Power.thy	Thu Sep 04 17:18:44 2008 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Sep 04 17:19:57 2008 +0200
     1.3 @@ -36,6 +36,9 @@
     1.4  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
     1.5    by (induct n) (simp_all add: power_Suc mult_assoc)
     1.6  
     1.7 +lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a"
     1.8 +  by (simp add: power_Suc power_commutes)
     1.9 +
    1.10  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
    1.11    by (induct m) (simp_all add: power_Suc mult_ac)
    1.12  
    1.13 @@ -202,10 +205,12 @@
    1.14       "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
    1.15  by (rule zero_le_power [OF abs_ge_zero])
    1.16  
    1.17 -lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n"
    1.18 -proof -
    1.19 -  have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
    1.20 -  thus ?thesis by (simp only: power_mult_distrib)
    1.21 +lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring_1,recpower}) ^ n"
    1.22 +proof (induct n)
    1.23 +  case 0 show ?case by simp
    1.24 +next
    1.25 +  case (Suc n) then show ?case
    1.26 +    by (simp add: power_Suc2 mult_assoc)
    1.27  qed
    1.28  
    1.29  text{*Lemma for @{text power_strict_decreasing}*}