author immler Wed Nov 12 17:36:36 2014 +0100 (2014-11-12) changeset 58984 ae0c56c485ae parent 58983 9c390032e4eb child 58985 bf498e0af9e3
```     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.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
```