author immler Sun, 27 Oct 2019 21:38:41 -0400 changeset 70960 84f79d82df0a parent 70959 ba0b65d45aec child 70961 70fb697be418 child 70962 e8207714d505
some applications of "metric"
```--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Oct 27 20:55:58 2019 -0400
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sun Oct 27 21:38:41 2019 -0400
@@ -84,14 +84,7 @@
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"
@@ -133,9 +126,7 @@

lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
unfolding mem_ball set_eq_iff
-  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

@@ -251,8 +242,7 @@
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}"
@@ -345,15 +335,10 @@
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])
@@ -542,11 +527,8 @@
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>
@@ -833,14 +815,10 @@
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 (erule subset_trans)
-    apply (clarsimp simp add: cball_def)
+    by (intro exI[where x="dist x y + e + 1"]) metric
qed

lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
@@ -860,7 +838,7 @@
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
@@ -1409,7 +1387,7 @@
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"
@@ -1636,9 +1614,8 @@
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
}
@@ -1729,9 +1706,8 @@
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"
+        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"
@@ -2150,7 +2126,7 @@
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"
@@ -2208,14 +2184,12 @@
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"])
@@ -2434,7 +2408,7 @@
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
@@ -2514,13 +2488,11 @@
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>)
@@ -2568,26 +2540,19 @@
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
-     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
-     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
+    moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
+    ultimately show "dist (f y) (f x) < e" by metric
qed
qed

@@ -2634,7 +2599,7 @@
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>
@@ -2699,14 +2664,8 @@
dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
also
-        {
-          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"