Switching to inverse image and constant_on, plus some new material
authorpaulson <lp15@cam.ac.uk>
Thu Oct 19 17:16:01 2017 +0100 (22 months ago)
changeset 66884c2128ab11f61
parent 66878 91da58bb560d
child 66885 d3d508b23d1d
Switching to inverse image and constant_on, plus some new material
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Jordan_Curve.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Winding_Numbers.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Oct 17 13:56:58 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Oct 19 17:16:01 2017 +0100
     1.3 @@ -2279,7 +2279,7 @@
     1.4  lemma retraction_imp_quotient_map:
     1.5     "retraction s t r
     1.6      \<Longrightarrow> u \<subseteq> t
     1.7 -            \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> r x \<in> u} \<longleftrightarrow>
     1.8 +            \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>
     1.9                   openin (subtopology euclidean t) u)"
    1.10  apply (clarsimp simp add: retraction)
    1.11  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
    1.12 @@ -2941,21 +2941,21 @@
    1.13                and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
    1.14      by (metis Dugundji [OF C cloUT contgf gfTC])
    1.15    show ?thesis
    1.16 -  proof (rule_tac V = "{x \<in> U. f' x \<in> D}" and g = "h o r o f'" in that)
    1.17 -    show "T \<subseteq> {x \<in> U. f' x \<in> D}"
    1.18 +  proof (rule_tac V = "U \<inter> f' -` D" and g = "h o r o f'" in that)
    1.19 +    show "T \<subseteq> U \<inter> f' -` D"
    1.20        using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
    1.21        by fastforce
    1.22 -    show ope: "openin (subtopology euclidean U) {x \<in> U. f' x \<in> D}"
    1.23 +    show ope: "openin (subtopology euclidean U) (U \<inter> f' -` D)"
    1.24        using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
    1.25 -    have conth: "continuous_on (r ` f' ` {x \<in> U. f' x \<in> D}) h"
    1.26 +    have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
    1.27        apply (rule continuous_on_subset [of S'])
    1.28        using homeomorphism_def homgh apply blast
    1.29        using \<open>r ` D \<subseteq> S'\<close> by blast
    1.30 -    show "continuous_on {x \<in> U. f' x \<in> D} (h \<circ> r \<circ> f')"
    1.31 +    show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
    1.32        apply (intro continuous_on_compose conth
    1.33                     continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
    1.34        done
    1.35 -    show "(h \<circ> r \<circ> f') ` {x \<in> U. f' x \<in> D} \<subseteq> S"
    1.36 +    show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
    1.37        using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
    1.38        by (auto simp: homeomorphism_def)
    1.39      show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
    1.40 @@ -3150,36 +3150,36 @@
    1.41    have "S' \<subseteq> W" using WS' closedin_closed by auto
    1.42    have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
    1.43      by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
    1.44 -  have "S' retract_of {x \<in> W. h x \<in> X}"
    1.45 +  have "S' retract_of (W \<inter> h -` X)"
    1.46    proof (simp add: retraction_def retract_of_def, intro exI conjI)
    1.47 -    show "S' \<subseteq> {x \<in> W. h x \<in> X}"
    1.48 -      using him WS' closedin_imp_subset by blast
    1.49 -    show "continuous_on {x \<in> W. h x \<in> X} (f o r o h)"
    1.50 +    show "S' \<subseteq> W" "S' \<subseteq> h -` X"
    1.51 +      using him WS' closedin_imp_subset by blast+
    1.52 +    show "continuous_on (W \<inter> h -` X) (f o r o h)"
    1.53      proof (intro continuous_on_compose)
    1.54 -      show "continuous_on {x \<in> W. h x \<in> X} h"
    1.55 -        by (metis (no_types) Collect_restrict conth continuous_on_subset)
    1.56 -      show "continuous_on (h ` {x \<in> W. h x \<in> X}) r"
    1.57 +      show "continuous_on (W \<inter> h -` X) h"
    1.58 +        by (meson conth continuous_on_subset inf_le1)
    1.59 +      show "continuous_on (h ` (W \<inter> h -` X)) r"
    1.60        proof -
    1.61 -        have "h ` {b \<in> W. h b \<in> X} \<subseteq> X"
    1.62 +        have "h ` (W \<inter> h -` X) \<subseteq> X"
    1.63            by blast
    1.64 -        then show "continuous_on (h ` {b \<in> W. h b \<in> X}) r"
    1.65 +        then show "continuous_on (h ` (W \<inter> h -` X)) r"
    1.66            by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
    1.67        qed
    1.68 -      show "continuous_on (r ` h ` {x \<in> W. h x \<in> X}) f"
    1.69 +      show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
    1.70          apply (rule continuous_on_subset [of S])
    1.71           using hom homeomorphism_def apply blast
    1.72          apply clarify
    1.73          apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
    1.74          done
    1.75      qed
    1.76 -    show "(f \<circ> r \<circ> h) ` {x \<in> W. h x \<in> X} \<subseteq> S'"
    1.77 +    show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
    1.78        using \<open>retraction X S r\<close> hom
    1.79        by (auto simp: retraction_def homeomorphism_def)
    1.80      show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
    1.81        using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
    1.82    qed
    1.83    then show ?thesis
    1.84 -    apply (rule_tac V = "{x. x \<in> W \<and> h x \<in> X}" in that)
    1.85 +    apply (rule_tac V = "W \<inter> h -` X" in that)
    1.86       apply (rule openin_trans [OF _ UW])
    1.87       using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
    1.88       done
    1.89 @@ -3248,8 +3248,7 @@
    1.90      using \<open>ANR S\<close>
    1.91      apply (simp add: ANR_def)
    1.92      apply (drule_tac x=UNIV in spec)
    1.93 -    apply (drule_tac x=T in spec)
    1.94 -    apply (auto simp: closed_closedin)
    1.95 +    apply (drule_tac x=T in spec, clarsimp)
    1.96      apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
    1.97      done
    1.98  qed
    1.99 @@ -3455,10 +3454,10 @@
   1.100    define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
   1.101    have US': "closedin (subtopology euclidean U) S'"
   1.102      using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
   1.103 -    by (simp add: S'_def continuous_intros)
   1.104 +    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   1.105    have UT': "closedin (subtopology euclidean U) T'"
   1.106      using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
   1.107 -    by (simp add: T'_def continuous_intros)
   1.108 +    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   1.109    have "S \<subseteq> S'"
   1.110      using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
   1.111    have "T \<subseteq> T'"
   1.112 @@ -3543,19 +3542,19 @@
   1.113    proof -
   1.114      obtain f g where hom: "homeomorphism (S \<union> T) C f g"
   1.115        using hom by (force simp: homeomorphic_def)
   1.116 -    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
   1.117 +    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
   1.118        apply (rule closedin_trans [OF _ UC])
   1.119        apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
   1.120        using hom homeomorphism_def apply blast
   1.121        apply (metis hom homeomorphism_def set_eq_subset)
   1.122        done
   1.123 -    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
   1.124 +    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
   1.125        apply (rule closedin_trans [OF _ UC])
   1.126        apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
   1.127        using hom homeomorphism_def apply blast
   1.128        apply (metis hom homeomorphism_def set_eq_subset)
   1.129        done
   1.130 -    have ARS: "AR {x \<in> C. g x \<in> S}"
   1.131 +    have ARS: "AR (C \<inter> g -` S)"
   1.132        apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
   1.133        apply (simp add: homeomorphic_def)
   1.134        apply (rule_tac x=g in exI)
   1.135 @@ -3563,7 +3562,7 @@
   1.136        using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.137        apply (rule_tac x="f x" in image_eqI, auto)
   1.138        done
   1.139 -    have ART: "AR {x \<in> C. g x \<in> T}"
   1.140 +    have ART: "AR (C \<inter> g -` T)"
   1.141        apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
   1.142        apply (simp add: homeomorphic_def)
   1.143        apply (rule_tac x=g in exI)
   1.144 @@ -3571,7 +3570,7 @@
   1.145        using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.146        apply (rule_tac x="f x" in image_eqI, auto)
   1.147        done
   1.148 -    have ARI: "AR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
   1.149 +    have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
   1.150        apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
   1.151        apply (simp add: homeomorphic_def)
   1.152        apply (rule_tac x=g in exI)
   1.153 @@ -3580,7 +3579,7 @@
   1.154        apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.155        apply (rule_tac x="f x" in image_eqI, auto)
   1.156        done
   1.157 -    have "C = {x \<in> C. g x \<in> S} \<union> {x \<in> C. g x \<in> T}"
   1.158 +    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
   1.159        using hom  by (auto simp: homeomorphism_def)
   1.160      then show ?thesis
   1.161        by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
   1.162 @@ -3615,10 +3614,10 @@
   1.163    define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
   1.164    have cloUS': "closedin (subtopology euclidean U) S'"
   1.165      using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
   1.166 -    by (simp add: S'_def continuous_intros)
   1.167 +    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   1.168    have cloUT': "closedin (subtopology euclidean U) T'"
   1.169      using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
   1.170 -    by (simp add: T'_def continuous_intros)
   1.171 +    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   1.172    have "S \<subseteq> S'"
   1.173      using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
   1.174    have "T \<subseteq> T'"
   1.175 @@ -3752,19 +3751,19 @@
   1.176    proof -
   1.177      obtain f g where hom: "homeomorphism (S \<union> T) C f g"
   1.178        using hom by (force simp: homeomorphic_def)
   1.179 -    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
   1.180 +    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
   1.181        apply (rule closedin_trans [OF _ UC])
   1.182        apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
   1.183        using hom [unfolded homeomorphism_def] apply blast
   1.184        apply (metis hom homeomorphism_def set_eq_subset)
   1.185        done
   1.186 -    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
   1.187 +    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
   1.188        apply (rule closedin_trans [OF _ UC])
   1.189        apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
   1.190        using hom [unfolded homeomorphism_def] apply blast
   1.191        apply (metis hom homeomorphism_def set_eq_subset)
   1.192        done
   1.193 -    have ANRS: "ANR {x \<in> C. g x \<in> S}"
   1.194 +    have ANRS: "ANR (C \<inter> g -` S)"
   1.195        apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
   1.196        apply (simp add: homeomorphic_def)
   1.197        apply (rule_tac x=g in exI)
   1.198 @@ -3772,7 +3771,7 @@
   1.199        using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.200        apply (rule_tac x="f x" in image_eqI, auto)
   1.201        done
   1.202 -    have ANRT: "ANR {x \<in> C. g x \<in> T}"
   1.203 +    have ANRT: "ANR (C \<inter> g -` T)"
   1.204        apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
   1.205        apply (simp add: homeomorphic_def)
   1.206        apply (rule_tac x=g in exI)
   1.207 @@ -3780,7 +3779,7 @@
   1.208        using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.209        apply (rule_tac x="f x" in image_eqI, auto)
   1.210        done
   1.211 -    have ANRI: "ANR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
   1.212 +    have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
   1.213        apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
   1.214        apply (simp add: homeomorphic_def)
   1.215        apply (rule_tac x=g in exI)
   1.216 @@ -3789,8 +3788,8 @@
   1.217        apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
   1.218        apply (rule_tac x="f x" in image_eqI, auto)
   1.219        done
   1.220 -    have "C = {x. x \<in> C \<and> g x \<in> S} \<union> {x. x \<in> C \<and> g x \<in> T}"
   1.221 -      by auto (metis Un_iff hom homeomorphism_def imageI)
   1.222 +    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
   1.223 +      using hom by (auto simp: homeomorphism_def)
   1.224      then show ?thesis
   1.225        by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
   1.226    qed
   1.227 @@ -3822,13 +3821,13 @@
   1.228      using fim by auto
   1.229    show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
   1.230    proof (intro exI conjI)
   1.231 -    show "C \<subseteq> {x \<in> W. g x \<in> S}"
   1.232 +    show "C \<subseteq> W \<inter> g -` S"
   1.233        using \<open>C \<subseteq> W\<close> fim geq by blast
   1.234 -    show "openin (subtopology euclidean U) {x \<in> W. g x \<in> S}"
   1.235 +    show "openin (subtopology euclidean U) (W \<inter> g -` S)"
   1.236        by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
   1.237 -    show "continuous_on {x \<in> W. g x \<in> S} g"
   1.238 +    show "continuous_on (W \<inter> g -` S) g"
   1.239        by (blast intro: continuous_on_subset [OF contg])
   1.240 -    show "g ` {x \<in> W. g x \<in> S} \<subseteq> S"
   1.241 +    show "g ` (W \<inter> g -` S) \<subseteq> S"
   1.242        using gim by blast
   1.243      show "\<forall>x\<in>C. g x = f x"
   1.244        using geq by blast
   1.245 @@ -4074,15 +4073,14 @@
   1.246      apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
   1.247      done
   1.248    finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
   1.249 -  moreover have "openin (subtopology euclidean UNIV) {x \<in> UNIV. closest_point (affine hull S) x \<in> - {a}}"
   1.250 +  moreover have "openin (subtopology euclidean UNIV) (UNIV \<inter> closest_point (affine hull S) -` (- {a}))"
   1.251      apply (rule continuous_openin_preimage_gen)
   1.252      apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
   1.253      done
   1.254    ultimately show ?thesis
   1.255 -    apply (simp add: ENR_def)
   1.256 -    apply (rule_tac x = "{x. x \<in> UNIV \<and>
   1.257 -                             closest_point (affine hull S) x \<in> (- {a})}" in exI)
   1.258 -    apply simp
   1.259 +    unfolding ENR_def
   1.260 +    apply (rule_tac x = "closest_point (affine hull S) -` (- {a})" in exI)
   1.261 +    apply (simp add: vimage_def)
   1.262      done
   1.263  qed
   1.264  
   1.265 @@ -4881,5 +4879,4 @@
   1.266    using connected_complement_homeomorphic_convex_compact [OF assms]
   1.267    using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
   1.268  
   1.269 -
   1.270  end
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Oct 17 13:56:58 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Oct 19 17:16:01 2017 +0100
     2.3 @@ -4111,30 +4111,29 @@
     2.4  subsection\<open>The winding number is constant on a connected region\<close>
     2.5  
     2.6  lemma winding_number_constant:
     2.7 -  assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected s" and sg: "s \<inter> path_image \<gamma> = {}"
     2.8 -  obtains k where "\<And>z. z \<in> s \<Longrightarrow> winding_number \<gamma> z = k"
     2.9 +  assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected S" and sg: "S \<inter> path_image \<gamma> = {}"
    2.10 +  shows "winding_number \<gamma> constant_on S"
    2.11  proof -
    2.12    have *: "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
    2.13 -      if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> s" "z \<in> s" for y z
    2.14 +      if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> S" "z \<in> S" for y z
    2.15    proof -
    2.16      have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
    2.17 -      using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> s\<close> by auto
    2.18 +      using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
    2.19      with ne show ?thesis
    2.20        by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
    2.21    qed
    2.22 -  have cont: "continuous_on s (\<lambda>w. winding_number \<gamma> w)"
    2.23 +  have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
    2.24      using continuous_on_winding_number [OF \<gamma>] sg
    2.25      by (meson continuous_on_subset disjoint_eq_subset_Compl)
    2.26    show ?thesis
    2.27 -    apply (rule continuous_discrete_range_constant [OF cs cont])
    2.28 -    using "*" zero_less_one apply blast
    2.29 -    by (simp add: that)
    2.30 +    using "*" zero_less_one
    2.31 +    by (blast intro: continuous_discrete_range_constant [OF cs cont])
    2.32  qed
    2.33  
    2.34  lemma winding_number_eq:
    2.35 -     "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> s; z \<in> s; connected s; s \<inter> path_image \<gamma> = {}\<rbrakk>
    2.36 +     "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
    2.37        \<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
    2.38 -  using winding_number_constant by blast
    2.39 +  using winding_number_constant by (metis constant_on_def) 
    2.40  
    2.41  lemma open_winding_number_levelsets:
    2.42    assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
    2.43 @@ -4149,7 +4148,7 @@
    2.44      have "\<exists>e>0. \<forall>y. dist y z < e \<longrightarrow> y \<notin> path_image \<gamma> \<and> winding_number \<gamma> y = winding_number \<gamma> z"
    2.45        apply (rule_tac x=e in exI)
    2.46        using e apply (simp add: dist_norm ball_def norm_minus_commute)
    2.47 -      apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where s = "ball z e"])
    2.48 +      apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where S = "ball z e"])
    2.49        done
    2.50    } then
    2.51    show ?thesis
    2.52 @@ -4171,11 +4170,11 @@
    2.53      using B subset_ball by auto
    2.54    then have wout: "w \<in> outside (path_image \<gamma>)"
    2.55      using w by blast
    2.56 -  moreover obtain k where "\<And>z. z \<in> outside (path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
    2.57 +  moreover have "winding_number \<gamma> constant_on outside (path_image \<gamma>)"
    2.58      using winding_number_constant [OF \<gamma> loop, of "outside(path_image \<gamma>)"] connected_outside
    2.59      by (metis DIM_complex bounded_path_image dual_order.refl \<gamma> outside_no_overlap)
    2.60    ultimately have "winding_number \<gamma> z = winding_number \<gamma> w"
    2.61 -    using z by blast
    2.62 +    by (metis (no_types, hide_lams) constant_on_def z)
    2.63    also have "... = 0"
    2.64    proof -
    2.65      have wnot: "w \<notin> path_image \<gamma>"  using wout by (simp add: outside_def)
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Oct 17 13:56:58 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Thu Oct 19 17:16:01 2017 +0100
     3.3 @@ -127,7 +127,7 @@
     3.4        apply (rule Cauchy_inequality)
     3.5           using holf holomorphic_on_subset apply force
     3.6          using holf holomorphic_on_imp_continuous_on holomorphic_on_subset apply blast
     3.7 -       using \<open>w \<noteq> 0\<close> apply (simp add:)
     3.8 +       using \<open>w \<noteq> 0\<close> apply simp
     3.9         by (metis nof wgeA dist_0_norm dist_norm)
    3.10      also have "... = fact k * (B * 1 / cmod w ^ (k-n))"
    3.11        apply (simp only: mult_cancel_left times_divide_eq_right [symmetric])
    3.12 @@ -327,7 +327,7 @@
    3.13      ultimately obtain w where w: "w \<in> frontier(cball \<xi> r)"
    3.14                            and now: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (f w) \<le> norm (f x)"
    3.15        apply (rule bexE [OF continuous_attains_inf [OF compact_frontier [OF compact_cball]]])
    3.16 -      apply (simp add:)
    3.17 +      apply simp
    3.18        done
    3.19      then have fw: "0 < norm (f w)"
    3.20        by (simp add: fnz')
    3.21 @@ -336,7 +336,7 @@
    3.22      then obtain v where v: "v \<in> frontier(cball \<xi> r)"
    3.23                 and nov: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (g v) \<ge> norm (g x)"
    3.24        apply (rule bexE [OF continuous_attains_sup [OF compact_frontier [OF compact_cball] froc]])
    3.25 -      apply (simp add:)
    3.26 +      apply simp
    3.27        done
    3.28      then have fv: "0 < norm (f v)"
    3.29        by (simp add: fnz')
    3.30 @@ -628,7 +628,7 @@
    3.31        unfolding powf_def by (rule holomorphic_power_series [OF holfb w])
    3.32      moreover have "(\<Sum>i<n. powf i) = f \<xi>"
    3.33        apply (subst Groups_Big.comm_monoid_add_class.sum.setdiff_irrelevant [symmetric])
    3.34 -      apply (simp add:)
    3.35 +      apply simp
    3.36        apply (simp only: dfz sing)
    3.37        apply (simp add: powf_def)
    3.38        done
    3.39 @@ -640,7 +640,7 @@
    3.40      have "summable (\<lambda>i. (deriv ^^ (i + n)) f \<xi> * (w - \<xi>) ^ i / fact (i + n))"
    3.41      proof (cases "w=\<xi>")
    3.42        case False then show ?thesis
    3.43 -        using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by (simp add:)
    3.44 +        using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by simp
    3.45      next
    3.46        case True then show ?thesis
    3.47          by (auto simp: Power.semiring_1_class.power_0_left intro!: summable_finite [of "{0}"]
    3.48 @@ -716,7 +716,7 @@
    3.49      apply (rule holomorphic_intros)+
    3.50      using h holomorphic_on_open apply blast
    3.51      apply (rule holomorphic_intros)+
    3.52 -    using \<open>0 < n\<close> apply (simp add:)
    3.53 +    using \<open>0 < n\<close> apply simp
    3.54      apply (rule holomorphic_intros)+
    3.55      done
    3.56    show ?thesis
    3.57 @@ -924,7 +924,7 @@
    3.58          using \<open>0 < r\<close> by simp
    3.59        have "\<exists>B. 0<B \<and> eventually (\<lambda>z. cmod ((inverse \<circ> f \<circ> inverse) z) \<le> B) (at 0)"
    3.60          apply (rule exI [where x=1])
    3.61 -        apply (simp add:)
    3.62 +        apply simp
    3.63          using tendstoD [OF lim [unfolded lim_at_infinity_0] zero_less_one]
    3.64          apply (rule eventually_mono)
    3.65          apply (simp add: dist_norm)
    3.66 @@ -969,8 +969,7 @@
    3.67        qed
    3.68        then show ?thesis
    3.69          apply (rule_tac a = "\<lambda>k. (deriv ^^ k) f 0 / (fact k)" and n=n in that)
    3.70 -        apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf])
    3.71 -        apply (simp add:)
    3.72 +        apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf], simp)
    3.73          done
    3.74    next
    3.75      case False
    3.76 @@ -1041,11 +1040,12 @@
    3.77    have "bounded {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
    3.78      using polyfun_extremal [where c=c and B="B+1", OF c]
    3.79      by (auto simp: bounded_pos eventually_at_infinity_pos *)
    3.80 -  moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
    3.81 -    apply (intro allI continuous_closed_preimage_univ continuous_intros)
    3.82 +  moreover have "closed ((\<lambda>z. (\<Sum>i\<le>n. c i * z ^ i)) -` K)"
    3.83 +    apply (intro allI continuous_closed_vimage continuous_intros)
    3.84      using \<open>compact K\<close> compact_eq_bounded_closed by blast
    3.85    ultimately show ?thesis
    3.86 -    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
    3.87 +    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed
    3.88 +    by (auto simp add: vimage_def)
    3.89  qed
    3.90  
    3.91  corollary proper_map_polyfun_univ:
    3.92 @@ -1095,7 +1095,7 @@
    3.93      fix e::real assume "0 < e"
    3.94      with compf [of "cball 0 (inverse e)"]
    3.95      show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
    3.96 -      apply (simp add:)
    3.97 +      apply simp
    3.98        apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
    3.99        apply (rule_tac x="b+1" in exI)
   3.100        apply (metis inverse_inverse_eq less_add_same_cancel2 less_imp_inverse_less add.commute not_le not_less_iff_gr_or_eq order_trans zero_less_one)
   3.101 @@ -1134,7 +1134,7 @@
   3.102      with \<open>\<delta>>0\<close> have "\<exists>\<delta>>0. \<forall>x. dist \<xi> x < \<delta> \<longrightarrow> onorm (\<lambda>v. deriv f x * v - deriv f \<xi> * v) \<le> e/2"
   3.103        apply (rule_tac x="min \<delta> \<epsilon>" in exI)
   3.104        apply (intro conjI allI impI Operator_Norm.onorm_le)
   3.105 -      apply (simp add:)
   3.106 +      apply simp
   3.107        apply (simp only: Rings.ring_class.left_diff_distrib [symmetric] norm_mult)
   3.108        apply (rule mult_right_mono [OF \<delta>])
   3.109        apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>)
     4.1 --- a/src/HOL/Analysis/Connected.thy	Tue Oct 17 13:56:58 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Oct 19 17:16:01 2017 +0100
     4.3 @@ -395,29 +395,6 @@
     4.4      by (simp add: th0 th1)
     4.5  qed
     4.6  
     4.7 -lemma connected_continuous_image:
     4.8 -  assumes "continuous_on s f"
     4.9 -    and "connected s"
    4.10 -  shows "connected(f ` s)"
    4.11 -proof -
    4.12 -  {
    4.13 -    fix T
    4.14 -    assume as:
    4.15 -      "T \<noteq> {}"
    4.16 -      "T \<noteq> f ` s"
    4.17 -      "openin (subtopology euclidean (f ` s)) T"
    4.18 -      "closedin (subtopology euclidean (f ` s)) T"
    4.19 -    have "{x \<in> s. f x \<in> T} = {} \<or> {x \<in> s. f x \<in> T} = s"
    4.20 -      using assms(1)[unfolded continuous_on_open, THEN spec[where x=T]]
    4.21 -      using assms(1)[unfolded continuous_on_closed, THEN spec[where x=T]]
    4.22 -      using assms(2)[unfolded connected_clopen, THEN spec[where x="{x \<in> s. f x \<in> T}"]] as(3,4) by auto
    4.23 -    then have False using as(1,2)
    4.24 -      using as(4)[unfolded closedin_def topspace_euclidean_subtopology] by auto
    4.25 -  }
    4.26 -  then show ?thesis
    4.27 -    unfolding connected_clopen by auto
    4.28 -qed
    4.29 -
    4.30  lemma connected_linear_image:
    4.31    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    4.32    assumes "linear f" and "connected s"
    4.33 @@ -1442,13 +1419,13 @@
    4.34  
    4.35  lemma continuous_closedin_preimage_constant:
    4.36    fixes f :: "_ \<Rightarrow> 'b::t1_space"
    4.37 -  shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
    4.38 -  using continuous_closedin_preimage[of s f "{a}"] by auto
    4.39 +  shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
    4.40 +  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
    4.41  
    4.42  lemma continuous_closed_preimage_constant:
    4.43    fixes f :: "_ \<Rightarrow> 'b::t1_space"
    4.44 -  shows "continuous_on s f \<Longrightarrow> closed s \<Longrightarrow> closed {x \<in> s. f x = a}"
    4.45 -  using continuous_closed_preimage[of s f "{a}"] by auto
    4.46 +  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
    4.47 +  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
    4.48  
    4.49  lemma continuous_constant_on_closure:
    4.50    fixes f :: "_ \<Rightarrow> 'b::t1_space"
    4.51 @@ -1462,17 +1439,17 @@
    4.52      by auto
    4.53  
    4.54  lemma image_closure_subset:
    4.55 -  assumes "continuous_on (closure s) f"
    4.56 -    and "closed t"
    4.57 -    and "(f ` s) \<subseteq> t"
    4.58 -  shows "f ` (closure s) \<subseteq> t"
    4.59 +  assumes contf: "continuous_on (closure S) f"
    4.60 +    and "closed T"
    4.61 +    and "(f ` S) \<subseteq> T"
    4.62 +  shows "f ` (closure S) \<subseteq> T"
    4.63  proof -
    4.64 -  have "s \<subseteq> {x \<in> closure s. f x \<in> t}"
    4.65 +  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
    4.66      using assms(3) closure_subset by auto
    4.67 -  moreover have "closed {x \<in> closure s. f x \<in> t}"
    4.68 -    using continuous_closed_preimage[OF assms(1)] and assms(2) by auto
    4.69 -  ultimately have "closure s = {x \<in> closure s . f x \<in> t}"
    4.70 -    using closure_minimal[of s "{x \<in> closure s. f x \<in> t}"] by auto
    4.71 +  moreover have "closed (closure S \<inter> f -` T)"
    4.72 +    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
    4.73 +  ultimately have "closure S = (closure S \<inter> f -` T)"
    4.74 +    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
    4.75    then show ?thesis by auto
    4.76  qed
    4.77  
    4.78 @@ -1967,7 +1944,7 @@
    4.79  lemma bounded_uniformly_continuous_image:
    4.80    fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
    4.81    assumes "uniformly_continuous_on S f" "bounded S"
    4.82 -  shows "bounded(image f S)"
    4.83 +  shows "bounded(f ` S)"
    4.84    by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
    4.85  
    4.86  subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
    4.87 @@ -2023,61 +2000,61 @@
    4.88  subsection\<open>Quotient maps\<close>
    4.89  
    4.90  lemma quotient_map_imp_continuous_open:
    4.91 -  assumes t: "f ` s \<subseteq> t"
    4.92 -      and ope: "\<And>u. u \<subseteq> t
    4.93 -              \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
    4.94 -                   openin (subtopology euclidean t) u)"
    4.95 -    shows "continuous_on s f"
    4.96 +  assumes T: "f ` S \<subseteq> T"
    4.97 +      and ope: "\<And>U. U \<subseteq> T
    4.98 +              \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
    4.99 +                   openin (subtopology euclidean T) U)"
   4.100 +    shows "continuous_on S f"
   4.101  proof -
   4.102 -  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
   4.103 +  have [simp]: "S \<inter> f -` f ` S = S" by auto
   4.104    show ?thesis
   4.105 -    using ope [OF t]
   4.106 +    using ope [OF T]
   4.107      apply (simp add: continuous_on_open)
   4.108 -    by (metis (no_types, lifting) "ope"  openin_imp_subset openin_trans)
   4.109 +    by (meson ope openin_imp_subset openin_trans)
   4.110  qed
   4.111  
   4.112  lemma quotient_map_imp_continuous_closed:
   4.113 -  assumes t: "f ` s \<subseteq> t"
   4.114 -      and ope: "\<And>u. u \<subseteq> t
   4.115 -                  \<Longrightarrow> (closedin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
   4.116 -                       closedin (subtopology euclidean t) u)"
   4.117 -    shows "continuous_on s f"
   4.118 +  assumes T: "f ` S \<subseteq> T"
   4.119 +      and ope: "\<And>U. U \<subseteq> T
   4.120 +                  \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
   4.121 +                       closedin (subtopology euclidean T) U)"
   4.122 +    shows "continuous_on S f"
   4.123  proof -
   4.124 -  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
   4.125 +  have [simp]: "S \<inter> f -` f ` S = S" by auto
   4.126    show ?thesis
   4.127 -    using ope [OF t]
   4.128 +    using ope [OF T]
   4.129      apply (simp add: continuous_on_closed)
   4.130 -    by (metis (no_types, lifting) "ope" closedin_imp_subset closedin_subtopology_refl closedin_trans openin_subtopology_refl openin_subtopology_self)
   4.131 +    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
   4.132  qed
   4.133  
   4.134  lemma open_map_imp_quotient_map:
   4.135 -  assumes contf: "continuous_on s f"
   4.136 -      and t: "t \<subseteq> f ` s"
   4.137 -      and ope: "\<And>t. openin (subtopology euclidean s) t
   4.138 -                   \<Longrightarrow> openin (subtopology euclidean (f ` s)) (f ` t)"
   4.139 -    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} =
   4.140 -           openin (subtopology euclidean (f ` s)) t"
   4.141 +  assumes contf: "continuous_on S f"
   4.142 +      and T: "T \<subseteq> f ` S"
   4.143 +      and ope: "\<And>T. openin (subtopology euclidean S) T
   4.144 +                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
   4.145 +    shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
   4.146 +           openin (subtopology euclidean (f ` S)) T"
   4.147  proof -
   4.148 -  have "t = image f {x. x \<in> s \<and> f x \<in> t}"
   4.149 -    using t by blast
   4.150 +  have "T = f ` (S \<inter> f -` T)"
   4.151 +    using T by blast
   4.152    then show ?thesis
   4.153 -    using "ope" contf continuous_on_open by fastforce
   4.154 +    using "ope" contf continuous_on_open by metis
   4.155  qed
   4.156  
   4.157  lemma closed_map_imp_quotient_map:
   4.158 -  assumes contf: "continuous_on s f"
   4.159 -      and t: "t \<subseteq> f ` s"
   4.160 -      and ope: "\<And>t. closedin (subtopology euclidean s) t
   4.161 -              \<Longrightarrow> closedin (subtopology euclidean (f ` s)) (f ` t)"
   4.162 -    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} \<longleftrightarrow>
   4.163 -           openin (subtopology euclidean (f ` s)) t"
   4.164 +  assumes contf: "continuous_on S f"
   4.165 +      and T: "T \<subseteq> f ` S"
   4.166 +      and ope: "\<And>T. closedin (subtopology euclidean S) T
   4.167 +              \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
   4.168 +    shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
   4.169 +           openin (subtopology euclidean (f ` S)) T"
   4.170            (is "?lhs = ?rhs")
   4.171  proof
   4.172    assume ?lhs
   4.173 -  then have *: "closedin (subtopology euclidean s) (s - {x \<in> s. f x \<in> t})"
   4.174 +  then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
   4.175      using closedin_diff by fastforce
   4.176 -  have [simp]: "(f ` s - f ` (s - {x \<in> s. f x \<in> t})) = t"
   4.177 -    using t by blast
   4.178 +  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
   4.179 +    using T by blast
   4.180    show ?rhs
   4.181      using ope [OF *, unfolded closedin_def] by auto
   4.182  next
   4.183 @@ -2087,51 +2064,50 @@
   4.184  qed
   4.185  
   4.186  lemma continuous_right_inverse_imp_quotient_map:
   4.187 -  assumes contf: "continuous_on s f" and imf: "f ` s \<subseteq> t"
   4.188 -      and contg: "continuous_on t g" and img: "g ` t \<subseteq> s"
   4.189 -      and fg [simp]: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y"
   4.190 -      and u: "u \<subseteq> t"
   4.191 -    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
   4.192 -           openin (subtopology euclidean t) u"
   4.193 +  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
   4.194 +      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
   4.195 +      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
   4.196 +      and U: "U \<subseteq> T"
   4.197 +    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
   4.198 +           openin (subtopology euclidean T) U"
   4.199            (is "?lhs = ?rhs")
   4.200  proof -
   4.201 -  have f: "\<And>z. openin (subtopology euclidean (f ` s)) z \<Longrightarrow>
   4.202 -                openin (subtopology euclidean s) {x \<in> s. f x \<in> z}"
   4.203 -  and  g: "\<And>z. openin (subtopology euclidean (g ` t)) z \<Longrightarrow>
   4.204 -                openin (subtopology euclidean t) {x \<in> t. g x \<in> z}"
   4.205 +  have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
   4.206 +                openin (subtopology euclidean S) (S \<inter> f -` Z)"
   4.207 +  and  g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
   4.208 +                openin (subtopology euclidean T) (T \<inter> g -` Z)"
   4.209      using contf contg by (auto simp: continuous_on_open)
   4.210    show ?thesis
   4.211    proof
   4.212 -    have "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = {x \<in> t. f (g x) \<in> u}"
   4.213 +    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
   4.214        using imf img by blast
   4.215 -    also have "... = u"
   4.216 -      using u by auto
   4.217 -    finally have [simp]: "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = u" .
   4.218 +    also have "... = U"
   4.219 +      using U by auto
   4.220 +    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
   4.221      assume ?lhs
   4.222 -    then have *: "openin (subtopology euclidean (g ` t)) (g ` t \<inter> {x \<in> s. f x \<in> u})"
   4.223 +    then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
   4.224        by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
   4.225      show ?rhs
   4.226 -      using g [OF *] by simp
   4.227 +      using g [OF *] eq by auto
   4.228    next
   4.229      assume rhs: ?rhs
   4.230      show ?lhs
   4.231 -      apply (rule f)
   4.232 -      by (metis fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
   4.233 +      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
   4.234    qed
   4.235  qed
   4.236  
   4.237  lemma continuous_left_inverse_imp_quotient_map:
   4.238 -  assumes "continuous_on s f"
   4.239 -      and "continuous_on (f ` s) g"
   4.240 -      and  "\<And>x. x \<in> s \<Longrightarrow> g(f x) = x"
   4.241 -      and "u \<subseteq> f ` s"
   4.242 -    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
   4.243 -           openin (subtopology euclidean (f ` s)) u"
   4.244 +  assumes "continuous_on S f"
   4.245 +      and "continuous_on (f ` S) g"
   4.246 +      and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
   4.247 +      and "U \<subseteq> f ` S"
   4.248 +    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
   4.249 +           openin (subtopology euclidean (f ` S)) U"
   4.250  apply (rule continuous_right_inverse_imp_quotient_map)
   4.251 -using assms
   4.252 -apply force+
   4.253 +using assms apply force+
   4.254  done
   4.255  
   4.256 +
   4.257  text \<open>Proving a function is constant by proving that a level set is open\<close>
   4.258  
   4.259  lemma continuous_levelset_openin_cases:
   4.260 @@ -3234,17 +3210,19 @@
   4.261        and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
   4.262      shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
   4.263  proof -
   4.264 -  have s: "s = {t \<in> s. h t \<in> atMost a} \<union> {t \<in> s. h t \<in> atLeast a}"
   4.265 +  have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
   4.266      by force
   4.267 -  have 1: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atMost a}"
   4.268 +  have 1: "closedin (subtopology euclidean s) (s \<inter> h -` atMost a)"
   4.269      by (rule continuous_closedin_preimage [OF h closed_atMost])
   4.270 -  have 2: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atLeast a}"
   4.271 +  have 2: "closedin (subtopology euclidean s) (s \<inter> h -` atLeast a)"
   4.272      by (rule continuous_closedin_preimage [OF h closed_atLeast])
   4.273 +  have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
   4.274 +    by auto
   4.275    show ?thesis
   4.276      apply (rule continuous_on_subset [of s, OF _ order_refl])
   4.277      apply (subst s)
   4.278      apply (rule continuous_on_cases_local)
   4.279 -    using 1 2 s assms apply auto
   4.280 +    using 1 2 s assms apply (auto simp: eq)
   4.281      done
   4.282  qed
   4.283  
   4.284 @@ -3761,7 +3739,7 @@
   4.285  proof -
   4.286    from imf injf have gTS: "g ` T = S"
   4.287      by force
   4.288 -  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
   4.289 +  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
   4.290      by force
   4.291    show ?thesis
   4.292      by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
   4.293 @@ -3776,7 +3754,7 @@
   4.294  proof -
   4.295    from imf injf have gTS: "g ` T = S"
   4.296      by force
   4.297 -  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
   4.298 +  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
   4.299      by force
   4.300    show ?thesis
   4.301      by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
   4.302 @@ -3813,7 +3791,7 @@
   4.303      and oo: "openin (subtopology euclidean S) U"
   4.304    shows "openin (subtopology euclidean T) (f ` U)"
   4.305  proof -
   4.306 -  from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
   4.307 +  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
   4.308      using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   4.309    from hom have "continuous_on T g"
   4.310      unfolding homeomorphism_def by blast
   4.311 @@ -3828,7 +3806,7 @@
   4.312      and oo: "closedin (subtopology euclidean S) U"
   4.313    shows "closedin (subtopology euclidean T) (f ` U)"
   4.314  proof -
   4.315 -  from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
   4.316 +  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
   4.317      using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   4.318    from hom have "continuous_on T g"
   4.319      unfolding homeomorphism_def by blast
   4.320 @@ -4750,17 +4728,263 @@
   4.321  lemma continuous_imp_closed_map:
   4.322    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   4.323    assumes "closedin (subtopology euclidean S) U"
   4.324 -          "continuous_on S f" "image f S = T" "compact S"
   4.325 -    shows "closedin (subtopology euclidean T) (image f U)"
   4.326 +          "continuous_on S f" "f ` S = T" "compact S"
   4.327 +    shows "closedin (subtopology euclidean T) (f ` U)"
   4.328    by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
   4.329  
   4.330  lemma continuous_imp_quotient_map:
   4.331    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   4.332 -  assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
   4.333 -    shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
   4.334 +  assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
   4.335 +    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
   4.336             openin (subtopology euclidean T) U"
   4.337 -  by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
   4.338 -
   4.339 +  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
   4.340 +
   4.341 +
   4.342 +lemma open_map_restrict:
   4.343 +  assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
   4.344 +    and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
   4.345 +    and "T' \<subseteq> T"
   4.346 +  shows "openin (subtopology euclidean T') (f ` U)"
   4.347 +proof -
   4.348 +  obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
   4.349 +    using opeU by (auto simp: openin_open)
   4.350 +  with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
   4.351 +    by (fastforce simp add: openin_open)
   4.352 +qed
   4.353 +
   4.354 +lemma closed_map_restrict:
   4.355 +  assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
   4.356 +    and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
   4.357 +    and "T' \<subseteq> T"
   4.358 +  shows "closedin (subtopology euclidean T') (f ` U)"
   4.359 +proof -
   4.360 +  obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
   4.361 +    using cloU by (auto simp: closedin_closed)
   4.362 +  with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
   4.363 +    by (fastforce simp add: closedin_closed)
   4.364 +qed
   4.365 +
   4.366 +lemma connected_monotone_quotient_preimage:
   4.367 +  assumes "connected T"
   4.368 +      and contf: "continuous_on S f" and fim: "f ` S = T"
   4.369 +      and opT: "\<And>U. U \<subseteq> T
   4.370 +                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
   4.371 +                     openin (subtopology euclidean T) U"
   4.372 +      and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   4.373 +    shows "connected S"
   4.374 +proof (rule connectedI)
   4.375 +  fix U V
   4.376 +  assume "open U" and "open V" and "U \<inter> S \<noteq> {}" and "V \<inter> S \<noteq> {}"
   4.377 +    and "U \<inter> V \<inter> S = {}" and "S \<subseteq> U \<union> V"
   4.378 +  moreover
   4.379 +  have disjoint: "f ` (S \<inter> U) \<inter> f ` (S \<inter> V) = {}"
   4.380 +  proof -
   4.381 +    have False if "y \<in> f ` (S \<inter> U) \<inter> f ` (S \<inter> V)" for y
   4.382 +    proof -
   4.383 +      have "y \<in> T"
   4.384 +        using fim that by blast
   4.385 +      show ?thesis
   4.386 +        using connectedD [OF connT [OF \<open>y \<in> T\<close>] \<open>open U\<close> \<open>open V\<close>]
   4.387 +              \<open>S \<subseteq> U \<union> V\<close> \<open>U \<inter> V \<inter> S = {}\<close> that by fastforce
   4.388 +    qed
   4.389 +    then show ?thesis by blast
   4.390 +  qed
   4.391 +  ultimately have UU: "(S \<inter> f -` f ` (S \<inter> U)) = S \<inter> U" and VV: "(S \<inter> f -` f ` (S \<inter> V)) = S \<inter> V"
   4.392 +    by auto
   4.393 +  have opeU: "openin (subtopology euclidean T) (f ` (S \<inter> U))"
   4.394 +    by (metis UU \<open>open U\<close> fim image_Int_subset le_inf_iff opT openin_open_Int)
   4.395 +  have opeV: "openin (subtopology euclidean T) (f ` (S \<inter> V))"
   4.396 +    by (metis opT fim VV \<open>open V\<close> openin_open_Int image_Int_subset inf.bounded_iff)
   4.397 +  have "T \<subseteq> f ` (S \<inter> U) \<union> f ` (S \<inter> V)"
   4.398 +    using \<open>S \<subseteq> U \<union> V\<close> fim by auto
   4.399 +  then show False
   4.400 +    using \<open>connected T\<close> disjoint opeU opeV \<open>U \<inter> S \<noteq> {}\<close> \<open>V \<inter> S \<noteq> {}\<close>
   4.401 +    by (auto simp: connected_openin)
   4.402 +qed
   4.403 +
   4.404 +lemma connected_open_monotone_preimage:
   4.405 +  assumes contf: "continuous_on S f" and fim: "f ` S = T"
   4.406 +    and ST: "\<And>C. openin (subtopology euclidean S) C \<Longrightarrow> openin (subtopology euclidean T) (f ` C)"
   4.407 +    and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   4.408 +    and "connected C" "C \<subseteq> T"
   4.409 +  shows "connected (S \<inter> f -` C)"
   4.410 +proof -
   4.411 +  have contf': "continuous_on (S \<inter> f -` C) f"
   4.412 +    by (meson contf continuous_on_subset inf_le1)
   4.413 +  have eqC: "f ` (S \<inter> f -` C) = C"
   4.414 +    using \<open>C \<subseteq> T\<close> fim by blast
   4.415 +  show ?thesis
   4.416 +  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
   4.417 +    show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
   4.418 +    proof -
   4.419 +      have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
   4.420 +        using that by blast
   4.421 +      moreover have "connected (S \<inter> f -` {y})"
   4.422 +        using \<open>C \<subseteq> T\<close> connT that by blast
   4.423 +      ultimately show ?thesis
   4.424 +        by metis
   4.425 +    qed
   4.426 +    have "\<And>U. openin (subtopology euclidean (S \<inter> f -` C)) U
   4.427 +               \<Longrightarrow> openin (subtopology euclidean C) (f ` U)"
   4.428 +      using open_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
   4.429 +    then show "\<And>D. D \<subseteq> C
   4.430 +          \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
   4.431 +              openin (subtopology euclidean C) D"
   4.432 +      using open_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
   4.433 +  qed
   4.434 +qed
   4.435 +
   4.436 +
   4.437 +lemma connected_closed_monotone_preimage:
   4.438 +  assumes contf: "continuous_on S f" and fim: "f ` S = T"
   4.439 +    and ST: "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
   4.440 +    and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   4.441 +    and "connected C" "C \<subseteq> T"
   4.442 +  shows "connected (S \<inter> f -` C)"
   4.443 +proof -
   4.444 +  have contf': "continuous_on (S \<inter> f -` C) f"
   4.445 +    by (meson contf continuous_on_subset inf_le1)
   4.446 +  have eqC: "f ` (S \<inter> f -` C) = C"
   4.447 +    using \<open>C \<subseteq> T\<close> fim by blast
   4.448 +  show ?thesis
   4.449 +  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
   4.450 +    show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
   4.451 +    proof -
   4.452 +      have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
   4.453 +        using that by blast
   4.454 +      moreover have "connected (S \<inter> f -` {y})"
   4.455 +        using \<open>C \<subseteq> T\<close> connT that by blast
   4.456 +      ultimately show ?thesis
   4.457 +        by metis
   4.458 +    qed
   4.459 +    have "\<And>U. closedin (subtopology euclidean (S \<inter> f -` C)) U
   4.460 +               \<Longrightarrow> closedin (subtopology euclidean C) (f ` U)"
   4.461 +      using closed_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
   4.462 +    then show "\<And>D. D \<subseteq> C
   4.463 +          \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
   4.464 +              openin (subtopology euclidean C) D"
   4.465 +      using closed_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
   4.466 +  qed
   4.467 +qed
   4.468 +
   4.469 +
   4.470 +
   4.471 +subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
   4.472 +
   4.473 +
   4.474 +lemma connected_Un_clopen_in_complement:
   4.475 +  fixes S U :: "'a::metric_space set"
   4.476 +  assumes "connected S" "connected U" "S \<subseteq> U" 
   4.477 +      and opeT: "openin (subtopology euclidean (U - S)) T" 
   4.478 +      and cloT: "closedin (subtopology euclidean (U - S)) T"
   4.479 +    shows "connected (S \<union> T)"
   4.480 +proof -
   4.481 +  have *: "\<lbrakk>\<And>x y. P x y \<longleftrightarrow> P y x; \<And>x y. P x y \<Longrightarrow> S \<subseteq> x \<or> S \<subseteq> y;
   4.482 +            \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> ~(\<exists>x y. (P x y))" for P
   4.483 +    by metis
   4.484 +  show ?thesis
   4.485 +    unfolding connected_closedin_eq
   4.486 +  proof (rule *)
   4.487 +    fix H1 H2
   4.488 +    assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and> 
   4.489 +               closedin (subtopology euclidean (S \<union> T)) H2 \<and>
   4.490 +               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
   4.491 +    then have clo: "closedin (subtopology euclidean S) (S \<inter> H1)"
   4.492 +                   "closedin (subtopology euclidean S) (S \<inter> H2)"
   4.493 +      by (metis Un_upper1 closedin_closed_subset inf_commute)+
   4.494 +    have Seq: "S \<inter> (H1 \<union> H2) = S"
   4.495 +      by (simp add: H)
   4.496 +    have "S \<inter> ((S \<union> T) \<inter> H1) \<union> S \<inter> ((S \<union> T) \<inter> H2) = S"
   4.497 +      using Seq by auto
   4.498 +    moreover have "H1 \<inter> (S \<inter> ((S \<union> T) \<inter> H2)) = {}"
   4.499 +      using H by blast
   4.500 +    ultimately have "S \<inter> H1 = {} \<or> S \<inter> H2 = {}"
   4.501 +      by (metis (no_types) H Int_assoc \<open>S \<inter> (H1 \<union> H2) = S\<close> \<open>connected S\<close>
   4.502 +          clo Seq connected_closedin inf_bot_right inf_le1)
   4.503 +    then show "S \<subseteq> H1 \<or> S \<subseteq> H2"
   4.504 +      using H \<open>connected S\<close> unfolding connected_closedin by blast
   4.505 +  next
   4.506 +    fix H1 H2
   4.507 +    assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and>
   4.508 +               closedin (subtopology euclidean (S \<union> T)) H2 \<and>
   4.509 +               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}" 
   4.510 +       and "S \<subseteq> H1"
   4.511 +    then have H2T: "H2 \<subseteq> T"
   4.512 +      by auto
   4.513 +    have "T \<subseteq> U"
   4.514 +      using Diff_iff opeT openin_imp_subset by auto
   4.515 +    with \<open>S \<subseteq> U\<close> have Ueq: "U = (U - S) \<union> (S \<union> T)" 
   4.516 +      by auto
   4.517 +    have "openin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
   4.518 +    proof (rule openin_subtopology_Un)
   4.519 +      show "openin (subtopology euclidean (S \<union> T)) H2"
   4.520 +        using \<open>H2 \<subseteq> T\<close> apply (auto simp: openin_closedin_eq)
   4.521 +        by (metis Diff_Diff_Int Diff_disjoint Diff_partition Diff_subset H Int_absorb1 Un_Diff)
   4.522 +      then show "openin (subtopology euclidean (U - S)) H2"
   4.523 +        by (meson H2T Un_upper2 opeT openin_subset_trans openin_trans)
   4.524 +    qed
   4.525 +    moreover have "closedin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
   4.526 +    proof (rule closedin_subtopology_Un)
   4.527 +      show "closedin (subtopology euclidean (U - S)) H2"
   4.528 +        using H H2T cloT closedin_subset_trans 
   4.529 +        by (blast intro: closedin_subtopology_Un closedin_trans)
   4.530 +    qed (simp add: H)
   4.531 +    ultimately
   4.532 +    have H2: "H2 = {} \<or> H2 = U"
   4.533 +      using Ueq \<open>connected U\<close> unfolding connected_clopen by metis   
   4.534 +    then have "H2 \<subseteq> S"
   4.535 +      by (metis Diff_partition H Un_Diff_cancel Un_subset_iff \<open>H2 \<subseteq> T\<close> assms(3) inf.orderE opeT openin_imp_subset)
   4.536 +    moreover have "T \<subseteq> H2 - S"
   4.537 +      by (metis (no_types) H2 H opeT openin_closedin_eq topspace_euclidean_subtopology)
   4.538 +    ultimately show False
   4.539 +      using H \<open>S \<subseteq> H1\<close> by blast
   4.540 +  qed blast
   4.541 +qed
   4.542 +
   4.543 +
   4.544 +proposition component_complement_connected:
   4.545 +  fixes S :: "'a::metric_space set"
   4.546 +  assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
   4.547 +  shows "connected(U - C)"
   4.548 +  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
   4.549 +proof clarify
   4.550 +  fix H3 H4 
   4.551 +  assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
   4.552 +    and clo4: "closedin (subtopology euclidean (U - C)) H4" 
   4.553 +    and "H3 \<union> H4 = U - C" and "H3 \<inter> H4 = {}" and "H3 \<noteq> {}" and "H4 \<noteq> {}"
   4.554 +    and * [rule_format]:
   4.555 +    "\<forall>H1 H2. \<not> closedin (subtopology euclidean S) H1 \<or>
   4.556 +                      \<not> closedin (subtopology euclidean S) H2 \<or>
   4.557 +                      H1 \<union> H2 \<noteq> S \<or> H1 \<inter> H2 \<noteq> {} \<or> \<not> H1 \<noteq> {} \<or> \<not> H2 \<noteq> {}"
   4.558 +  then have "H3 \<subseteq> U-C" and ope3: "openin (subtopology euclidean (U - C)) (U - C - H3)"
   4.559 +    and "H4 \<subseteq> U-C" and ope4: "openin (subtopology euclidean (U - C)) (U - C - H4)"
   4.560 +    by (auto simp: closedin_def)
   4.561 +  have "C \<noteq> {}" "C \<subseteq> U-S" "connected C"
   4.562 +    using C in_components_nonempty in_components_subset in_components_maximal by blast+
   4.563 +  have cCH3: "connected (C \<union> H3)"
   4.564 +  proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo3])
   4.565 +    show "openin (subtopology euclidean (U - C)) H3"
   4.566 +      apply (simp add: openin_closedin_eq \<open>H3 \<subseteq> U - C\<close>)
   4.567 +      apply (simp add: closedin_subtopology)
   4.568 +      by (metis Diff_cancel Diff_triv Un_Diff clo4 \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> closedin_closed inf_commute sup_bot.left_neutral)
   4.569 +  qed (use clo3 \<open>C \<subseteq> U - S\<close> in auto)
   4.570 +  have cCH4: "connected (C \<union> H4)"
   4.571 +  proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo4])
   4.572 +    show "openin (subtopology euclidean (U - C)) H4"
   4.573 +      apply (simp add: openin_closedin_eq \<open>H4 \<subseteq> U - C\<close>)
   4.574 +      apply (simp add: closedin_subtopology)
   4.575 +      by (metis Diff_cancel Int_commute Un_Diff Un_Diff_Int \<open>H3 \<inter> H4 = {}\<close> \<open>H3 \<union> H4 = U - C\<close> clo3 closedin_closed)
   4.576 +  qed (use clo4 \<open>C \<subseteq> U - S\<close> in auto)
   4.577 +  have "closedin (subtopology euclidean S) (S \<inter> H3)" "closedin (subtopology euclidean S) (S \<inter> H4)"
   4.578 +    using clo3 clo4 \<open>S \<subseteq> U\<close> \<open>C \<subseteq> U - S\<close> by (auto simp: closedin_closed)
   4.579 +  moreover have "S \<inter> H3 \<noteq> {}"      
   4.580 +    using components_maximal [OF C cCH3] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<noteq> {}\<close> \<open>H3 \<subseteq> U - C\<close> by auto
   4.581 +  moreover have "S \<inter> H4 \<noteq> {}"
   4.582 +    using components_maximal [OF C cCH4] \<open>C \<noteq> {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H4 \<noteq> {}\<close> \<open>H4 \<subseteq> U - C\<close> by auto
   4.583 +  ultimately show False
   4.584 +    using * [of "S \<inter> H3" "S \<inter> H4"] \<open>H3 \<inter> H4 = {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<union> H4 = U - C\<close> \<open>S \<subseteq> U\<close> 
   4.585 +    by auto
   4.586 +qed
   4.587  
   4.588  subsection\<open> Finite intersection property\<close>
   4.589  
   4.590 @@ -4952,15 +5176,12 @@
   4.591    assume "open U"
   4.592    have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
   4.593      using clo openin_imp_subset by blast
   4.594 -  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
   4.595 -    apply (auto simp: dest: S)
   4.596 -      apply (metis (no_types, lifting) g mem_Collect_eq)
   4.597 -    using clo f g openin_imp_subset by fastforce
   4.598 -  show "openin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
   4.599 +  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
   4.600 +    using S f g by fastforce
   4.601 +  show "openin (subtopology euclidean S) (S \<inter> g -` U)"
   4.602      apply (subst *)
   4.603      apply (rule openin_Union, clarify)
   4.604 -    apply (metis (full_types) \<open>open U\<close> cont clo openin_trans continuous_openin_preimage_gen)
   4.605 -    done
   4.606 +    using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
   4.607  qed
   4.608  
   4.609  lemma pasting_lemma_exists:
   4.610 @@ -4996,13 +5217,11 @@
   4.611  proof (clarsimp simp: continuous_closedin_preimage_eq)
   4.612    fix U :: "'b set"
   4.613    assume "closed U"
   4.614 -  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
   4.615 -    apply auto
   4.616 -    apply (metis (no_types, lifting) g mem_Collect_eq)
   4.617 -    using clo closedin_closed apply blast
   4.618 -    apply (metis Int_iff f g clo closedin_limpt inf.absorb_iff2)
   4.619 -    done
   4.620 -  show "closedin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
   4.621 +  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
   4.622 +    using clo closedin_imp_subset by blast
   4.623 +  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
   4.624 +    using S f g by fastforce
   4.625 +  show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
   4.626      apply (subst *)
   4.627      apply (rule closedin_Union)
   4.628      using \<open>finite I\<close> apply simp
   4.629 @@ -5119,9 +5338,10 @@
   4.630        and conf: "continuous_on S f"
   4.631        and fim: "f ` S \<subseteq> t"
   4.632        and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
   4.633 -    shows "\<exists>a. \<forall>x \<in> S. f x = a"
   4.634 +    shows "f constant_on S"
   4.635  proof (cases "S = {}")
   4.636 -  case True then show ?thesis by force
   4.637 +  case True then show ?thesis
   4.638 +    by (simp add: constant_on_def)
   4.639  next
   4.640    case False
   4.641    { fix x assume "x \<in> S"
   4.642 @@ -5129,7 +5349,7 @@
   4.643      by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   4.644    }
   4.645    with False show ?thesis
   4.646 -    by blast
   4.647 +    unfolding constant_on_def by blast
   4.648  qed
   4.649  
   4.650  lemma discrete_subset_disconnected:
   4.651 @@ -5195,7 +5415,7 @@
   4.652  text\<open>This proof requires the existence of two separate values of the range type.\<close>
   4.653  lemma finite_range_constant_imp_connected:
   4.654    assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   4.655 -              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
   4.656 +              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S"
   4.657      shows "connected S"
   4.658  proof -
   4.659    { fix t u
   4.660 @@ -5212,7 +5432,7 @@
   4.661        by (rule finite_subset [of _ "{0,1}"]) auto
   4.662      have "t = {} \<or> u = {}"
   4.663        using assms [OF conif fi] tus [symmetric]
   4.664 -      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
   4.665 +      by (auto simp: Ball_def constant_on_def) (metis IntI empty_iff one_neq_zero tue)
   4.666    }
   4.667    then show ?thesis
   4.668      by (simp add: connected_closedin_eq)
   4.669 @@ -5222,18 +5442,18 @@
   4.670        "(connected S \<longleftrightarrow>
   4.671             (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   4.672              \<forall>t. continuous_on S f \<and> f ` S \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
   4.673 -            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis1)
   4.674 +            \<longrightarrow> f constant_on S))" (is ?thesis1)
   4.675    and continuous_discrete_range_constant_eq:
   4.676        "(connected S \<longleftrightarrow>
   4.677           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   4.678            continuous_on S f \<and>
   4.679            (\<forall>x \<in> S. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> S \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
   4.680 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis2)
   4.681 +          \<longrightarrow> f constant_on S))" (is ?thesis2)
   4.682    and continuous_finite_range_constant_eq:
   4.683        "(connected S \<longleftrightarrow>
   4.684           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   4.685            continuous_on S f \<and> finite (f ` S)
   4.686 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis3)
   4.687 +          \<longrightarrow> f constant_on S))" (is ?thesis3)
   4.688  proof -
   4.689    have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
   4.690      \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
   4.691 @@ -5255,18 +5475,16 @@
   4.692    assumes S: "connected S"
   4.693        and "continuous_on S f"
   4.694        and "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> S \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   4.695 -    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
   4.696 -  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms
   4.697 -  by blast
   4.698 +    shows "f constant_on S"
   4.699 +  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast
   4.700  
   4.701  lemma continuous_finite_range_constant:
   4.702    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   4.703    assumes "connected S"
   4.704        and "continuous_on S f"
   4.705        and "finite (f ` S)"
   4.706 -    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
   4.707 -  using assms continuous_finite_range_constant_eq
   4.708 -  by blast
   4.709 +    shows "f constant_on S"
   4.710 +  using assms continuous_finite_range_constant_eq  by blast
   4.711  
   4.712  
   4.713  
     5.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Tue Oct 17 13:56:58 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Thu Oct 19 17:16:01 2017 +0100
     5.3 @@ -281,10 +281,7 @@
     5.4            "\<And>x. f x \<in> closed_segment a b"
     5.5            "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
     5.6            "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
     5.7 -apply (rule Urysohn_local_strong [of UNIV S T])
     5.8 -using assms
     5.9 -apply (auto simp: closed_closedin)
    5.10 -done
    5.11 +using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
    5.12  
    5.13  proposition Urysohn:
    5.14    assumes US: "closed S"
    5.15 @@ -295,10 +292,7 @@
    5.16            "\<And>x. f x \<in> closed_segment a b"
    5.17            "\<And>x. x \<in> S \<Longrightarrow> f x = a"
    5.18            "\<And>x. x \<in> T \<Longrightarrow> f x = b"
    5.19 -apply (rule Urysohn_local [of UNIV S T a b])
    5.20 -using assms
    5.21 -apply (auto simp: closed_closedin)
    5.22 -done
    5.23 +using assms by (auto intro: Urysohn_local [of UNIV S T a b])
    5.24  
    5.25  
    5.26  subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
     6.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 17 13:56:58 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Oct 19 17:16:01 2017 +0100
     6.3 @@ -1271,15 +1271,17 @@
     6.4      using g by (simp add: image_comp)
     6.5    have cgf: "closed (g ` f ` S)"
     6.6      by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
     6.7 -  have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
     6.8 -    using g by (simp add: o_def id_def image_def) metis
     6.9 +  have [simp]: "(range f \<inter> g -` S) = f ` S"
    6.10 +    using g unfolding o_def id_def image_def by auto metis+
    6.11    show ?thesis
    6.12 -    apply (rule closedin_closed_trans [of "range f"])
    6.13 -    apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
    6.14 -    apply (rule closed_injective_image_subspace)
    6.15 -    using f
    6.16 -    apply (auto simp: linear_linear linear_injective_0)
    6.17 -    done
    6.18 +  proof (rule closedin_closed_trans [of "range f"])
    6.19 +    show "closedin (subtopology euclidean (range f)) (f ` S)"
    6.20 +      using continuous_closedin_preimage [OF confg cgf] by simp
    6.21 +    show "closed (range f)"
    6.22 +      apply (rule closed_injective_image_subspace)
    6.23 +      using f apply (auto simp: linear_linear linear_injective_0)
    6.24 +      done
    6.25 +  qed
    6.26  qed
    6.27  
    6.28  lemma closed_injective_linear_image_eq:
    6.29 @@ -2374,16 +2376,13 @@
    6.30    by(simp add: convex_connected)
    6.31  
    6.32  proposition clopen:
    6.33 -  fixes s :: "'a :: real_normed_vector set"
    6.34 -  shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
    6.35 -apply (rule iffI)
    6.36 - apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
    6.37 - apply (force simp add: closed_closedin, force)
    6.38 -done
    6.39 +  fixes S :: "'a :: real_normed_vector set"
    6.40 +  shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
    6.41 +    by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
    6.42  
    6.43  corollary compact_open:
    6.44 -  fixes s :: "'a :: euclidean_space set"
    6.45 -  shows "compact s \<and> open s \<longleftrightarrow> s = {}"
    6.46 +  fixes S :: "'a :: euclidean_space set"
    6.47 +  shows "compact S \<and> open S \<longleftrightarrow> S = {}"
    6.48    by (auto simp: compact_eq_bounded_closed clopen)
    6.49  
    6.50  corollary finite_imp_not_open:
     7.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 17 13:56:58 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Thu Oct 19 17:16:01 2017 +0100
     7.3 @@ -2318,9 +2318,9 @@
     7.4  proof (clarsimp simp add: continuous_openin_preimage_eq)
     7.5    fix T :: "'a set"
     7.6    assume "open T"
     7.7 -  have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
     7.8 +  have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
     7.9      by (auto simp: gf)
    7.10 -  show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
    7.11 +  show "openin (subtopology euclidean (f ` S)) (f ` S \<inter> g -` T)"
    7.12      apply (subst eq)
    7.13      apply (rule open_openin_trans)
    7.14        apply (rule invariance_of_domain_gen)
    7.15 @@ -3173,7 +3173,7 @@
    7.16    have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
    7.17      using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
    7.18    have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
    7.19 -               (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
    7.20 +               (\<exists>v. \<Union>v = -{0} \<inter> (\<lambda>z. z ^ n) -` T \<and>
    7.21                      (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
    7.22                      pairwise disjnt v \<and>
    7.23                      (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
    7.24 @@ -3216,8 +3216,6 @@
    7.25        by (intro continuous_intros)
    7.26      have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
    7.27        by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
    7.28 -    have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
    7.29 -      by (rule invariance_of_domain [OF cont open_ball inj])
    7.30      have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
    7.31                  if z': "z'^n = z^n" for z'
    7.32      proof -
    7.33 @@ -3262,6 +3260,7 @@
    7.34        qed
    7.35        then show ?thesis by blast
    7.36      qed
    7.37 +
    7.38      have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
    7.39                    if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
    7.40      proof -
    7.41 @@ -3286,50 +3285,63 @@
    7.42          apply (simp add: dist_norm)
    7.43          done
    7.44      qed
    7.45 -    have ball1: "\<Union>{ball z' d |z'. z'^n = z^n} = {x. x \<noteq> 0 \<and> x^n \<in> (\<lambda>w. w^n) ` ball z d}"
    7.46 -      apply (rule equalityI)
    7.47 -       prefer 2 apply (force simp: ex_ball, clarsimp)
    7.48 -      apply (subst im_eq [symmetric], assumption)
    7.49 -      using assms
    7.50 -      apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
    7.51 -      done
    7.52 -    have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
    7.53 -    proof (clarsimp simp add: pairwise_def disjnt_iff)
    7.54 -      fix \<xi> \<zeta> x
    7.55 -      assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
    7.56 -         and "dist \<xi> x < d" "dist \<zeta> x < d"
    7.57 -      then have "dist \<xi> \<zeta> < d+d"
    7.58 -        using dist_triangle_less_add by blast
    7.59 -      then have "cmod (\<xi> - \<zeta>) < 2*d"
    7.60 -        by (simp add: dist_norm)
    7.61 -      also have "... \<le> e * cmod z"
    7.62 -        using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
    7.63 -      finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
    7.64 -      with e have "\<xi> = \<zeta>"
    7.65 -        by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
    7.66 -      then show "False"
    7.67 -        using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
    7.68 +
    7.69 +    show ?thesis
    7.70 +    proof (rule exI, intro conjI)
    7.71 +      show "z ^ n \<in> (\<lambda>w. w ^ n) ` ball z d"
    7.72 +        using \<open>d > 0\<close> by simp
    7.73 +      show "open ((\<lambda>w. w ^ n) ` ball z d)"
    7.74 +        by (rule invariance_of_domain [OF cont open_ball inj])
    7.75 +      show "0 \<notin> (\<lambda>w. w ^ n) ` ball z d"
    7.76 +        using \<open>z \<noteq> 0\<close> assms by (force simp: d_def)
    7.77 +      show "\<exists>v. \<Union>v = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d \<and>
    7.78 +                (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
    7.79 +                disjoint v \<and>
    7.80 +                (\<forall>u\<in>v. Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n)))"
    7.81 +      proof (rule exI, intro ballI conjI)
    7.82 +        show "\<Union>{ball z' d |z'. z'^n = z^n} = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d" (is "?l = ?r")
    7.83 +        proof 
    7.84 +          show "?l \<subseteq> ?r"
    7.85 +            apply auto
    7.86 +             apply (simp add: assms d_def power_eq_imp_eq_norm that)
    7.87 +            by (metis im_eq image_eqI mem_ball)
    7.88 +          show "?r \<subseteq> ?l"
    7.89 +            by auto (meson ex_ball)
    7.90 +        qed
    7.91 +        show "\<And>u. u \<in> {ball z' d |z'. z' ^ n = z ^ n} \<Longrightarrow> 0 \<notin> u"
    7.92 +          by (force simp add: assms d_def power_eq_imp_eq_norm that)
    7.93 +
    7.94 +        show "disjoint {ball z' d |z'. z' ^ n = z ^ n}"
    7.95 +        proof (clarsimp simp add: pairwise_def disjnt_iff)
    7.96 +          fix \<xi> \<zeta> x
    7.97 +          assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
    7.98 +            and "dist \<xi> x < d" "dist \<zeta> x < d"
    7.99 +          then have "dist \<xi> \<zeta> < d+d"
   7.100 +            using dist_triangle_less_add by blast
   7.101 +          then have "cmod (\<xi> - \<zeta>) < 2*d"
   7.102 +            by (simp add: dist_norm)
   7.103 +          also have "... \<le> e * cmod z"
   7.104 +            using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
   7.105 +          finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
   7.106 +          with e have "\<xi> = \<zeta>"
   7.107 +            by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
   7.108 +          then show "False"
   7.109 +            using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
   7.110 +        qed
   7.111 +        show "Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
   7.112 +          if "u \<in> {ball z' d |z'. z' ^ n = z ^ n}" for u
   7.113 +        proof (rule invariance_of_domain_homeomorphism [of "u" "\<lambda>z. z^n"])
   7.114 +          show "open u"
   7.115 +            using that by auto
   7.116 +          show "continuous_on u (\<lambda>z. z ^ n)"
   7.117 +            by (intro continuous_intros)
   7.118 +          show "inj_on (\<lambda>z. z ^ n) u"
   7.119 +            using that by (auto simp: iff_x_eq_y inj_on_def)
   7.120 +          show "\<And>g. homeomorphism u ((\<lambda>z. z ^ n) ` u) (\<lambda>z. z ^ n) g \<Longrightarrow> Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
   7.121 +            using im_eq that by clarify metis
   7.122 +        qed auto
   7.123 +      qed auto
   7.124      qed
   7.125 -    have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
   7.126 -            if zeq: "z'^n = z^n" for z'
   7.127 -    proof -
   7.128 -      have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
   7.129 -        by (meson iff_x_eq_y inj_onI zeq)
   7.130 -      show ?thesis
   7.131 -        apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
   7.132 -          apply (rule open_ball continuous_intros order_refl inj)+
   7.133 -        apply (force simp: im_eq [OF zeq])
   7.134 -        done
   7.135 -    qed
   7.136 -    show ?thesis
   7.137 -      apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
   7.138 -      apply (intro conjI open_imball)
   7.139 -        using \<open>d > 0\<close> apply simp
   7.140 -       using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
   7.141 -      apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
   7.142 -      apply (intro conjI ball1 ball2)
   7.143 -       apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
   7.144 -      by (metis ball3)
   7.145    qed
   7.146    show ?thesis
   7.147      using assms
   7.148 @@ -3353,7 +3365,7 @@
   7.149    show "range exp = - {0::complex}"
   7.150      by auto (metis exp_Ln range_eqI)
   7.151    show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
   7.152 -             (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
   7.153 +             (\<exists>v. \<Union>v = exp -` T \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
   7.154                    (\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
   7.155          if "z \<in> - {0::complex}" for z
   7.156    proof -
   7.157 @@ -3374,8 +3386,8 @@
   7.158          using pi_ge_two by (simp add: ball_subset_ball_iff)
   7.159        ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
   7.160          by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
   7.161 -      show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
   7.162 -        by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
   7.163 +      show "\<Union>\<V> = exp -` exp ` ball (Ln z) 1"
   7.164 +        by (force simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
   7.165        show "\<forall>V\<in>\<V>. open V"
   7.166          by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
   7.167        have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
   7.168 @@ -4314,7 +4326,7 @@
   7.169      qed
   7.170    next
   7.171      case False
   7.172 -    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
   7.173 +    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
   7.174      proof (rule continuous_discrete_range_constant [OF ST])
   7.175        show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
   7.176          apply (intro continuous_intros)
   7.177 @@ -4338,7 +4350,9 @@
   7.178          then show ?thesis
   7.179            by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
   7.180        qed
   7.181 -    qed blast
   7.182 +    qed 
   7.183 +    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
   7.184 +      by (auto simp: constant_on_def)
   7.185      with False have "exp a = 1"
   7.186        by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
   7.187      with a show ?thesis
   7.188 @@ -4382,7 +4396,7 @@
   7.189      qed
   7.190    next
   7.191      case False
   7.192 -    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
   7.193 +    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
   7.194      proof (rule continuous_discrete_range_constant [OF ST])
   7.195        show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
   7.196          apply (intro continuous_intros)
   7.197 @@ -4406,7 +4420,9 @@
   7.198          then show ?thesis
   7.199            by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
   7.200        qed
   7.201 -    qed blast
   7.202 +    qed
   7.203 +    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
   7.204 +      by (auto simp: constant_on_def)
   7.205      with False have "exp a = 1"
   7.206        by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
   7.207      with a show ?thesis
   7.208 @@ -4441,7 +4457,7 @@
   7.209      using fim by auto
   7.210    then obtain f' where f': "\<And>y. y \<in> T \<longrightarrow> f' y \<in> S \<and> f (f' y) = y"
   7.211      by metis
   7.212 -  have *: "\<exists>a. \<forall>x \<in> {x. x \<in> S \<and> f x = y}. h x - h(f' y) = a" if "y \<in> T" for y
   7.213 +  have *: "(\<lambda>x. h x - h(f' y)) constant_on {x. x \<in> S \<and> f x = y}" if "y \<in> T" for y
   7.214    proof (rule continuous_discrete_range_constant [OF conn [OF that], of "\<lambda>x. h x - h (f' y)"], simp_all add: algebra_simps)
   7.215      show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
   7.216        by (intro continuous_intros continuous_on_subset [OF conth]) auto
   7.217 @@ -4462,13 +4478,12 @@
   7.218      qed
   7.219    qed 
   7.220    have "h x = h (f' (f x))" if "x \<in> S" for x
   7.221 -    using * [of "f x"] fim that apply clarsimp
   7.222 -    by (metis f' imageI right_minus_eq)
   7.223 +    using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
   7.224    moreover have "\<And>x. x \<in> T \<Longrightarrow> \<exists>u. u \<in> S \<and> x = f u \<and> h (f' x) = h u"
   7.225      using f' by fastforce
   7.226    ultimately
   7.227    have eq: "((\<lambda>x. (x, (h \<circ> f') x)) ` T) =
   7.228 -            {p. \<exists>x. x \<in> S \<and> (x, p) \<in> {z \<in> S \<times> UNIV. snd z - ((f \<circ> fst) z, (h \<circ> fst) z) \<in> {0}}}"
   7.229 +            {p. \<exists>x. x \<in> S \<and> (x, p) \<in> (S \<times> UNIV) \<inter> ((\<lambda>z. snd z - ((f \<circ> fst) z, (h \<circ> fst) z)) -` {0})}"
   7.230      using fim by (auto simp: image_iff)
   7.231    show "\<exists>h. continuous_on T h \<and> (\<forall>x\<in>T. g x = exp (h x))"
   7.232    proof (intro exI conjI)
   7.233 @@ -4513,9 +4528,10 @@
   7.234      proof (rule compact_continuous_image)
   7.235        show "continuous_on {x \<in> S. f x = y} h"
   7.236          by (rule continuous_on_subset [OF conth]) auto
   7.237 -      have "compact {x \<in> S. f x \<in> {y}}"
   7.238 +      have "compact (S \<inter> f -` {y})"
   7.239          by (rule proper_map_from_compact [OF contf _ \<open>compact S\<close>, of T]) (simp_all add: fim that)
   7.240 -      then show "compact {x \<in> S. f x = y}" by simp
   7.241 +      then show "compact {x \<in> S. f x = y}" 
   7.242 +        by (auto simp: vimage_def Int_def)
   7.243      qed
   7.244      have 2: "h ` {x \<in> S. f x = y} \<noteq> {}"
   7.245        using fim that by auto
     8.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Oct 17 13:56:58 2017 +0200
     8.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Oct 19 17:16:01 2017 +0100
     8.3 @@ -3187,17 +3187,15 @@
     8.4    proof -
     8.5      have "e * r > 0" using that \<open>0 < r\<close> by simp
     8.6      with intfi[unfolded has_integral]
     8.7 -    obtain d where d: "gauge d"
     8.8 -                   "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
     8.9 +    obtain d where "gauge d"
    8.10 +               and d: "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
    8.11                          \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e * r" 
    8.12        by metis
    8.13 -    define d' where "d' x = {y. g y \<in> d (g x)}" for x
    8.14 -    have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
    8.15 -      unfolding d'_def ..
    8.16 +    define d' where "d' x = g -` d (g x)" for x
    8.17      show ?thesis
    8.18      proof (rule_tac x=d' in exI, safe)
    8.19        show "gauge d'"
    8.20 -        using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
    8.21 +        using \<open>gauge d\<close> continuous_open_vimage[OF _ contg] by (auto simp: gauge_def d'_def)
    8.22      next
    8.23        fix p
    8.24        assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
    8.25 @@ -3211,7 +3209,7 @@
    8.26          show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
    8.27            using ptag by auto
    8.28          show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
    8.29 -          using finep unfolding fine_def d' by auto
    8.30 +          using finep unfolding fine_def d'_def by auto
    8.31        next
    8.32          fix x k
    8.33          assume xk: "(x, k) \<in> p"
    8.34 @@ -3259,7 +3257,7 @@
    8.35          using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
    8.36        finally have eq: "?l = ?r" .
    8.37        show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
    8.38 -        using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
    8.39 +        using d[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
    8.40      qed
    8.41    qed
    8.42    then show ?thesis
    8.43 @@ -4229,7 +4227,7 @@
    8.44      and "x \<in> S"
    8.45    shows "f x = y"
    8.46  proof -
    8.47 -  have xx: "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}" if "x \<in> S" for x
    8.48 +  have "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})" if "x \<in> S" for x
    8.49    proof -
    8.50      obtain e where "0 < e" and e: "ball x e \<subseteq> S"
    8.51        using \<open>x \<in> S\<close> \<open>open S\<close> open_contains_ball by blast
    8.52 @@ -4248,15 +4246,15 @@
    8.53            by (metis Diff_iff contra_subsetD derf e has_derivative_within_subset that)
    8.54        qed (use y e \<open>0 < e\<close> in auto)
    8.55      qed
    8.56 -    then show "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}"
    8.57 +    then show "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})"
    8.58        using \<open>0 < e\<close> by blast
    8.59    qed
    8.60 -  then have "openin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
    8.61 +  then have "openin (subtopology euclidean S) (S \<inter> f -` {y})"
    8.62      by (auto intro!: open_openin_trans[OF \<open>open S\<close>] simp: open_contains_ball)
    8.63 -  moreover have "closedin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
    8.64 +  moreover have "closedin (subtopology euclidean S) (S \<inter> f -` {y})"
    8.65      by (force intro!: continuous_closedin_preimage [OF contf])
    8.66 -  ultimately have "{x \<in> S. f x \<in> {y}} = {} \<or> {x \<in> S. f x \<in> {y}} = S"
    8.67 -    using \<open>connected S\<close> connected_clopen by blast
    8.68 +  ultimately have "(S \<inter> f -` {y}) = {} \<or> (S \<inter> f -` {y}) = S"
    8.69 +    using \<open>connected S\<close> by (simp add: connected_clopen)
    8.70    then show ?thesis
    8.71      using \<open>x \<in> S\<close> \<open>f c = y\<close> \<open>c \<in> S\<close> by auto
    8.72  qed
     9.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 17 13:56:58 2017 +0200
     9.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Oct 19 17:16:01 2017 +0100
     9.3 @@ -1089,14 +1089,14 @@
     9.4        by force
     9.5      have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
     9.6        by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
     9.7 -    have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
     9.8 +    have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
     9.9        apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
    9.10        apply (rule_tac x=a in image_eqI)
    9.11        apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
    9.12        done
    9.13      then have clfU: "closed (f ` U)"
    9.14        apply (rule ssubst)
    9.15 -      apply (rule continuous_closed_preimage_univ)
    9.16 +      apply (rule continuous_closed_vimage)
    9.17        apply (auto intro: continuous_intros cont [unfolded o_def])
    9.18        done
    9.19      have "closed (f ` S)"
    9.20 @@ -1278,7 +1278,7 @@
    9.21    "covering_space c p S \<equiv>
    9.22         continuous_on c p \<and> p ` c = S \<and>
    9.23         (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
    9.24 -                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
    9.25 +                    (\<exists>v. \<Union>v = c \<inter> p -` T \<and>
    9.26                          (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
    9.27                          pairwise disjnt v \<and>
    9.28                          (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
    9.29 @@ -1302,16 +1302,16 @@
    9.30                        "homeomorphism T u p q"
    9.31  using assms
    9.32  apply (simp add: covering_space_def, clarify)
    9.33 -apply (drule_tac x="p x" in bspec, force)
    9.34 -by (metis (no_types, lifting) Union_iff mem_Collect_eq)
    9.35 +  apply (drule_tac x="p x" in bspec, force)
    9.36 +  by (metis IntI UnionE vimage_eq) 
    9.37  
    9.38  
    9.39  lemma covering_space_local_homeomorphism_alt:
    9.40    assumes p: "covering_space c p S" and "y \<in> S"
    9.41 -  obtains x T u q where "p x = y"
    9.42 +  obtains x T U q where "p x = y"
    9.43                          "x \<in> T" "openin (subtopology euclidean c) T"
    9.44 -                        "y \<in> u" "openin (subtopology euclidean S) u"
    9.45 -                          "homeomorphism T u p q"
    9.46 +                        "y \<in> U" "openin (subtopology euclidean S) U"
    9.47 +                          "homeomorphism T U p q"
    9.48  proof -
    9.49    obtain x where "p x = y" "x \<in> c"
    9.50      using assms covering_space_imp_surjective by blast
    9.51 @@ -1329,7 +1329,7 @@
    9.52     and covs:
    9.53         "\<And>x. x \<in> S \<Longrightarrow>
    9.54              \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
    9.55 -                  \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
    9.56 +                  \<Union>VS = c \<inter> p -` X \<and>
    9.57                    (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
    9.58                    pairwise disjnt VS \<and>
    9.59                    (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
    9.60 @@ -1340,7 +1340,7 @@
    9.61    proof -
    9.62      have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
    9.63      obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
    9.64 -                  and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
    9.65 +                  and VS: "\<Union>VS = c \<inter> p -` U"
    9.66                    and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
    9.67                    and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
    9.68        using covs [OF \<open>y \<in> S\<close>] by auto
    9.69 @@ -1349,16 +1349,16 @@
    9.70        using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
    9.71      with VS obtain V where "x \<in> V" "V \<in> VS" by auto
    9.72      then obtain q where q: "homeomorphism V U p q" using homVS by blast
    9.73 -    then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
    9.74 +    then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)"
    9.75        using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
    9.76      have ocv: "openin (subtopology euclidean c) V"
    9.77        by (simp add: \<open>V \<in> VS\<close> openVS)
    9.78 -    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
    9.79 +    have "openin (subtopology euclidean U) (U \<inter> q -` (T \<inter> V))"
    9.80        apply (rule continuous_on_open [THEN iffD1, rule_format])
    9.81         using homeomorphism_def q apply blast
    9.82        using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
    9.83        by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
    9.84 -    then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
    9.85 +    then have os: "openin (subtopology euclidean S) (U \<inter> q -` (T \<inter> V))"
    9.86        using openin_trans [of U] by (simp add: Collect_conj_eq U)
    9.87      show ?thesis
    9.88        apply (rule_tac x = "p ` (T \<inter> V)" in exI)
    9.89 @@ -1400,20 +1400,19 @@
    9.90         using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
    9.91        done
    9.92      have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
    9.93 -    have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
    9.94 +    have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g
    9.95        by auto
    9.96      have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
    9.97        using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
    9.98 -    then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
    9.99 +    then have 1: "openin (subtopology euclidean U) (U \<inter> g1 -` v)"
   9.100        unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
   9.101      have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
   9.102        using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
   9.103 -    then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
   9.104 +    then have 2: "openin (subtopology euclidean U) (U \<inter> g2 -` v)"
   9.105        unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
   9.106 -    show "\<exists>T. openin (subtopology euclidean U) T \<and>
   9.107 -              z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
   9.108 +    show "\<exists>T. openin (subtopology euclidean U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
   9.109        using z
   9.110 -      apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI)
   9.111 +      apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI)
   9.112        apply (intro conjI)
   9.113        apply (rule openin_Int [OF 1 2])
   9.114        using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
   9.115 @@ -1475,7 +1474,7 @@
   9.116        by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
   9.117      then obtain T \<V> where "p x \<in> T"
   9.118                        and opeT: "openin (subtopology euclidean S) T"
   9.119 -                      and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}"
   9.120 +                      and veq: "\<Union>\<V> = C \<inter> p -` T"
   9.121                        and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
   9.122                        and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
   9.123        using cov unfolding covering_space_def by (blast intro: that)
   9.124 @@ -1583,7 +1582,7 @@
   9.125          if "y \<in> U" for y
   9.126    proof -
   9.127      obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s) \<and>
   9.128 -                                        (\<exists>\<V>. \<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU s)} \<and>
   9.129 +                                        (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and>
   9.130                                              (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
   9.131                                              pairwise disjnt \<V> \<and>
   9.132                                              (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))"
   9.133 @@ -1595,13 +1594,13 @@
   9.134      proof -
   9.135        have hinS: "h (t, y) \<in> S"
   9.136          using \<open>y \<in> U\<close> him that by blast
   9.137 -      then have "(t,y) \<in> {z \<in> {0..1} \<times> U. h z \<in> UU (h (t, y))}"
   9.138 +      then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))"
   9.139          using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close>  by (auto simp: ope)
   9.140 -      moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) {z. z \<in> ({0..1} \<times> U) \<and> h z \<in> UU(h(t, y))}"
   9.141 +      moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
   9.142          using hinS ope continuous_on_open_gen [OF him] conth by blast
   9.143        ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V"
   9.144                                and opeW: "open W" and "y \<in> U" "y \<in> W"
   9.145 -                              and VW: "({0..1} \<inter> V) \<times> (U \<inter> W)  \<subseteq> {z. z \<in> ({0..1} \<times> U) \<and> h z \<in> UU(h(t, y))}"
   9.146 +                              and VW: "({0..1} \<inter> V) \<times> (U \<inter> W)  \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
   9.147          by (rule Times_in_interior_subtopology) (auto simp: openin_open)
   9.148        then show ?thesis
   9.149          using hinS by blast
   9.150 @@ -1677,7 +1676,7 @@
   9.151        qed blast
   9.152        have t01: "t \<in> {0..1}"
   9.153          using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
   9.154 -      obtain \<V> where "\<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU (X t))}"
   9.155 +      obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)"
   9.156                   and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (subtopology euclidean C) U"
   9.157                   and "pairwise disjnt \<V>"
   9.158                   and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
   9.159 @@ -1686,7 +1685,7 @@
   9.160          using N by (auto simp: divide_simps algebra_simps)
   9.161        with t have nN_in_kkt: "real n / real N \<in> K t"
   9.162          by blast
   9.163 -      have "k (real n / real N, y) \<in> {x. x \<in> C \<and> p x \<in> (UU (X t))}"
   9.164 +      have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
   9.165        proof (simp, rule conjI)
   9.166          show "k (real n / real N, y) \<in> C"
   9.167            using \<open>y \<in> V\<close> kim keq by force
   9.168 @@ -1701,8 +1700,8 @@
   9.169            using him t01 by blast
   9.170          finally show "p (k (real n / real N, y)) \<in> UU (X t)" .
   9.171        qed
   9.172 -      then have "k (real n / real N, y) \<in> \<Union>\<V>"
   9.173 -        using \<open>\<Union>\<V> = {x \<in> C. p x \<in> UU (X t)}\<close> by blast
   9.174 +      with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>"
   9.175 +        by blast
   9.176        then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>"
   9.177          by blast
   9.178        then obtain p' where opeC': "openin (subtopology euclidean C) W"
   9.179 @@ -1711,14 +1710,14 @@
   9.180        then have "W \<subseteq> C"
   9.181          using openin_imp_subset by blast
   9.182        define W' where "W' = UU(X t)"
   9.183 -      have opeVW: "openin (subtopology euclidean V) {z \<in> V. (k \<circ> Pair (real n / real N)) z \<in> W}"
   9.184 +      have opeVW: "openin (subtopology euclidean V) (V \<inter> (k \<circ> Pair (n / N)) -` W)"
   9.185          apply (rule continuous_openin_preimage [OF _ _ opeC'])
   9.186           apply (intro continuous_intros continuous_on_subset [OF contk])
   9.187          using kim apply (auto simp: \<open>y \<in> V\<close> W)
   9.188          done
   9.189        obtain N' where opeUN': "openin (subtopology euclidean U) N'"
   9.190                    and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W"
   9.191 -        apply (rule_tac N' = "{z \<in> V. (k \<circ> Pair ((real n / real N))) z \<in> W}" in that)
   9.192 +        apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that)
   9.193          apply (fastforce simp:  \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+
   9.194          done
   9.195        obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q"
   9.196 @@ -2283,7 +2282,7 @@
   9.197        using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
   9.198      show LC: "l ` U \<subseteq> C"
   9.199        by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
   9.200 -    have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> {x \<in> U. l x \<in> X}"
   9.201 +    have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X"
   9.202           if X: "openin (subtopology euclidean C) X" and "y \<in> U" "l y \<in> X" for X y
   9.203      proof -
   9.204        have "X \<subseteq> C"
   9.205 @@ -2292,7 +2291,7 @@
   9.206          using fim \<open>y \<in> U\<close> by blast
   9.207        then obtain W \<V>
   9.208                where WV: "f y \<in> W \<and> openin (subtopology euclidean S) W \<and>
   9.209 -                         (\<Union>\<V> = {x. x \<in> C \<and> p x \<in> W} \<and>
   9.210 +                         (\<Union>\<V> = C \<inter> p -` W \<and>
   9.211                            (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
   9.212                            pairwise disjnt \<V> \<and>
   9.213                            (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))"
   9.214 @@ -2309,12 +2308,12 @@
   9.215        obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U"
   9.216                   and "path_connected V" and opeUV: "openin (subtopology euclidean U) V"
   9.217        proof -
   9.218 -        have "openin (subtopology euclidean U) {c \<in> U. f c \<in> W}"
   9.219 +        have "openin (subtopology euclidean U) (U \<inter> f -` W)"
   9.220            using WV contf continuous_on_open_gen fim by auto
   9.221          then show ?thesis
   9.222            using U WV
   9.223            apply (auto simp: locally_path_connected)
   9.224 -          apply (drule_tac x="{x. x \<in> U \<and> f x \<in> W}" in spec)
   9.225 +          apply (drule_tac x="U \<inter> f -` W" in spec)
   9.226            apply (drule_tac x=y in spec)
   9.227            apply (auto simp: \<open>y \<in> U\<close> intro: that)
   9.228            done
   9.229 @@ -2325,23 +2324,23 @@
   9.230          using homUW' homeomorphism_image2 by fastforce
   9.231        show ?thesis
   9.232        proof (intro exI conjI)
   9.233 -        have "openin (subtopology euclidean S) {x \<in> W. p' x \<in> W' \<inter> X}"
   9.234 +        have "openin (subtopology euclidean S) (W \<inter> p' -` (W' \<inter> X))"
   9.235          proof (rule openin_trans)
   9.236 -          show "openin (subtopology euclidean W) {x \<in> W. p' x \<in> W' \<inter> X}"
   9.237 +          show "openin (subtopology euclidean W) (W \<inter> p' -` (W' \<inter> X))"
   9.238              apply (rule continuous_openin_preimage [OF contp' p'im])
   9.239              using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open)
   9.240              done
   9.241            show "openin (subtopology euclidean S) W"
   9.242              using WV by blast
   9.243          qed
   9.244 -        then show "openin (subtopology euclidean U) (V \<inter> {x. x \<in> U \<and> f x \<in> {x. x \<in> W \<and> p' x \<in> W' \<inter> X}})"
   9.245 -          by (intro openin_Int opeUV continuous_openin_preimage [OF contf fim])
   9.246 -        have "p' (f y) \<in> X"
   9.247 +        then show "openin (subtopology euclidean U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))"
   9.248 +          by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim])
   9.249 +         have "p' (f y) \<in> X"
   9.250            using \<open>l y \<in> W'\<close> homeomorphism_apply1 [OF homUW'] pleq \<open>y \<in> U\<close> \<open>l y \<in> X\<close> by fastforce
   9.251 -        then show "y \<in> V \<inter> {x \<in> U. f x \<in> {x \<in> W. p' x \<in> W' \<inter> X}}"
   9.252 +        then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))"
   9.253            using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto
   9.254 -        show "V \<inter> {x \<in> U. f x \<in> {x \<in> W. p' x \<in> W' \<inter> X}} \<subseteq> {x \<in> U. l x \<in> X}"
   9.255 -        proof clarsimp
   9.256 +        show "V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X))) \<subseteq> U \<inter> l -` X"
   9.257 +        proof (intro subsetI IntI; clarify)
   9.258            fix y'
   9.259            assume y': "y' \<in> V" "y' \<in> U" "f y' \<in> W" "p' (f y') \<in> W'" "p' (f y') \<in> X"
   9.260            then obtain \<gamma> where "path \<gamma>" "path_image \<gamma> \<subseteq> V" "pathstart \<gamma> = y" "pathfinish \<gamma> = y'"
   9.261 @@ -2354,7 +2353,7 @@
   9.262            have finW: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> f (\<gamma> x) \<in> W"
   9.263              using \<open>path_image \<gamma> \<subseteq> V\<close> by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
   9.264            have "pathfinish (qq +++ (p' \<circ> f \<circ> \<gamma>)) = l y'"
   9.265 -          proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)" ])
   9.266 +          proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)"])
   9.267              show "path (pp +++ \<gamma>)"
   9.268                by (simp add: \<open>path \<gamma>\<close> \<open>path pp\<close> \<open>pathfinish pp = y\<close> \<open>pathstart \<gamma> = y\<close>)
   9.269              show "path_image (pp +++ \<gamma>) \<subseteq> U"
   9.270 @@ -2395,14 +2394,13 @@
   9.271                  using that \<xi> by auto
   9.272              qed
   9.273            qed
   9.274 -          with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "l y' \<in> X"
   9.275 +          with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "y' \<in> l -` X"
   9.276              unfolding pathfinish_join by (simp add: pathfinish_def)
   9.277          qed
   9.278        qed
   9.279      qed
   9.280      then show "continuous_on U l"
   9.281 -      using openin_subopen continuous_on_open_gen [OF LC]
   9.282 -      by (metis (no_types, lifting) mem_Collect_eq)
   9.283 +      by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
   9.284    qed
   9.285  qed
   9.286  
    10.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Tue Oct 17 13:56:58 2017 +0200
    10.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Thu Oct 19 17:16:01 2017 +0100
    10.3 @@ -88,8 +88,10 @@
    10.4        then show ?thesis
    10.5          by (rule_tac x="2*pi" in exI) auto
    10.6      qed
    10.7 -    ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
    10.8 +    ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
    10.9        using continuous_discrete_range_constant [OF conST contgh] by blast
   10.10 +    then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
   10.11 +      by (auto simp: constant_on_def)
   10.12      obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
   10.13        using disc z False
   10.14        by auto (metis diff_add_cancel g h of_real_add)
    11.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Oct 17 13:56:58 2017 +0200
    11.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Oct 19 17:16:01 2017 +0100
    11.3 @@ -1546,7 +1546,7 @@
    11.4      by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
    11.5    ultimately show False
    11.6      using *[unfolded connected_local not_ex, rule_format,
    11.7 -      of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
    11.8 +      of "{0..1} \<inter> g -` e1" "{0..1} \<inter> g -` e2"]
    11.9      using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
   11.10      using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
   11.11      by auto
   11.12 @@ -4946,58 +4946,57 @@
   11.13  proposition homeomorphism_locally_imp:
   11.14    fixes S :: "'a::metric_space set" and t :: "'b::t2_space set"
   11.15    assumes S: "locally P S" and hom: "homeomorphism S t f g"
   11.16 -      and Q: "\<And>S t. \<lbrakk>P S; homeomorphism S t f g\<rbrakk> \<Longrightarrow> Q t"
   11.17 +      and Q: "\<And>S S'. \<lbrakk>P S; homeomorphism S S' f g\<rbrakk> \<Longrightarrow> Q S'"
   11.18      shows "locally Q t"
   11.19  proof (clarsimp simp: locally_def)
   11.20 -  fix w y
   11.21 -  assume "y \<in> w" and "openin (subtopology euclidean t) w"
   11.22 -  then obtain T where T: "open T" "w = t \<inter> T"
   11.23 +  fix W y
   11.24 +  assume "y \<in> W" and "openin (subtopology euclidean t) W"
   11.25 +  then obtain T where T: "open T" "W = t \<inter> T"
   11.26      by (force simp: openin_open)
   11.27 -  then have "w \<subseteq> t" by auto
   11.28 +  then have "W \<subseteq> t" by auto
   11.29    have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f"
   11.30     and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g"
   11.31      using hom by (auto simp: homeomorphism_def)
   11.32 -  have gw: "g ` w = S \<inter> {x. f x \<in> w}"
   11.33 -    using \<open>w \<subseteq> t\<close>
   11.34 +  have gw: "g ` W = S \<inter> f -` W"
   11.35 +    using \<open>W \<subseteq> t\<close>
   11.36      apply auto
   11.37 -    using \<open>g ` t = S\<close> \<open>w \<subseteq> t\<close> apply blast
   11.38 -    using g \<open>w \<subseteq> t\<close> apply auto[1]
   11.39 +    using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
   11.40 +    using g \<open>W \<subseteq> t\<close> apply auto[1]
   11.41      by (simp add: f rev_image_eqI)
   11.42 -  have o: "openin (subtopology euclidean S) (g ` w)"
   11.43 +  have o: "openin (subtopology euclidean S) (g ` W)"
   11.44    proof -
   11.45      have "continuous_on S f"
   11.46        using f(3) by blast
   11.47 -    then show "openin (subtopology euclidean S) (g ` w)"
   11.48 -      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) w\<close> continuous_on_open f(2))
   11.49 +    then show "openin (subtopology euclidean S) (g ` W)"
   11.50 +      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) W\<close> continuous_on_open f(2))
   11.51    qed
   11.52    then obtain u v
   11.53 -    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` w"
   11.54 -    using S [unfolded locally_def, rule_format, of "g ` w" "g y"] \<open>y \<in> w\<close> by force
   11.55 +    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
   11.56 +    using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
   11.57    have "v \<subseteq> S" using uv by (simp add: gw)
   11.58    have fv: "f ` v = t \<inter> {x. g x \<in> v}"
   11.59      using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto
   11.60 -  have "f ` v \<subseteq> w"
   11.61 +  have "f ` v \<subseteq> W"
   11.62      using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
   11.63    have contvf: "continuous_on v f"
   11.64      using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
   11.65    have contvg: "continuous_on (f ` v) g"
   11.66 -    using \<open>f ` v \<subseteq> w\<close> \<open>w \<subseteq> t\<close> continuous_on_subset g(3) by blast
   11.67 +    using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset g(3) by blast
   11.68    have homv: "homeomorphism v (f ` v) f g"
   11.69 -    using \<open>v \<subseteq> S\<close> \<open>w \<subseteq> t\<close> f
   11.70 +    using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
   11.71      apply (simp add: homeomorphism_def contvf contvg, auto)
   11.72      by (metis f(1) rev_image_eqI rev_subsetD)
   11.73 -  have 1: "openin (subtopology euclidean t) {x \<in> t. g x \<in> u}"
   11.74 +  have 1: "openin (subtopology euclidean t) (t \<inter> g -` u)"
   11.75      apply (rule continuous_on_open [THEN iffD1, rule_format])
   11.76      apply (rule \<open>continuous_on t g\<close>)
   11.77      using \<open>g ` t = S\<close> apply (simp add: osu)
   11.78      done
   11.79 -  have 2: "\<exists>v. Q v \<and> y \<in> {x \<in> t. g x \<in> u} \<and> {x \<in> t. g x \<in> u} \<subseteq> v \<and> v \<subseteq> w"
   11.80 +  have 2: "\<exists>V. Q V \<and> y \<in> (t \<inter> g -` u) \<and> (t \<inter> g -` u) \<subseteq> V \<and> V \<subseteq> W"
   11.81      apply (rule_tac x="f ` v" in exI)
   11.82      apply (intro conjI Q [OF \<open>P v\<close> homv])
   11.83 -    using \<open>w \<subseteq> t\<close> \<open>y \<in> w\<close>  \<open>f ` v \<subseteq> w\<close>  uv  apply (auto simp: fv)
   11.84 +    using \<open>W \<subseteq> t\<close> \<open>y \<in> W\<close>  \<open>f ` v \<subseteq> W\<close>  uv  apply (auto simp: fv)
   11.85      done
   11.86 -  show "\<exists>u. openin (subtopology euclidean t) u \<and>
   11.87 -            (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
   11.88 +  show "\<exists>U. openin (subtopology euclidean t) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
   11.89      by (meson 1 2)
   11.90  qed
   11.91  
   11.92 @@ -5057,22 +5056,21 @@
   11.93        and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
   11.94      shows "locally Q (f ` S)"
   11.95  proof (clarsimp simp add: locally_def)
   11.96 -  fix w y
   11.97 -  assume oiw: "openin (subtopology euclidean (f ` S)) w" and "y \<in> w"
   11.98 -  then have "w \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
   11.99 -  have oivf: "openin (subtopology euclidean S) {x \<in> S. f x \<in> w}"
  11.100 +  fix W y
  11.101 +  assume oiw: "openin (subtopology euclidean (f ` S)) W" and "y \<in> W"
  11.102 +  then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
  11.103 +  have oivf: "openin (subtopology euclidean S) (S \<inter> f -` W)"
  11.104      by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
  11.105    then obtain x where "x \<in> S" "f x = y"
  11.106 -    using \<open>w \<subseteq> f ` S\<close> \<open>y \<in> w\<close> by blast
  11.107 -  then obtain u v
  11.108 -    where "openin (subtopology euclidean S) u" "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> {x \<in> S. f x \<in> w}"
  11.109 -    using P [unfolded locally_def, rule_format, of "{x. x \<in> S \<and> f x \<in> w}" x] oivf \<open>y \<in> w\<close>
  11.110 +    using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
  11.111 +  then obtain U V
  11.112 +    where "openin (subtopology euclidean S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
  11.113 +    using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
  11.114      by auto
  11.115 -  then show "\<exists>u. openin (subtopology euclidean (f ` S)) u \<and>
  11.116 -            (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
  11.117 -    apply (rule_tac x="f ` u" in exI)
  11.118 +  then show "\<exists>X. openin (subtopology euclidean (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
  11.119 +    apply (rule_tac x="f ` U" in exI)
  11.120      apply (rule conjI, blast intro!: oo)
  11.121 -    apply (rule_tac x="f ` v" in exI)
  11.122 +    apply (rule_tac x="f ` V" in exI)
  11.123      apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q)
  11.124      done
  11.125  qed
  11.126 @@ -6087,7 +6085,7 @@
  11.127  proposition locally_connected_quotient_image:
  11.128    assumes lcS: "locally connected S"
  11.129        and oo: "\<And>T. T \<subseteq> f ` S
  11.130 -                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
  11.131 +                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
  11.132                      openin (subtopology euclidean (f ` S)) T"
  11.133      shows "locally connected (f ` S)"
  11.134  proof (clarsimp simp: locally_connected_open_component)
  11.135 @@ -6096,53 +6094,53 @@
  11.136    then have "C \<subseteq> U" "U \<subseteq> f ` S"
  11.137      by (meson in_components_subset openin_imp_subset)+
  11.138    then have "openin (subtopology euclidean (f ` S)) C \<longleftrightarrow>
  11.139 -             openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
  11.140 +             openin (subtopology euclidean S) (S \<inter> f -` C)"
  11.141      by (auto simp: oo)
  11.142 -  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
  11.143 +  moreover have "openin (subtopology euclidean S) (S \<inter> f -` C)"
  11.144    proof (subst openin_subopen, clarify)
  11.145      fix x
  11.146      assume "x \<in> S" "f x \<in> C"
  11.147 -    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> C}"
  11.148 +    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` C)"
  11.149      proof (intro conjI exI)
  11.150 -      show "openin (subtopology euclidean S) (connected_component_set {w \<in> S. f w \<in> U} x)"
  11.151 +      show "openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
  11.152        proof (rule ccontr)
  11.153 -        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set {a \<in> S. f a \<in> U} x)"
  11.154 -        then have "x \<notin> {a \<in> S. f a \<in> U}"
  11.155 +        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
  11.156 +        then have "x \<notin> (S \<inter> f -` U)"
  11.157            using \<open>U \<subseteq> f ` S\<close> opefSU lcS locally_connected_2 oo by blast
  11.158          with ** show False
  11.159            by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen)
  11.160        qed
  11.161      next
  11.162 -      show "x \<in> connected_component_set {w \<in> S. f w \<in> U} x"
  11.163 +      show "x \<in> connected_component_set (S \<inter> f -` U) x"
  11.164          using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by auto
  11.165      next
  11.166        have contf: "continuous_on S f"
  11.167          by (simp add: continuous_on_open oo openin_imp_subset)
  11.168 -      then have "continuous_on (connected_component_set {w \<in> S. f w \<in> U} x) f"
  11.169 +      then have "continuous_on (connected_component_set (S \<inter> f -` U) x) f"
  11.170          apply (rule continuous_on_subset)
  11.171          using connected_component_subset apply blast
  11.172          done
  11.173 -      then have "connected (f ` connected_component_set {w \<in> S. f w \<in> U} x)"
  11.174 +      then have "connected (f ` connected_component_set (S \<inter> f -` U) x)"
  11.175          by (rule connected_continuous_image [OF _ connected_connected_component])
  11.176 -      moreover have "f ` connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
  11.177 +      moreover have "f ` connected_component_set (S \<inter> f -` U) x \<subseteq> U"
  11.178          using connected_component_in by blast
  11.179 -      moreover have "C \<inter> f ` connected_component_set {w \<in> S. f w \<in> U} x \<noteq> {}"
  11.180 +      moreover have "C \<inter> f ` connected_component_set (S \<inter> f -` U) x \<noteq> {}"
  11.181          using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by fastforce
  11.182 -      ultimately have fC: "f ` (connected_component_set {w \<in> S. f w \<in> U} x) \<subseteq> C"
  11.183 +      ultimately have fC: "f ` (connected_component_set (S \<inter> f -` U) x) \<subseteq> C"
  11.184          by (rule components_maximal [OF \<open>C \<in> components U\<close>])
  11.185 -      have cUC: "connected_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> C}"
  11.186 +      have cUC: "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)"
  11.187          using connected_component_subset fC by blast
  11.188 -      have "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> connected_component_set {w \<in> S. f w \<in> C} x"
  11.189 +      have "connected_component_set (S \<inter> f -` U) x \<subseteq> connected_component_set (S \<inter> f -` C) x"
  11.190        proof -
  11.191 -        { assume "x \<in> connected_component_set {a \<in> S. f a \<in> U} x"
  11.192 +        { assume "x \<in> connected_component_set (S \<inter> f -` U) x"
  11.193            then have ?thesis
  11.194 -            by (simp add: cUC connected_component_maximal) }
  11.195 +            using cUC connected_component_idemp connected_component_mono by blast }
  11.196          then show ?thesis
  11.197            using connected_component_eq_empty by auto
  11.198        qed
  11.199 -      also have "... \<subseteq> {w \<in> S. f w \<in> C}"
  11.200 +      also have "... \<subseteq> (S \<inter> f -` C)"
  11.201          by (rule connected_component_subset)
  11.202 -      finally show "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> C}" .
  11.203 +      finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
  11.204      qed
  11.205    qed
  11.206    ultimately show "openin (subtopology euclidean (f ` S)) C"
  11.207 @@ -6153,8 +6151,7 @@
  11.208  proposition locally_path_connected_quotient_image:
  11.209    assumes lcS: "locally path_connected S"
  11.210        and oo: "\<And>T. T \<subseteq> f ` S
  11.211 -                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
  11.212 -                    openin (subtopology euclidean (f ` S)) T"
  11.213 +                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
  11.214      shows "locally path_connected (f ` S)"
  11.215  proof (clarsimp simp: locally_path_connected_open_path_component)
  11.216    fix U y
  11.217 @@ -6162,62 +6159,62 @@
  11.218    then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
  11.219      by (meson path_component_subset openin_imp_subset)+
  11.220    then have "openin (subtopology euclidean (f ` S)) (path_component_set U y) \<longleftrightarrow>
  11.221 -             openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
  11.222 +             openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
  11.223    proof -
  11.224      have "path_component_set U y \<subseteq> f ` S"
  11.225        using \<open>U \<subseteq> f ` S\<close> \<open>path_component_set U y \<subseteq> U\<close> by blast
  11.226      then show ?thesis
  11.227        using oo by blast
  11.228    qed
  11.229 -  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
  11.230 +  moreover have "openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
  11.231    proof (subst openin_subopen, clarify)
  11.232      fix x
  11.233      assume "x \<in> S" and Uyfx: "path_component U y (f x)"
  11.234      then have "f x \<in> U"
  11.235        using path_component_mem by blast
  11.236 -    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> path_component_set U y}"
  11.237 +    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` path_component_set U y)"
  11.238      proof (intro conjI exI)
  11.239 -      show "openin (subtopology euclidean S) (path_component_set {w \<in> S. f w \<in> U} x)"
  11.240 +      show "openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
  11.241        proof (rule ccontr)
  11.242 -        assume **: "\<not> openin (subtopology euclidean S) (path_component_set {a \<in> S. f a \<in> U} x)"
  11.243 -        then have "x \<notin> {a \<in> S. f a \<in> U}"
  11.244 +        assume **: "\<not> openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
  11.245 +        then have "x \<notin> (S \<inter> f -` U)"
  11.246            by (metis (no_types, lifting) \<open>U \<subseteq> f ` S\<close> opefSU lcS oo locally_path_connected_open_path_component)
  11.247          then show False
  11.248            using ** \<open>path_component_set U y \<subseteq> U\<close>  \<open>x \<in> S\<close> \<open>path_component U y (f x)\<close> by blast
  11.249        qed
  11.250      next
  11.251 -      show "x \<in> path_component_set {w \<in> S. f w \<in> U} x"
  11.252 -        by (metis (no_types, lifting) \<open>x \<in> S\<close> IntD2 Int_Collect \<open>path_component U y (f x)\<close> path_component_mem(2) path_component_refl)
  11.253 +      show "x \<in> path_component_set (S \<inter> f -` U) x"
  11.254 +        by (simp add: \<open>f x \<in> U\<close> \<open>x \<in> S\<close> path_component_refl)
  11.255      next
  11.256        have contf: "continuous_on S f"
  11.257          by (simp add: continuous_on_open oo openin_imp_subset)
  11.258 -      then have "continuous_on (path_component_set {w \<in> S. f w \<in> U} x) f"
  11.259 +      then have "continuous_on (path_component_set (S \<inter> f -` U) x) f"
  11.260          apply (rule continuous_on_subset)
  11.261          using path_component_subset apply blast
  11.262          done
  11.263 -      then have "path_connected (f ` path_component_set {w \<in> S. f w \<in> U} x)"
  11.264 -        by (simp add: path_connected_continuous_image path_connected_path_component)
  11.265 -      moreover have "f ` path_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
  11.266 +      then have "path_connected (f ` path_component_set (S \<inter> f -` U) x)"
  11.267 +        by (simp add: path_connected_continuous_image)
  11.268 +      moreover have "f ` path_component_set (S \<inter> f -` U) x \<subseteq> U"
  11.269          using path_component_mem by fastforce
  11.270 -      moreover have "f x \<in> f ` path_component_set {w \<in> S. f w \<in> U} x"
  11.271 +      moreover have "f x \<in> f ` path_component_set (S \<inter> f -` U) x"
  11.272          by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
  11.273 -      ultimately have "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U (f x)"
  11.274 +      ultimately have "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U (f x)"
  11.275          by (meson path_component_maximal)
  11.276         also have  "... \<subseteq> path_component_set U y"
  11.277 -        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym path_connected_path_component)
  11.278 -      finally have fC: "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U y" .
  11.279 -      have cUC: "path_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> path_component_set U y}"
  11.280 +        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
  11.281 +      finally have fC: "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U y" .
  11.282 +      have cUC: "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)"
  11.283          using path_component_subset fC by blast
  11.284 -      have "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> path_component_set {w \<in> S. f w \<in> path_component_set U y} x"
  11.285 +      have "path_component_set (S \<inter> f -` U) x \<subseteq> path_component_set (S \<inter> f -` path_component_set U y) x"
  11.286        proof -
  11.287 -        have "\<And>a. path_component_set (path_component_set {a \<in> S. f a \<in> U} x) a \<subseteq> path_component_set {a \<in> S. f a \<in> path_component_set U y} a"
  11.288 +        have "\<And>a. path_component_set (path_component_set (S \<inter> f -` U) x) a \<subseteq> path_component_set (S \<inter> f -` path_component_set U y) a"
  11.289            using cUC path_component_mono by blast
  11.290          then show ?thesis
  11.291            using path_component_path_component by blast
  11.292        qed
  11.293 -      also have "... \<subseteq> {w \<in> S. f w \<in> path_component_set U y}"
  11.294 +      also have "... \<subseteq> (S \<inter> f -` path_component_set U y)"
  11.295          by (rule path_component_subset)
  11.296 -      finally show "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> path_component_set U y}" .
  11.297 +      finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
  11.298      qed
  11.299    qed
  11.300    ultimately show "openin (subtopology euclidean (f ` S)) (path_component_set U y)"
  11.301 @@ -6234,13 +6231,10 @@
  11.302  proof (clarsimp simp: continuous_openin_preimage_eq)
  11.303    fix t :: "'b set"
  11.304    assume "open t"
  11.305 -  have "{x. x \<in> S \<and> f x \<in> t} = \<Union>{{x. x \<in> c \<and> f x \<in> t} |c. c \<in> components S}"
  11.306 -    apply auto
  11.307 -    apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
  11.308 -    using Union_components by blast
  11.309 -  then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
  11.310 -    using \<open>open t\<close> assms
  11.311 -    by (fastforce intro: openin_trans continuous_openin_preimage_gen)
  11.312 +  have *: "S \<inter> f -` t = (\<Union>c \<in> components S. c \<inter> f -` t)"
  11.313 +    by auto
  11.314 +  show "openin (subtopology euclidean S) (S \<inter> f -` t)"
  11.315 +    unfolding * using \<open>open t\<close> assms continuous_openin_preimage_gen openin_trans openin_Union by blast
  11.316  qed
  11.317  
  11.318  lemma continuous_on_components:
  11.319 @@ -6308,11 +6302,9 @@
  11.320  proof -
  11.321    have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
  11.322      apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
  11.323 -    using S apply (simp add: closed_closedin)
  11.324 -    using c apply (simp add: Compl_eq_Diff_UNIV)
  11.325 +    using S c apply (simp_all add: Compl_eq_Diff_UNIV)
  11.326      done
  11.327 -  then show ?thesis
  11.328 -    by (simp add: closed_closedin)
  11.329 +  then show ?thesis by simp
  11.330  qed
  11.331  
  11.332  lemma closedin_Un_complement_component:
    12.1 --- a/src/HOL/Analysis/Starlike.thy	Tue Oct 17 13:56:58 2017 +0200
    12.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Oct 19 17:16:01 2017 +0100
    12.3 @@ -4973,10 +4973,16 @@
    12.4  
    12.5  lemma setdist_eq_0_closedin:
    12.6    fixes S :: "'a::euclidean_space set"
    12.7 -  shows "\<lbrakk>closedin (subtopology euclidean u) S; x \<in> u\<rbrakk>
    12.8 +  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
    12.9           \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
   12.10    by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
   12.11  
   12.12 +lemma setdist_gt_0_closedin:
   12.13 +  fixes S :: "'a::euclidean_space set"
   12.14 +  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
   12.15 +         \<Longrightarrow> setdist {x} S > 0"
   12.16 +  using less_eq_real_def setdist_eq_0_closedin by fastforce
   12.17 +
   12.18  subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
   12.19  
   12.20  lemma hyperplane_eq_Ex:
   12.21 @@ -5089,25 +5095,19 @@
   12.22    have contf: "continuous_on U f"
   12.23      unfolding f_def by (intro continuous_intros)
   12.24    show ?thesis
   12.25 -  proof (rule_tac S' = "{x\<in>U. f x > 0}" and T' = "{x\<in>U. f x < 0}" in that)
   12.26 -    show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
   12.27 +  proof (rule_tac S' = "(U \<inter> f -` {0<..})" and T' = "(U \<inter> f -` {..<0})" in that)
   12.28 +    show "(U \<inter> f -` {0<..}) \<inter> (U \<inter> f -` {..<0}) = {}"
   12.29        by auto
   12.30 -    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
   12.31 -      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
   12.32 -    then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
   12.33 -  next
   12.34 -    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
   12.35 +    show "openin (subtopology euclidean U) (U \<inter> f -` {0<..})"
   12.36        by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
   12.37 -    then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
   12.38 +  next
   12.39 +    show "openin (subtopology euclidean U) (U \<inter> f -` {..<0})"
   12.40 +      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
   12.41    next
   12.42 -    show "S \<subseteq> {x \<in> U. 0 < f x}"
   12.43 -      apply (clarsimp simp add: f_def setdist_sing_in_set)
   12.44 -      using assms
   12.45 -      by (metis False Int_insert_right closedin_imp_subset empty_not_insert insert_absorb insert_subset linorder_neqE_linordered_idom not_le setdist_eq_0_closedin setdist_pos_le)
   12.46 -    show "T \<subseteq> {x \<in> U. f x < 0}"
   12.47 -      apply (clarsimp simp add: f_def setdist_sing_in_set)
   12.48 -      using assms
   12.49 -      by (metis False closedin_subset disjoint_iff_not_equal insert_absorb insert_subset linorder_neqE_linordered_idom not_less setdist_eq_0_closedin setdist_pos_le topspace_euclidean_subtopology)
   12.50 +    have "S \<subseteq> U" "T \<subseteq> U"
   12.51 +      using closedin_imp_subset assms by blast+
   12.52 +    then show "S \<subseteq> U \<inter> f -` {0<..}" "T \<subseteq> U \<inter> f -` {..<0}"
   12.53 +      using assms False by (force simp add: f_def setdist_sing_in_set intro!: setdist_gt_0_closedin)+
   12.54    qed
   12.55  qed
   12.56  
   12.57 @@ -5282,7 +5282,7 @@
   12.58  proposition proper_map:
   12.59    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   12.60    assumes "closedin (subtopology euclidean S) K"
   12.61 -      and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact {x \<in> S. f x \<in> U}"
   12.62 +      and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
   12.63        and "f ` S \<subseteq> T"
   12.64      shows "closedin (subtopology euclidean T) (f ` K)"
   12.65  proof -
   12.66 @@ -5298,7 +5298,7 @@
   12.67        by metis
   12.68      then have fX: "\<And>n. f (X n) = h n"
   12.69        by metis
   12.70 -    have "compact (C \<inter> {a \<in> S. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))})" for n
   12.71 +    have "compact (C \<inter> (S \<inter> f -` insert y (range (\<lambda>i. f(X(n + i))))))" for n
   12.72        apply (rule closed_Int_compact [OF \<open>closed C\<close>])
   12.73        apply (rule com)
   12.74         using X \<open>K \<subseteq> S\<close> \<open>f ` S \<subseteq> T\<close> \<open>y \<in> T\<close> apply blast
   12.75 @@ -5350,16 +5350,16 @@
   12.76    assume RHS: ?rhs
   12.77    obtain g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
   12.78      by (metis inv_into_f_f f)
   12.79 -  then have *: "{x \<in> S. f x \<in> U} = g ` U" if "U \<subseteq> f ` S" for U
   12.80 +  then have *: "(S \<inter> f -` U) = g ` U" if "U \<subseteq> f ` S" for U
   12.81      using that by fastforce
   12.82    have gfim: "g ` f ` S \<subseteq> S" using gf by auto
   12.83 -  have **: "compact {x \<in> f ` S. g x \<in> C}" if C: "C \<subseteq> S" "compact C" for C
   12.84 +  have **: "compact (f ` S \<inter> g -` C)" if C: "C \<subseteq> S" "compact C" for C
   12.85    proof -
   12.86 -    obtain h :: "'a set \<Rightarrow> 'a" where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
   12.87 +    obtain h where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
   12.88        by (force simp: C RHS)
   12.89 -    moreover have "f ` C = {b \<in> f ` S. g b \<in> C}"
   12.90 +    moreover have "f ` C = (f ` S \<inter> g -` C)"
   12.91        using C gf by auto
   12.92 -    ultimately show "compact {b \<in> f ` S. g b \<in> C}"
   12.93 +    ultimately show ?thesis
   12.94        using C by auto
   12.95    qed
   12.96    show ?lhs
   12.97 @@ -5510,14 +5510,14 @@
   12.98    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   12.99    assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
  12.100            "closedin (subtopology euclidean T) K"
  12.101 -  shows "compact {x. x \<in> S \<and> f x \<in> K}"
  12.102 +  shows "compact (S \<inter> f -` K)"
  12.103  by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
  12.104  
  12.105  lemma proper_map_fst:
  12.106    assumes "compact T" "K \<subseteq> S" "compact K"
  12.107 -    shows "compact {z \<in> S \<times> T. fst z \<in> K}"
  12.108 -proof -
  12.109 -  have "{z \<in> S \<times> T. fst z \<in> K} = K \<times> T"
  12.110 +    shows "compact (S \<times> T \<inter> fst -` K)"
  12.111 +proof -
  12.112 +  have "(S \<times> T \<inter> fst -` K) = K \<times> T"
  12.113      using assms by auto
  12.114    then show ?thesis by (simp add: assms compact_Times)
  12.115  qed
  12.116 @@ -5535,9 +5535,9 @@
  12.117  
  12.118  lemma proper_map_snd:
  12.119    assumes "compact S" "K \<subseteq> T" "compact K"
  12.120 -    shows "compact {z \<in> S \<times> T. snd z \<in> K}"
  12.121 -proof -
  12.122 -  have "{z \<in> S \<times> T. snd z \<in> K} = S \<times> K"
  12.123 +    shows "compact (S \<times> T \<inter> snd -` K)"
  12.124 +proof -
  12.125 +  have "(S \<times> T \<inter> snd -` K) = S \<times> K"
  12.126      using assms by auto
  12.127    then show ?thesis by (simp add: assms compact_Times)
  12.128  qed
  12.129 @@ -7872,8 +7872,7 @@
  12.130                 and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
  12.131                 and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
  12.132                                 finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
  12.133 -using paracompact_closedin [of UNIV S \<C>] assms
  12.134 -by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
  12.135 +using paracompact_closedin [of UNIV S \<C>] assms by auto
  12.136  
  12.137    
  12.138  subsection\<open>Closed-graph characterization of continuity\<close>
  12.139 @@ -7883,7 +7882,7 @@
  12.140    assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
  12.141      shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
  12.142  proof -
  12.143 -  have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
  12.144 +  have eq: "((\<lambda>x. Pair x (f x)) ` S) =(S \<times> T \<inter> (\<lambda>z. (f \<circ> fst)z - snd z) -` {0})"
  12.145      using fim by auto
  12.146    show ?thesis
  12.147      apply (subst eq)
  12.148 @@ -7902,9 +7901,9 @@
  12.149    proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
  12.150      fix U
  12.151      assume U: "closedin (subtopology euclidean T) U"
  12.152 -    have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
  12.153 +    have eq: "(S \<inter> f -` U) = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
  12.154        by (force simp: image_iff)
  12.155 -    show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
  12.156 +    show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
  12.157        by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
  12.158    qed
  12.159    with continuous_closed_graph_gen assms show ?thesis by blast
    13.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Tue Oct 17 13:56:58 2017 +0200
    13.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Oct 19 17:16:01 2017 +0100
    13.3 @@ -66,7 +66,7 @@
    13.4    shows "interior i \<subseteq> interior S"
    13.5  proof -
    13.6    have "box a b \<inter> cbox c d = {}"
    13.7 -     using inter_interval_mixed_eq_empty[of c d a b] assms
    13.8 +     using Int_interval_mixed_eq_empty[of c d a b] assms
    13.9       unfolding interior_cbox by auto
   13.10    moreover
   13.11    have "box a b \<subseteq> cbox c d \<union> S"
    14.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 17 13:56:58 2017 +0200
    14.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 19 17:16:01 2017 +0100
    14.3 @@ -858,10 +858,15 @@
    14.4  by (simp add: closedin_def topspace_subtopology)
    14.5  
    14.6  lemma openin_subtopology_Un:
    14.7 -    "openin (subtopology U T) S \<and> openin (subtopology U u) S
    14.8 -     \<Longrightarrow> openin (subtopology U (T \<union> u)) S"
    14.9 +    "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
   14.10 +     \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
   14.11  by (simp add: openin_subtopology) blast
   14.12  
   14.13 +lemma closedin_subtopology_Un:
   14.14 +    "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
   14.15 +     \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
   14.16 +by (simp add: closedin_subtopology) blast
   14.17 +
   14.18  
   14.19  subsubsection \<open>The standard Euclidean topology\<close>
   14.20  
   14.21 @@ -886,6 +891,8 @@
   14.22  lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
   14.23    by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
   14.24  
   14.25 +declare closed_closedin [symmetric, simp]
   14.26 +
   14.27  lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
   14.28    using openI by auto
   14.29  
   14.30 @@ -913,7 +920,7 @@
   14.31    by (auto simp: openin_open)
   14.32  
   14.33  lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   14.34 -  by (simp add: closedin_subtopology closed_closedin Int_ac)
   14.35 +  by (simp add: closedin_subtopology Int_ac)
   14.36  
   14.37  lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
   14.38    by (metis closedin_closed)
   14.39 @@ -965,7 +972,7 @@
   14.40         ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
   14.41                   openin (subtopology euclidean s) e2 \<and>
   14.42                   s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
   14.43 -  apply (simp add: connected_def openin_open, safe)
   14.44 +  apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   14.45    apply (simp_all, blast+)  (* SLOW *)
   14.46    done
   14.47  
   14.48 @@ -1032,7 +1039,7 @@
   14.49  lemma closedin_trans[trans]:
   14.50    "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
   14.51      closedin (subtopology euclidean U) S"
   14.52 -  by (auto simp: closedin_closed closed_closedin closed_Inter Int_assoc)
   14.53 +  by (auto simp: closedin_closed closed_Inter Int_assoc)
   14.54  
   14.55  lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   14.56    by (auto simp: closedin_closed intro: closedin_trans)
   14.57 @@ -5304,9 +5311,9 @@
   14.58  qed
   14.59  
   14.60  lemma continuous_on_open:
   14.61 -  "continuous_on s f \<longleftrightarrow>
   14.62 -    (\<forall>t. openin (subtopology euclidean (f ` s)) t \<longrightarrow>
   14.63 -      openin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
   14.64 +  "continuous_on S f \<longleftrightarrow>
   14.65 +    (\<forall>T. openin (subtopology euclidean (f ` S)) T \<longrightarrow>
   14.66 +      openin (subtopology euclidean S) (S \<inter> f -` T))"
   14.67    unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
   14.68    by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
   14.69  
   14.70 @@ -5315,37 +5322,42 @@
   14.71    assumes "f ` S \<subseteq> T"
   14.72      shows "continuous_on S f \<longleftrightarrow>
   14.73               (\<forall>U. openin (subtopology euclidean T) U
   14.74 -                  \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
   14.75 +                  \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
   14.76       (is "?lhs = ?rhs")
   14.77  proof
   14.78    assume ?lhs
   14.79    then show ?rhs
   14.80 -    apply (auto simp: openin_euclidean_subtopology_iff continuous_on_iff)
   14.81 +    apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff)
   14.82      by (metis assms image_subset_iff)
   14.83  next
   14.84    have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e
   14.85      by (simp add: Int_commute openin_open_Int)
   14.86 -  assume ?rhs
   14.87 -  then show ?lhs
   14.88 -    apply (clarsimp simp add: continuous_on_iff)
   14.89 -    apply (drule_tac x = "ball (f x) e \<inter> T" in spec)
   14.90 -    apply (clarsimp simp add: ope openin_euclidean_subtopology_iff [of S])
   14.91 -    by (metis (no_types, hide_lams) assms dist_commute dist_self image_subset_iff)
   14.92 +  assume R [rule_format]: ?rhs
   14.93 +  show ?lhs
   14.94 +  proof (clarsimp simp add: continuous_on_iff)
   14.95 +    fix x and e::real
   14.96 +    assume "x \<in> S" and "0 < e"
   14.97 +    then have x: "x \<in> S \<inter> (f -` ball (f x) e \<inter> f -` T)"
   14.98 +      using assms by auto
   14.99 +    show "\<exists>d>0. \<forall>x'\<in>S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
  14.100 +      using R [of "ball (f x) e \<inter> T"] x
  14.101 +      by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute)
  14.102 +  qed
  14.103  qed
  14.104  
  14.105  lemma continuous_openin_preimage:
  14.106    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
  14.107    shows
  14.108     "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
  14.109 -        \<Longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
  14.110 +        \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
  14.111  by (simp add: continuous_on_open_gen)
  14.112  
  14.113  text \<open>Similarly in terms of closed sets.\<close>
  14.114  
  14.115  lemma continuous_on_closed:
  14.116 -  "continuous_on s f \<longleftrightarrow>
  14.117 -    (\<forall>t. closedin (subtopology euclidean (f ` s)) t \<longrightarrow>
  14.118 -      closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
  14.119 +  "continuous_on S f \<longleftrightarrow>
  14.120 +    (\<forall>T. closedin (subtopology euclidean (f ` S)) T \<longrightarrow>
  14.121 +      closedin (subtopology euclidean S) (S \<inter> f -` T))"
  14.122    unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
  14.123    by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
  14.124  
  14.125 @@ -5354,61 +5366,73 @@
  14.126    assumes "f ` S \<subseteq> T"
  14.127      shows "continuous_on S f \<longleftrightarrow>
  14.128               (\<forall>U. closedin (subtopology euclidean T) U
  14.129 -                  \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
  14.130 +                  \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
  14.131 +     (is "?lhs = ?rhs")
  14.132  proof -
  14.133 -  have *: "U \<subseteq> T \<Longrightarrow> {x \<in> S. f x \<in> T \<and> f x \<notin> U} = S - {x \<in> S. f x \<in> U}" for U
  14.134 +  have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
  14.135      using assms by blast
  14.136    show ?thesis
  14.137 -    apply (simp add: continuous_on_open_gen [OF assms], safe)
  14.138 -    apply (drule_tac [!] x="T-U" in spec)
  14.139 -    apply (force simp: closedin_def *)
  14.140 -    apply (force simp: openin_closedin_eq *)
  14.141 -    done
  14.142 +  proof
  14.143 +    assume L: ?lhs
  14.144 +    show ?rhs
  14.145 +    proof clarify
  14.146 +      fix U
  14.147 +      assume "closedin (subtopology euclidean T) U"
  14.148 +      then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
  14.149 +        using L unfolding continuous_on_open_gen [OF assms]
  14.150 +        by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
  14.151 +    qed
  14.152 +  next
  14.153 +    assume R [rule_format]: ?rhs
  14.154 +    show ?lhs
  14.155 +      unfolding continuous_on_open_gen [OF assms]
  14.156 +      by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
  14.157 +  qed
  14.158  qed
  14.159  
  14.160  lemma continuous_closedin_preimage_gen:
  14.161    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
  14.162    assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
  14.163 -    shows "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
  14.164 +    shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
  14.165  using assms continuous_on_closed_gen by blast
  14.166  
  14.167  lemma continuous_on_imp_closedin:
  14.168    assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
  14.169 -    shows "closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T}"
  14.170 +    shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
  14.171  using assms continuous_on_closed by blast
  14.172  
  14.173  subsection \<open>Half-global and completely global cases.\<close>
  14.174  
  14.175  lemma continuous_openin_preimage_gen:
  14.176 -  assumes "continuous_on s f"  "open t"
  14.177 -  shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
  14.178 +  assumes "continuous_on S f"  "open T"
  14.179 +  shows "openin (subtopology euclidean S) (S \<inter> f -` T)"
  14.180  proof -
  14.181 -  have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
  14.182 +  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
  14.183      by auto
  14.184 -  have "openin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
  14.185 -    using openin_open_Int[of t "f ` s", OF assms(2)] unfolding openin_open by auto
  14.186 +  have "openin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
  14.187 +    using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
  14.188    then show ?thesis
  14.189 -    using assms(1)[unfolded continuous_on_open, THEN spec[where x="t \<inter> f ` s"]]
  14.190 +    using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
  14.191      using * by auto
  14.192  qed
  14.193  
  14.194  lemma continuous_closedin_preimage:
  14.195 -  assumes "continuous_on s f" and "closed t"
  14.196 -  shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
  14.197 +  assumes "continuous_on S f" and "closed T"
  14.198 +  shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
  14.199  proof -
  14.200 -  have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
  14.201 +  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
  14.202      by auto
  14.203 -  have "closedin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
  14.204 -    using closedin_closed_Int[of t "f ` s", OF assms(2)]
  14.205 +  have "closedin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
  14.206 +    using closedin_closed_Int[of T "f ` S", OF assms(2)]
  14.207      by (simp add: Int_commute)
  14.208    then show ?thesis
  14.209 -    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="t \<inter> f ` s"]]
  14.210 +    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
  14.211      using * by auto
  14.212  qed
  14.213  
  14.214  lemma continuous_openin_preimage_eq:
  14.215     "continuous_on S f \<longleftrightarrow>
  14.216 -    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
  14.217 +    (\<forall>T. open T \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T))"
  14.218  apply safe
  14.219  apply (simp add: continuous_openin_preimage_gen)
  14.220  apply (fastforce simp add: continuous_on_open openin_open)
  14.221 @@ -5416,66 +5440,55 @@
  14.222  
  14.223  lemma continuous_closedin_preimage_eq:
  14.224     "continuous_on S f \<longleftrightarrow>
  14.225 -    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
  14.226 +    (\<forall>T. closed T \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` T))"
  14.227  apply safe
  14.228  apply (simp add: continuous_closedin_preimage)
  14.229  apply (fastforce simp add: continuous_on_closed closedin_closed)
  14.230  done
  14.231  
  14.232  lemma continuous_open_preimage:
  14.233 -  assumes "continuous_on s f"
  14.234 -    and "open s"
  14.235 -    and "open t"
  14.236 -  shows "open {x \<in> s. f x \<in> t}"
  14.237 +  assumes contf: "continuous_on S f" and "open S" "open T"
  14.238 +  shows "open (S \<inter> f -` T)"
  14.239  proof-
  14.240 -  obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
  14.241 -    using continuous_openin_preimage_gen[OF assms(1,3)] unfolding openin_open by auto
  14.242 +  obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
  14.243 +    using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
  14.244 +    unfolding openin_open by auto
  14.245    then show ?thesis
  14.246 -    using open_Int[of s T, OF assms(2)] by auto
  14.247 +    using open_Int[of S U, OF \<open>open S\<close>] by auto
  14.248  qed
  14.249  
  14.250  lemma continuous_closed_preimage:
  14.251 -  assumes "continuous_on s f"
  14.252 -    and "closed s"
  14.253 -    and "closed t"
  14.254 -  shows "closed {x \<in> s. f x \<in> t}"
  14.255 +  assumes contf: "continuous_on S f" and "closed S" "closed T"
  14.256 +  shows "closed (S \<inter> f -` T)"
  14.257  proof-
  14.258 -  obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
  14.259 -    using continuous_closedin_preimage[OF assms(1,3)]
  14.260 +  obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
  14.261 +    using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
  14.262      unfolding closedin_closed by auto
  14.263 -  then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
  14.264 +  then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
  14.265  qed
  14.266  
  14.267 -lemma continuous_open_preimage_univ:
  14.268 -  "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open {x. f x \<in> s}"
  14.269 -  using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
  14.270 -
  14.271 -lemma continuous_closed_preimage_univ:
  14.272 -  "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed {x. f x \<in> s}"
  14.273 -  using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
  14.274 -
  14.275 -lemma continuous_open_vimage: "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` s)"
  14.276 -  unfolding vimage_def by (rule continuous_open_preimage_univ)
  14.277 -
  14.278 -lemma continuous_closed_vimage: "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` s)"
  14.279 -  unfolding vimage_def by (rule continuous_closed_preimage_univ)
  14.280 +lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
  14.281 +  by (metis continuous_on_eq_continuous_within open_vimage) 
  14.282 + 
  14.283 +lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
  14.284 +  by (simp add: closed_vimage continuous_on_eq_continuous_within)
  14.285  
  14.286  lemma interior_image_subset:
  14.287    assumes "inj f" "\<And>x. continuous (at x) f"
  14.288 -  shows "interior (f ` s) \<subseteq> f ` (interior s)"
  14.289 +  shows "interior (f ` S) \<subseteq> f ` (interior S)"
  14.290  proof
  14.291 -  fix x assume "x \<in> interior (f ` s)"
  14.292 -  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
  14.293 -  then have "x \<in> f ` s" by auto
  14.294 -  then obtain y where y: "y \<in> s" "x = f y" by auto
  14.295 -  have "open (vimage f T)"
  14.296 -    using assms \<open>open T\<close> by (metis continuous_open_vimage)
  14.297 +  fix x assume "x \<in> interior (f ` S)"
  14.298 +  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" ..
  14.299 +  then have "x \<in> f ` S" by auto
  14.300 +  then obtain y where y: "y \<in> S" "x = f y" by auto
  14.301 +  have "open (f -` T)"
  14.302 +    using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
  14.303    moreover have "y \<in> vimage f T"
  14.304      using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
  14.305 -  moreover have "vimage f T \<subseteq> s"
  14.306 -    using \<open>T \<subseteq> image f s\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
  14.307 -  ultimately have "y \<in> interior s" ..
  14.308 -  with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
  14.309 +  moreover have "vimage f T \<subseteq> S"
  14.310 +    using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
  14.311 +  ultimately have "y \<in> interior S" ..
  14.312 +  with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
  14.313  qed
  14.314  
  14.315  subsection \<open>Topological properties of linear functions.\<close>
  14.316 @@ -5853,7 +5866,7 @@
  14.317      by auto
  14.318  qed
  14.319  
  14.320 -lemma inter_interval_mixed_eq_empty:
  14.321 +lemma Int_interval_mixed_eq_empty:
  14.322    fixes a :: "'a::euclidean_space"
  14.323     assumes "box c d \<noteq> {}"
  14.324    shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
    15.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Tue Oct 17 13:56:58 2017 +0200
    15.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Thu Oct 19 17:16:01 2017 +0100
    15.3 @@ -740,22 +740,20 @@
    15.4    case True
    15.5    have "path \<gamma>"
    15.6      by (simp add: assms simple_path_imp_path)
    15.7 -  then obtain k where k: "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
    15.8 +  then have const: "winding_number \<gamma> constant_on inside(path_image \<gamma>)"
    15.9    proof (rule winding_number_constant)
   15.10      show "connected (inside(path_image \<gamma>))"
   15.11        by (simp add: Jordan_inside_outside True assms)
   15.12    qed (use inside_no_overlap True in auto)
   15.13    obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
   15.14      using simple_closed_path_wn3 [of \<gamma>] True assms by blast
   15.15 -  with k have "winding_number \<gamma> z = k"
   15.16 -    by blast
   15.17    have "winding_number \<gamma> z \<in> \<int>"
   15.18      using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
   15.19    with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
   15.20      apply (auto simp: Ints_def abs_if split: if_split_asm)
   15.21      by (metis of_int_1 of_int_eq_iff of_int_minus)
   15.22 -  then show ?thesis
   15.23 -    using that \<open>winding_number \<gamma> z = k\<close> k by auto
   15.24 +  with that const zin show ?thesis
   15.25 +    unfolding constant_on_def by metis
   15.26  next
   15.27    case False
   15.28    then show ?thesis