src/HOL/Power.thy
changeset 47191 ebd8c46d156b
parent 45231 d85a2fdc586c
child 47192 0c0501cb6da6
     1.1 --- a/src/HOL/Power.thy	Thu Mar 29 08:59:56 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Mar 29 11:47:30 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Exponentiation *}
     1.5  
     1.6  theory Power
     1.7 -imports Nat
     1.8 +imports Num
     1.9  begin
    1.10  
    1.11  subsection {* Powers for Arbitrary Monoids *}
    1.12 @@ -66,6 +66,21 @@
    1.13  
    1.14  end
    1.15  
    1.16 +context semiring_numeral
    1.17 +begin
    1.18 +
    1.19 +lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k"
    1.20 +  by (simp only: sqr_conv_mult numeral_mult)
    1.21 +
    1.22 +lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l"
    1.23 +  by (induct l, simp_all only: numeral_class.numeral.simps pow.simps
    1.24 +    numeral_sqr numeral_mult power_add power_one_right)
    1.25 +
    1.26 +lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)"
    1.27 +  by (rule numeral_pow [symmetric])
    1.28 +
    1.29 +end
    1.30 +
    1.31  context semiring_1
    1.32  begin
    1.33  
    1.34 @@ -73,6 +88,9 @@
    1.35    "of_nat (m ^ n) = of_nat m ^ n"
    1.36    by (induct n) (simp_all add: of_nat_mult)
    1.37  
    1.38 +lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
    1.39 +  by (cases "numeral k :: nat", simp_all)
    1.40 +
    1.41  end
    1.42  
    1.43  context comm_semiring_1
    1.44 @@ -128,6 +146,23 @@
    1.45      by (simp del: power_Suc add: power_Suc2 mult_assoc)
    1.46  qed
    1.47  
    1.48 +lemma power_minus_Bit0:
    1.49 +  "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
    1.50 +  by (induct k, simp_all only: numeral_class.numeral.simps power_add
    1.51 +    power_one_right mult_minus_left mult_minus_right minus_minus)
    1.52 +
    1.53 +lemma power_minus_Bit1:
    1.54 +  "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
    1.55 +  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
    1.56 +
    1.57 +lemma power_neg_numeral_Bit0 [simp]:
    1.58 +  "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
    1.59 +  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
    1.60 +
    1.61 +lemma power_neg_numeral_Bit1 [simp]:
    1.62 +  "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
    1.63 +  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
    1.64 +
    1.65  end
    1.66  
    1.67  context linordered_semidom