src/HOL/Power.thy
changeset 59741 5b762cd73a8e
parent 59009 348561aa3869
child 59865 8a20dd967385
     1.1 --- a/src/HOL/Power.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/Power.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -51,6 +51,10 @@
     1.4    "a ^ 1 = a"
     1.5    by simp
     1.6  
     1.7 +lemma power_Suc0_right [simp]:
     1.8 +  "a ^ Suc 0 = a"
     1.9 +  by simp
    1.10 +
    1.11  lemma power_commutes:
    1.12    "a ^ n * a = a * a ^ n"
    1.13    by (induct n) (simp_all add: mult.assoc)
    1.14 @@ -127,6 +131,9 @@
    1.15  
    1.16  end
    1.17  
    1.18 +declare power_mult_distrib [where a = "numeral w" for w, simp]
    1.19 +declare power_mult_distrib [where b = "numeral w" for w, simp]
    1.20 +
    1.21  context semiring_numeral
    1.22  begin
    1.23  
    1.24 @@ -301,6 +308,8 @@
    1.25    "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
    1.26    by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
    1.27  
    1.28 +declare nonzero_power_divide [where b = "numeral w" for w, simp]
    1.29 +
    1.30  end
    1.31  
    1.32