src/HOL/Power.thy
 changeset 30056 0a35bee25c20 parent 29978 33df3c4eb629 child 30079 293b896b9c25
```     1.1 --- a/src/HOL/Power.thy	Sun Feb 22 11:30:57 2009 +0100
1.2 +++ b/src/HOL/Power.thy	Sun Feb 22 17:25:28 2009 +0100
1.3 @@ -143,11 +143,13 @@
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>0)"
1.8 +  "(a^n = 0) \<longleftrightarrow>
1.9 +   (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
1.10  apply (induct "n")
1.11 -apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
1.12 +apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
1.13  done
1.14
1.15 +
1.16  lemma field_power_not_zero:
1.17    "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
1.18  by force
1.19 @@ -370,6 +372,13 @@
1.20  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
1.21  by (induct "n", auto)
1.22
1.23 +lemma nat_power_eq_Suc_0_iff [simp]:
1.24 +  "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
1.25 +by (induct_tac m, auto)
1.26 +
1.27 +lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
1.28 +by simp
1.29 +
1.30  text{*Valid for the naturals, but what if @{text"0<i<1"}?
1.31  Premises cannot be weakened: consider the case where @{term "i=0"},
1.32  @{term "m=1"} and @{term "n=0"}.*}
```