# HG changeset patch # User paulson # Date 1689011302 -3600 # Node ID 9e0c035d026d71dd2a3964ff3768166cd3895007 # Parent f10aee81ab93f35dbc375ababdb862e7104c73cb# Parent 6fa0812135e0add5f358fcebc37a08ee373f9b4c merged diff -r f10aee81ab93 -r 9e0c035d026d src/HOL/Analysis/Abstract_Metric_Spaces.thy --- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Mon Jul 10 16:56:42 2023 +0200 +++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Mon Jul 10 18:48:22 2023 +0100 @@ -49,7 +49,7 @@ definition mcball where "mcball x r \ {y. x \ M \ y \ M \ d x y \ r}" lemma in_mball [simp]: "y \ mball x r \ x \ M \ y \ M \ d x y < r" - by (simp add: local.Metric_space_axioms Metric_space.mball_def) + by (simp add: mball_def) lemma centre_in_mball_iff [iff]: "x \ mball x r \ x \ M \ 0 < r" using in_mball mdist_zero by force @@ -70,7 +70,7 @@ by auto lemma in_mcball [simp]: "y \ mcball x r \ x \ M \ y \ M \ d x y \ r" - by (simp add: local.Metric_space_axioms Metric_space.mcball_def) + by (simp add: mcball_def) lemma centre_in_mcball_iff [iff]: "x \ mcball x r \ x \ M \ 0 \ r" using mdist_zero by force @@ -181,13 +181,13 @@ lemma openin_mtopology_mcball: "openin mtopology U \ U \ M \ (\x. x \ U \ (\r. 0 < r \ mcball x r \ U))" - using mball_iff_mcball openin_mtopology by presburger + by (simp add: mball_iff_mcball openin_mtopology) lemma metric_derived_set_of: "mtopology derived_set_of S = {x \ M. \r>0. \y\S. y\x \ y \ mball x r}" (is "?lhs=?rhs") proof show "?lhs \ ?rhs" - unfolding openin_mtopology derived_set_of_def + unfolding openin_mtopology derived_set_of_def by clarsimp (metis in_mball openin_mball openin_mtopology zero) show "?rhs \ ?lhs" unfolding openin_mtopology derived_set_of_def @@ -375,10 +375,8 @@ by blast with \S \ M\ gt_ex have "S \ \(range (mball a))" by force - moreover have "\U \ range (mball a). openin mtopology U" - by (simp add: openin_mball) - ultimately obtain \ where "finite \" "\ \ range (mball a)" "S \ \\" - by (meson com) + then obtain \ where "finite \" "\ \ range (mball a)" "S \ \\" + by (metis (no_types, opaque_lifting) com imageE openin_mball) then show ?thesis using mbounded_Union mbounded_subset by fastforce qed auto @@ -451,7 +449,7 @@ end lemma (in Metric_space) submetric_empty [iff]: "Submetric M d {}" - by (simp add: Metric_space_axioms Submetric.intro Submetric_axioms_def) +proof qed auto subsection \Abstract type of metric spaces\ @@ -486,11 +484,11 @@ lemma (in Metric_space) mspace_metric[simp]: "mspace (metric (M,d)) = M" - by (simp add: mspace_def Metric_space_axioms metric_inverse) + by (simp add: metric_inverse mspace_def subspace) lemma (in Metric_space) mdist_metric[simp]: "mdist (metric (M,d)) = d" - by (simp add: mdist_def Metric_space_axioms metric_inverse) + by (simp add: mdist_def metric_inverse subspace) lemma metric_collapse [simp]: "metric (mspace m, mdist m) = m" by (simp add: dest_metric_inverse mdist_def mspace_def) @@ -849,8 +847,7 @@ lemma metrizable_space_euclidean: "metrizable_space (euclidean :: 'a::metric_space topology)" - unfolding metrizable_space_def - by (metis Met_TC.Metric_space_axioms Met_TC.mtopology_def mopen_eq_open) + using Met_TC.metrizable_space_mtopology by auto lemma (in Metric_space) regular_space_mtopology: "regular_space mtopology" @@ -1109,7 +1106,7 @@ then obtain N where "\n. n\N \ \ n \ M \ d (\ n) l < \/2" by (force simp: eventually_sequentially) then show "\N. \n n'. N \ n \ N \ n' \ d (\ n) (\ n') < \" - by (smt (verit) Metric_space.limitin_mspace Metric_space.mdist_reverse_triangle Metric_space_axioms field_sum_of_halves lim) + by (smt (verit) limitin_mspace mdist_reverse_triangle field_sum_of_halves lim) qed (use assms in blast) @@ -1233,7 +1230,7 @@ and dynn': "d (y (n div 2)) (y (n' div 2)) < \/2" using Nx Ny Nxy by blast+ have inM: "x (n div 2) \ M" "x (n' div 2) \ M""y (n div 2) \ M" "y (n' div 2) \ M" - using Metric_space.MCauchy_def Metric_space_axioms R by blast+ + using MCauchy_def R by blast+ show "d (if even n then x (n div 2) else y (n div 2)) (if even n' then x (n' div 2) else y (n' div 2)) < \" proof (cases "even n") case nt: True @@ -1846,7 +1843,7 @@ then have "j > i" and dxj: "d x (\ j) < \/4" by auto have "(\ -` mball x (\/4)) \ (\ -` mball y (\/2))" if "d x y < \/4" "y \ M" for y - using that by (simp add: mball_subset Metric_space_axioms vimage_mono) + using that by (simp add: mball_subset vimage_mono) then have infj: "infinite (\ -` mball (\ j) (\/2))" by (meson True \d x (\ j) < \/4\ \ in_mono infx rangeI finite_subset) have "\ i \ M" "\ j \ M" "x \ M" @@ -1981,7 +1978,7 @@ shows "Metric_space.mtotally_bounded T d S" proof - interpret Submetric M d T - by (simp add: Metric_space_axioms assms Submetric.intro Submetric_axioms.intro) + using \T \ M\ by unfold_locales show ?thesis using assms unfolding sub.mtotally_bounded_def mtotally_bounded_def @@ -1994,10 +1991,10 @@ have "mtotally_bounded S" if "S \ M" "Metric_space.mtotally_bounded S d S" proof - interpret Submetric M d S - by (simp add: Metric_space_axioms Submetric_axioms.intro Submetric_def \S \ M\) + using \S \ M\ by unfold_locales show ?thesis using that - by (metis MCauchy_submetric Metric_space.mtotally_bounded_sequentially Metric_space_axioms subspace) + by (meson MCauchy_submetric mtotally_bounded_sequentially sub.mtotally_bounded_sequentially) qed moreover have "mtotally_bounded S \ Metric_space.mtotally_bounded S d S" by (simp add: mtotally_bounded_imp_subset mtotally_bounded_submetric) diff -r f10aee81ab93 -r 9e0c035d026d src/HOL/Analysis/Urysohn.thy --- a/src/HOL/Analysis/Urysohn.thy Mon Jul 10 16:56:42 2023 +0200 +++ b/src/HOL/Analysis/Urysohn.thy Mon Jul 10 18:48:22 2023 +0100 @@ -3442,7 +3442,6 @@ qed - subsection\Contractions\ lemma (in Metric_space) contraction_imp_unique_fixpoint: @@ -3452,7 +3451,7 @@ and "\x y. \x \ M; y \ M\ \ d (f x) (f y) \ k * d x y" and "x \ M" "y \ M" shows "x = y" - by (smt (verit, ccfv_SIG) Metric_space.mdist_pos_less Metric_space_axioms assms mult_le_cancel_right1) + by (smt (verit, ccfv_SIG) mdist_pos_less mult_le_cancel_right1 assms) text \Banach Fixed-Point Theorem (aka, Contraction Mapping Principle)\ lemma (in Metric_space) Banach_fixedpoint_thm: