--- a/src/HOL/Power.thy Tue Jul 12 12:49:46 2005 +0200
+++ b/src/HOL/Power.thy Tue Jul 12 17:56:03 2005 +0200
@@ -50,7 +50,7 @@
lemma zero_less_power:
"0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
apply (induct "n")
-apply (simp_all add: power_Suc zero_less_one mult_pos)
+apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
done
lemma zero_le_power:
@@ -165,6 +165,12 @@
apply (auto simp add: power_Suc inverse_mult_distrib)
done
+lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n =
+ (1 / a)^n"
+apply (simp add: divide_inverse)
+apply (rule power_inverse)
+done
+
lemma nonzero_power_divide:
"b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)