# HG changeset patch # User huffman # Date 1333213858 -7200 # Node ID 243b33052e344781a4f6faa45023292b6231cb79 # Parent a92d3620e1566ae860e5261575246af2003d7797 add lemma power_le_one diff -r a92d3620e156 -r 243b33052e34 src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Mar 30 21:08:00 2012 +0200 +++ b/src/HOL/Power.thy Sat Mar 31 19:10:58 2012 +0200 @@ -289,13 +289,15 @@ "0 \ a \ 0 \ a ^ n" by (induct n) (simp_all add: mult_nonneg_nonneg) -lemma one_le_power[simp]: - "1 \ a \ 1 \ a ^ n" - apply (induct n) - apply simp_all - apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) - apply (simp_all add: order_trans [OF zero_le_one]) - done +lemma power_mono: + "a \ b \ 0 \ a \ a ^ n \ b ^ n" + by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) + +lemma one_le_power [simp]: "1 \ a \ 1 \ a ^ n" + using power_mono [of 1 a n] by simp + +lemma power_le_one: "\0 \ a; a \ 1\ \ a ^ n \ 1" + using power_mono [of a 1 n] by simp lemma power_gt1_lemma: assumes gt1: "1 < a" @@ -353,11 +355,6 @@ by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp) -lemma power_mono: - "a \ b \ 0 \ a \ a ^ n \ b ^ n" - by (induct n) - (auto intro: mult_mono order_trans [of 0 a b]) - lemma power_strict_mono [rule_format]: "a < b \ 0 \ a \ 0 < n \ a ^ n < b ^ n" by (induct n)