src/HOL/Power.thy
changeset 61531 ab2e862263e7
parent 61378 3e04c9ca001a
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Power.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -283,6 +283,9 @@
     1.4      by (simp del: power_Suc add: power_Suc2 mult.assoc)
     1.5  qed
     1.6  
     1.7 +lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
     1.8 +  by (rule power_minus)
     1.9 +
    1.10  lemma power_minus_Bit0:
    1.11    "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
    1.12    by (induct k, simp_all only: numeral_class.numeral.simps power_add
    1.13 @@ -307,7 +310,7 @@
    1.14  lemma power_minus1_odd:
    1.15    "(- 1) ^ Suc (2*n) = -1"
    1.16    by simp
    1.17 -
    1.18 +  
    1.19  lemma power_minus_even [simp]:
    1.20    "(-a) ^ (2*n) = a ^ (2*n)"
    1.21    by (simp add: power_minus [of a])