src/HOL/Transcendental.thy
 changeset 65578 e4997c181cce parent 65552 f533820e7248 child 65583 8d53b3bebab4
```     1.1 --- a/src/HOL/Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1506,7 +1506,7 @@
1.4    finally show False by simp
1.5  qed
1.6
1.7 -lemma exp_minus_inverse: "exp x * exp (- x) = 1"
1.8 +lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
1.10
1.11  lemma exp_minus: "exp (- x) = inverse (exp x)"
1.12 @@ -1517,17 +1517,18 @@
1.13    for x :: "'a::{real_normed_field,banach}"
1.14    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
1.15
1.16 -lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
1.17 +lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
1.18    for x :: "'a::{real_normed_field,banach}"
1.20
1.21 -corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
1.22 -  by (simp add: exp_of_nat_mult)
1.23 +corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
1.24 +  for x :: "'a::{real_normed_field,banach}"
1.25 +  by (metis exp_of_nat_mult mult_of_nat_commute)
1.26
1.27  lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
1.28    by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
1.29
1.30 -lemma exp_divide_power_eq:
1.31 +lemma exp_divide_power_eq [simp]:
1.32    fixes x :: "'a::{real_normed_field,banach}"
1.33    assumes "n > 0"
1.34    shows "exp (x / of_nat n) ^ n = exp x"
1.35 @@ -1742,7 +1743,7 @@
1.36    for x :: real
1.37    by (erule subst) (rule ln_exp)
1.38
1.39 -lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.40 +lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.41    for x :: real
1.43
1.44 @@ -1750,7 +1751,7 @@
1.45    for f :: "'a \<Rightarrow> real"
1.46    by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
1.47
1.48 -lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.49 +lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.50    for x :: real
1.51    by (rule ln_unique) (simp add: exp_minus)
1.52
1.53 @@ -1758,8 +1759,8 @@
1.54    for x :: real
1.55    by (rule ln_unique) (simp add: exp_diff)
1.56
1.57 -lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
1.58 -  by (rule ln_unique) (simp add: exp_real_of_nat_mult)
1.59 +lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
1.60 +  by (rule ln_unique) simp
1.61
1.62  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.63    for x :: real
1.64 @@ -1781,6 +1782,9 @@
1.65    for x :: real
1.66    by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
1.67
1.68 +lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
1.69 +  using exp_le_cancel_iff exp_total by force
1.70 +
1.71  lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
1.72    for x :: real
1.73    using ln_le_cancel_iff [of 1 x] by simp
1.74 @@ -2298,7 +2302,7 @@
1.75    also from assms False have "ln (1 + x / real n) \<le> x / real n"
1.77    with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
1.78 -    by (simp add: field_simps)
1.79 +    by (simp add: field_simps del: exp_of_nat_mult)
1.80    finally show ?thesis .
1.81  next
1.82    case True
1.83 @@ -2701,7 +2705,7 @@
1.84  lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
1.86
1.87 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
1.88 +lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
1.89    by (metis of_nat_numeral powr_realpow)
1.90
1.91  lemma numeral_powr_numeral[simp]:
1.92 @@ -2841,14 +2845,26 @@
1.93    for x :: real
1.95
1.96 -lemma powr_mono2: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x powr a \<le> y powr a"
1.97 +lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
1.98    for x :: real
1.99 -  apply (case_tac "a = 0")
1.100 -   apply simp
1.101 -  apply (case_tac "x = y")
1.102 -   apply simp
1.103 -  apply (metis dual_order.strict_iff_order powr_less_mono2)
1.104 -  done
1.105 +proof (cases "a = 0")
1.106 +  case True
1.107 +  with that show ?thesis by simp
1.108 +next
1.109 +  case False show ?thesis
1.110 +  proof (cases "x = y")
1.111 +    case True
1.112 +    then show ?thesis by simp
1.113 +  next
1.114 +    case False
1.115 +    then show ?thesis
1.116 +      by (metis dual_order.strict_iff_order powr_less_mono2 that \<open>a \<noteq> 0\<close>)
1.117 +  qed
1.118 +qed
1.119 +
1.120 +lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
1.121 +  for x :: real
1.122 +  using powr_mono2 by fastforce
1.123
1.124  lemma powr_mono2':
1.125    fixes a x y :: real
1.126 @@ -2861,6 +2877,12 @@
1.127      by (auto simp add: powr_minus field_simps)
1.128  qed
1.129
1.130 +lemma powr_mono_both:
1.131 +  fixes x :: real
1.132 +  assumes "0 \<le> a" "a \<le> b" "1 \<le> x" "x \<le> y"
1.133 +    shows "x powr a \<le> y powr b"
1.134 +  by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
1.135 +
1.136  lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
1.137    for x :: real
1.138    unfolding powr_def exp_inj_iff by simp
```