src/HOL/Power.thy
changeset 59009 348561aa3869
parent 58889 5b7a9633cfa8
child 59741 5b762cd73a8e
     1.1 --- a/src/HOL/Power.thy	Mon Nov 17 14:55:32 2014 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Nov 17 14:55:33 2014 +0100
     1.3 @@ -149,7 +149,12 @@
     1.4    "of_nat (m ^ n) = of_nat m ^ n"
     1.5    by (induct n) (simp_all add: of_nat_mult)
     1.6  
     1.7 -lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
     1.8 +lemma zero_power:
     1.9 +  "0 < n \<Longrightarrow> 0 ^ n = 0"
    1.10 +  by (cases n) simp_all
    1.11 +
    1.12 +lemma power_zero_numeral [simp]:
    1.13 +  "0 ^ numeral k = 0"
    1.14    by (simp add: numeral_eq_Suc)
    1.15  
    1.16  lemma zero_power2: "0\<^sup>2 = 0" (* delete? *)