add lemma power_le_one
authorhuffman
Sat Mar 31 19:10:58 2012 +0200 (2012-03-31)
changeset 47241243b33052e34
parent 47235 a92d3620e156
child 47242 1caeecc72aea
add lemma power_le_one
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Fri Mar 30 21:08:00 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Sat Mar 31 19:10:58 2012 +0200
     1.3 @@ -289,13 +289,15 @@
     1.4    "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
     1.5    by (induct n) (simp_all add: mult_nonneg_nonneg)
     1.6  
     1.7 -lemma one_le_power[simp]:
     1.8 -  "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
     1.9 -  apply (induct n)
    1.10 -  apply simp_all
    1.11 -  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
    1.12 -  apply (simp_all add: order_trans [OF zero_le_one])
    1.13 -  done
    1.14 +lemma power_mono:
    1.15 +  "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
    1.16 +  by (induct n) (auto intro: mult_mono order_trans [of 0 a b])
    1.17 +
    1.18 +lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
    1.19 +  using power_mono [of 1 a n] by simp
    1.20 +
    1.21 +lemma power_le_one: "\<lbrakk>0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> a ^ n \<le> 1"
    1.22 +  using power_mono [of a 1 n] by simp
    1.23  
    1.24  lemma power_gt1_lemma:
    1.25    assumes gt1: "1 < a"
    1.26 @@ -353,11 +355,6 @@
    1.27    by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"]
    1.28      power_le_imp_le_exp)
    1.29  
    1.30 -lemma power_mono:
    1.31 -  "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
    1.32 -  by (induct n)
    1.33 -    (auto intro: mult_mono order_trans [of 0 a b])
    1.34 -
    1.35  lemma power_strict_mono [rule_format]:
    1.36    "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
    1.37    by (induct n)