src/HOL/Power.thy
changeset 47255 30a1692557b0
parent 47241 243b33052e34
child 49824 c26665a197dc
     1.1 --- a/src/HOL/Power.thy	Sun Apr 01 09:12:03 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Apr 01 16:09:58 2012 +0200
     1.3 @@ -81,6 +81,15 @@
     1.4    "a ^ Suc (2*n) = a * (a ^ n) ^ 2"
     1.5    by (simp add: power_even_eq)
     1.6  
     1.7 +lemma power_numeral_even:
     1.8 +  "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)"
     1.9 +  unfolding numeral_Bit0 power_add Let_def ..
    1.10 +
    1.11 +lemma power_numeral_odd:
    1.12 +  "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
    1.13 +  unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
    1.14 +  unfolding power_Suc power_add Let_def mult_assoc ..
    1.15 +
    1.16  end
    1.17  
    1.18  context comm_monoid_mult
    1.19 @@ -596,6 +605,9 @@
    1.20  
    1.21  subsection {* Miscellaneous rules *}
    1.22  
    1.23 +lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
    1.24 +  unfolding One_nat_def by (cases m) simp_all
    1.25 +
    1.26  lemma power2_sum:
    1.27    fixes x y :: "'a::comm_semiring_1"
    1.28    shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    1.29 @@ -647,6 +659,16 @@
    1.30  apply assumption
    1.31  done
    1.32  
    1.33 +text {* Simprules for comparisons where common factors can be cancelled. *}
    1.34 +
    1.35 +lemmas zero_compare_simps =
    1.36 +    add_strict_increasing add_strict_increasing2 add_increasing
    1.37 +    zero_le_mult_iff zero_le_divide_iff 
    1.38 +    zero_less_mult_iff zero_less_divide_iff 
    1.39 +    mult_le_0_iff divide_le_0_iff 
    1.40 +    mult_less_0_iff divide_less_0_iff 
    1.41 +    zero_le_power2 power2_less_0
    1.42 +
    1.43  
    1.44  subsection {* Exponentiation for the Natural Numbers *}
    1.45