src/HOL/Analysis/Elementary_Metric_Spaces.thy

 
 lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
   by (auto simp: mem_ball mem_cball)
 
 lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
-  unfolding mem_cball
-proof -
-  have "dist z x \<le> dist z y + dist y x"
-    by (rule dist_triangle)
-  also assume "dist z y \<le> b"
-  also assume "dist y x \<le> a"
-  finally show "dist z x \<le> b + a" by arith
-qed
+  by metric
 
 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   by (simp add: set_eq_iff) arith
 
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"

 lemma open_contains_ball_eq: "open S \<Longrightarrow> x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
   by (metis open_contains_ball subset_eq centre_in_ball)
 
 lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
   unfolding mem_ball set_eq_iff
-  apply (simp add: not_less)
-  apply (metis zero_le_dist order_trans dist_self)
-  done
+  by (simp add: not_less) metric
 
 lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
 
 lemma closed_cball [iff]: "closed (cball x e)"
 proof -

   apply (clarsimp simp add: islimpt_approachable)
   apply (drule_tac x="e/2" in spec)
   apply (auto simp: simp del: less_divide_eq_numeral1)
   apply (drule_tac x="dist x' x" in spec)
   apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)
-  apply (erule rev_bexI)
-  apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl)
+  apply metric
   done
 
 lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
   using closed_limpt limpt_of_limpts by blast
 

   have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   proof -
     from e have e2: "e/2 > 0" by arith
     from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
       by blast
-    let ?m = "min (e/2) (dist x y) "
-    from e2 y(2) have mp: "?m > 0"
+    from e2 y(2) have mp: "min (e/2) (dist x y) > 0"
       by simp
-    from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
-      by blast
-    from z y have "dist z y < e"
-      by (intro dist_triangle_lt [where z=x]) simp
-    from d[rule_format, OF y(1) z(1) this] y z show ?thesis
-      by (auto simp: dist_commute)
+    from d y C[OF mp] show ?thesis
+      by metric
   qed
   then show ?thesis
     by (metis islimpt_approachable closed_limpt [where 'a='a])
 qed
 

     {
       fix y
       assume "y \<in> f ` (ball x d \<inter> s)"
       then have "y \<in> ball (f x) e"
         using d(2)
-        apply (auto simp: dist_commute)
-        apply (erule_tac x=xa in ballE, auto)
         using \<open>e > 0\<close>
-        apply auto
-        done
+        by (auto simp: dist_commute)
     }
     then have "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e"
       using \<open>d > 0\<close>
       unfolding subset_eq ball_def by (auto simp: dist_commute)
   }

   by (meson bounded_ball bounded_subset)
 
 lemma bounded_subset_ballD:
   assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
 proof -
-  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
+  obtain e::real and y where "S \<subseteq> cball y e" "0 \<le> e"
     using assms by (auto simp: bounded_subset_cball)
   then show ?thesis
-    apply (rule_tac x="dist x y + e + 1" in exI)
-    apply (simp add: add.commute add_pos_nonneg)
-    apply (erule subset_trans)
-    apply (clarsimp simp add: cball_def)
-    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
+    by (intro exI[where x="dist x y + e + 1"]) metric
 qed
 
 lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
   by (induct set: finite) simp_all
 

 proof -
   from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
     by (auto simp: bounded_any_center[of _ undefined] dist_commute)
   have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
     using *[OF that]
-    by (rule order_trans[OF dist_triangle add_mono])
+    by metric
   then show ?thesis
     by (auto intro!: boundedI)
 qed
 
 lemma bounded_Times:

       then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"
         using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
       have "ball y \<delta> \<subseteq> ball y (r x)"
         by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
       also have "... \<subseteq> ball x (2*r x)"
-        by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)
+        using x by metric
       finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"
         by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
       have "bounded T"
         using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
       then have "T \<subseteq> ball y \<delta>"

           using n M by auto
         moreover have "r n \<ge> N"
           using lr'[of n] n by auto
         then have "dist (f n) ((f \<circ> r) n) < e / 2"
           using N and n by auto
-        ultimately have "dist (f n) l < e"
-          using dist_triangle_half_r[of "f (r n)" "f n" e l]
-          by (auto simp: dist_commute)
+        ultimately have "dist (f n) l < e" using n M
+          by metric
       }
       then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
     }
     then have "\<exists>l\<in>s. (f \<longlongrightarrow> l) sequentially" using \<open>l\<in>s\<close>
       unfolding lim_sequentially by auto

         assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
         then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
           using F_dec t by (auto simp: e_def field_simps of_nat_Suc)
         with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
           by (auto simp: subset_eq)
-        with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] \<open>2 * e N < r\<close>
-        show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
-          by (simp add: dist_commute)
+        with \<open>2 * e N < r\<close> show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
+          by metric
       qed
 
       ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
         using assms unfolding complete_def by blast
     qed

 
     have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
     proof (auto)
       fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
       have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
-        using dist_triangle[of x y z] by (auto simp add: dist_commute)
+        by metric
       also have "... < infdist x T + infdist y S"
         using H by auto
       finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
         by auto
       then show False

   moreover
   from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
     by (auto simp: compact_eq_bounded_closed bounded_def)
   {
     fix y
-    assume le: "infdist y A \<le> e"
+    assume "infdist y A \<le> e"
+    moreover
     from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
-    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
-    have "dist x0 y \<le> dist y z + dist x0 z"
-      by (metis dist_commute dist_triangle)
-    also have "dist y z \<le> e" using le z by simp
-    also have "dist x0 z \<le> b" using b z by simp
-    finally have "dist x0 y \<le> b + e" by arith
+    obtain z where "z \<in> A" "infdist y A = dist y z" by blast
+    ultimately
+    have "dist x0 y \<le> b + e" using b by metric
   } then
   have "bounded {x. infdist x A \<le> e}"
     by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
   ultimately show "compact {x. infdist x A \<le> e}"
     by (simp add: compact_eq_bounded_closed)

       using N2 \<open>0 < e\<close> by (simp add: field_simps)
     finally have "dist (f (r (max N1 N2))) x < e / 2" .
     moreover have "dist (f (r (max N1 N2))) l < e/2"
       using N1 max.cobounded1 by blast
     ultimately have "dist x l < e"
-      using dist_triangle_half_r by blast
+      by metric
     then show ?thesis
       using e \<open>x \<notin> G\<close> by blast
   qed
   then show ?thesis
     by (meson that)

         using R [of y "e/2"] \<open>0 < e\<close> y by auto
       obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
         using closure_approachable y
         by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
       have "dist (f z) (f y) < e/2"
-        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>'\<close> by linarith
+        using \<delta>' [OF \<open>z \<in> S\<close>] z \<open>0 < \<delta>'\<close> by metric
       moreover have "dist (f z) (f x) < e/2"
-        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
-        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
+        using \<delta>[OF \<open>z \<in> S\<close>] z dyx by metric
       ultimately show ?thesis
-        by (metis dist_commute dist_triangle_half_l less_imp_le)
+        by metric
     qed
     then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
       by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
   qed
 qed

         using closure_approachable [of x S]
         by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
     obtain d2::real where "d2 > 0"
            and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
       using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
-     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
-        using closure_approachable [of y S]
-        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
-     have "dist x' x < d/3" using x' by auto
-     moreover have "dist x y < d/3"
-       by (metis dist_commute dyx less_divide_eq_numeral1(1))
-     moreover have "dist y y' < d/3"
-       by (metis (no_types) dist_commute min_less_iff_conj y')
-     ultimately have "dist x' y' < d/3 + d/3 + d/3"
-       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
-     then have "dist x' y' < d" by simp
-     then have "dist (f x') (f y') < e/3"
-       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
-     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
-       by (simp add: closure_def)
-     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
-       by (simp add: closure_def)
-     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
-       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
-    then show "dist (f y) (f x) < e" by simp
+    obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
+      using closure_approachable [of y S]
+      by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
+    have "dist x' x < d/3" using x' by auto
+    then have "dist x' y' < d"
+      using dyx y' by metric
+    then have "dist (f x') (f y') < e/3"
+      by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
+    moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
+      by (simp add: closure_def)
+    moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
+      by (simp add: closure_def)
+    ultimately show "dist (f y) (f x) < e" by metric
   qed
 qed
 
 lemma uniformly_continuous_on_extension_at_closure:
   fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"

       ultimately
       show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
       proof eventually_elim
         case (elim n)
         have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
-          by (metis dist_triangle dist_commute)
+          by metric
         also have "dist (f (xs n)) (f (xs' n)) < e'"
           by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
         also note \<open>dist (f (xs n)) l < e'\<close>
         also have "e' + e' = e" by (simp add: e'_def)
         finally show ?case by simp

         case (elim n)
         have "dist (?g x') (?g x) \<le>
           dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
           by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
         also
-        {
-          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
-            by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)
-          also note \<open>dist (xs' n) x' < d'\<close>
-          also note \<open>dist x' x < d'\<close>
-          also note \<open>dist (xs n) x < d'\<close>
-          finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
-        }
+        from \<open>dist (xs' n) x' < d'\<close> \<open>dist x' x < d'\<close> \<open>dist (xs n) x < d'\<close>
+        have "dist (xs' n) (xs n) < d" unfolding d'_def by metric
         with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
           by (rule d)
         also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
         also note \<open>dist (f (xs n)) (?g x) < e'\<close>
         finally show ?case by (simp add: e'_def)