1.1 --- a/src/HOL/Log.thy	Wed Apr 18 14:29:05 2012 +0200
     1.2 +++ b/src/HOL/Log.thy	Wed Apr 18 14:29:16 2012 +0200
     1.3 @@ -168,6 +168,29 @@
     1.4       "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
     1.5  by (simp add: linorder_not_less [symmetric])
     1.6  
     1.7 +lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
     1.8 +  using log_less_cancel_iff[of a 1 x] by simp
     1.9 +
    1.10 +lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
    1.11 +  using log_le_cancel_iff[of a 1 x] by simp
    1.12 +
    1.13 +lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
    1.14 +  using log_less_cancel_iff[of a x 1] by simp
    1.15 +
    1.16 +lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
    1.17 +  using log_le_cancel_iff[of a x 1] by simp
    1.18 +
    1.19 +lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
    1.20 +  using log_less_cancel_iff[of a a x] by simp
    1.21 +
    1.22 +lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
    1.23 +  using log_le_cancel_iff[of a a x] by simp
    1.24 +
    1.25 +lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
    1.26 +  using log_less_cancel_iff[of a x a] by simp
    1.27 +
    1.28 +lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
    1.29 +  using log_le_cancel_iff[of a x a] by simp
    1.30  
    1.31  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
    1.32    apply (induct n, simp)