# HG changeset patch
# User hoelzl
# Date 1334752156 -7200
# Node ID 69f0af2b7d542f9c55cc522031b2d081532e9268
# Parent  a6b76247534d5f142d30418f99b67595bc7ec1ef
add lemmas to compare log with 0 and 1

diff -r a6b76247534d -r 69f0af2b7d54 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Wed Apr 18 14:29:05 2012 +0200
+++ b/src/HOL/Log.thy	Wed Apr 18 14:29:16 2012 +0200
@@ -168,6 +168,29 @@
      "[| 1 < a; 0 < x; 0 < y |] ==> (log a x \<le> log a y) = (x \<le> y)"
 by (simp add: linorder_not_less [symmetric])
 
+lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x"
+  using log_less_cancel_iff[of a 1 x] by simp
+
+lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x"
+  using log_le_cancel_iff[of a 1 x] by simp
+
+lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1"
+  using log_less_cancel_iff[of a x 1] by simp
+
+lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1"
+  using log_le_cancel_iff[of a x 1] by simp
+
+lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x"
+  using log_less_cancel_iff[of a a x] by simp
+
+lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x"
+  using log_le_cancel_iff[of a a x] by simp
+
+lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a"
+  using log_less_cancel_iff[of a x a] by simp
+
+lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
+  using log_le_cancel_iff[of a x a] by simp
 
 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
   apply (induct n, simp)