src/HOL/Power.thy
changeset 25162 ad4d5365d9d8
parent 25134 3d4953e88449
child 25231 1aa9c8f022d0
     1.1 --- a/src/HOL/Power.thy	Tue Oct 23 22:48:25 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Oct 23 23:27:23 2007 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  done
     1.5  
     1.6  lemma power_eq_0_iff [simp]:
     1.7 -  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
     1.8 +  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
     1.9  apply (induct "n")
    1.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.11  done
    1.12 @@ -342,7 +342,7 @@
    1.13  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.14  by (insert one_le_power [of i n], simp)
    1.15  
    1.16 -lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
    1.17 +lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    1.18  by (induct "n", auto)
    1.19  
    1.20  text{*Valid for the naturals, but what if @{text"0<i<1"}?