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.9    by (simp add: exp_add_commuting[symmetric])
    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.19    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
    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.42    by (rule ln_unique) (simp add: exp_add)
    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.76      by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
    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.85    by (induct n) (simp_all add: ac_simps powr_add)
    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.94    by (simp add: powr_def)
    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