# HG changeset patch # User paulson # Date 1672692384 0 # Node ID d6b02d54dbf8ae32946d9bdb34a631f38590f713 # Parent 04c7ec38874e8a8805cb690dcf3b3e9de8f70c88 Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path" diff -r 04c7ec38874e -r d6b02d54dbf8 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Sun Jan 01 12:24:00 2023 +0000 +++ b/src/HOL/Analysis/Further_Topology.thy Mon Jan 02 20:46:24 2023 +0000 @@ -2936,7 +2936,8 @@ have "(Arg2pi x / (2*pi)) \ {0..1}" "(Arg2pi y / (2*pi)) \ {0..1}" using Arg2pi_ge_0 Arg2pi_lt_2pi dual_order.strict_iff_order by fastforce+ with eq show ?thesis - using \simple_path \\ Arg2pi_lt_2pi unfolding simple_path_def o_def + using \simple_path \\ Arg2pi_lt_2pi + unfolding simple_path_def loop_free_def o_def by (metis eq_divide_eq_1 not_less_iff_gr_or_eq) qed with xy show "x = y" diff -r 04c7ec38874e -r d6b02d54dbf8 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Sun Jan 01 12:24:00 2023 +0000 +++ b/src/HOL/Analysis/Homotopy.thy Mon Jan 02 20:46:24 2023 +0000 @@ -4294,7 +4294,7 @@ have "g 0 \ path_image g" "g (1/2) \ path_image g" by (simp_all add: path_defs) moreover have "g 0 \ g (1/2)" - using assms by (fastforce simp add: simple_path_def) + using assms by (fastforce simp add: simple_path_def loop_free_def) ultimately have "\a. \ path_image g \ {a}" by blast then show ?thesis diff -r 04c7ec38874e -r d6b02d54dbf8 src/HOL/Analysis/Jordan_Curve.thy --- a/src/HOL/Analysis/Jordan_Curve.thy Sun Jan 01 12:24:00 2023 +0000 +++ b/src/HOL/Analysis/Jordan_Curve.thy Mon Jan 02 20:46:24 2023 +0000 @@ -203,14 +203,15 @@ by (metis \pathfinish h = g u\ pathfinish_def pathfinish_subpath u(3)) show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) = {a, b}" proof - show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) \ {a, b}" - using v \pathfinish (subpath v 1 h) = a\ \simple_path h\ - apply (auto simp: simple_path_def path_image_subpath image_iff Ball_def) - by (metis (full_types) less_eq_real_def less_irrefl less_le_trans) + have "loop_free h" + using \simple_path h\ simple_path_def by blast + then show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) \ {a, b}" + using v \pathfinish (subpath v 1 h) = a\ + apply (clarsimp simp add: loop_free_def path_image_subpath Ball_def) + by (smt (verit)) show "{a, b} \ path_image (subpath 0 v h) \ path_image (subpath v 1 h)" using v \pathstart (subpath 0 v h) = a\ \pathfinish (subpath v 1 h) = a\ - apply (auto simp: path_image_subpath image_iff) - by (metis atLeastAtMost_iff order_refl) + by (auto simp: path_image_subpath image_iff Bex_def) qed show "path_image (subpath 0 v h) \ path_image (subpath v 1 h) = path_image g" using v apply (simp add: path_image_subpath pihg [symmetric]) diff -r 04c7ec38874e -r d6b02d54dbf8 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sun Jan 01 12:24:00 2023 +0000 +++ b/src/HOL/Analysis/Path_Connected.thy Mon Jan 02 20:46:24 2023 +0000 @@ -13,30 +13,32 @@ subsection \Paths and Arcs\ definition\<^marker>\tag important\ path :: "(real \ 'a::topological_space) \ bool" - where "path g \ continuous_on {0..1} g" + where "path g \ continuous_on {0..1} g" definition\<^marker>\tag important\ pathstart :: "(real \ 'a::topological_space) \ 'a" - where "pathstart g = g 0" + where "pathstart g \ g 0" definition\<^marker>\tag important\ pathfinish :: "(real \ 'a::topological_space) \ 'a" - where "pathfinish g = g 1" + where "pathfinish g \ g 1" definition\<^marker>\tag important\ path_image :: "(real \ 'a::topological_space) \ 'a set" - where "path_image g = g ` {0 .. 1}" + where "path_image g \ g ` {0 .. 1}" definition\<^marker>\tag important\ reversepath :: "(real \ 'a::topological_space) \ real \ 'a" - where "reversepath g = (\x. g(1 - x))" + where "reversepath g \ (\x. g(1 - x))" definition\<^marker>\tag important\ joinpaths :: "(real \ 'a::topological_space) \ (real \ 'a) \ real \ 'a" (infixr "+++" 75) - where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" + where "g1 +++ g2 \ (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" + +definition\<^marker>\tag important\ loop_free :: "(real \ 'a::topological_space) \ bool" + where "loop_free g \ \x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" definition\<^marker>\tag important\ simple_path :: "(real \ 'a::topological_space) \ bool" - where "simple_path g \ - path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" + where "simple_path g \ path g \ loop_free g" definition\<^marker>\tag important\ arc :: "(real \ 'a :: topological_space) \ bool" - where "arc g \ path g \ inj_on g {0..1}" + where "arc g \ path g \ inj_on g {0..1}" subsection\<^marker>\tag unimportant\\Invariance theorems\ @@ -71,12 +73,8 @@ from linear_injective_left_inverse [OF assms] obtain h where h: "linear h" "h \ f = id" by blast - then have g: "g = h \ (f \ g)" - by (metis comp_assoc id_comp) - show ?thesis - unfolding path_def - using h assms - by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear) + with assms show ?thesis + by (metis comp_assoc id_comp linear_continuous_on linear_linear path_continuous_image) qed lemma pathstart_translation: "pathstart((\x. a + x) \ g) = a + pathstart g" @@ -110,21 +108,32 @@ lemma joinpaths_linear_image: "linear f \ (f \ g1) +++ (f \ g2) = f \ (g1 +++ g2)" by (rule ext) (simp add: joinpaths_def) +lemma loop_free_translation_eq: + fixes g :: "real \ 'a::euclidean_space" + shows "loop_free((\x. a + x) \ g) = loop_free g" + by (simp add: loop_free_def) + lemma simple_path_translation_eq: fixes g :: "real \ 'a::euclidean_space" shows "simple_path((\x. a + x) \ g) = simple_path g" - by (simp add: simple_path_def path_translation_eq) + by (simp add: simple_path_def loop_free_translation_eq path_translation_eq) + +lemma loop_free_linear_image_eq: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "linear f" "inj f" + shows "loop_free(f \ g) = loop_free g" + using assms inj_on_eq_iff [of f] by (auto simp: loop_free_def) lemma simple_path_linear_image_eq: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "linear f" "inj f" shows "simple_path(f \ g) = simple_path g" - using assms inj_on_eq_iff [of f] - by (auto simp: path_linear_image_eq simple_path_def path_translation_eq) + using assms + by (simp add: loop_free_linear_image_eq path_linear_image_eq simple_path_def) lemma arc_translation_eq: fixes g :: "real \ 'a::euclidean_space" - shows "arc((\x. a + x) \ g) = arc g" + shows "arc((\x. a + x) \ g) \ arc g" by (auto simp: arc_def inj_on_def path_translation_eq) lemma arc_linear_image_eq: @@ -161,8 +170,11 @@ lemma continuous_on_path: "path f \ t \ {0..1} \ continuous_on t f" using continuous_on_subset path_def by blast +lemma inj_on_imp_loop_free: "inj_on g {0..1} \ loop_free g" + by (simp add: inj_onD loop_free_def) + lemma arc_imp_simple_path: "arc g \ simple_path g" - by (simp add: arc_def inj_on_def simple_path_def) + by (simp add: arc_def inj_on_imp_loop_free simple_path_def) lemma arc_imp_path: "arc g \ path g" using arc_def by blast @@ -173,9 +185,11 @@ lemma simple_path_imp_path: "simple_path g \ path g" using simple_path_def by blast +lemma loop_free_cases: "loop_free g \ inj_on g {0..1} \ pathfinish g = pathstart g" + by (force simp: inj_on_def loop_free_def pathfinish_def pathstart_def) + lemma simple_path_cases: "simple_path g \ arc g \ pathfinish g = pathstart g" - unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def - by force + using arc_def loop_free_cases simple_path_def by blast lemma simple_path_imp_arc: "simple_path g \ pathfinish g \ pathstart g \ arc g" using simple_path_cases by auto @@ -250,12 +264,9 @@ lemma path_reversepath [simp]: "path (reversepath g) \ path g" proof - have *: "\g. path g \ path (reversepath g)" - unfolding path_def reversepath_def - apply (rule continuous_on_compose[unfolded o_def, of _ "\x. 1 - x"]) - apply (auto intro: continuous_intros continuous_on_subset[of "{0..1}"]) - done - show ?thesis - using "*" by force + by (metis cancel_comm_monoid_add_class.diff_cancel continuous_on_compose + continuous_on_op_minus diff_zero image_diff_atLeastAtMost path_def reversepath_o) + then show ?thesis by force qed lemma arc_reversepath: @@ -270,10 +281,12 @@ using assms by (clarsimp simp: arc_def intro!: inj_onI) (simp add: inj_onD reversepath_def **) qed +lemma loop_free_reversepath: + assumes "loop_free g" shows "loop_free(reversepath g)" + using assms by (simp add: reversepath_def loop_free_def Ball_def) (smt (verit)) + lemma simple_path_reversepath: "simple_path g \ simple_path (reversepath g)" - apply (simp add: simple_path_def) - apply (force simp: reversepath_def) - done + by (simp add: loop_free_reversepath simple_path_def) lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath @@ -362,8 +375,7 @@ by auto lemma subset_path_image_join: - assumes "path_image g1 \ s" - and "path_image g2 \ s" + assumes "path_image g1 \ s" and "path_image g2 \ s" shows "path_image (g1 +++ g2) \ s" using path_image_join_subset[of g1 g2] and assms by auto @@ -394,8 +406,7 @@ qed lemma not_in_path_image_join: - assumes "x \ path_image g1" - and "x \ path_image g2" + assumes "x \ path_image g1" and "x \ path_image g2" shows "x \ path_image (g1 +++ g2)" using assms and path_image_join_subset[of g1 g2] by auto @@ -421,8 +432,11 @@ \ t \ {0..1} \ (p +++ q) t = (p' +++ q') t" by (auto simp: joinpaths_def) +lemma loop_free_inj_on: "loop_free g \ inj_on g {0<..<1}" + by (force simp: inj_on_def loop_free_def) + lemma simple_path_inj_on: "simple_path g \ inj_on g {0<..<1}" - by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def) + using loop_free_inj_on simple_path_def by auto subsection\<^marker>\tag unimportant\\Simple paths with the endpoints removed\ @@ -435,8 +449,8 @@ using less_eq_real_def by (auto simp: path_image_def pathstart_def pathfinish_def) show "?rhs \ ?lhs" using assms - apply (auto simp: simple_path_def path_image_def pathstart_def pathfinish_def Ball_def) - using less_eq_real_def zero_le_one by blast+ + apply (simp add: image_subset_iff path_image_def pathstart_def pathfinish_def simple_path_def loop_free_def Ball_def) + by (smt (verit)) qed lemma connected_simple_path_endless: @@ -470,21 +484,16 @@ lemma continuous_on_joinpaths: assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2" shows "continuous_on {0..1} (g1 +++ g2)" -proof - - have "{0..1::real} = {0..1/2} \ {1/2..1}" - by auto - then show ?thesis - using assms by (metis path_def path_join) -qed + using assms path_def path_join by blast lemma path_join_imp: "\path g1; path g2; pathfinish g1 = pathstart g2\ \ path(g1 +++ g2)" by simp -lemma simple_path_join_loop: +lemma arc_join: assumes "arc g1" "arc g2" - "pathfinish g1 = pathstart g2" "pathfinish g2 = pathstart g1" - "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}" - shows "simple_path(g1 +++ g2)" + "pathfinish g1 = pathstart g2" + "path_image g1 \ path_image g2 \ {pathstart g2}" + shows "arc(g1 +++ g2)" proof - have injg1: "inj_on g1 {0..1}" using assms @@ -492,6 +501,32 @@ have injg2: "inj_on g2 {0..1}" using assms by (simp add: arc_def) + have g11: "g1 1 = g2 0" + and sb: "g1 ` {0..1} \ g2 ` {0..1} \ {g2 0}" + using assms + by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) + { fix x and y::real + assume xy: "g2 (2 * x - 1) = g1 (2 * y)" "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1" + then have "g1 (2 * y) = g2 0" + using sb by force + then have False + using xy inj_onD injg2 by fastforce + } note * = this + have "inj_on (g1 +++ g2) {0..1}" + using inj_onD [OF injg1] inj_onD [OF injg2] * + by (simp add: inj_on_def joinpaths_def Ball_def) (smt (verit)) + then show ?thesis + using arc_def assms path_join_imp by blast +qed + +lemma simple_path_join_loop: + assumes "arc g1" "arc g2" + "pathfinish g1 = pathstart g2" "pathfinish g2 = pathstart g1" + "path_image g1 \ path_image g2 \ {pathstart g1, pathstart g2}" + shows "simple_path(g1 +++ g2)" +proof - + have injg1: "inj_on g1 {0..1}" and injg2: "inj_on g2 {0..1}" + using assms by (auto simp add: arc_def) have g12: "g1 1 = g2 0" and g21: "g2 1 = g1 0" and sb: "g1 ` {0..1} \ g2 ` {0..1} \ {g1 0, g2 0}" @@ -516,49 +551,12 @@ using g2_eq g12 inj_onD [OF injg2] atLeastAtMost_iff xy(1) xy(4) by fastforce with xy show False by auto qed - } note * = this - { fix x and y::real - assume xy: "g1 (2 * x) = g2 (2 * y - 1)" "y \ 1" "0 \ x" "\ y * 2 \ 1" "x * 2 \ 1" - then have "x = 0 \ y = 1" - using * xy by force - } note ** = this - show ?thesis - using assms - apply (simp add: arc_def simple_path_def) - apply (auto simp: joinpaths_def split: if_split_asm - dest!: * ** dest: inj_onD [OF injg1] inj_onD [OF injg2]) - done -qed - -lemma arc_join: - assumes "arc g1" "arc g2" - "pathfinish g1 = pathstart g2" - "path_image g1 \ path_image g2 \ {pathstart g2}" - shows "arc(g1 +++ g2)" -proof - - have injg1: "inj_on g1 {0..1}" - using assms - by (simp add: arc_def) - have injg2: "inj_on g2 {0..1}" - using assms - by (simp add: arc_def) - have g11: "g1 1 = g2 0" - and sb: "g1 ` {0..1} \ g2 ` {0..1} \ {g2 0}" - using assms - by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) - { fix x and y::real - assume xy: "g2 (2 * x - 1) = g1 (2 * y)" "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1" - then have "g1 (2 * y) = g2 0" - using sb by force - then have False - using xy inj_onD injg2 by fastforce - } note * = this - show ?thesis - using assms - apply (simp add: arc_def inj_on_def) - apply (auto simp: joinpaths_def arc_imp_path split: if_split_asm - dest: * *[OF sym] inj_onD [OF injg1] inj_onD [OF injg2]) - done + } note * = this + have "loop_free(g1 +++ g2)" + using inj_onD [OF injg1] inj_onD [OF injg2] * + by (simp add: loop_free_def joinpaths_def Ball_def) (smt (verit)) + then show ?thesis + by (simp add: arc_imp_path assms simple_path_def) qed lemma reversepath_joinpaths: @@ -625,7 +623,7 @@ proof - have *: "\x y. \0 \ x; x \ 1; 0 \ y; y \ 1; (g1 +++ g2) x = (g1 +++ g2) y\ \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" - using assms by (simp add: simple_path_def) + using assms by (simp add: simple_path_def loop_free_def) have "path g1" using assms path_join simple_path_imp_path by blast moreover have "inj_on g1 {0..1}" @@ -646,7 +644,7 @@ fix x y assume "g2 x = g2 y" "0 \ x" "x \ 1" "0 \ y" "y \ 1" then show "x = y" - using * [of "(x + 1) / 2" "(y + 1) / 2"] + using * [of "(x+1) / 2" "(y+1) / 2"] by (force simp: joinpaths_def split_ifs field_split_simps) qed ultimately have "arc g2" @@ -672,19 +670,10 @@ arc g1 \ arc g2 \ path_image g1 \ path_image g2 \ {pathstart g2}" (is "?lhs = ?rhs") proof - assume ?lhs - then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path) - then have *: "\x y. \0 \ x; x \ 1; 0 \ y; y \ 1; (g1 +++ g2) x = (g1 +++ g2) y\ - \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" - using assms by (simp add: simple_path_def) - have False if "g1 0 = g2 u" "0 \ u" "u \ 1" for u - using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \?lhs\] - by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs field_split_simps) - then have n1: "pathstart g1 \ path_image g2" - unfolding pathstart_def path_image_def - using atLeastAtMost_iff by blast - show ?rhs using \?lhs\ - using \simple_path (g1 +++ g2)\ assms n1 simple_path_joinE by auto + assume ?lhs then show ?rhs + using reversepath_simps assms + by (smt (verit, ccfv_threshold) Int_commute arc_distinct_ends arc_imp_simple_path arc_reversepath + in_mono insertE pathfinish_join reversepath_joinpaths simple_path_joinE subsetI) next assume ?rhs then show ?lhs using assms @@ -694,8 +683,7 @@ lemma arc_join_eq_alt: "pathfinish g1 = pathstart g2 \ (arc(g1 +++ g2) \ - arc g1 \ arc g2 \ - path_image g1 \ path_image g2 = {pathstart g2})" + arc g1 \ arc g2 \ path_image g1 \ path_image g2 = {pathstart g2})" using pathfinish_in_path_image by (fastforce simp: arc_join_eq) @@ -791,11 +779,10 @@ assumes "path g" "u \ {0..1}" "v \ {0..1}" shows "path(subpath u v g)" proof - - have "continuous_on {0..1} (g \ (\x. ((v-u) * x+ u)))" - using assms - apply (intro continuous_intros; simp add: image_affinity_atLeastAtMost [where c=u]) - apply (auto simp: path_def continuous_on_subset) - done + have "continuous_on {u..v} g" "continuous_on {v..u} g" + using assms continuous_on_path by fastforce+ + then have "continuous_on {0..1} (g \ (\x. ((v-u) * x+ u)))" + by (intro continuous_intros; simp add: image_affinity_atLeastAtMost [where c=u]) then show ?thesis by (simp add: path_def subpath_def) qed @@ -847,7 +834,7 @@ then have p: "path (\x. g ((v - u) * x + u))" and sim: "(\x y. \x\{0..1}; y\{0..1}; g ((v - u) * x + u) = g ((v - u) * y + u)\ \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" - by (auto simp: simple_path_def subpath_def) + by (auto simp: simple_path_def loop_free_def subpath_def) { fix x y assume "x \ closed_segment u v" "y \ closed_segment u v" "g x = g y" then have "x = y \ x = u \ y = v \ x = v \ y = u" @@ -871,45 +858,13 @@ have [simp]: "\x. u + x * v = v + x * u \ u=v \ x=1" by algebra show ?lhs using psp ne - unfolding simple_path_def subpath_def + unfolding simple_path_def loop_free_def subpath_def by (fastforce simp add: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2) qed lemma arc_subpath_eq: "arc(subpath u v g) \ path(subpath u v g) \ u\v \ inj_on g (closed_segment u v)" - (is "?lhs = ?rhs") -proof - assume ?lhs - then have p: "path (\x. g ((v - u) * x + u))" - and sim: "(\x y. \x\{0..1}; y\{0..1}; g ((v - u) * x + u) = g ((v - u) * y + u)\ - \ x = y)" - by (auto simp: arc_def inj_on_def subpath_def) - { fix x y - assume "x \ closed_segment u v" "y \ closed_segment u v" "g x = g y" - then have "x = y" - using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p - by (cases "v = u") - (simp_all split: if_split_asm add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost, - simp add: field_simps) - } moreover - have "path(subpath u v g) \ u\v" - using sim [of "1/3" "2/3"] p - by (auto simp: subpath_def) - ultimately show ?rhs - unfolding inj_on_def - by metis -next - assume ?rhs - then - have d1: "\x y. \g x = g y; u \ x; x \ v; u \ y; y \ v\ \ x = y" - and d2: "\x y. \g x = g y; v \ x; x \ u; v \ y; y \ u\ \ x = y" - and ne: "u < v \ v < u" - and psp: "path (subpath u v g)" - by (auto simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost) - show ?lhs using psp ne - unfolding arc_def subpath_def inj_on_def - by (auto simp: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2) -qed + by (smt (verit, best) arc_simple_path closed_segment_commute ends_in_segment(2) inj_on_def pathfinish_subpath pathstart_subpath simple_path_subpath_eq) lemma simple_path_subpath: @@ -917,7 +872,7 @@ shows "simple_path(subpath u v g)" using assms apply (simp add: simple_path_subpath_eq simple_path_imp_path) - apply (simp add: simple_path_def closed_segment_real_eq image_affinity_atLeastAtMost, fastforce) + apply (simp add: simple_path_def loop_free_def closed_segment_real_eq image_affinity_atLeastAtMost, fastforce) done lemma arc_simple_path_subpath: @@ -930,7 +885,7 @@ lemma arc_simple_path_subpath_interior: "\simple_path g; u \ {0..1}; v \ {0..1}; u \ v; \u-v\ < 1\ \ arc(subpath u v g)" - by (force simp: simple_path_def intro: arc_simple_path_subpath) + by (force simp: simple_path_def loop_free_def intro: arc_simple_path_subpath) lemma path_image_subpath_subset: "\u \ {0..1}; v \ {0..1}\ \ path_image(subpath u v g) \ path_image g" @@ -1065,17 +1020,8 @@ assumes S: "closed S" and g: "path g" and g0: "pathstart g \ S" and g1: "pathfinish g \ S" obtains h where "path h" "pathstart h = pathstart g" "path_image h \ path_image g \ S" "pathfinish h \ frontier S" -proof - - obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \ path_image g" - "path_image h - {pathfinish h} \ interior S" - "pathfinish h \ frontier S" - using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto - show ?thesis - proof - show "path_image h \ path_image g \ S" - using assms h interior_subset [of S] by (auto simp: frontier_def) - qed (use h in auto) -qed + by (smt (verit, del_insts) Diff_iff Int_iff S closure_closed exists_path_subpath_to_frontier + frontier_def g g0 g1 interior_subset singletonD subset_eq) subsection \Shift Path to Start at Some Given Point\ @@ -1121,8 +1067,7 @@ have *: "{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto have **: "\x. x + a = 1 \ g (x + a - 1) = g (x + a)" - using assms(2)[unfolded pathfinish_def pathstart_def] - by auto + by (smt (verit, best) assms(2) pathfinish_def pathstart_def) show ?thesis unfolding path_def shiftpath_def * proof (rule continuous_on_closed_Un) @@ -1175,20 +1120,21 @@ by (auto simp: image_iff) qed +lemma loop_free_shiftpath: + assumes "loop_free g" "pathfinish g = pathstart g" and a: "0 \ a" "a \ 1" + shows "loop_free (shiftpath a g)" + unfolding loop_free_def +proof (intro conjI impI ballI) + show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" + if "x \ {0..1}" "y \ {0..1}" "shiftpath a g x = shiftpath a g y" for x y + using that a assms unfolding shiftpath_def loop_free_def + by (smt (verit, ccfv_threshold) atLeastAtMost_iff) +qed + lemma simple_path_shiftpath: assumes "simple_path g" "pathfinish g = pathstart g" and a: "0 \ a" "a \ 1" - shows "simple_path (shiftpath a g)" - unfolding simple_path_def -proof (intro conjI impI ballI) - show "path (shiftpath a g)" - by (simp add: assms path_shiftpath simple_path_imp_path) - have *: "\x y. \g x = g y; x \ {0..1}; y \ {0..1}\ \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" - using assms by (simp add: simple_path_def) - show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" - if "x \ {0..1}" "y \ {0..1}" "shiftpath a g x = shiftpath a g y" for x y - using that a unfolding shiftpath_def - by (force split: if_split_asm dest!: *) -qed + shows "simple_path (shiftpath a g)" + using assms loop_free_shiftpath path_shiftpath simple_path_def by fastforce subsection \Straight-Line Paths\ @@ -1281,14 +1227,7 @@ lemma inj_on_linepath: assumes "a \ b" shows "inj_on (linepath a b) {0..1}" -proof (clarsimp simp: inj_on_def linepath_def) - fix x y - assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b" "0 \ x" "x \ 1" "0 \ y" "y \ 1" - then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)" - by (auto simp: algebra_simps) - then show "x=y" - using assms by auto -qed + using arc_imp_inj_on arc_linepath assms by blast lemma linepath_le_1: fixes a::"'a::linordered_idom" shows "\a \ 1; b \ 1; 0 \ u; u \ 1\ \ (1 - u) * a + u * b \ 1" @@ -1303,16 +1242,11 @@ lemma linepath_in_convex_hull: fixes x::real - assumes a: "a \ convex hull S" - and b: "b \ convex hull S" - and x: "0\x" "x\1" + assumes "a \ convex hull S" + and "b \ convex hull S" + and "0\x" "x\1" shows "linepath a b x \ convex hull S" -proof - - have "linepath a b x \ closed_segment a b" - using x by (auto simp flip: linepath_image_01) - then show ?thesis - using a b convex_contains_segment by blast -qed + by (meson assms atLeastAtMost_iff convex_contains_segment convex_convex_hull linepath_in_path subset_eq) lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b" by (simp add: linepath_def) @@ -1358,12 +1292,7 @@ lemma midpoints_in_convex_hull: assumes "x \ convex hull s" "y \ convex hull s" shows "midpoint x y \ convex hull s" -proof - - have "(1 - inverse(2)) *\<^sub>R x + inverse(2) *\<^sub>R y \ convex hull s" - by (rule convexD_alt) (use assms in auto) - then show ?thesis - by (simp add: midpoint_def algebra_simps) -qed + using assms closed_segment_subset_convex_hull csegment_midpoint_subset by blast lemma not_in_interior_convex_hull_3: fixes a :: "complex" @@ -1381,27 +1310,18 @@ lemma continuous_IVT_local_extremum: fixes f :: "'a::euclidean_space \ real" assumes contf: "continuous_on (closed_segment a b) f" - and "a \ b" "f a = f b" + and ab: "a \ b" "f a = f b" obtains z where "z \ open_segment a b" "(\w \ closed_segment a b. (f w) \ (f z)) \ (\w \ closed_segment a b. (f z) \ (f w))" proof - obtain c where "c \ closed_segment a b" and c: "\y. y \ closed_segment a b \ f y \ f c" using continuous_attains_sup [of "closed_segment a b" f] contf by auto + moreover obtain d where "d \ closed_segment a b" and d: "\y. y \ closed_segment a b \ f d \ f y" using continuous_attains_inf [of "closed_segment a b" f] contf by auto - show ?thesis - proof (cases "c \ open_segment a b \ d \ open_segment a b") - case True - then show ?thesis - using c d that by blast - next - case False - then have "(c = a \ c = b) \ (d = a \ d = b)" - by (simp add: \c \ closed_segment a b\ \d \ closed_segment a b\ open_segment_def) - with \a \ b\ \f a = f b\ c d show ?thesis - by (rule_tac z = "midpoint a b" in that) (fastforce+) - qed + ultimately show ?thesis + by (smt (verit) UnE ab closed_segment_eq_open empty_iff insert_iff midpoint_in_open_segment that) qed text\An injective map into R is also an open map w.r.T. the universe, and conversely. \ @@ -1483,14 +1403,8 @@ assumes "path g" and "z \ path_image g" shows "\e>0. cball z e \ (path_image g) = {}" -proof - - obtain e where "ball z e \ path_image g = {}" "e > 0" - using not_on_path_ball[OF assms] by auto - moreover have "cball z (e/2) \ ball z e" - using \e > 0\ by auto - ultimately show ?thesis - by (rule_tac x="e/2" in exI) auto -qed + by (smt (verit, ccfv_threshold) open_ball assms centre_in_ball inf.orderE inf_assoc + inf_bot_right not_on_path_ball open_contains_cball_eq) subsection \Path component\ @@ -1538,8 +1452,7 @@ lemma path_component_linepath: fixes S :: "'a::real_normed_vector set" shows "closed_segment a b \ S \ path_component S a b" - unfolding path_component_def - by (rule_tac x="linepath a b" in exI, auto) + unfolding path_component_def by fastforce subsubsection\<^marker>\tag unimportant\ \Path components as sets\ @@ -1605,7 +1518,7 @@ assume as: "open e1" "open e2" "S \ e1 \ e2" "e1 \ e2 \ S = {}" "e1 \ S \ {}" "e2 \ S \ {}" then obtain x1 x2 where obt:"x1 \ e1 \ S" "x2 \ e2 \ S" by auto - then obtain g where g: "path g" "path_image g \ S" "pathstart g = x1" "pathfinish g = x2" + then obtain g where g: "path g" "path_image g \ S" and pg: "pathstart g = x1" "pathfinish g = x2" using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto have *: "connected {0..1::real}" by (auto intro!: convex_connected) @@ -1616,9 +1529,7 @@ unfolding subset_eq by auto moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" - using g(3,4)[unfolded path_defs] - using obt - by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) + by (smt (verit, ccfv_threshold) IntE atLeastAtMost_iff empty_iff pg mem_Collect_eq obt pathfinish_def pathstart_def) ultimately show False using *[unfolded connected_local not_ex, rule_format, of "{0..1} \ g -` e1" "{0..1} \ g -` e2"] @@ -1632,18 +1543,8 @@ assumes "open S" shows "open (path_component_set S x)" unfolding open_contains_ball -proof - fix y - assume as: "y \ path_component_set S x" - then have "y \ S" - by (simp add: path_component_mem(2)) - then obtain e where e: "e > 0" "ball y e \ S" - using assms openE by blast -have "\u. dist y u < e \ path_component S x u" - by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component) - then show "\e > 0. ball y e \ path_component_set S x" - using \e>0\ by auto -qed + by (metis assms centre_in_ball convex_ball convex_imp_path_connected equals0D openE + path_component_eq path_component_eq_empty path_component_maximal) lemma open_non_path_component: fixes S :: "'a::real_normed_vector set" @@ -1660,14 +1561,8 @@ show "\x. x \ ball y e \ x \ S" using e by blast show False if "z \ ball y e" "z \ path_component_set S x" for z - proof - - have "y \ path_component_set S z" - by (meson assms convex_ball convex_imp_path_connected e open_contains_ball_eq open_path_component path_component_maximal that(1)) - then have "y \ path_component_set S x" - using path_component_eq that(2) by blast - then show False - using y by blast - qed + by (metis (no_types, lifting) Diff_iff centre_in_ball convex_ball convex_imp_path_connected + path_component_eq path_component_maximal subsetD that y e) qed (use e in auto) qed @@ -1688,8 +1583,8 @@ by auto ultimately show False - using \y \ S\ open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] - using assms(2)[unfolded connected_def not_ex, rule_format, + using \y \ S\ open_non_path_component[OF \open S\] open_path_component[OF \open S\] + using \connected S\[unfolded connected_def not_ex, rule_format, of "path_component_set S x" "S - path_component_set S x"] by auto qed @@ -1700,16 +1595,14 @@ and "path_connected S" shows "path_connected (f ` S)" unfolding path_connected_def -proof (rule, rule) - fix x' y' - assume "x' \ f ` S" "y' \ f ` S" - then obtain x y where x: "x \ S" and y: "y \ S" and x': "x' = f x" and y': "y' = f y" - by auto - from x y obtain g where "path g \ path_image g \ S \ pathstart g = x \ pathfinish g = y" - using assms(2)[unfolded path_connected_def] by fast - then show "\g. path g \ path_image g \ f ` S \ pathstart g = x' \ pathfinish g = y'" - unfolding x' y' path_defs - by (fastforce intro: continuous_on_compose continuous_on_subset[OF contf]) +proof clarsimp + fix x y + assume x: "x \ S" and y: "y \ S" + with \path_connected S\ + show "\g. path g \ path_image g \ f ` S \ pathstart g = f x \ pathfinish g = f y" + unfolding path_defs path_connected_def + using continuous_on_subset[OF contf] + by (smt (verit, ccfv_threshold) continuous_on_compose2 image_eqI image_subset_iff) qed lemma path_connected_translationI: @@ -1759,25 +1652,9 @@ assume x: "x \ S \ T" and y: "y \ S \ T" from assms obtain z where z: "z \ S" "z \ T" by auto - show "path_component (S \ T) x y" - using x y - proof safe - assume "x \ S" "y \ S" - then show "path_component (S \ T) x y" - by (meson Un_upper1 \path_connected S\ path_component_of_subset path_connected_component) - next - assume "x \ S" "y \ T" - then show "path_component (S \ T) x y" - by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component) - next - assume "x \ T" "y \ S" - then show "path_component (S \ T) x y" - by (metis z assms(1-2) le_sup_iff order_refl path_component_of_subset path_component_trans path_connected_component) - next - assume "x \ T" "y \ T" - then show "path_component (S \ T) x y" - by (metis Un_upper1 assms(2) path_component_of_subset path_connected_component sup_commute) - qed + with x y show "path_component (S \ T) x y" + by (smt (verit) assms(1,2) in_mono mem_Collect_eq path_component_eq path_component_maximal + sup.bounded_iff sup.cobounded2 sup_ge1) qed lemma path_connected_UNION: @@ -1791,7 +1668,7 @@ then have "path_component (S i) x z" and "path_component (S j) z y" using assms by (simp_all add: path_connected_component) then have "path_component (\i\A. S i) x z" and "path_component (\i\A. S i) z y" - using *(1,3) by (auto elim!: path_component_of_subset [rotated]) + using *(1,3) by (meson SUP_upper path_component_of_subset)+ then show "path_component (\i\A. S i) x y" by (rule path_component_trans) qed @@ -1821,26 +1698,31 @@ by (meson path_component_path_image_pathstart path_component_sym path_component_trans) lemma path_connected_path_component [simp]: - "path_connected (path_component_set s x)" -proof - - { fix y z - assume pa: "path_component s x y" "path_component s x z" - then have pae: "path_component_set s x = path_component_set s y" - using path_component_eq by auto - have yz: "path_component s y z" - using pa path_component_sym path_component_trans by blast - then have "\g. path g \ path_image g \ path_component_set s x \ pathstart g = y \ pathfinish g = z" - apply (simp add: path_component_def) - by (metis pae path_component_maximal path_connected_path_image pathstart_in_path_image) - } - then show ?thesis - by (simp add: path_connected_def) + "path_connected (path_component_set S x)" +proof (clarsimp simp: path_connected_def) + fix y z + assume pa: "path_component S x y" "path_component S x z" + then have pae: "path_component_set S x = path_component_set S y" + using path_component_eq by auto + obtain g where g: "path g \ path_image g \ S \ pathstart g = y \ pathfinish g = z" + using pa path_component_sym path_component_trans path_component_def by metis + then have "path_image g \ path_component_set S x" + using pae path_component_maximal path_connected_path_image by blast + then show "\g. path g \ path_image g \ path_component_set S x \ + pathstart g = y \ pathfinish g = z" + using g by blast qed -lemma path_component: "path_component S x y \ (\t. path_connected t \ t \ S \ x \ t \ y \ t)" - apply (intro iffI) - apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image) - using path_component_of_subset path_connected_component by blast +lemma path_component: + "path_component S x y \ (\t. path_connected t \ t \ S \ x \ t \ y \ t)" + (is "?lhs = ?rhs") +proof + assume ?lhs then show ?rhs + by (metis path_component_def path_connected_path_image pathfinish_in_path_image pathstart_in_path_image) +next + assume ?rhs then show ?lhs + by (meson path_component_of_subset path_connected_component) +qed lemma path_component_path_component [simp]: "path_component_set (path_component_set S x) x = path_component_set S x" @@ -1976,9 +1858,7 @@ lemma Union_path_component [simp]: "Union {path_component_set S x |x. x \ S} = S" -apply (rule subset_antisym) -using path_component_subset apply force -using path_component_refl by auto + using path_component_subset path_component_refl by blast lemma path_component_disjoint: "disjnt (path_component_set S a) (path_component_set S b) \ @@ -2244,27 +2124,21 @@ lemma path_components_of_maximal: "\C \ path_components_of X; path_connectedin X S; ~disjnt C S\ \ S \ C" - apply (auto simp: path_components_of_def path_component_of_equiv) - using path_component_of_maximal path_connectedin_def apply fastforce - by (meson disjnt_subset2 path_component_of_disjoint path_component_of_equiv path_component_of_maximal) + by (smt (verit, ccfv_SIG) disjnt_iff imageE mem_Collect_eq path_component_of_equiv + path_component_of_maximal path_components_of_def) lemma pairwise_disjoint_path_components_of: "pairwise disjnt (path_components_of X)" by (auto simp: path_components_of_def pairwise_def path_component_of_disjoint path_component_of_equiv) lemma complement_path_components_of_Union: - "C \ path_components_of X - \ topspace X - C = \(path_components_of X - {C})" - by (metis Diff_cancel Diff_subset Union_path_components_of cSup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_path_components_of) + "C \ path_components_of X \ topspace X - C = \(path_components_of X - {C})" + by (metis Union_path_components_of bot.extremum ccpo_Sup_singleton diff_Union_pairwise_disjoint + insert_subsetI pairwise_disjoint_path_components_of) lemma nonempty_path_components_of: assumes "C \ path_components_of X" shows "C \ {}" -proof - - have "C \ path_component_of_set X ` topspace X" - using assms path_components_of_def by blast - then show ?thesis - using path_component_of_refl by fastforce -qed + by (metis assms imageE path_component_of_eq_empty path_components_of_def) lemma path_components_of_subset: "C \ path_components_of X \ C \ topspace X" by (auto simp: path_components_of_def path_component_of_equiv) @@ -2324,18 +2198,8 @@ next case False have "(path_components_of X = {S}) \ (path_connected_space X \ topspace X = S)" - proof (intro iffI conjI) - assume L: "path_components_of X = {S}" - then show "path_connected_space X" - by (simp add: path_connected_space_iff_components_eq) - show "topspace X = S" - by (metis L ccpo_Sup_singleton [of S] Union_path_components_of) - next - assume R: "path_connected_space X \ topspace X = S" - then show "path_components_of X = {S}" - using ccpo_Sup_singleton [of S] - by (metis False all_not_in_conv insert_iff mk_disjoint_insert path_component_in_path_components_of path_connected_space_iff_components_eq path_connected_space_path_component_set) - qed + by (metis False Set.set_insert ex_in_conv insert_iff path_component_in_path_components_of + path_connected_space_iff_components_eq path_connected_space_path_component_set) with False show ?thesis by (simp add: path_components_of_eq_empty subset_singleton_iff) qed @@ -2367,22 +2231,7 @@ lemma exists_path_component_of_superset: assumes S: "path_connectedin X S" and ne: "topspace X \ {}" obtains C where "C \ path_components_of X" "S \ C" -proof (cases "S = {}") - case True - then show ?thesis - using ne path_components_of_eq_empty that by fastforce -next - case False - then obtain a where "a \ S" - by blast - show ?thesis - proof - show "Collect (path_component_of X a) \ path_components_of X" - by (meson \a \ S\ S subsetD path_component_in_path_components_of path_connectedin_subset_topspace) - show "S \ Collect (path_component_of X a)" - by (simp add: S \a \ S\ path_component_of_maximal) - qed -qed + by (metis S ne ex_in_conv path_component_in_path_components_of path_component_of_maximal path_component_of_subset_topspace subset_eq that) lemma path_component_of_eq_overlap: "path_component_of X x = path_component_of X y \ @@ -2444,8 +2293,8 @@ have "Collect (path_component_of Y (f x)) \ topspace Y" by (simp add: path_component_of_subset_topspace) moreover have "g ` Collect(path_component_of Y (f x)) \ Collect (path_component_of X (g (f x)))" - using g x unfolding homeomorphic_maps_def - by (metis f homeomorphic_imp_surjective_map imageI mem_Collect_eq path_component_of_maximal path_component_of_refl path_connectedin_continuous_map_image path_connectedin_path_component_of) + using f g x unfolding homeomorphic_maps_def + by (metis image_Collect_subsetI image_eqI mem_Collect_eq path_component_of_equiv path_component_of_maximal path_connectedin_continuous_map_image path_connectedin_path_component_of) ultimately show "Collect (path_component_of Y (f x)) \ f ` Collect (path_component_of X x)" using g x unfolding homeomorphic_maps_def continuous_map_def image_iff subset_iff by metis @@ -2460,7 +2309,6 @@ lemma homeomorphic_map_path_components_of: assumes "homeomorphic_map X Y f" shows "path_components_of Y = (image f) ` (path_components_of X)" - (is "?lhs = ?rhs") unfolding path_components_of_def homeomorphic_imp_surjective_map [OF assms, symmetric] using assms homeomorphic_map_path_component_of by fastforce @@ -2527,11 +2375,11 @@ proof (cases r "0::real" rule: linorder_cases) case less then show ?thesis - by (simp) + by simp next case equal then show ?thesis - by (simp) + by simp next case greater then have eq: "(sphere (0::'a) r) = (\x. (r / norm x) *\<^sub>R x) ` (- {0::'a})" @@ -2712,10 +2560,13 @@ case empty show ?case using \connected S\ by simp next - case (insert x F) - then have "connected (S-F)" by auto - moreover have "open (S - F)" using finite_imp_closed[OF \finite F\] \open S\ by auto - ultimately have "connected (S - F - {x})" using connected_open_delete[OF _ _ 2] by auto + case (insert x T) + then have "connected (S-T)" + by auto + moreover have "open (S - T)" + using finite_imp_closed[OF \finite T\] \open S\ by auto + ultimately have "connected (S - T - {x})" + using connected_open_delete[OF _ _ 2] by auto thus ?case by (metis Diff_insert) qed @@ -2755,13 +2606,8 @@ fixes a :: "'a :: euclidean_space" assumes "DIM('a) = 1" and "r > 0" obtains x y where "sphere a r = {x,y} \ dist x y = 2*r" -proof - - have "sphere a r = (+) a ` sphere 0 r" - by (metis add.right_neutral sphere_translation) - then show ?thesis - using sphere_1D_doubleton_zero [OF assms] - by (metis (mono_tags, lifting) dist_add_cancel image_empty image_insert that) -qed + using sphere_1D_doubleton_zero [OF assms] dist_add_cancel image_empty image_insert + by (metis (no_types, opaque_lifting) add.right_neutral sphere_translation) lemma psubset_sphere_Compl_connected: fixes S :: "'a::euclidean_space set" @@ -2779,8 +2625,7 @@ moreover have "connected {x. dist a x \ r \ x \ S}" using assms by (force intro: connected_intermediate_closure [of "ball a r"]) - moreover - have "connected {x. r \ dist a x \ x \ S}" + moreover have "connected {x. r \ dist a x \ x \ S}" proof (rule connected_intermediate_closure [of "- cball a r"]) show "{x. r \ dist a x \ x \ S} \ closure (- cball a r)" using interior_closure by (force intro: connected_complement_bounded_convex) @@ -2871,12 +2716,8 @@ assumes x: "x \ S" and S: "open S" shows "x \ closure (connected_component_set S y) \ x \ connected_component_set S y" proof - - { assume "x \ closure (connected_component_set S y)" - moreover have "x \ connected_component_set S x" - using x by simp - ultimately have "x \ connected_component_set S y" - using S by (meson Compl_disjoint closure_iff_nhds_not_empty connected_component_disjoint disjoint_eq_subset_Compl open_connected_component) - } + have "x islimpt connected_component_set S y \ connected_component S y x" + by (metis (no_types, lifting) S connected_component_eq connected_component_refl islimptE mem_Collect_eq open_connected_component x) then show ?thesis by (auto simp: closure_def) qed @@ -2902,10 +2743,8 @@ from connectedD [OF \connected S\ 1 2 4 3] have "S \ \(B-{T}) = {}" by (auto simp: Int_commute \S \ T \ {}\) - with \T \ B\ have "S \ T" - using "3" by auto - show ?thesis - using \S \ \(B - {T}) = {}\ \S \ T\ \T \ B\ that by auto + with \T \ B\ 3 that show ?thesis + by (metis IntI UnE empty_iff subsetD subsetI) qed lemma connected_disjoint_Union_open_subset: @@ -2934,7 +2773,7 @@ and SB: "\S. S \ B \ open S \ connected S \ S \ {}" and eq [simp]: "\A = \B" shows "A = B" -by (rule subset_antisym; metis connected_disjoint_Union_open_subset assms) +by (metis subset_antisym connected_disjoint_Union_open_subset assms) proposition components_open_unique: fixes S :: "'a::real_normed_vector set" @@ -2997,11 +2836,9 @@ then have *: "\x. B \ norm x \ x \ S" by (force simp: ball_def dist_norm) obtain x' where x': "connected_component S x x'" "norm x' > B" - using bo [unfolded bounded_def dist_norm, simplified, rule_format] - by (metis diff_zero norm_minus_commute not_less) + using B(1) bo(1) bounded_pos by force obtain y' where y': "connected_component S y y'" "norm y' > B" - using bo [unfolded bounded_def dist_norm, simplified, rule_format] - by (metis diff_zero norm_minus_commute not_less) + using B(1) bo(2) bounded_pos by force have x'y': "connected_component S x' y'" unfolding connected_component_def proof (intro exI conjI) @@ -3009,11 +2846,8 @@ using assms by (auto intro: connected_complement_bounded_convex) qed (use x' y' dist_norm * in auto) show ?thesis - proof (rule connected_component_eq) - show "x \ connected_component_set S y" using x' y' x'y' - by (metis (no_types) connected_component_eq_eq connected_component_in mem_Collect_eq) - qed + by (metis connected_component_eq mem_Collect_eq) qed lemma cobounded_unbounded_components: @@ -3087,12 +2921,8 @@ fixes u::real assumes "x \ B" "y \ B" "0 \ u" "u \ 1" shows "(1 - u) * x + u * y \ B" -proof - - obtain dx dy where "dx \ 0" "dy \ 0" "x = B + dx" "y = B + dy" - using assms by auto (metis add.commute diff_add_cancel) - with \0 \ u\ \u \ 1\ show ?thesis - by (simp add: add_increasing2 mult_left_le field_simps) -qed + by (smt (verit) assms convex_bound_le ge_iff_diff_ge_0 minus_add_distrib + mult_minus_right neg_le_iff_le) lemma cobounded_outside: fixes S :: "'a :: real_normed_vector set" @@ -3150,7 +2980,7 @@ lemma connected_outside: fixes S :: "'a::euclidean_space set" assumes "bounded S" "2 \ DIM('a)" - shows "connected(outside S)" + shows "connected(outside S)" apply (clarsimp simp add: connected_iff_connected_component outside) apply (rule_tac S="connected_component_set (- S) x" in connected_component_of_subset) apply (metis (no_types) assms cobounded_unbounded_component cobounded_unique_unbounded_component connected_component_eq_eq connected_component_idemp double_complement mem_Collect_eq) @@ -3158,9 +2988,14 @@ lemma outside_connected_component_lt: "outside S = {x. \B. \y. B < norm(y) \ connected_component (- S) x y}" - apply (auto simp: outside bounded_def dist_norm) - apply (metis diff_0 norm_minus_cancel not_less) - by (metis less_diff_eq norm_minus_commute norm_triangle_ineq2 order.trans pinf(6)) +proof - + have "\x B. x \ outside S \ \y. B < norm y \ connected_component (- S) x y" + by (metis boundedI linorder_not_less mem_Collect_eq outside) + moreover + have "\x. \B. \y. B < norm y \ connected_component (- S) x y \ x \ outside S" + by (metis bounded_pos linorder_not_less mem_Collect_eq outside) + ultimately show ?thesis by auto +qed lemma outside_connected_component_le: "outside S = {x. \B. \y. B \ norm(y) \ connected_component (- S) x y}" @@ -3174,14 +3009,15 @@ proof - obtain B::real where B: "0 < B" and Bno: "\x. x \ S \ norm x \ B" using S [simplified bounded_pos] by auto - { fix y::'a and z::'a - assume yz: "B < norm z" "B < norm y" + have cyz: "connected_component (- S) y z" + if yz: "B < norm z" "B < norm y" for y::'a and z::'a + proof - have "connected_component (- cball 0 B) y z" using assms yz by (force simp: dist_norm intro: connected_componentI [OF _ subset_refl] connected_complement_bounded_convex) - then have "connected_component (- S) y z" + then show ?thesis by (metis connected_component_of_subset Bno Compl_anti_mono mem_cball_0 subset_iff) - } note cyz = this + qed show ?thesis apply (auto simp: outside bounded_pos) apply (metis Compl_iff bounded_iff cobounded_imp_unbounded mem_Collect_eq not_le) @@ -3210,9 +3046,8 @@ lemma inside_subset: assumes "connected U" and "\ bounded U" and "T \ U = - S" shows "inside S \ T" - apply (auto simp: inside_def) - by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal - Compl_iff Un_iff assms subsetI) + using bounded_subset [of "connected_component_set (- S) _" U] assms + by (metis (no_types, lifting) ComplI Un_iff connected_component_maximal inside_def mem_Collect_eq subsetI) lemma frontier_not_empty: fixes S :: "'a :: real_normed_vector set" @@ -3263,23 +3098,12 @@ by (metis Diff_iff Sup_upper closure_subset contra_subsetD dist_self frontier_def interior_mono) next case False - have 1: "closed_segment x y \ T \ {}" - using \y \ T\ by blast - have 2: "closed_segment x y - T \ {}" - using False by blast + have \
: "closed_segment x y \ T \ {}" "closed_segment x y - T \ {}" + using \y \ T\ False by blast+ obtain c where "c \ closed_segment x y" "c \ frontier T" - using False connected_Int_frontier [OF connected_segment 1 2] by auto - then show ?thesis - proof - - have "norm (y - x) < e" - by (metis dist_norm \dist y x < e\) - moreover have "norm (c - x) \ norm (y - x)" - by (simp add: \c \ closed_segment x y\ segment_bound(1)) - ultimately have "norm (c - x) < e" - by linarith - then show ?thesis - by (metis (no_types) \c \ frontier T\ dist_norm that(1)) - qed + using False connected_Int_frontier [OF connected_segment \
] by auto + with that show ?thesis + by (smt (verit) dist_norm segment_bound1) qed then show ?thesis by (fastforce simp add: frontier_def closure_approachable) @@ -3288,8 +3112,7 @@ lemma frontier_Union_subset: fixes F :: "'a::real_normed_vector set set" shows "finite F \ frontier(\F) \ (\t \ F. frontier t)" -by (rule order_trans [OF frontier_Union_subset_closure]) - (auto simp: closure_subset_eq) + by (metis closed_UN closure_closed frontier_Union_subset_closure frontier_closed) lemma frontier_of_components_subset: fixes S :: "'a::real_normed_vector set" @@ -3328,7 +3151,7 @@ show "- frontier C \ C \ - closure C" by (simp add: \open C\ closed_Compl frontier_closures) then show "- closure C \ - frontier C \ {}" - by (metis (no_types, lifting) C Compl_subset_Compl_iff \frontier C \ S\ compl_sup frontier_closures in_components_subset psubsetE sup.absorb_iff2 sup.boundedE sup_bot.right_neutral sup_inf_absorb) + by (metis C Compl_Diff_eq Un_Int_eq(4) Un_commute \frontier C \ S\ \open C\ compl_le_compl_iff frontier_def in_components_subset interior_eq leD sup_bot.right_neutral) qed then show False using \connected (- frontier C)\ by blast @@ -3367,10 +3190,8 @@ using connected_component_in by auto } then show ?thesis - apply (auto simp: inside_def frontier_def) - apply (rule classical) - apply (rule bounded_subset [OF assms], blast) - done + using bounded_subset [OF assms] + by (metis (no_types, lifting) Diff_iff frontier_def inside_def mem_Collect_eq subsetI) qed lemma inside_empty [simp]: "inside {} = ({} :: 'a :: {real_normed_vector, perfect_space} set)" @@ -3482,17 +3303,7 @@ fixes S :: "'a::real_normed_vector set" assumes "bounded S" shows "outside(frontier S) \ - closure S" - unfolding outside_inside boolean_algebra_class.compl_le_compl_iff -proof - - { assume "interior S \ inside (frontier S)" - hence "interior S \ inside (frontier S) = inside (frontier S)" - by (simp add: subset_Un_eq) - then have "closure S \ frontier S \ inside (frontier S)" - using frontier_def by auto - } - then show "closure S \ frontier S \ inside (frontier S)" - using interior_inside_frontier [OF assms] by blast -qed + using assms frontier_def interior_inside_frontier outside_inside by fastforce lemma outside_frontier_eq_complement_closure: fixes S :: "'a :: {real_normed_vector, perfect_space} set" @@ -3556,18 +3367,7 @@ fixes S :: "'a::real_normed_vector set" assumes "closed S" shows "frontier(inside S) \ S" -proof - - have "closure (inside S) \ - inside S = closure (inside S) - interior (inside S)" - by (metis (no_types) Diff_Compl assms closure_closed interior_closure open_closed open_inside) - moreover have "- inside S \ - outside S = S" - by (metis (no_types) compl_sup double_compl inside_Un_outside) - moreover have "closure (inside S) \ - outside S" - by (metis (no_types) assms closure_inside_subset union_with_inside) - ultimately have "closure (inside S) - interior (inside S) \ S" - by blast - then show ?thesis - by (simp add: frontier_def open_inside interior_open) -qed + using assms closure_inside_subset frontier_closures frontier_disjoint_eq open_inside by fastforce lemma closure_outside_subset: fixes S :: "'a::real_normed_vector set" @@ -3623,10 +3423,8 @@ lemma outside_bounded_nonempty: fixes S :: "'a :: {real_normed_vector, perfect_space} set" - assumes "bounded S" shows "outside S \ {}" - by (metis (no_types, lifting) Collect_empty_eq Collect_mem_eq Compl_eq_Diff_UNIV Diff_cancel - Diff_disjoint UNIV_I assms ball_eq_empty bounded_diff cobounded_outside convex_ball - double_complement order_refl outside_convex outside_def) + assumes "bounded S" shows "outside S \ {}" + using assms unbounded_outside by force lemma outside_compact_in_open: fixes S :: "'a :: {real_normed_vector,perfect_space} set" @@ -3700,14 +3498,7 @@ then obtain r where "0 < r" and r: "S \ T \ ball 0 r" using bounded_subset_ballD by blast have outst: "outside S \ outside T \ {}" - proof - - have "- ball 0 r \ outside S" - by (meson convex_ball le_supE outside_subset_convex r) - moreover have "- ball 0 r \ outside T" - by (meson convex_ball le_supE outside_subset_convex r) - ultimately show ?thesis - by (metis Compl_subset_Compl_iff Int_subset_iff bounded_ball inf.orderE outside_bounded_nonempty outside_no_overlap) - qed + by (metis bounded_Un bounded_subset bst cobounded_outside disjoint_eq_subset_Compl unbounded_outside) have "S \ T = {}" using assms by (metis disjoint_iff_not_equal inside_no_overlap subsetCE) moreover have "outside S \ inside T \ {}" @@ -3734,27 +3525,29 @@ using that proof assume "a \ S" then show ?thesis - by (rule_tac x=a in exI, rule_tac x="{a}" in exI, simp) + using cons by blast next assume a: "a \ inside S" then have ain: "a \ closure (inside S)" by (simp add: closure_def) - show ?thesis - apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "inside S"]) - apply (simp_all add: ain b) - subgoal for h - apply (rule_tac x="pathfinish h" in exI) - apply (simp add: subsetD [OF frontier_inside_subset[OF S]]) - apply (rule_tac x="path_image h" in exI) - apply (simp add: pathfinish_in_path_image connected_path_image, auto) - by (metis Diff_single_insert S frontier_inside_subset insert_iff interior_subset subsetD) - done + obtain h where h: "path h" "pathstart h = a" + "path_image h - {pathfinish h} \ interior (inside S)" + "pathfinish h \ frontier (inside S)" + using ain b + by (metis exists_path_subpath_to_frontier path_linepath pathfinish_linepath pathstart_linepath) + moreover + have h1S: "pathfinish h \ S" + using S h frontier_inside_subset by blast + moreover + have "path_image h \ S \ inside S" + using IntD1 S h1S h interior_eq open_inside by fastforce + ultimately show ?thesis by blast qed show ?thesis apply (simp add: connected_iff_connected_component) apply (clarsimp simp add: connected_component_def dest!: *) subgoal for x y u u' T t' - by (rule_tac x="(S \ T \ t')" in exI) (auto intro!: connected_Un cons) + by (rule_tac x = "S \ T \ t'" in exI) (auto intro!: connected_Un cons) done qed @@ -3776,16 +3569,19 @@ assume a: "a \ outside S" then have ain: "a \ closure (outside S)" by (simp add: closure_def) - show ?thesis - apply (rule exists_path_subpath_to_frontier [OF path_linepath [of a b], of "outside S"]) - apply (simp_all add: ain b) - subgoal for h - apply (rule_tac x="pathfinish h" in exI) - apply (simp add: subsetD [OF frontier_outside_subset[OF S]]) - apply (rule_tac x="path_image h" in exI) - apply (simp add: pathfinish_in_path_image connected_path_image, auto) - by (metis (no_types, lifting) frontier_outside_subset insertE insert_Diff interior_eq open_outside pathfinish_in_path_image S subsetCE) - done + obtain h where h: "path h" "pathstart h = a" + "path_image h - {pathfinish h} \ interior (outside S)" + "pathfinish h \ frontier (outside S)" + using ain b + by (metis exists_path_subpath_to_frontier path_linepath pathfinish_linepath pathstart_linepath) + moreover + have h1S: "pathfinish h \ S" + using S frontier_outside_subset h(4) by blast + moreover + have "path_image h \ S \ outside S" + using IntD1 S h1S h interior_eq open_outside by fastforce + ultimately show ?thesis + by blast qed show ?thesis apply (simp add: connected_iff_connected_component) @@ -3798,9 +3594,13 @@ lemma inside_inside_eq_empty [simp]: fixes S :: "'a :: {real_normed_vector, perfect_space} set" assumes S: "closed S" and cons: "connected S" - shows "inside (inside S) = {}" - by (metis (no_types) unbounded_outside connected_with_outside [OF assms] bounded_Un - inside_complement_unbounded_connected_empty unbounded_outside union_with_outside) + shows "inside (inside S) = {}" +proof - + have "connected (- inside S)" + by (metis S connected_with_outside cons union_with_outside) + then show ?thesis + by (metis bounded_Un inside_complement_unbounded_connected_empty unbounded_outside union_with_outside) +qed lemma inside_in_components: "inside S \ components (- S) \ connected(inside S) \ inside S \ {}" (is "?lhs = ?rhs") @@ -3828,9 +3628,10 @@ lemma bounded_unique_outside: fixes S :: "'a :: euclidean_space set" assumes "bounded S" "DIM('a) \ 2" - shows "(c \ components (- S) \ \ bounded c \ c = outside S)" + shows "(c \ components (- S) \ \ bounded c) \ c = outside S" using assms - by (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside) + by (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty + outside_in_components unbounded_outside) subsection\Condition for an open map's image to contain a ball\ @@ -3868,21 +3669,20 @@ then have "(\ \ K) \ f y" by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially) with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto - have rle: "r \ norm (f y - f a)" + have "r \ norm (f y - f a)" proof (rule le_no) show "y \ frontier S" using w wy oint by (force simp: imageI image_mono interiorI interior_subset frontier_def y) qed - have **: "(b \ (- S) \ {} \ b - (- S) \ {} \ b \ f \ {}) - \ (b \ S \ {}) \ b \ f = {} \ b \ S" - for b f and S :: "'b set" - by blast - have \
: "\y. \norm (f a - y) < r; y \ frontier (f ` S)\ \ False" - by (metis dw_le norm_minus_commute not_less order_trans rle wy) - show ?thesis - apply (rule ** [OF connected_Int_frontier [where t = "f`S", OF connected_ball]]) - (*such a horrible mess*) - using \a \ S\ \0 < r\ by (auto simp: disjoint_iff_not_equal dist_norm dest: \
) + then have "\y. \norm (f a - y) < r; y \ frontier (f ` S)\ \ False" + by (metis dw_le norm_minus_commute not_less order_trans wy) + then have "ball (f a) r \ frontier (f ` S) = {}" + by (metis disjoint_iff_not_equal dist_norm mem_ball) + moreover + have "ball (f a) r \ f ` S \ {}" + using \a \ S\ \0 < r\ centre_in_ball by blast + ultimately show ?thesis + by (meson connected_Int_frontier connected_ball diff_shunt_var) qed @@ -3891,8 +3691,7 @@ lemma Hausdorff_space_euclidean [simp]: "Hausdorff_space (euclidean :: 'a::metric_space topology)" proof - have "\U V. open U \ open V \ x \ U \ y \ V \ disjnt U V" - if "x \ y" - for x y :: 'a + if "x \ y" for x y :: 'a proof (intro exI conjI) let ?r = "dist x y / 2" have [simp]: "?r > 0" @@ -4139,7 +3938,6 @@ lemma path_image_rectpath_cbox_minus_box: assumes "Re a \ Re b" "Im a \ Im b" shows "path_image (rectpath a b) = cbox a b - box a b" - using assms by (auto simp: path_image_rectpath in_cbox_complex_iff - in_box_complex_iff) + using assms by (auto simp: path_image_rectpath in_cbox_complex_iff in_box_complex_iff) end