# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1722244432 -3600
# Node ID 6c369fec315a8fde892fd55141ddbe4967f1ccd4
# Parent  ee77d9d40be604976686c211468a447169e496c3
Migration of new material mostly about exp, ln

diff -r ee77d9d40be6 -r 6c369fec315a src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Fields.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -949,7 +949,7 @@
   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
 
 lemma divide_left_mono:
-  "\<lbrakk>b \<le> a; 0 \<le> c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
+  "\<lbrakk>b \<le> a; 0 \<le> c; 0 < b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
   by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
 
 lemma divide_strict_left_mono_neg:
@@ -957,16 +957,16 @@
   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
 
 lemma mult_imp_div_pos_le: "0 < y \<Longrightarrow> x \<le> z * y \<Longrightarrow> x / y \<le> z"
-by (subst pos_divide_le_eq, assumption+)
+  by (subst pos_divide_le_eq, assumption+)
 
 lemma mult_imp_le_div_pos: "0 < y \<Longrightarrow> z * y \<le> x \<Longrightarrow> z \<le> x / y"
-by(simp add:field_simps)
+  by(simp add:field_simps)
 
 lemma mult_imp_div_pos_less: "0 < y \<Longrightarrow> x < z * y \<Longrightarrow> x / y < z"
-by(simp add:field_simps)
+  by(simp add:field_simps)
 
 lemma mult_imp_less_div_pos: "0 < y \<Longrightarrow> z * y < x \<Longrightarrow> z < x / y"
-by(simp add:field_simps)
+  by(simp add:field_simps)
 
 lemma frac_le:
   assumes "0 \<le> y" "x \<le> y" "0 < w" "w \<le> z"
@@ -1010,6 +1010,11 @@
     using assms by (force intro: mult_imp_less_div_pos mult_le_less_imp_less)
 qed
 
+text \<open>As above, with a better name\<close>
+lemma divide_mono:
+  "\<lbrakk>b \<le> a; c \<le> d; 0 < b; 0 \<le> c\<rbrakk> \<Longrightarrow> c / a \<le> d / b"
+  by (simp add: frac_le)
+
 lemma less_half_sum: "a < b \<Longrightarrow> a < (a+b) / (1+1)"
   by (simp add: field_simps zero_less_two)
 
diff -r ee77d9d40be6 -r 6c369fec315a src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Library/Discrete.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -63,7 +63,7 @@
   then show ?thesis by (simp add: log_rec)
 qed
 
-lemma log_exp [simp]: "log (2 ^ n) = n"
+lemma log_power [simp]: "log (2 ^ n) = n"
   by (induct n) simp_all
 
 lemma log_mono: "mono log"
diff -r ee77d9d40be6 -r 6c369fec315a src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Real.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -1303,6 +1303,8 @@
   for x y :: real
   by auto
 
+lemma mult_ge1_I: "\<lbrakk>x\<ge>1; y\<ge>1\<rbrakk> \<Longrightarrow> x*y \<ge> (1::real)"
+  using mult_mono by fastforce
 
 subsection \<open>Lemmas about powers\<close>
 
diff -r ee77d9d40be6 -r 6c369fec315a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Transcendental.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -1494,6 +1494,16 @@
   for x y :: real
   by (auto simp: linorder_not_less [symmetric])
 
+lemma exp_mono:
+  fixes x y :: real
+  assumes "x \<le> y"
+  shows "exp x \<le> exp y"
+  using assms exp_le_cancel_iff by fastforce
+
+lemma exp_minus': "exp (-x) = 1 / (exp x)"
+  for x :: "'a::{real_normed_field,banach}"
+  by (simp add: exp_minus inverse_eq_divide)
+
 lemma exp_inj_iff [iff]: "exp x = exp y \<longleftrightarrow> x = y"
   for x y :: real
   by (simp add: order_eq_iff)
@@ -1668,8 +1678,11 @@
   for x :: real
   by (simp add: linorder_not_less [symmetric])
 
-lemma ln_mono: "\<And>x::real. \<lbrakk>x \<le> y; 0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y"
-  using ln_le_cancel_iff by presburger
+lemma ln_mono: "\<And>x::real. \<lbrakk>x \<le> y; 0 < x\<rbrakk> \<Longrightarrow> ln x \<le> ln y"
+  by simp
+
+lemma ln_strict_mono: "\<And>x::real. \<lbrakk>x < y; 0 < x\<rbrakk> \<Longrightarrow> ln x < ln y"
+  by simp
 
 lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   for x :: real
@@ -2327,6 +2340,9 @@
   \<comment> \<open>logarithm of \<^term>\<open>x\<close> to base \<^term>\<open>a\<close>\<close>
   where "log a x = ln x / ln a"
 
+lemma log_exp [simp]: "log b (exp x) = x / ln b"
+  by (simp add: log_def)
+
 lemma tendsto_log [tendsto_intros]:
   "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> b\<noteq>0 \<Longrightarrow>
     ((\<lambda>x. log (f x) (g x)) \<longlongrightarrow> log a b) F"