--- a/src/HOL/Power.thy Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Power.thy Wed Mar 18 14:13:27 2015 +0000
@@ -51,6 +51,10 @@
"a ^ 1 = a"
by simp
+lemma power_Suc0_right [simp]:
+ "a ^ Suc 0 = a"
+ by simp
+
lemma power_commutes:
"a ^ n * a = a * a ^ n"
by (induct n) (simp_all add: mult.assoc)
@@ -127,6 +131,9 @@
end
+declare power_mult_distrib [where a = "numeral w" for w, simp]
+declare power_mult_distrib [where b = "numeral w" for w, simp]
+
context semiring_numeral
begin
@@ -301,6 +308,8 @@
"b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+declare nonzero_power_divide [where b = "numeral w" for w, simp]
+
end