# HG changeset patch
# User nipkow
# Date 1479828125 -3600
# Node ID ec766f7b887ec63ade54669b4137e1bae90596b7
# Parent  233a11ed2dfb437455a497fbdd475e9618273ac7
added simp rule

diff -r 233a11ed2dfb -r ec766f7b887e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Nov 15 17:39:40 2016 +0100
+++ b/src/HOL/Transcendental.thy	Tue Nov 22 16:22:05 2016 +0100
@@ -2634,6 +2634,10 @@
   and less_powr_iff = log_less_iff[symmetric]
   and le_powr_iff = log_le_iff[symmetric]
 
+lemma gr_one_powr[simp]:
+  fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
+by(simp add: less_powr_iff)
+
 lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
 
@@ -2712,6 +2716,7 @@
 lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
   by (simp add: log_def ln_powr)
 
+(* [simp] is not worth it, interferes with some proofs *)
 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
   by (simp add: log_powr powr_realpow [symmetric])