src/HOL/Analysis/Path_Connected.thy
changeset 68607 67bb59e49834
parent 68532 f8b98d31ad45
child 68721 53ad5c01be3f
     1.1 --- a/src/HOL/Analysis/Path_Connected.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -1964,11 +1964,11 @@
     1.4    "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
     1.5    by (simp add: path_connected_punctured_universe path_connected_imp_connected)
     1.6  
     1.7 -lemma%important path_connected_sphere:
     1.8 +proposition path_connected_sphere:
     1.9    fixes a :: "'a :: euclidean_space"
    1.10    assumes "2 \<le> DIM('a)"
    1.11    shows "path_connected(sphere a r)"
    1.12 -proof%unimportant (cases r "0::real" rule: linorder_cases)
    1.13 +proof (cases r "0::real" rule: linorder_cases)
    1.14    case less
    1.15    then show ?thesis
    1.16      by (simp add: path_connected_empty)
    1.17 @@ -2289,23 +2289,23 @@
    1.18      using path_connected_translation by metis
    1.19  qed
    1.20  
    1.21 -lemma%important path_connected_annulus:
    1.22 +proposition path_connected_annulus:
    1.23    fixes a :: "'N::euclidean_space"
    1.24    assumes "2 \<le> DIM('N)"
    1.25    shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
    1.26          "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
    1.27          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
    1.28          "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
    1.29 -  by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
    1.30 -
    1.31 -lemma%important connected_annulus:
    1.32 +  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
    1.33 +
    1.34 +proposition connected_annulus:
    1.35    fixes a :: "'N::euclidean_space"
    1.36    assumes "2 \<le> DIM('N::euclidean_space)"
    1.37    shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
    1.38          "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
    1.39          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
    1.40          "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
    1.41 -  by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
    1.42 +  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
    1.43  
    1.44  
    1.45  subsection%unimportant\<open>Relations between components and path components\<close>
    1.46 @@ -3302,14 +3302,14 @@
    1.47  
    1.48  subsection\<open>Condition for an open map's image to contain a ball\<close>
    1.49  
    1.50 -lemma%important ball_subset_open_map_image:
    1.51 +proposition ball_subset_open_map_image:
    1.52    fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
    1.53    assumes contf: "continuous_on (closure S) f"
    1.54        and oint: "open (f ` interior S)"
    1.55        and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
    1.56        and "bounded S" "a \<in> S" "0 < r"
    1.57      shows "ball (f a) r \<subseteq> f ` S"
    1.58 -proof%unimportant (cases "f ` S = UNIV")
    1.59 +proof (cases "f ` S = UNIV")
    1.60    case True then show ?thesis by simp
    1.61  next
    1.62    case False
    1.63 @@ -3868,26 +3868,26 @@
    1.64  
    1.65  text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
    1.66  
    1.67 -proposition%important homotopic_paths_rid:
    1.68 +proposition homotopic_paths_rid:
    1.69      "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
    1.70 -  apply%unimportant (subst homotopic_paths_sym)
    1.71 +  apply (subst homotopic_paths_sym)
    1.72    apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if  t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
    1.73    apply (simp_all del: le_divide_eq_numeral1)
    1.74    apply (subst split_01)
    1.75    apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
    1.76    done
    1.77  
    1.78 -proposition%important homotopic_paths_lid:
    1.79 +proposition homotopic_paths_lid:
    1.80     "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
    1.81 -using%unimportant homotopic_paths_rid [of "reversepath p" s]
    1.82 +  using homotopic_paths_rid [of "reversepath p" s]
    1.83    by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
    1.84          pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
    1.85  
    1.86 -proposition%important homotopic_paths_assoc:
    1.87 +proposition homotopic_paths_assoc:
    1.88     "\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
    1.89       pathfinish q = pathstart r\<rbrakk>
    1.90      \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
    1.91 -  apply%unimportant (subst homotopic_paths_sym)
    1.92 +  apply (subst homotopic_paths_sym)
    1.93    apply (rule homotopic_paths_reparametrize
    1.94             [where f = "\<lambda>t. if  t \<le> 1 / 2 then inverse 2 *\<^sub>R t
    1.95                             else if  t \<le> 3 / 4 then t - (1 / 4)
    1.96 @@ -3898,10 +3898,10 @@
    1.97    apply (auto simp: joinpaths_def)
    1.98    done
    1.99  
   1.100 -proposition%important homotopic_paths_rinv:
   1.101 +proposition homotopic_paths_rinv:
   1.102    assumes "path p" "path_image p \<subseteq> s"
   1.103      shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
   1.104 -proof%unimportant -
   1.105 +proof -
   1.106    have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
   1.107      using assms
   1.108      apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
   1.109 @@ -3921,10 +3921,10 @@
   1.110      done
   1.111  qed
   1.112  
   1.113 -proposition%important homotopic_paths_linv:
   1.114 +proposition homotopic_paths_linv:
   1.115    assumes "path p" "path_image p \<subseteq> s"
   1.116      shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
   1.117 -using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
   1.118 +  using homotopic_paths_rinv [of "reversepath p" s] assms by simp
   1.119  
   1.120  
   1.121  subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
   1.122 @@ -3994,14 +3994,14 @@
   1.123  
   1.124  subsection\<open>Relations between the two variants of homotopy\<close>
   1.125  
   1.126 -proposition%important homotopic_paths_imp_homotopic_loops:
   1.127 +proposition homotopic_paths_imp_homotopic_loops:
   1.128      "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
   1.129 -  by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
   1.130 -
   1.131 -proposition%important homotopic_loops_imp_homotopic_paths_null:
   1.132 +  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
   1.133 +
   1.134 +proposition homotopic_loops_imp_homotopic_paths_null:
   1.135    assumes "homotopic_loops s p (linepath a a)"
   1.136      shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
   1.137 -proof%unimportant -
   1.138 +proof -
   1.139    have "path p" by (metis assms homotopic_loops_imp_path)
   1.140    have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
   1.141    have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
   1.142 @@ -4069,12 +4069,12 @@
   1.143      by (blast intro: homotopic_paths_trans)
   1.144  qed
   1.145  
   1.146 -proposition%important homotopic_loops_conjugate:
   1.147 +proposition homotopic_loops_conjugate:
   1.148    fixes s :: "'a::real_normed_vector set"
   1.149    assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
   1.150        and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
   1.151      shows "homotopic_loops s (p +++ q +++ reversepath p) q"
   1.152 -proof%unimportant -
   1.153 +proof -
   1.154    have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
   1.155    have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
   1.156    have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
   1.157 @@ -4326,10 +4326,10 @@
   1.158      using homotopic_join_subpaths2 by blast
   1.159  qed
   1.160  
   1.161 -proposition%important homotopic_join_subpaths:
   1.162 +proposition homotopic_join_subpaths:
   1.163     "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
   1.164      \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
   1.165 -apply%unimportant (rule le_cases3 [of u v w])
   1.166 +  apply (rule le_cases3 [of u v w])
   1.167  using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
   1.168  
   1.169  text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
   1.170 @@ -5043,7 +5043,7 @@
   1.171  
   1.172  subsection\<open>Sort of induction principle for connected sets\<close>
   1.173  
   1.174 -lemma%important connected_induction:
   1.175 +proposition connected_induction:
   1.176    assumes "connected S"
   1.177        and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   1.178        and opI: "\<And>a. a \<in> S
   1.179 @@ -5051,7 +5051,7 @@
   1.180                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
   1.181        and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
   1.182      shows "Q b"
   1.183 -proof%unimportant -
   1.184 +proof -
   1.185    have 1: "openin (subtopology euclidean S)
   1.186               {b. \<exists>T. openin (subtopology euclidean S) T \<and>
   1.187                       b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
   1.188 @@ -5142,14 +5142,14 @@
   1.189  
   1.190  subsection\<open>Basic properties of local compactness\<close>
   1.191  
   1.192 -lemma%important locally_compact:
   1.193 +proposition locally_compact:
   1.194    fixes s :: "'a :: metric_space set"
   1.195    shows
   1.196      "locally compact s \<longleftrightarrow>
   1.197       (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
   1.198                      openin (subtopology euclidean s) u \<and> compact v)"
   1.199       (is "?lhs = ?rhs")
   1.200 -proof%unimportant
   1.201 +proof
   1.202    assume ?lhs
   1.203    then show ?rhs
   1.204      apply clarify
   1.205 @@ -5696,12 +5696,12 @@
   1.206      by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
   1.207  qed
   1.208  
   1.209 -corollary%important Sura_Bura:
   1.210 +corollary Sura_Bura:
   1.211    fixes S :: "'a::euclidean_space set"
   1.212    assumes "locally compact S" "C \<in> components S" "compact C"
   1.213    shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
   1.214           (is "C = ?rhs")
   1.215 -proof%unimportant
   1.216 +proof
   1.217    show "?rhs \<subseteq> C"
   1.218    proof (clarsimp, rule ccontr)
   1.219      fix x
   1.220 @@ -5831,17 +5831,17 @@
   1.221      by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
   1.222  qed
   1.223  
   1.224 -proposition%important locally_path_connected:
   1.225 +proposition locally_path_connected:
   1.226    "locally path_connected S \<longleftrightarrow>
   1.227     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.228            \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   1.229 -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.230 -
   1.231 -proposition%important locally_path_connected_open_path_component:
   1.232 +  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.233 +
   1.234 +proposition locally_path_connected_open_path_component:
   1.235    "locally path_connected S \<longleftrightarrow>
   1.236     (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
   1.237            \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
   1.238 -by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.239 +  by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.240  
   1.241  lemma locally_connected_open_component:
   1.242    "locally connected S \<longleftrightarrow>
   1.243 @@ -5849,14 +5849,14 @@
   1.244            \<longrightarrow> openin (subtopology euclidean S) c)"
   1.245  by (metis components_iff locally_connected_open_connected_component)
   1.246  
   1.247 -proposition%important locally_connected_im_kleinen:
   1.248 +proposition locally_connected_im_kleinen:
   1.249    "locally connected S \<longleftrightarrow>
   1.250     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.251         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   1.252                  x \<in> u \<and> u \<subseteq> v \<and>
   1.253                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
   1.254     (is "?lhs = ?rhs")
   1.255 -proof%unimportant
   1.256 +proof
   1.257    assume ?lhs
   1.258    then show ?rhs
   1.259      by (fastforce simp add: locally_connected)
   1.260 @@ -5890,7 +5890,7 @@
   1.261      done
   1.262  qed
   1.263  
   1.264 -proposition%important locally_path_connected_im_kleinen:
   1.265 +proposition locally_path_connected_im_kleinen:
   1.266    "locally path_connected S \<longleftrightarrow>
   1.267     (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.268         \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   1.269 @@ -5898,7 +5898,7 @@
   1.270                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
   1.271                                  pathstart p = x \<and> pathfinish p = y))))"
   1.272     (is "?lhs = ?rhs")
   1.273 -proof%unimportant
   1.274 +proof
   1.275    assume ?lhs
   1.276    then show ?rhs
   1.277      apply (simp add: locally_path_connected path_connected_def)
   1.278 @@ -6048,13 +6048,13 @@
   1.279    shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
   1.280  by (simp add: open_path_connected_component)
   1.281  
   1.282 -proposition%important locally_connected_quotient_image:
   1.283 +proposition locally_connected_quotient_image:
   1.284    assumes lcS: "locally connected S"
   1.285        and oo: "\<And>T. T \<subseteq> f ` S
   1.286                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
   1.287                      openin (subtopology euclidean (f ` S)) T"
   1.288      shows "locally connected (f ` S)"
   1.289 -proof%unimportant (clarsimp simp: locally_connected_open_component)
   1.290 +proof (clarsimp simp: locally_connected_open_component)
   1.291    fix U C
   1.292    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
   1.293    then have "C \<subseteq> U" "U \<subseteq> f ` S"
   1.294 @@ -6114,12 +6114,12 @@
   1.295  qed
   1.296  
   1.297  text\<open>The proof resembles that above but is not identical!\<close>
   1.298 -proposition%important locally_path_connected_quotient_image:
   1.299 +proposition locally_path_connected_quotient_image:
   1.300    assumes lcS: "locally path_connected S"
   1.301        and oo: "\<And>T. T \<subseteq> f ` S
   1.302                  \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
   1.303      shows "locally path_connected (f ` S)"
   1.304 -proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
   1.305 +proof (clarsimp simp: locally_path_connected_open_path_component)
   1.306    fix U y
   1.307    assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
   1.308    then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
   1.309 @@ -6345,7 +6345,7 @@
   1.310      by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
   1.311  qed
   1.312  
   1.313 -proposition%important isometries_subspaces:
   1.314 +proposition isometries_subspaces:
   1.315    fixes S :: "'a::euclidean_space set"
   1.316      and T :: "'b::euclidean_space set"
   1.317    assumes S: "subspace S"
   1.318 @@ -6356,7 +6356,7 @@
   1.319                      "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
   1.320                      "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   1.321                      "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
   1.322 -proof%unimportant -
   1.323 +proof -
   1.324    obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
   1.325               and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
   1.326               and "independent B" "finite B" "card B = dim S" "span B = S"
   1.327 @@ -7815,7 +7815,7 @@
   1.328    qed
   1.329  qed
   1.330  
   1.331 -proposition%important homeomorphism_moving_points_exists:
   1.332 +proposition homeomorphism_moving_points_exists:
   1.333    fixes S :: "'a::euclidean_space set"
   1.334    assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
   1.335        and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
   1.336 @@ -7823,7 +7823,7 @@
   1.337        and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   1.338    obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
   1.339                      "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
   1.340 -proof%unimportant (cases "S = {}")
   1.341 +proof (cases "S = {}")
   1.342    case True
   1.343    then show ?thesis
   1.344      using KS homeomorphism_ident that by fastforce
   1.345 @@ -8082,12 +8082,12 @@
   1.346    qed
   1.347  qed
   1.348  
   1.349 -proposition%important homeomorphism_grouping_points_exists:
   1.350 +proposition homeomorphism_grouping_points_exists:
   1.351    fixes S :: "'a::euclidean_space set"
   1.352    assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   1.353    obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
   1.354                      "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
   1.355 -proof%unimportant (cases "2 \<le> DIM('a)")
   1.356 +proof (cases "2 \<le> DIM('a)")
   1.357    case True
   1.358    have TS: "T \<subseteq> affine hull S"
   1.359      using affine_hull_open assms by blast
   1.360 @@ -8364,13 +8364,13 @@
   1.361    qed
   1.362  qed
   1.363  
   1.364 -proposition%important nullhomotopic_from_sphere_extension:
   1.365 +proposition nullhomotopic_from_sphere_extension:
   1.366    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   1.367    shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
   1.368            (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
   1.369                 (\<forall>x \<in> sphere a r. g x = f x))"
   1.370           (is "?lhs = ?rhs")
   1.371 -proof%unimportant (cases r "0::real" rule: linorder_cases)
   1.372 +proof (cases r "0::real" rule: linorder_cases)
   1.373    case equal
   1.374    then show ?thesis
   1.375      apply (auto simp: homotopic_with)