added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
authorimmler
Wed Nov 12 17:36:36 2014 +0100 (2014-11-12)
changeset 58984ae0c56c485ae
parent 58983 9c390032e4eb
child 58985 bf498e0af9e3
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Wed Nov 12 17:36:32 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Nov 12 17:36:36 2014 +0100
     1.3 @@ -1861,6 +1861,9 @@
     1.4  lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
     1.5    by (simp add: divide_inverse powr_minus)
     1.6  
     1.7 +lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
     1.8 +  by (simp add: powr_minus_divide)
     1.9 +
    1.10  lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
    1.11    by (simp add: powr_def)
    1.12  
    1.13 @@ -1926,6 +1929,12 @@
    1.14  lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
    1.15    by (simp add: log_mult divide_inverse log_inverse)
    1.16  
    1.17 +lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
    1.18 +  and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
    1.19 +  and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"
    1.20 +  and minus_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y - log b x = log b (b powr y / x)"
    1.21 +  by (simp_all add: log_mult log_divide)
    1.22 +
    1.23  lemma log_less_cancel_iff [simp]:
    1.24    "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x < log a y \<longleftrightarrow> x < y"
    1.25    apply safe
    1.26 @@ -1982,6 +1991,34 @@
    1.27  lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a"
    1.28    using log_le_cancel_iff[of a x a] by simp
    1.29  
    1.30 +lemma le_log_iff:
    1.31 +  assumes "1 < b" "x > 0"
    1.32 +  shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
    1.33 +  by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel
    1.34 +    powr_one_eq_one powr_one_gt_zero_iff)
    1.35 +
    1.36 +lemma less_log_iff:
    1.37 +  assumes "1 < b" "x > 0"
    1.38 +  shows "y < log b x \<longleftrightarrow> b powr y < x"
    1.39 +  by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff
    1.40 +    powr_log_cancel zero_less_one)
    1.41 +
    1.42 +lemma
    1.43 +  assumes "1 < b" "x > 0"
    1.44 +  shows log_less_iff: "log b x < y \<longleftrightarrow> x < b powr y"
    1.45 +    and log_le_iff: "log b x \<le> y \<longleftrightarrow> x \<le> b powr y"
    1.46 +  using le_log_iff[OF assms, of y] less_log_iff[OF assms, of y]
    1.47 +  by auto
    1.48 +
    1.49 +lemmas powr_le_iff = le_log_iff[symmetric]
    1.50 +  and powr_less_iff = le_log_iff[symmetric]
    1.51 +  and less_powr_iff = log_less_iff[symmetric]
    1.52 +  and le_powr_iff = log_le_iff[symmetric]
    1.53 +
    1.54 +lemma
    1.55 +  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)"
    1.56 +  by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
    1.57 +
    1.58  lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
    1.59    apply (induct n)
    1.60    apply simp