src/HOL/Power.thy
changeset 60155 91477b3a2d6b
parent 59867 58043346ca64
child 60685 cb21b7022b00
     1.1 --- a/src/HOL/Power.thy	Tue Apr 28 22:57:07 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Apr 29 14:04:22 2015 +0100
     1.3 @@ -131,9 +131,25 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text{*Extract constant factors from powers*}
     1.8  declare power_mult_distrib [where a = "numeral w" for w, simp]
     1.9  declare power_mult_distrib [where b = "numeral w" for w, simp]
    1.10  
    1.11 +lemma power_add_numeral [simp]:
    1.12 +  fixes a :: "'a :: monoid_mult"
    1.13 +  shows "a^numeral m * a^numeral n = a^numeral (m + n)"
    1.14 +  by (simp add: power_add [symmetric])
    1.15 +
    1.16 +lemma power_add_numeral2 [simp]:
    1.17 +  fixes a :: "'a :: monoid_mult"
    1.18 +  shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b"
    1.19 +  by (simp add: mult.assoc [symmetric])
    1.20 +
    1.21 +lemma power_mult_numeral [simp]:
    1.22 +  fixes a :: "'a :: monoid_mult"
    1.23 +  shows"(a^numeral m)^numeral n = a^numeral (m * n)"
    1.24 +  by (simp only: numeral_mult power_mult)
    1.25 +
    1.26  context semiring_numeral
    1.27  begin
    1.28