Some new material. SIMPRULE STATUS for sum/prod.delta rules!
authorpaulson <lp15@cam.ac.uk>
Thu Jun 15 17:22:23 2017 +0100 (23 months ago)
changeset 66089def95e0bc529
parent 66088 c9c9438cfc0f
child 66103 8ff7fd4ee919
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Groups_Big.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Jun 15 11:11:36 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Jun 15 17:22:23 2017 +0100
     1.3 @@ -387,7 +387,7 @@
     1.4    have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
     1.5      = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
     1.6      using b
     1.7 -    by (auto simp add: algebra_simps inner_sum_left inner_Basis split: if_split intro!: sum.cong)
     1.8 +    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
     1.9    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
    1.10      using b by (simp add: sum.delta)
    1.11    also have "\<dots> = f x \<bullet> b"
     2.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 11:11:36 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 17:22:23 2017 +0100
     2.3 @@ -919,7 +919,6 @@
     2.4    apply (auto simp:  bounded_linear_mult_right)
     2.5    done
     2.6  
     2.7 -(*Used only once, in Multivariate/cauchy.ml. *)
     2.8  lemma has_complex_derivative_inverse_strong:
     2.9    fixes f :: "complex \<Rightarrow> complex"
    2.10    shows "DERIV f x :> f' \<Longrightarrow>
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 15 11:11:36 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 15 17:22:23 2017 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4  lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
     3.5    by simp
     3.6  
     3.7 -lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
     3.8 +lemma content_pos_le [iff]: "0 \<le> content X"
     3.9    by simp
    3.10  
    3.11  corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
    3.12 @@ -157,20 +157,18 @@
    3.13  lemma sum_content_null:
    3.14    assumes "content (cbox a b) = 0"
    3.15      and "p tagged_division_of (cbox a b)"
    3.16 -  shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
    3.17 +  shows "(\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) = (0::'a::real_normed_vector)"
    3.18  proof (rule sum.neutral, rule)
    3.19    fix y
    3.20    assume y: "y \<in> p"
    3.21    obtain x k where xk: "y = (x, k)"
    3.22      using surj_pair[of y] by blast
    3.23 -  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
    3.24 -  from this(2) obtain c d where k: "k = cbox c d" by blast
    3.25 +  then obtain c d where k: "k = cbox c d" "k \<subseteq> cbox a b"
    3.26 +    by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
    3.27    have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
    3.28      unfolding xk by auto
    3.29    also have "\<dots> = 0"
    3.30 -    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
    3.31 -    unfolding assms(1) k
    3.32 -    by auto
    3.33 +    using assms(1) content_0_subset k(2) by auto
    3.34    finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
    3.35  qed
    3.36  
    3.37 @@ -446,6 +444,11 @@
    3.38    "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
    3.39    using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
    3.40  
    3.41 +lemma integrable_on_scaleR_left:
    3.42 +  assumes "f integrable_on A" 
    3.43 +  shows "(\<lambda>x. f x *\<^sub>R y) integrable_on A" 
    3.44 +  using assms has_integral_scaleR_left unfolding integrable_on_def by blast
    3.45 +
    3.46  lemma has_integral_mult_left:
    3.47    fixes c :: "_ :: real_normed_algebra"
    3.48    shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
    3.49 @@ -670,12 +673,8 @@
    3.50    by (auto intro: has_integral_sum integrable_integral)
    3.51  
    3.52  lemma integrable_sum:
    3.53 -  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s"
    3.54 -  unfolding integrable_on_def
    3.55 -  apply (drule bchoice)
    3.56 -  using has_integral_sum[of t]
    3.57 -  apply auto
    3.58 -  done
    3.59 +  "\<lbrakk>finite I;  \<And>a. a \<in> I \<Longrightarrow> f a integrable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>I. f a x) integrable_on S"
    3.60 +  unfolding integrable_on_def using has_integral_sum[of I] by metis
    3.61  
    3.62  lemma has_integral_eq:
    3.63    assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
    3.64 @@ -5493,32 +5492,10 @@
    3.65        apply (rule_tac[!] sum_nonneg)
    3.66        apply safe
    3.67        unfolding real_scaleR_def right_diff_distrib[symmetric]
    3.68 -      apply (rule_tac[!] mult_nonneg_nonneg)
    3.69 -    proof -
    3.70 -      fix a b
    3.71 -      assume ab: "(a, b) \<in> p1"
    3.72 -      show "0 \<le> content b"
    3.73 -        using *(3)[OF ab]
    3.74 -        apply safe
    3.75 -        apply (rule content_pos_le)
    3.76 +         apply (rule_tac[!] mult_nonneg_nonneg)
    3.77 +        apply simp_all
    3.78 +      using obt(4) prems(1) prems(4) apply (blast intro:  elim: dest!: bspec)+
    3.79          done
    3.80 -      then show "0 \<le> content b" .
    3.81 -      show "0 \<le> f a - g a" "0 \<le> h a - f a"
    3.82 -        using *(1-2)[OF ab]
    3.83 -        using obt(4)[rule_format,of a]
    3.84 -        by auto
    3.85 -    next
    3.86 -      fix a b
    3.87 -      assume ab: "(a, b) \<in> p2"
    3.88 -      show "0 \<le> content b"
    3.89 -        using *(6)[OF ab]
    3.90 -        apply safe
    3.91 -        apply (rule content_pos_le)
    3.92 -        done
    3.93 -      then show "0 \<le> content b" .
    3.94 -      show "0 \<le> f a - g a" and "0 \<le> h a - f a"
    3.95 -        using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto
    3.96 -    qed
    3.97      then show ?case
    3.98        apply -
    3.99        unfolding real_norm_def
   3.100 @@ -6317,7 +6294,7 @@
   3.101      proof (rule, goal_cases)
   3.102        case prems: (1 x)
   3.103        have "e / (4 * content (cbox a b)) > 0"
   3.104 -        using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
   3.105 +        by (simp add: False content_lt_nz e)
   3.106        from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
   3.107        guess n .. note n=this
   3.108        then show ?case
   3.109 @@ -7094,9 +7071,10 @@
   3.110        also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
   3.111          by simp
   3.112        also have "\<dots> < e' * norm (x - x0)"
   3.113 -        using \<open>e' > 0\<close> content_pos_le[of a b]
   3.114 -        by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
   3.115 -           (auto simp: divide_simps e_def simp del: measure_nonneg)
   3.116 +        using \<open>e' > 0\<close>
   3.117 +        apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])  
   3.118 +        apply  (auto simp: divide_simps e_def)
   3.119 +        by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
   3.120        finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
   3.121        then show ?case
   3.122          by (auto simp: divide_simps)
   3.123 @@ -7207,8 +7185,7 @@
   3.124        define e' where "e' = e / 2"
   3.125        with \<open>e > 0\<close> have "e' > 0" by simp
   3.126        then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
   3.127 -        using u content_nonzero content_pos_le[of a b]
   3.128 -        by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
   3.129 +        using u content_nonzero by (auto simp: uniform_limit_iff dist_norm zero_less_measure_iff)
   3.130        then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
   3.131        proof eventually_elim
   3.132          case (elim n)
     4.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 15 11:11:36 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 15 17:22:23 2017 +0100
     4.3 @@ -1665,8 +1665,8 @@
     4.4  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
     4.5    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
     4.6  
     4.7 -lemma is_interval_cbox: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
     4.8 -  and is_interval_box: "is_interval (box a b)" (is ?th2)
     4.9 +lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
    4.10 +  and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
    4.11    unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
    4.12    by (meson order_trans le_less_trans less_le_trans less_trans)+
    4.13  
    4.14 @@ -1726,12 +1726,28 @@
    4.15    by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
    4.16  
    4.17  lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
    4.18 -  by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
    4.19 +  by (simp add: box_ne_empty inner_Basis inner_sum_left)
    4.20  
    4.21  lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
    4.22    using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
    4.23  
    4.24 -
    4.25 +lemma interval_subset_is_interval:
    4.26 +  assumes "is_interval S"
    4.27 +  shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
    4.28 +proof
    4.29 +  assume ?lhs
    4.30 +  then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
    4.31 +next
    4.32 +  assume ?rhs
    4.33 +  have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
    4.34 +    using assms unfolding is_interval_def
    4.35 +    apply (clarsimp simp add: mem_box)
    4.36 +    using that by blast
    4.37 +  with \<open>?rhs\<close> show ?lhs
    4.38 +    by blast
    4.39 +qed
    4.40 +
    4.41 +  
    4.42  subsection \<open>Connectedness\<close>
    4.43  
    4.44  lemma connected_local:
    4.45 @@ -5641,35 +5657,6 @@
    4.46    qed
    4.47  qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
    4.48  
    4.49 -lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
    4.50 -proof -
    4.51 -  {
    4.52 -    assume ?rhs
    4.53 -    {
    4.54 -      fix e::real
    4.55 -      assume "e>0"
    4.56 -      with \<open>?rhs\<close> obtain N where N:"\<forall>n\<ge>N. dist (s n) (s N) < e/2"
    4.57 -        by (erule_tac x="e/2" in allE) auto
    4.58 -      {
    4.59 -        fix n m
    4.60 -        assume nm:"N \<le> m \<and> N \<le> n"
    4.61 -        then have "dist (s m) (s n) < e" using N
    4.62 -          using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
    4.63 -          by blast
    4.64 -      }
    4.65 -      then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
    4.66 -        by blast
    4.67 -    }
    4.68 -    then have ?lhs
    4.69 -      unfolding cauchy_def
    4.70 -      by blast
    4.71 -  }
    4.72 -  then show ?thesis
    4.73 -    unfolding cauchy_def
    4.74 -    using dist_triangle_half_l
    4.75 -    by blast
    4.76 -qed
    4.77 -
    4.78  lemma cauchy_imp_bounded:
    4.79    assumes "Cauchy s"
    4.80    shows "bounded (range s)"
    4.81 @@ -6978,6 +6965,11 @@
    4.82    ultimately show ?thesis ..
    4.83  qed
    4.84  
    4.85 +lemma bounded_uniformly_continuous_image:
    4.86 +  fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
    4.87 +  assumes "uniformly_continuous_on S f" "bounded S"
    4.88 +  shows "bounded(image f S)"
    4.89 +  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
    4.90  
    4.91  subsection\<open>Quotient maps\<close>
    4.92  
    4.93 @@ -9521,7 +9513,7 @@
    4.94    have "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" if "d > 0" for d :: real
    4.95    proof -
    4.96      from that obtain N where N: "\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
    4.97 -      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
    4.98 +      using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e
    4.99        by auto
   4.100      have "norm (x n - x N) < d" if "n \<ge> N" for n
   4.101      proof -
   4.102 @@ -9538,7 +9530,7 @@
   4.103      then show ?thesis by auto
   4.104    qed
   4.105    then show ?thesis
   4.106 -    by (simp add: cauchy dist_norm)
   4.107 +    by (simp add: Cauchy_altdef2 dist_norm)
   4.108  qed
   4.109  
   4.110  lemma complete_isometric_image:
     5.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 15 11:11:36 2017 +0200
     5.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 15 17:22:23 2017 +0100
     5.3 @@ -923,9 +923,7 @@
     5.4  
     5.5  lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
     5.6      (if n \<le> m then a$n else 0::'a::comm_ring_1)"
     5.7 -  apply (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
     5.8 -  apply (simp add: sum.delta')
     5.9 -  done
    5.10 +  by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
    5.11  
    5.12  lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
    5.13    (is "?s \<longlonglongrightarrow> a")
     6.1 --- a/src/HOL/Groups_Big.thy	Thu Jun 15 11:11:36 2017 +0200
     6.2 +++ b/src/HOL/Groups_Big.thy	Thu Jun 15 17:22:23 2017 +0100
     6.3 @@ -332,7 +332,7 @@
     6.4      by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
     6.5  qed
     6.6  
     6.7 -lemma delta:
     6.8 +lemma delta [simp]:
     6.9    assumes fS: "finite S"
    6.10    shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
    6.11  proof -
    6.12 @@ -355,7 +355,7 @@
    6.13    qed
    6.14  qed
    6.15  
    6.16 -lemma delta':
    6.17 +lemma delta' [simp]:
    6.18    assumes fin: "finite S"
    6.19    shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
    6.20    using delta [OF fin, of a b, symmetric] by (auto intro: cong)
     7.1 --- a/src/HOL/Probability/Fin_Map.thy	Thu Jun 15 11:11:36 2017 +0200
     7.2 +++ b/src/HOL/Probability/Fin_Map.thy	Thu Jun 15 17:22:23 2017 +0100
     7.3 @@ -474,7 +474,7 @@
     7.4    fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b"
     7.5    assume "Cauchy P"
     7.6    then obtain Nd where Nd: "\<And>n. n \<ge> Nd \<Longrightarrow> dist (P n) (P Nd) < 1"
     7.7 -    by (force simp: cauchy)
     7.8 +    by (force simp: Cauchy_altdef2)
     7.9    define d where "d = domain (P Nd)"
    7.10    with Nd have dim: "\<And>n. n \<ge> Nd \<Longrightarrow> domain (P n) = d" using dist_le_1_imp_domain_eq by auto
    7.11    have [simp]: "finite d" unfolding d_def by simp
    7.12 @@ -484,11 +484,11 @@
    7.13    have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse)
    7.14    {
    7.15      fix i assume "i \<in> d"
    7.16 -    have "Cauchy (p i)" unfolding cauchy p_def
    7.17 +    have "Cauchy (p i)" unfolding Cauchy_altdef2 p_def
    7.18      proof safe
    7.19        fix e::real assume "0 < e"
    7.20        with \<open>Cauchy P\<close> obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> dist (P n) (P N) < min e 1"
    7.21 -        by (force simp: cauchy min_def)
    7.22 +        by (force simp: Cauchy_altdef2 min_def)
    7.23        hence "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto
    7.24        with dim have dim: "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = d" by (metis nat_le_linear)
    7.25        show "\<exists>N. \<forall>n\<ge>N. dist ((P n) i) ((P N) i) < e"
     8.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jun 15 11:11:36 2017 +0200
     8.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jun 15 17:22:23 2017 +0100
     8.3 @@ -2111,7 +2111,7 @@
     8.4      by (rule sum.commute)
     8.5    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
     8.6                       (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
     8.7 -    by (auto intro!: sum.cong sum.neutral)
     8.8 +    by (auto intro!: sum.cong sum.neutral simp del: sum.delta)
     8.9    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
    8.10      by (intro sum.cong refl) (simp_all add: sum.delta)
    8.11    also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Jun 15 11:11:36 2017 +0200
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jun 15 17:22:23 2017 +0100
     9.3 @@ -1949,6 +1949,33 @@
     9.4    qed
     9.5  qed
     9.6  
     9.7 +lemma (in metric_space) Cauchy_altdef2: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
     9.8 +proof 
     9.9 +  assume "Cauchy s"
    9.10 +  then show ?rhs by (force simp add: Cauchy_def)
    9.11 +next
    9.12 +    assume ?rhs
    9.13 +    {
    9.14 +      fix e::real
    9.15 +      assume "e>0"
    9.16 +      with \<open>?rhs\<close> obtain N where N: "\<forall>n\<ge>N. dist (s n) (s N) < e/2"
    9.17 +        by (erule_tac x="e/2" in allE) auto
    9.18 +      {
    9.19 +        fix n m
    9.20 +        assume nm: "N \<le> m \<and> N \<le> n"
    9.21 +        then have "dist (s m) (s n) < e" using N
    9.22 +          using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
    9.23 +          by blast
    9.24 +      }
    9.25 +      then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
    9.26 +        by blast
    9.27 +    }
    9.28 +    then have ?lhs
    9.29 +      unfolding Cauchy_def by blast
    9.30 +  then show ?lhs
    9.31 +    by blast
    9.32 +qed
    9.33 +
    9.34  lemma (in metric_space) metric_CauchyI:
    9.35    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
    9.36    by (simp add: Cauchy_def)