: "g2 u \ (\x. g2 (2 * x - 1)) ` ({0..1} \ {x. \ x * 2 \ 1})" + if "0 < u" "u \ 1" for u + using that assms + by (rule_tac x="(u+1)/2" in image_eqI) (auto simp: field_simps pathfinish_def pathstart_def) + have "g2 0 \ (\x. g1 (2 * x)) ` ({0..1} \ {x. x * 2 \ 1})" + using assms + by (rule_tac x="1/2" in image_eqI) (auto simp: pathfinish_def pathstart_def) + then have "path_image g2 \ path_image (g1 +++ g2)" + by (auto simp: path_image_def joinpaths_def intro!: \

) + ultimately show ?thesis + using path_image_join_subset by blast +qed lemma not_in_path_image_join: assumes "x \ path_image g1" @@ -396,20 +407,28 @@ subsection\<^marker>\tag unimportant\\Simple paths with the endpoints removed\ lemma simple_path_endless: - "simple_path c \ path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}" - apply (auto simp: simple_path_def path_image_def pathstart_def pathfinish_def Ball_def Bex_def image_def) - apply (metis eq_iff le_less_linear) - apply (metis leD linear) - using less_eq_real_def zero_le_one apply blast - using less_eq_real_def zero_le_one apply blast - done + assumes "simple_path c" + shows "path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}" (is "?lhs = ?rhs") +proof + show "?lhs \ ?rhs" + 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+ +qed lemma connected_simple_path_endless: - "simple_path c \ connected(path_image c - {pathstart c,pathfinish c})" -apply (simp add: simple_path_endless) -apply (rule connected_continuous_image) -apply (meson continuous_on_subset greaterThanLessThan_subseteq_atLeastAtMost_iff le_numeral_extra(3) le_numeral_extra(4) path_def simple_path_imp_path) -by auto + assumes "simple_path c" + shows "connected(path_image c - {pathstart c,pathfinish c})" +proof - + have "continuous_on {0<..<1} c" + using assms by (simp add: simple_path_def continuous_on_path path_def subset_iff) + then have "connected (c ` {0<..<1})" + using connected_Ioo connected_continuous_image by blast + then show ?thesis + using assms by (simp add: simple_path_endless) +qed lemma nonempty_simple_path_endless: "simple_path c \ path_image c - {pathstart c,pathfinish c} \ {}" @@ -419,13 +438,10 @@ subsection\<^marker>\tag unimportant\\The operations on paths\ lemma path_image_subset_reversepath: "path_image(reversepath g) \ path_image g" - by (auto simp: path_image_def reversepath_def) + by simp lemma path_imp_reversepath: "path g \ path(reversepath g)" - apply (auto simp: path_def reversepath_def) - using continuous_on_compose [of "{0..1}" "\x. 1 - x" g] - apply (auto simp: continuous_on_op_minus) - done + by simp lemma half_bounded_equal: "1 \ x * 2 \ x * 2 \ 1 \ x = (1/2::real)" by simp @@ -434,32 +450,14 @@ 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}" + have "{0..1::real} = {0..1/2} \ {1/2..1}" by auto - have gg: "g2 0 = g1 1" - by (metis assms(3) pathfinish_def pathstart_def) - have 1: "continuous_on {0..1/2} (g1 +++ g2)" - apply (rule continuous_on_eq [of _ "g1 \ (\x. 2*x)"]) - apply (rule continuous_intros | simp add: joinpaths_def assms)+ - done - have "continuous_on {1/2..1} (g2 \ (\x. 2*x-1))" - apply (rule continuous_on_subset [of "{1/2..1}"]) - apply (rule continuous_intros | simp add: image_affinity_atLeastAtMost_diff assms)+ - done - then have 2: "continuous_on {1/2..1} (g1 +++ g2)" - apply (rule continuous_on_eq [of "{1/2..1}" "g2 \ (\x. 2*x-1)"]) - apply (rule assms continuous_intros | simp add: joinpaths_def mult.commute half_bounded_equal gg)+ - done - show ?thesis - apply (subst *) - apply (rule continuous_on_closed_Un) - using 1 2 - apply auto - done + then show ?thesis + using assms by (metis path_def path_join) qed lemma path_join_imp: "\path g1; path g2; pathfinish g1 = pathstart g2\ \ path(g1 +++ g2)" - by (simp) + by simp lemma simple_path_join_loop: assumes "arc g1" "arc g2" @@ -479,44 +477,35 @@ using assms by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) { fix x and y::real - assume xyI: "x = 1 \ y \ 0" - and xy: "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1" "g2 (2 * x - 1) = g1 (2 * y)" - have g1im: "g1 (2 * y) \ g1 ` {0..1} \ g2 ` {0..1}" - using xy - apply simp - apply (rule_tac x="2 * x - 1" in image_eqI, auto) - done - have False - using subsetD [OF sb g1im] xy - apply auto - apply (drule inj_onD [OF injg1]) - using g21 [symmetric] xyI - apply (auto dest: inj_onD [OF injg2]) - done - } note * = this + assume g2_eq: "g2 (2 * x - 1) = g1 (2 * y)" + and xyI: "x \ 1 \ y \ 0" + and xy: "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1" + then consider "g1 (2 * y) = g1 0" | "g1 (2 * y) = g2 0" + using sb by force + then have False + proof cases + case 1 + then have "y = 0" + using xy g2_eq by (auto dest!: inj_onD [OF injg1]) + then show ?thesis + using xy g2_eq xyI by (auto dest: inj_onD [OF injg2] simp flip: g21) + next + case 2 + then have "2*x = 1" + 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: "y \ 1" "0 \ x" "\ y * 2 \ 1" "x * 2 \ 1" "g1 (2 * x) = g2 (2 * y - 1)" - have g1im: "g1 (2 * x) \ g1 ` {0..1} \ g2 ` {0..1}" - using xy - apply simp - apply (rule_tac x="2 * x" in image_eqI, auto) - done - have "x = 0 \ y = 1" - using subsetD [OF sb g1im] xy - apply auto - apply (force dest: inj_onD [OF injg1]) - using g21 [symmetric] - apply (auto dest: inj_onD [OF injg2]) - done + 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, clarify) - apply (simp add: joinpaths_def split: if_split_asm) - apply (force dest: inj_onD [OF injg1]) - apply (metis *) - apply (metis **) - apply (force dest: inj_onD [OF injg2]) + 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 @@ -537,24 +526,17 @@ using assms by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) { fix x and y::real - assume xy: "x \ 1" "0 \ y" " y * 2 \ 1" "\ x * 2 \ 1" "g2 (2 * x - 1) = g1 (2 * y)" - have g1im: "g1 (2 * y) \ g1 ` {0..1} \ g2 ` {0..1}" - using xy - apply simp - apply (rule_tac x="2 * x - 1" in image_eqI, auto) - done - have False - using subsetD [OF sb g1im] xy - by (auto dest: inj_onD [OF injg2]) + 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 (clarsimp simp add: arc_imp_path assms) - apply (simp add: joinpaths_def split: if_split_asm) - apply (force dest: inj_onD [OF injg1]) - apply (metis *) - apply (metis *) - apply (force dest: inj_onD [OF injg2]) + apply (auto simp: joinpaths_def arc_imp_path split: if_split_asm + dest: * *[OF sym] inj_onD [OF injg1] inj_onD [OF injg2]) done qed @@ -577,18 +559,18 @@ by auto then have "e > 0" by (metis e_def pathfinish_def pathstart_def) + then have "\e>0. \d>0. \x'\{0..1}. dist x' 0 < d \ dist (g2 x') (g2 0) < e" + using \path g2\ atLeastAtMost_iff zero_le_one unfolding path_def continuous_on_iff + by blast then obtain d1 where "d1 > 0" and d1: "\x'. \x'\{0..1}; norm x' < d1\ \ dist (g2 x') (g2 0) < e/2" - using assms(2) unfolding path_def continuous_on_iff - apply (drule_tac x=0 in bspec, simp) - by (metis half_gt_zero_iff norm_conv_dist) + by (metis \0 < e\ half_gt_zero_iff norm_conv_dist) obtain d2 where "d2 > 0" and d2: "\x'. \x'\{0..1}; dist x' (1/2) < d2\ \ dist ((g1 +++ g2) x') (g1 1) < e/2" using assms(1) \e > 0\ unfolding path_def continuous_on_iff apply (drule_tac x="1/2" in bspec, simp) - apply (drule_tac x="e/2" in spec) - apply (force simp: joinpaths_def) + apply (drule_tac x="e/2" in spec, force simp: joinpaths_def) done have int01_1: "min (1/2) (min d1 d2) / 2 \ {0..1}" using \d1 > 0\ \d2 > 0\ by (simp add: min_def) @@ -681,8 +663,7 @@ unfolding pathstart_def path_image_def using atLeastAtMost_iff by blast show ?rhs using \?lhs\ - apply (rule simple_path_joinE [OF arc_imp_simple_path assms]) - using n1 by force + using \simple_path (g1 +++ g2)\ assms n1 simple_path_joinE by auto next assume ?rhs then show ?lhs using assms @@ -790,9 +771,8 @@ shows "path(subpath u v g)" proof - have "continuous_on {0..1} (g \ (\x. ((v-u) * x+ u)))" - apply (rule continuous_intros | simp)+ - apply (simp add: image_affinity_atLeastAtMost [where c=u]) using assms + apply (intro continuous_intros; simp add: image_affinity_atLeastAtMost [where c=u]) apply (auto simp: path_def continuous_on_subset) done then show ?thesis @@ -841,7 +821,7 @@ (\x y. x \ closed_segment u v \ y \ closed_segment u v \ g x = g y \ x = y \ x = u \ y = v \ x = v \ y = u)" (is "?lhs = ?rhs") -proof (rule iffI) +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)\ @@ -877,7 +857,7 @@ 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 (rule iffI) +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)\ @@ -929,15 +909,11 @@ 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)" - apply (rule arc_simple_path_subpath) - apply (force simp: simple_path_def)+ - done + by (force simp: simple_path_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" - apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath) - apply (auto simp: path_image_def) - done + by (metis atLeastAtMost_iff atLeastatMost_subset_iff path_image_def path_image_subpath subset_image_iff) lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p" by (rule ext) (simp add: joinpaths_def subpath_def field_split_simps) @@ -952,11 +928,13 @@ "\x. 0 \ x \ x < u \ g x \ interior S" "(g u \ interior S)" "(u = 0 \ g u \ closure S)" proof - - have gcon: "continuous_on {0..1} g" using g by (simp add: path_def) - then have com: "compact ({0..1} \ {u. g u \ closure (- S)})" - apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def]) - using compact_eq_bounded_closed apply fastforce - done + have gcon: "continuous_on {0..1} g" + using g by (simp add: path_def) + moreover have "bounded ({u. g u \ closure (- S)} \ {0..1})" + using compact_eq_bounded_closed by fastforce + ultimately have com: "compact ({0..1} \ {u. g u \ closure (- S)})" + using closed_vimage_Int + by (metis (full_types) Int_commute closed_atLeastAtMost closed_closure compact_eq_bounded_closed vimage_def) have "1 \ {u. g u \ closure (- S)}" using assms by (simp add: pathfinish_def closure_def) then have dis: "{0..1} \ {u. g u \ closure (- S)} \ {}" @@ -966,8 +944,9 @@ using compact_attains_inf [OF com dis] by fastforce then have umin': "\t. \0 \ t; t \ 1; t < u\ \ g t \ S" using closure_def by fastforce - { assume "u \ 0" - then have "u > 0" using \0 \ u\ by auto + have \

: "g u \ closure S" if "u \ 0" + proof - + have "u > 0" using that \0 \ u\ by auto { fix e::real assume "e > 0" obtain d where "d>0" and d: "\x'. \x' \ {0..1}; dist x' u \ d\ \ dist (g x') (g u) < e" using continuous_onE [OF gcon _ \e > 0\] \0 \ _\ \_ \ 1\ atLeastAtMost_iff by auto @@ -977,14 +956,16 @@ using \0 < u\ \u \ 1\ \d > 0\ by (force intro: d [OF _ *] umin') } - then have "g u \ closure S" + then show ?thesis by (simp add: frontier_def closure_approachable) - } - then show ?thesis - apply (rule_tac u=u in that) - apply (auto simp: \0 \ u\ \u \ 1\ gu interior_closure umin) - using \_ \ 1\ interior_closure umin apply fastforce - done + qed + show ?thesis + proof + show "\x. 0 \ x \ x < u \ g x \ interior S" + using \u \ 1\ interior_closure umin by fastforce + show "g u \ interior S" + by (simp add: gu interior_closure) + qed (use \0 \ u\ \u \ 1\ \

in auto) qed lemma subpath_to_frontier_strong: @@ -997,30 +978,47 @@ and gunot: "(g u \ interior S)" and u0: "(u = 0 \ g u \ closure S)" using subpath_to_frontier_explicit [OF assms] by blast show ?thesis - apply (rule that [OF \0 \ u\ \u \ 1\]) - apply (simp add: gunot) - using \0 \ u\ u0 by (force simp: subpath_def gxin) + proof + show "g u \ interior S" + using gunot by blast + qed (use \0 \ u\ \u \ 1\ u0 in \(force simp: subpath_def gxin)+\) qed lemma subpath_to_frontier: assumes g: "path g" and g0: "pathstart g \ closure S" and g1: "pathfinish g \ S" - obtains u where "0 \ u" "u \ 1" "g u \ frontier S" "(path_image(subpath 0 u g) - {g u}) \ interior S" + obtains u where "0 \ u" "u \ 1" "g u \ frontier S" "path_image(subpath 0 u g) - {g u} \ interior S" proof - obtain u where "0 \ u" "u \ 1" and notin: "g u \ interior S" and disj: "u = 0 \ (\x. 0 \ x \ x < 1 \ subpath 0 u g x \ interior S) \ g u \ closure S" + (is "_ \ ?P") using subpath_to_frontier_strong [OF g g1] by blast show ?thesis - apply (rule that [OF \0 \ u\ \u \ 1\]) - apply (metis DiffI disj frontier_def g0 notin pathstart_def) - using \0 \ u\ g0 disj - apply (simp add: path_image_subpath_gen) - apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def) - apply (rename_tac y) - apply (drule_tac x="y/u" in spec) - apply (auto split: if_split_asm) - done + proof + show "g u \ frontier S" + by (metis DiffI disj frontier_def g0 notin pathstart_def) + show "path_image (subpath 0 u g) - {g u} \ interior S" + using disj + proof + assume "u = 0" + then show ?thesis + by (simp add: path_image_subpath) + next + assume P: ?P + show ?thesis + proof (clarsimp simp add: path_image_subpath_gen) + fix y + assume y: "y \ closed_segment 0 u" "g y \ interior S" + with \0 \ u\ have "0 \ y" "y \ u" + by (auto simp: closed_segment_eq_real_ivl split: if_split_asm) + then have "y=u \ subpath 0 u g (y/u) \ interior S" + using P less_eq_real_def by force + then show "g y = g u" + using y by (auto simp: subpath_def split: if_split_asm) + qed + qed + qed (use \0 \ u\ \u \ 1\ in auto) qed lemma exists_path_subpath_to_frontier: @@ -1033,12 +1031,12 @@ obtain u where u: "0 \ u" "u \ 1" "g u \ frontier S" "(path_image(subpath 0 u g) - {g u}) \ interior S" using subpath_to_frontier [OF assms] by blast show ?thesis - apply (rule that [of "subpath 0 u g"]) - using assms u - apply (simp_all add: path_image_subpath) - apply (simp add: pathstart_def) - apply (force simp: closed_segment_eq_real_ivl path_image_def) - done + proof + show "path_image (subpath 0 u g) \ path_image g" + by (simp add: path_image_subpath_subset u) + show "pathstart (subpath 0 u g) = pathstart g" + by (metis pathstart_def pathstart_subpath) + qed (use assms u in \auto simp: path_image_subpath\) qed lemma exists_path_subpath_to_frontier_closed: @@ -1052,11 +1050,10 @@ "pathfinish h \ frontier S" using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto show ?thesis - apply (rule that [OF \path h\]) - using assms h - apply auto - apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) - done + 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 @@ -1144,9 +1141,7 @@ case False then show ?thesis apply (rule_tac x="1 + x - a" in bexI) - using g gne[of "1 + x - a"] a - apply (force simp: field_simps)+ - done + using g gne[of "1 + x - a"] a by (force simp: field_simps)+ next case True then show ?thesis @@ -1286,15 +1281,17 @@ by (auto simp: segment linepath_def) 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" - shows "linepath a b x \ convex hull s" - apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD]) - using x - apply (auto simp: linepath_image_01 [symmetric]) - done + fixes x::real + assumes a: "a \ convex hull S" + and b: "b \ convex hull S" + and x: "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 lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b" by (simp add: linepath_def) @@ -1322,10 +1319,8 @@ by (auto simp: linepath_def) lemma has_vector_derivative_linepath_within: - "(linepath a b has_vector_derivative (b - a)) (at x within s)" -apply (simp add: linepath_def has_vector_derivative_def algebra_simps) -apply (rule derivative_eq_intros | simp)+ -done + "(linepath a b has_vector_derivative (b - a)) (at x within S)" + by (force intro: derivative_eq_intros simp add: linepath_def has_vector_derivative_def algebra_simps) subsection\<^marker>\tag unimportant\\Segments via convex hulls\ @@ -1480,105 +1475,98 @@ text \Original formalization by Tom Hales\ -definition\<^marker>\tag important\ "path_component s x y \ - (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" +definition\<^marker>\tag important\ "path_component S x y \ + (\g. path g \ path_image g \ S \ pathstart g = x \ pathfinish g = y)" abbreviation\<^marker>\tag important\ - "path_component_set s x \ Collect (path_component s x)" + "path_component_set S x \ Collect (path_component S x)" lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def lemma path_component_mem: - assumes "path_component s x y" - shows "x \ s" and "y \ s" + assumes "path_component S x y" + shows "x \ S" and "y \ S" using assms unfolding path_defs by auto lemma path_component_refl: - assumes "x \ s" - shows "path_component s x x" - unfolding path_defs - apply (rule_tac x="\u. x" in exI) + assumes "x \ S" + shows "path_component S x x" using assms - apply (auto intro!: continuous_intros) - done - -lemma path_component_refl_eq: "path_component s x x \ x \ s" + unfolding path_defs + by (metis (full_types) assms continuous_on_const image_subset_iff path_image_def) + +lemma path_component_refl_eq: "path_component S x x \ x \ S" by (auto intro!: path_component_mem path_component_refl) -lemma path_component_sym: "path_component s x y \ path_component s y x" +lemma path_component_sym: "path_component S x y \ path_component S y x" unfolding path_component_def - apply (erule exE) - apply (rule_tac x="reversepath g" in exI, auto) - done + by (metis (no_types) path_image_reversepath path_reversepath pathfinish_reversepath pathstart_reversepath) lemma path_component_trans: - assumes "path_component s x y" and "path_component s y z" - shows "path_component s x z" + assumes "path_component S x y" and "path_component S y z" + shows "path_component S x z" using assms unfolding path_component_def - apply (elim exE) - apply (rule_tac x="g +++ ga" in exI) - apply (auto simp: path_image_join) - done - -lemma path_component_of_subset: "s \ t \ path_component s x y \ path_component t x y" + by (metis path_join pathfinish_join pathstart_join subset_path_image_join) + +lemma path_component_of_subset: "S \ T \ path_component S x y \ path_component T x y" unfolding path_component_def by auto lemma path_component_linepath: - fixes s :: "'a::real_normed_vector set" - shows "closed_segment a b \ s \ path_component s a b" + 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) subsubsection\<^marker>\tag unimportant\ \Path components as sets\ lemma path_component_set: - "path_component_set s x = - {y. (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)}" + "path_component_set S x = + {y. (\g. path g \ path_image g \ S \ pathstart g = x \ pathfinish g = y)}" by (auto simp: path_component_def) -lemma path_component_subset: "path_component_set s x \ s" +lemma path_component_subset: "path_component_set S x \ S" by (auto simp: path_component_mem(2)) -lemma path_component_eq_empty: "path_component_set s x = {} \