--- a/src/HOL/Power.thy Tue Apr 28 22:57:07 2015 +0200
+++ b/src/HOL/Power.thy Wed Apr 29 14:04:22 2015 +0100
@@ -131,9 +131,25 @@
end
+text{*Extract constant factors from powers*}
declare power_mult_distrib [where a = "numeral w" for w, simp]
declare power_mult_distrib [where b = "numeral w" for w, simp]
+lemma power_add_numeral [simp]:
+ fixes a :: "'a :: monoid_mult"
+ shows "a^numeral m * a^numeral n = a^numeral (m + n)"
+ by (simp add: power_add [symmetric])
+
+lemma power_add_numeral2 [simp]:
+ fixes a :: "'a :: monoid_mult"
+ shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b"
+ by (simp add: mult.assoc [symmetric])
+
+lemma power_mult_numeral [simp]:
+ fixes a :: "'a :: monoid_mult"
+ shows"(a^numeral m)^numeral n = a^numeral (m * n)"
+ by (simp only: numeral_mult power_mult)
+
context semiring_numeral
begin