# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1676743805 0
# Node ID 8543e6b10a569d38bdc3463ca253664ded927fb1
# Parent  c16d423c9cb1f7f1f6d3a908da568a8b0708192e
Simplified a few proofs

diff -r c16d423c9cb1 -r 8543e6b10a56 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Feb 17 13:48:42 2023 +0000
+++ b/src/HOL/MacLaurin.thy	Sat Feb 18 18:10:05 2023 +0000
@@ -114,10 +114,8 @@
     qed (simp add: differentiable_difg n)
   next
     case (Suc m')
-    then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0"
-      by simp
     then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
-      by fast
+      by force
     have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
     proof (rule Rolle)
       show "0 < t" by fact
@@ -131,14 +129,11 @@
     with \<open>t < h\<close> show ?case
       by auto
   qed
-  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0"
-    by fast
-  with \<open>m < n\<close> have "difg (Suc m) t = 0"
-    by (simp add: difg_Suc_eq_0)
+  then obtain t where "0 < t" "t < h" "difg (Suc m) t = 0"
+    using \<open>m < n\<close> difg_Suc_eq_0 by force
   show ?thesis
   proof (intro exI conjI)
-    show "0 < t" by fact
-    show "t < h" by fact
+    show "0 < t" "t < h" by fact+
     show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
       using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def)
   qed
@@ -157,10 +152,8 @@
 next
   case Suc
   then have "n > 0" by simp
-  from INIT1 this INIT2 DERIV
-  have "\<exists>t>0. t < h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
-    by (rule Maclaurin)
-  then show ?thesis by fastforce
+  from Maclaurin [OF INIT1 this INIT2 DERIV]
+  show ?thesis by fastforce
 qed
 
 lemma Maclaurin_minus:
@@ -216,9 +209,7 @@
     then obtain t where "x < t" "t < 0"
       "diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
       by blast
-    with \<open>x < 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
-      by simp
-    then show ?thesis ..
+    with \<open>x < 0\<close> \<open>diff 0 = f\<close> show ?thesis by force
   next
     assume "x > 0"
     with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t"
@@ -247,20 +238,12 @@
   assume "x < 0"
   with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t"
     by (intro Maclaurin_minus) auto
-  then obtain t where "t > x" "t < 0" "f x = ?f x t"
-    by blast
-  with \<open>x < 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
-    by simp
-  then show ?thesis ..
+  then show ?thesis by force
 next
   assume "x > 0"
   with assms have "\<exists>t>0. t < x \<and> f x = ?f x t"
     by (intro Maclaurin) auto
-  then obtain t where "t > 0" "t < x" "f x = ?f x t"
-    by blast
-  with \<open>x > 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
-    by simp
-  then show ?thesis ..
+  then show ?thesis by force
 qed
 
 lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0"
@@ -280,22 +263,7 @@
 next
   case False
   show ?thesis
-  proof (cases "x = 0")
-    case True
-    with \<open>n \<noteq> 0\<close> have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
-      by (intro Maclaurin_zero) auto
-    with INIT \<open>x = 0\<close> \<open>n \<noteq> 0\<close> have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
-      by force
-    then show ?thesis ..
-  next
-    case False
-    with INIT \<open>n \<noteq> 0\<close> DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
-      by (intro Maclaurin_all_lt) auto
-    then obtain t where "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" ..
-    then have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
-      by simp
-    then show ?thesis ..
-  qed
+    using DERIV INIT Maclaurin_bi_le by auto
 qed
 
 lemma Maclaurin_all_le_objl:
@@ -324,12 +292,7 @@
   using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
 
 corollary ln_2_less_1: "ln 2 < (1::real)"
-proof -
-  have "2 < 5/(2::real)" by simp
-  also have "5/2 \<le> exp (1::real)" using exp_lower_Taylor_quadratic[of 1, simplified] by simp
-  finally have "exp (ln 2) < exp (1::real)" by simp
-  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
-qed
+  by (smt (verit) ln_eq_minus_one ln_le_minus_one)
 
 subsection \<open>Version for Sine Function\<close>
 
@@ -430,8 +393,8 @@
   proof (rule Maclaurin_all_lt)
     show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative
            cos (x + 1/2 * real (Suc m) * pi)) (at x)"
-      apply (rule allI derivative_eq_intros | simp)+
-      using cos_expansion_lemma by force
+      using cos_expansion_lemma
+      by (intro allI derivative_eq_intros | simp)+
   qed (use False in auto)
   then show ?thesis
     apply (rule ex_forward, simp)
@@ -511,10 +474,10 @@
     using mod_exhaust_less_4 [of m]
     by (auto simp: minus_one_power_iff even_even_mod_4_iff [of m] dest: even_mod_4_div_2 odd_mod_4_div_2)
   show ?thesis
-    unfolding sin_coeff_def
     apply (subst t2)
     apply (rule sin_bound_lemma)
      apply (rule sum.cong[OF refl])
+    unfolding sin_coeff_def
      apply (subst diff_m_0, simp)
     using est
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
@@ -559,10 +522,8 @@
       f (b - c + c) =
         (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
      by (rule Maclaurin [THEN exE])
-   then have "c < x + c \<and> x + c < b \<and> f b =
-     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
-    by fastforce
-  then show ?thesis by fastforce
+  then show ?thesis
+    by (smt (verit) sum.cong)
 qed
 
 lemma Taylor_down:
@@ -585,10 +546,8 @@
       by auto
     moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
       by (rule DERIV_add)
-    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
-      by (rule DERIV_chain2)
-    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
-      by simp
+    ultimately show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+      using DERIV_chain2 DERIV_shift by blast
   qed
   ultimately obtain x where
     "a - c < x \<and> x < 0 \<and>
@@ -614,26 +573,15 @@
   note INIT
   moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
     using DERIV and INTERV by fastforce
-  moreover note True
-  moreover from INTERV have "c \<le> b"
-    by simp
-  ultimately have "\<exists>t>x. t < c \<and> f x =
-    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
-    by (rule Taylor_down)
-  with True show ?thesis by simp
+  ultimately show ?thesis
+    using True INTERV Taylor_down by simp
 next
   case False
   note INIT
   moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
     using DERIV and INTERV by fastforce
-  moreover from INTERV have "a \<le> c"
-    by arith
-  moreover from False and INTERV have "c < x"
-    by arith
-  ultimately have "\<exists>t>c. t < x \<and> f x =
-    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
-    by (rule Taylor_up)
-  with False show ?thesis by simp
+  ultimately show ?thesis 
+    using Taylor_up INTERV False by simp
 qed
 
 end