diff -r a7f85074c169 -r 30a1692557b0 src/HOL/Power.thy --- a/src/HOL/Power.thy Sun Apr 01 09:12:03 2012 +0200 +++ b/src/HOL/Power.thy Sun Apr 01 16:09:58 2012 +0200 @@ -81,6 +81,15 @@ "a ^ Suc (2*n) = a * (a ^ n) ^ 2" by (simp add: power_even_eq) +lemma power_numeral_even: + "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" + unfolding numeral_Bit0 power_add Let_def .. + +lemma power_numeral_odd: + "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" + unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right + unfolding power_Suc power_add Let_def mult_assoc .. + end context comm_monoid_mult @@ -596,6 +605,9 @@ subsection {* Miscellaneous rules *} +lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" + unfolding One_nat_def by (cases m) simp_all + lemma power2_sum: fixes x y :: "'a::comm_semiring_1" shows "(x + y)\ = x\ + y\ + 2 * x * y" @@ -647,6 +659,16 @@ apply assumption done +text {* Simprules for comparisons where common factors can be cancelled. *} + +lemmas zero_compare_simps = + add_strict_increasing add_strict_increasing2 add_increasing + zero_le_mult_iff zero_le_divide_iff + zero_less_mult_iff zero_less_divide_iff + mult_le_0_iff divide_le_0_iff + mult_less_0_iff divide_less_0_iff + zero_le_power2 power2_less_0 + subsection {* Exponentiation for the Natural Numbers *}