--- a/src/HOL/Analysis/Jordan_Curve.thy Fri Aug 04 19:17:49 2023 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Sun Aug 06 18:29:09 2023 +0100
@@ -42,9 +42,9 @@
(\<forall>x\<in>S \<union> T. (x - a) /\<^sub>R cmod (x - a) / ((x - b) /\<^sub>R cmod (x - b)) = exp (\<i>*complex_of_real (g x)))"
proof (cases "S \<inter> T = {}")
case True
- have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
- apply (rule continuous_on_cases_local [OF clo contg conth])
- using True by auto
+ then have "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else h x)"
+ using continuous_on_cases_local [OF clo contg conth]
+ by (meson disjoint_iff)
then show ?thesis
by (rule_tac x="(\<lambda>x. if x \<in> S then g x else h x)" in exI) (auto simp: g h)
next
@@ -54,11 +54,10 @@
have "exp (\<i>* of_real (g x)) = exp (\<i>* of_real (h x))"
using that by (simp add: g h)
then obtain n where "complex_of_real (g x) = complex_of_real (h x) + 2* of_int n*complex_of_real pi"
- apply (auto simp: exp_eq)
+ apply (simp add: exp_eq)
by (metis complex_i_not_zero distrib_left mult.commute mult_cancel_left)
then show ?thesis
- apply (rule_tac x=n in exI)
- using of_real_eq_iff by fastforce
+ using of_real_eq_iff by (fastforce intro!: exI [where x=n])
qed
have contgh: "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
by (intro continuous_intros continuous_on_subset [OF contg] continuous_on_subset [OF conth]) auto
@@ -99,16 +98,16 @@
show ?thesis
proof (intro exI conjI)
show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then g x else z + h x)"
- apply (intro continuous_intros continuous_on_cases_local [OF clo contg] conth)
- using z by fastforce
+ by (intro continuous_intros continuous_on_cases_local [OF clo contg] conth) (use z in force)
qed (auto simp: g h algebra_simps exp_add)
qed
- ultimately have *: "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
+ ultimately have "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
(\<lambda>x. (x - a) /\<^sub>R cmod (x - a)) (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
- show ?thesis
- apply (rule Borsuk_maps_homotopic_in_connected_component_eq [THEN iffD1])
- using assms by (auto simp: *)
+ moreover have "compact (S \<union> T)"
+ using assms by blast
+ ultimately show ?thesis
+ using assms Borsuk_maps_homotopic_in_connected_component_eq by fastforce
qed
@@ -122,13 +121,8 @@
by (simp add: \<open>closed T\<close> ccT open_Compl open_path_connected_component)
then obtain g where g: "path g" "path_image g \<subseteq> - T" "pathstart g = a" "pathfinish g = b"
by (auto simp: path_component_def)
- obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
- proof
- show "compact (path_image g)"
- by (simp add: \<open>path g\<close> compact_path_image)
- show "connected (path_image g)"
- by (simp add: \<open>path g\<close> connected_path_image)
- qed (use g in auto)
+ then obtain C where C: "compact C" "connected C" "a \<in> C" "b \<in> C" "C \<inter> T = {}"
+ by fastforce
obtain r where "0 < r" and r: "C \<union> S \<subseteq> ball 0 r"
by (metis \<open>compact C\<close> \<open>compact S\<close> bounded_Un compact_imp_bounded bounded_subset_ballD)
have "connected_component (- (S \<union> (T \<inter> cball 0 r \<union> sphere 0 r))) a b"
@@ -160,10 +154,9 @@
lemma Janiszewski_connected:
fixes S :: "complex set"
assumes ST: "compact S" "closed T" "connected(S \<inter> T)"
- and notST: "connected (- S)" "connected (- T)"
- shows "connected(- (S \<union> T))"
-using Janiszewski [OF ST]
-by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
+ and notST: "connected (- S)" "connected (- T)"
+ shows "connected(- (S \<union> T))"
+ using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
subsection\<open>The Jordan Curve theorem\<close>
@@ -214,8 +207,8 @@
by (auto simp: path_image_subpath image_iff Bex_def)
qed
show "path_image (subpath 0 v h) \<union> path_image (subpath v 1 h) = path_image g"
- using v apply (simp add: path_image_subpath pihg [symmetric])
- using path_image_def by fastforce
+ using v path_image_subpath pihg path_image_def
+ by (metis (full_types) image_Un ivl_disj_un_two_touch(4))
qed
qed
@@ -257,7 +250,7 @@
by (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image outer open_Compl open_components)
show "connected outer"
using in_components_connected outer by blast
- show "inner \<inter> outer = {}"
+ show inner_outer: "inner \<inter> outer = {}"
by (meson \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>connected outer\<close> bounded_subset components_maximal in_components_subset inner outer)
show fro_inner: "frontier inner = path_image c"
by (simp add: Jordan_Brouwer_frontier [OF hom inner])
@@ -267,14 +260,13 @@
proof -
have "frontier middle = path_image c"
by (simp add: Jordan_Brouwer_frontier [OF hom] that)
- have middle: "open middle" "connected middle" "middle \<noteq> {}"
- apply (meson \<open>simple_path c\<close> compact_imp_closed compact_simple_path_image m open_Compl open_components)
- using in_components_connected in_components_nonempty m by blast+
+ obtain middle: "open middle" "connected middle" "middle \<noteq> {}"
+ by (metis fro_inner frontier_closed in_components_maximal m open_Compl open_components)
obtain a0 b0 where "a0 \<in> path_image c" "b0 \<in> path_image c" "a0 \<noteq> b0"
using simple_path_image_uncountable [OF \<open>simple_path c\<close>]
by (metis Diff_cancel countable_Diff_eq countable_empty insert_iff subsetI subset_singleton_iff)
obtain a b g where ab: "a \<in> path_image c" "b \<in> path_image c" "a \<noteq> b"
- and "arc g" "pathstart g = a" "pathfinish g = b"
+ and g: "arc g" "pathstart g = a" "pathfinish g = b"
and pag_sub: "path_image g - {a,b} \<subseteq> middle"
proof (rule dense_accessible_frontier_point_pairs [OF \<open>open middle\<close> \<open>connected middle\<close>, of "path_image c \<inter> ball a0 (dist a0 b0)" "path_image c \<inter> ball b0 (dist a0 b0)"])
show "openin (top_of_set (frontier middle)) (path_image c \<inter> ball a0 (dist a0 b0))"
@@ -303,22 +295,21 @@
show "closed (path_image d \<union> path_image g)"
by (simp add: \<open>arc d\<close> \<open>arc g\<close> closed_Un closed_arc_image)
show "connected ((path_image u \<union> path_image g) \<inter> (path_image d \<union> path_image g))"
- by (metis Un_Diff_cancel \<open>arc g\<close> \<open>path_image u \<inter> path_image d = {a, b}\<close> \<open>pathfinish g = b\<close> \<open>pathstart g = a\<close> connected_arc_image insert_Diff1 pathfinish_in_path_image pathstart_in_path_image sup_bot.right_neutral sup_commute sup_inf_distrib1)
+ using ud_ab
+ by (metis Un_insert_left g connected_arc_image insert_absorb pathfinish_in_path_image pathstart_in_path_image sup_bot_left sup_commute sup_inf_distrib1)
show "connected_component (- (path_image u \<union> path_image g)) x y"
unfolding connected_component_def
proof (intro exI conjI)
have "connected ((inner \<union> (path_image c - path_image u)) \<union> (outer \<union> (path_image c - path_image u)))"
proof (rule connected_Un)
show "connected (inner \<union> (path_image c - path_image u))"
- apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
- using fro_inner [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected inner\<close>]
+ by (metis Diff_subset closure_Un_frontier dual_order.refl fro_inner sup.mono sup_ge1)
show "connected (outer \<union> (path_image c - path_image u))"
- apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
- using fro_outer [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected outer\<close>]
+ by (simp add: Diff_eq closure_Un_frontier fro_outer sup_inf_distrib1)
have "(inner \<inter> outer) \<union> (path_image c - path_image u) \<noteq> {}"
- by (metis \<open>arc d\<close> ud_ab Diff_Int Diff_cancel Un_Diff \<open>inner \<inter> outer = {}\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_simple_path insert_commute nonempty_simple_path_endless sup_bot_left ud_Un)
+ using \<open>arc d\<close> \<open>pathfinish d = a\<close> \<open>pathstart d = b\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
then show "(inner \<union> (path_image c - path_image u)) \<inter> (outer \<union> (path_image c - path_image u)) \<noteq> {}"
by auto
qed
@@ -344,13 +335,11 @@
have "connected ((inner \<union> (path_image c - path_image d)) \<union> (outer \<union> (path_image c - path_image d)))"
proof (rule connected_Un)
show "connected (inner \<union> (path_image c - path_image d))"
- apply (rule connected_intermediate_closure [OF \<open>connected inner\<close>])
- using fro_inner [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected inner\<close>] fro_inner
+ by (simp add: closure_Un_frontier sup.coboundedI2)
show "connected (outer \<union> (path_image c - path_image d))"
- apply (rule connected_intermediate_closure [OF \<open>connected outer\<close>])
- using fro_outer [symmetric] apply (auto simp: closure_subset frontier_def)
- done
+ using connected_intermediate_closure [OF \<open>connected outer\<close>]
+ by (simp add: closure_Un_frontier fro_outer sup.coboundedI2)
have "(inner \<inter> outer) \<union> (path_image c - path_image d) \<noteq> {}"
using \<open>arc u\<close> \<open>pathfinish u = b\<close> \<open>pathstart u = a\<close> arc_imp_simple_path nonempty_simple_path_endless ud_Un ud_ab by fastforce
then show "(inner \<union> (path_image c - path_image d)) \<inter> (outer \<union> (path_image c - path_image d)) \<noteq> {}"
@@ -393,8 +382,8 @@
corollary\<^marker>\<open>tag unimportant\<close> Jordan_disconnected:
fixes c :: "real \<Rightarrow> complex"
assumes "simple_path c" "pathfinish c = pathstart c"
- shows "\<not> connected(- path_image c)"
-using Jordan_curve [OF assms]
+ shows "\<not> connected(- path_image c)"
+ using Jordan_curve [OF assms]
by (metis Jordan_Brouwer_separation assms homeomorphic_simple_path_image_circle zero_less_one)
@@ -484,7 +473,7 @@
using Jordan_inside_outside [of "c1 +++ reversepath c"]
using Jordan_inside_outside [of "c2 +++ reversepath c"] assms
apply (simp_all add: path_image_join closed_Un closed_simple_path_image open_inside open_outside)
- apply (blast elim: | metis connected_simple_path_endless)+
+ apply (blast | metis connected_simple_path_endless)+
done
have inout_12: "inside (?\<Theta>1 \<union> ?\<Theta>2) \<inter> (?\<Theta> - {pathstart c, pathfinish c}) \<noteq> {}"
by (metis (no_types, lifting) c c1c ne_12 Diff_Int_distrib Diff_empty Int_empty_right Int_left_commute inf_sup_absorb inf_sup_aci(1) inside_no_overlap)
@@ -494,9 +483,8 @@
then show False
using connectedD [OF co_c, of "inside(?\<Theta>1 \<union> ?\<Theta>2)" "outside(?\<Theta>1 \<union> ?\<Theta>2)"]
using c c1c2 pa_c op_in12 op_out12 inout_12
- apply auto
- apply (metis Un_Diff_cancel2 Un_iff compl_sup disjoint_insert(1) inf_commute inf_compl_bot_left2 inside_Un_outside mk_disjoint_insert sup_inf_absorb)
- done
+ apply clarsimp
+ by (smt (verit, ccfv_threshold) Diff_Int_distrib Diff_cancel Diff_empty Int_assoc inf_sup_absorb inf_sup_aci(1) outside_no_overlap)
qed
have out_sub12: "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)" "outside(?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
by (metis Un_commute pi_disjoint outside_Un_outside_Un)+
@@ -507,10 +495,11 @@
by (metis (no_types) Diff_Int_distrib Diff_cancel inf_sup_absorb inf_sup_aci(3) inside_no_overlap)
have 2: "outside (?\<Theta> \<union> ?\<Theta>2) \<inter> ?\<Theta> = {}"
by (metis (no_types) Int_empty_right Int_left_commute inf_sup_absorb outside_no_overlap)
- have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
- apply (subst Un_commute, rule outside_Un_outside_Un)
+ have "path_image c1 \<inter> outside (path_image c2 \<union> path_image c) = {}"
using connectedD [OF co_c1, of "inside(?\<Theta>2 \<union> ?\<Theta>)" "outside(?\<Theta>2 \<union> ?\<Theta>)"]
pa_c1 op_in2c op_out2c ne c1 c2c 1 2 by (auto simp: inf_sup_aci)
+ then have "outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
+ by (metis outside_Un_outside_Un sup_commute)
with out_sub12
have "outside(?\<Theta>1 \<union> ?\<Theta>2) = outside(?\<Theta>2 \<union> ?\<Theta>)" by blast
then have "frontier(outside(?\<Theta>1 \<union> ?\<Theta>2)) = frontier(outside(?\<Theta>2 \<union> ?\<Theta>))"
@@ -548,9 +537,8 @@
then have xnot: "x \<notin> ?\<Theta>"
by (simp add: inside_def)
obtain z where zim: "z \<in> ?\<Theta>1" and zout: "z \<in> outside(?\<Theta>2 \<union> ?\<Theta>)"
- apply (auto simp: outside_inside)
- using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>]
- by (metis Diff_Diff_Int Diff_iff ex_in_conv c1 c1c c1c2 pa1_disj_in2)
+ unfolding outside_inside
+ using nonempty_simple_path_endless [OF \<open>simple_path c1\<close>] c1 c1c c1c2 pa1_disj_in2 by auto
obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>2 \<union> ?\<Theta>)"
using zout op_out2c open_contains_ball_eq by blast
have "z \<in> frontier (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -560,11 +548,8 @@
then have w2: "w \<in> outside (?\<Theta>2 \<union> ?\<Theta>)"
by (metis e dist_commute mem_ball subsetCE)
then have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) z w"
- apply (simp add: connected_component_def)
- apply (rule_tac x = "outside(?\<Theta>2 \<union> ?\<Theta>)" in exI)
- using zout apply (auto simp: co_out2c)
- apply (simp_all add: outside_inside)
- done
+ unfolding connected_component_def
+ by (metis co_out2c compl_sup inside_Un_outside sup_ge2 zout)
moreover have "connected_component (- ?\<Theta>2 \<inter> - ?\<Theta>) w x"
unfolding connected_component_def
using pa2_disj_in1 co_in1c x w1 union_with_outside by fastforce
@@ -581,9 +566,8 @@
then have xnot: "x \<notin> ?\<Theta>"
by (simp add: inside_def)
obtain z where zim: "z \<in> ?\<Theta>2" and zout: "z \<in> outside(?\<Theta>1 \<union> ?\<Theta>)"
- apply (auto simp: outside_inside)
- using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>]
- by (metis (no_types, opaque_lifting) Diff_Diff_Int Diff_iff c1c2 c2 c2c ex_in_conv pa2_disj_in1)
+ unfolding outside_inside
+ using nonempty_simple_path_endless [OF \<open>simple_path c2\<close>] c1c2 c2 c2c pa2_disj_in1 by auto
obtain e where "e > 0" and e: "ball z e \<subseteq> outside(?\<Theta>1 \<union> ?\<Theta>)"
using zout op_out1c open_contains_ball_eq by blast
have "z \<in> frontier (inside (?\<Theta>2 \<union> ?\<Theta>))"
@@ -593,11 +577,8 @@
then have w1: "w \<in> outside (?\<Theta>1 \<union> ?\<Theta>)"
by (metis e dist_commute mem_ball subsetCE)
then have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) z w"
- apply (simp add: connected_component_def)
- apply (rule_tac x = "outside(?\<Theta>1 \<union> ?\<Theta>)" in exI)
- using zout apply (auto simp: co_out1c)
- apply (simp_all add: outside_inside)
- done
+ unfolding connected_component_def
+ by (metis Compl_Un co_out1c inside_Un_outside sup_ge2 zout)
moreover have "connected_component (- ?\<Theta>1 \<inter> - ?\<Theta>) w x"
unfolding connected_component_def
using pa1_disj_in2 co_in2c x w2 union_with_outside by fastforce
@@ -614,8 +595,8 @@
have *: "outside (?\<Theta>1 \<union> ?\<Theta>) \<inter> outside (?\<Theta>2 \<union> ?\<Theta>) \<subseteq> outside (?\<Theta>1 \<union> ?\<Theta>2)"
proof (rule components_maximal)
show out_in: "outside (?\<Theta>1 \<union> ?\<Theta>2) \<in> components (- (?\<Theta>1 \<union> ?\<Theta>2))"
- apply (simp only: outside_in_components co_out12c)
- by (metis bounded_empty fr_out(1) frontier_empty unbounded_outside)
+ unfolding outside_in_components co_out12c
+ using co_out12c fr_out(1) by force
have conn_U: "connected (- (closure (inside (?\<Theta>1 \<union> ?\<Theta>)) \<union> closure (inside (?\<Theta>2 \<union> ?\<Theta>))))"
proof (rule Janiszewski_connected, simp_all)
show "bounded (inside (?\<Theta>1 \<union> ?\<Theta>))"
@@ -661,9 +642,10 @@
show "inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta> - {a, b}) = inside (?\<Theta>1 \<union> ?\<Theta>2)"
(is "?lhs = ?rhs")
proof
- show "?lhs \<subseteq> ?rhs"
- apply (simp add: in_sub_in1 in_sub_in2)
+ have " path_image c - {a, b} \<subseteq> inside (path_image c1 \<union> path_image c2)"
using c1c c2c inside_outside pi_disjoint by fastforce
+ then show "?lhs \<subseteq> ?rhs"
+ by (simp add: in_sub_in1 in_sub_in2)
have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> inside (?\<Theta>1 \<union> ?\<Theta>) \<union> inside (?\<Theta>2 \<union> ?\<Theta>) \<union> (?\<Theta>)"
using Compl_anti_mono [OF *] by (force simp: inside_outside)
moreover have "inside (?\<Theta>1 \<union> ?\<Theta>2) \<subseteq> -{a,b}"