src/HOL/Analysis/Path_Connected.thy
```     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.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.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)
```