src/HOL/Power.thy
changeset 30056 0a35bee25c20
parent 29978 33df3c4eb629
child 30079 293b896b9c25
equal deleted inserted replaced
30053:044308b4948a 30056:0a35bee25c20
   141 apply (auto simp add: mult_strict_mono power_Suc
   141 apply (auto simp add: mult_strict_mono power_Suc
   142                       order_le_less_trans [of 0 a b])
   142                       order_le_less_trans [of 0 a b])
   143 done
   143 done
   144 
   144 
   145 lemma power_eq_0_iff [simp]:
   145 lemma power_eq_0_iff [simp]:
   146   "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
   146   "(a^n = 0) \<longleftrightarrow>
   147 apply (induct "n")
   147    (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
   148 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
   148 apply (induct "n")
   149 done
   149 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
       
   150 done
       
   151 
   150 
   152 
   151 lemma field_power_not_zero:
   153 lemma field_power_not_zero:
   152   "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
   154   "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
   153 by force
   155 by force
   154 
   156 
   367 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
   369 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
   368 by (insert one_le_power [of i n], simp)
   370 by (insert one_le_power [of i n], simp)
   369 
   371 
   370 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   372 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   371 by (induct "n", auto)
   373 by (induct "n", auto)
       
   374 
       
   375 lemma nat_power_eq_Suc_0_iff [simp]: 
       
   376   "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
       
   377 by (induct_tac m, auto)
       
   378 
       
   379 lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
       
   380 by simp
   372 
   381 
   373 text{*Valid for the naturals, but what if @{text"0<i<1"}?
   382 text{*Valid for the naturals, but what if @{text"0<i<1"}?
   374 Premises cannot be weakened: consider the case where @{term "i=0"},
   383 Premises cannot be weakened: consider the case where @{term "i=0"},
   375 @{term "m=1"} and @{term "n=0"}.*}
   384 @{term "m=1"} and @{term "n=0"}.*}
   376 lemma nat_power_less_imp_less:
   385 lemma nat_power_less_imp_less: