# HG changeset patch
# User paulson
# Date 1508429773 -3600
# Node ID d3d508b23d1d06da2d7c87724a98d8523b992c3e
# Parent  ee874941dfb830f7cee386bf9560e2994c97003a# Parent  c2128ab11f6171220bbae0d52ee0f3bca4ed5497
merged

diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -2279,7 +2279,7 @@
 lemma retraction_imp_quotient_map:
    "retraction s t r
     \<Longrightarrow> u \<subseteq> t
-            \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> r x \<in> u} \<longleftrightarrow>
+            \<Longrightarrow> (openin (subtopology euclidean s) (s \<inter> r -` u) \<longleftrightarrow>
                  openin (subtopology euclidean t) u)"
 apply (clarsimp simp add: retraction)
 apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
@@ -2941,21 +2941,21 @@
               and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
     by (metis Dugundji [OF C cloUT contgf gfTC])
   show ?thesis
-  proof (rule_tac V = "{x \<in> U. f' x \<in> D}" and g = "h o r o f'" in that)
-    show "T \<subseteq> {x \<in> U. f' x \<in> D}"
+  proof (rule_tac V = "U \<inter> f' -` D" and g = "h o r o f'" in that)
+    show "T \<subseteq> U \<inter> f' -` D"
       using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
       by fastforce
-    show ope: "openin (subtopology euclidean U) {x \<in> U. f' x \<in> D}"
+    show ope: "openin (subtopology euclidean U) (U \<inter> f' -` D)"
       using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
-    have conth: "continuous_on (r ` f' ` {x \<in> U. f' x \<in> D}) h"
+    have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
       apply (rule continuous_on_subset [of S'])
       using homeomorphism_def homgh apply blast
       using \<open>r ` D \<subseteq> S'\<close> by blast
-    show "continuous_on {x \<in> U. f' x \<in> D} (h \<circ> r \<circ> f')"
+    show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
       apply (intro continuous_on_compose conth
                    continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
       done
-    show "(h \<circ> r \<circ> f') ` {x \<in> U. f' x \<in> D} \<subseteq> S"
+    show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
       using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
       by (auto simp: homeomorphism_def)
     show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
@@ -3150,36 +3150,36 @@
   have "S' \<subseteq> W" using WS' closedin_closed by auto
   have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
     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)
-  have "S' retract_of {x \<in> W. h x \<in> X}"
+  have "S' retract_of (W \<inter> h -` X)"
   proof (simp add: retraction_def retract_of_def, intro exI conjI)
-    show "S' \<subseteq> {x \<in> W. h x \<in> X}"
-      using him WS' closedin_imp_subset by blast
-    show "continuous_on {x \<in> W. h x \<in> X} (f o r o h)"
+    show "S' \<subseteq> W" "S' \<subseteq> h -` X"
+      using him WS' closedin_imp_subset by blast+
+    show "continuous_on (W \<inter> h -` X) (f o r o h)"
     proof (intro continuous_on_compose)
-      show "continuous_on {x \<in> W. h x \<in> X} h"
-        by (metis (no_types) Collect_restrict conth continuous_on_subset)
-      show "continuous_on (h ` {x \<in> W. h x \<in> X}) r"
+      show "continuous_on (W \<inter> h -` X) h"
+        by (meson conth continuous_on_subset inf_le1)
+      show "continuous_on (h ` (W \<inter> h -` X)) r"
       proof -
-        have "h ` {b \<in> W. h b \<in> X} \<subseteq> X"
+        have "h ` (W \<inter> h -` X) \<subseteq> X"
           by blast
-        then show "continuous_on (h ` {b \<in> W. h b \<in> X}) r"
+        then show "continuous_on (h ` (W \<inter> h -` X)) r"
           by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
       qed
-      show "continuous_on (r ` h ` {x \<in> W. h x \<in> X}) f"
+      show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
         apply (rule continuous_on_subset [of S])
          using hom homeomorphism_def apply blast
         apply clarify
         apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
         done
     qed
-    show "(f \<circ> r \<circ> h) ` {x \<in> W. h x \<in> X} \<subseteq> S'"
+    show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
       using \<open>retraction X S r\<close> hom
       by (auto simp: retraction_def homeomorphism_def)
     show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
       using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
   qed
   then show ?thesis
-    apply (rule_tac V = "{x. x \<in> W \<and> h x \<in> X}" in that)
+    apply (rule_tac V = "W \<inter> h -` X" in that)
      apply (rule openin_trans [OF _ UW])
      using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
      done
@@ -3248,8 +3248,7 @@
     using \<open>ANR S\<close>
     apply (simp add: ANR_def)
     apply (drule_tac x=UNIV in spec)
-    apply (drule_tac x=T in spec)
-    apply (auto simp: closed_closedin)
+    apply (drule_tac x=T in spec, clarsimp)
     apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
     done
 qed
@@ -3455,10 +3454,10 @@
   define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
   have US': "closedin (subtopology euclidean U) S'"
     using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
-    by (simp add: S'_def continuous_intros)
+    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   have UT': "closedin (subtopology euclidean U) T'"
     using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
-    by (simp add: T'_def continuous_intros)
+    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   have "S \<subseteq> S'"
     using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
   have "T \<subseteq> T'"
@@ -3543,19 +3542,19 @@
   proof -
     obtain f g where hom: "homeomorphism (S \<union> T) C f g"
       using hom by (force simp: homeomorphic_def)
-    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
       apply (rule closedin_trans [OF _ UC])
       apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
       using hom homeomorphism_def apply blast
       apply (metis hom homeomorphism_def set_eq_subset)
       done
-    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
       apply (rule closedin_trans [OF _ UC])
       apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
       using hom homeomorphism_def apply blast
       apply (metis hom homeomorphism_def set_eq_subset)
       done
-    have ARS: "AR {x \<in> C. g x \<in> S}"
+    have ARS: "AR (C \<inter> g -` S)"
       apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3563,7 +3562,7 @@
       using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have ART: "AR {x \<in> C. g x \<in> T}"
+    have ART: "AR (C \<inter> g -` T)"
       apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3571,7 +3570,7 @@
       using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have ARI: "AR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+    have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
       apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3580,7 +3579,7 @@
       apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have "C = {x \<in> C. g x \<in> S} \<union> {x \<in> C. g x \<in> T}"
+    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
       using hom  by (auto simp: homeomorphism_def)
     then show ?thesis
       by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
@@ -3615,10 +3614,10 @@
   define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
   have cloUS': "closedin (subtopology euclidean U) S'"
     using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
-    by (simp add: S'_def continuous_intros)
+    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   have cloUT': "closedin (subtopology euclidean U) T'"
     using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
-    by (simp add: T'_def continuous_intros)
+    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
   have "S \<subseteq> S'"
     using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
   have "T \<subseteq> T'"
@@ -3752,19 +3751,19 @@
   proof -
     obtain f g where hom: "homeomorphism (S \<union> T) C f g"
       using hom by (force simp: homeomorphic_def)
-    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
       apply (rule closedin_trans [OF _ UC])
       apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
       using hom [unfolded homeomorphism_def] apply blast
       apply (metis hom homeomorphism_def set_eq_subset)
       done
-    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
       apply (rule closedin_trans [OF _ UC])
       apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
       using hom [unfolded homeomorphism_def] apply blast
       apply (metis hom homeomorphism_def set_eq_subset)
       done
-    have ANRS: "ANR {x \<in> C. g x \<in> S}"
+    have ANRS: "ANR (C \<inter> g -` S)"
       apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3772,7 +3771,7 @@
       using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have ANRT: "ANR {x \<in> C. g x \<in> T}"
+    have ANRT: "ANR (C \<inter> g -` T)"
       apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3780,7 +3779,7 @@
       using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have ANRI: "ANR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+    have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
       apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
       apply (simp add: homeomorphic_def)
       apply (rule_tac x=g in exI)
@@ -3789,8 +3788,8 @@
       apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
       apply (rule_tac x="f x" in image_eqI, auto)
       done
-    have "C = {x. x \<in> C \<and> g x \<in> S} \<union> {x. x \<in> C \<and> g x \<in> T}"
-      by auto (metis Un_iff hom homeomorphism_def imageI)
+    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
+      using hom by (auto simp: homeomorphism_def)
     then show ?thesis
       by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
   qed
@@ -3822,13 +3821,13 @@
     using fim by auto
   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)"
   proof (intro exI conjI)
-    show "C \<subseteq> {x \<in> W. g x \<in> S}"
+    show "C \<subseteq> W \<inter> g -` S"
       using \<open>C \<subseteq> W\<close> fim geq by blast
-    show "openin (subtopology euclidean U) {x \<in> W. g x \<in> S}"
+    show "openin (subtopology euclidean U) (W \<inter> g -` S)"
       by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
-    show "continuous_on {x \<in> W. g x \<in> S} g"
+    show "continuous_on (W \<inter> g -` S) g"
       by (blast intro: continuous_on_subset [OF contg])
-    show "g ` {x \<in> W. g x \<in> S} \<subseteq> S"
+    show "g ` (W \<inter> g -` S) \<subseteq> S"
       using gim by blast
     show "\<forall>x\<in>C. g x = f x"
       using geq by blast
@@ -4074,15 +4073,14 @@
     apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
     done
   finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
-  moreover have "openin (subtopology euclidean UNIV) {x \<in> UNIV. closest_point (affine hull S) x \<in> - {a}}"
+  moreover have "openin (subtopology euclidean UNIV) (UNIV \<inter> closest_point (affine hull S) -` (- {a}))"
     apply (rule continuous_openin_preimage_gen)
     apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
     done
   ultimately show ?thesis
-    apply (simp add: ENR_def)
-    apply (rule_tac x = "{x. x \<in> UNIV \<and>
-                             closest_point (affine hull S) x \<in> (- {a})}" in exI)
-    apply simp
+    unfolding ENR_def
+    apply (rule_tac x = "closest_point (affine hull S) -` (- {a})" in exI)
+    apply (simp add: vimage_def)
     done
 qed
 
@@ -4881,5 +4879,4 @@
   using connected_complement_homeomorphic_convex_compact [OF assms]
   using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
 
-
 end
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -4111,30 +4111,29 @@
 subsection\<open>The winding number is constant on a connected region\<close>
 
 lemma winding_number_constant:
-  assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected s" and sg: "s \<inter> path_image \<gamma> = {}"
-  obtains k where "\<And>z. z \<in> s \<Longrightarrow> winding_number \<gamma> z = k"
+  assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and cs: "connected S" and sg: "S \<inter> path_image \<gamma> = {}"
+  shows "winding_number \<gamma> constant_on S"
 proof -
   have *: "1 \<le> cmod (winding_number \<gamma> y - winding_number \<gamma> z)"
-      if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> s" "z \<in> s" for y z
+      if ne: "winding_number \<gamma> y \<noteq> winding_number \<gamma> z" and "y \<in> S" "z \<in> S" for y z
   proof -
     have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
-      using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> s\<close> by auto
+      using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
     with ne show ?thesis
       by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
   qed
-  have cont: "continuous_on s (\<lambda>w. winding_number \<gamma> w)"
+  have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
     using continuous_on_winding_number [OF \<gamma>] sg
     by (meson continuous_on_subset disjoint_eq_subset_Compl)
   show ?thesis
-    apply (rule continuous_discrete_range_constant [OF cs cont])
-    using "*" zero_less_one apply blast
-    by (simp add: that)
+    using "*" zero_less_one
+    by (blast intro: continuous_discrete_range_constant [OF cs cont])
 qed
 
 lemma winding_number_eq:
-     "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> s; z \<in> s; connected s; s \<inter> path_image \<gamma> = {}\<rbrakk>
+     "\<lbrakk>path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; w \<in> S; z \<in> S; connected S; S \<inter> path_image \<gamma> = {}\<rbrakk>
       \<Longrightarrow> winding_number \<gamma> w = winding_number \<gamma> z"
-  using winding_number_constant by blast
+  using winding_number_constant by (metis constant_on_def) 
 
 lemma open_winding_number_levelsets:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
@@ -4149,7 +4148,7 @@
     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"
       apply (rule_tac x=e in exI)
       using e apply (simp add: dist_norm ball_def norm_minus_commute)
-      apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where s = "ball z e"])
+      apply (auto simp: dist_norm norm_minus_commute intro!: winding_number_eq [OF assms, where S = "ball z e"])
       done
   } then
   show ?thesis
@@ -4171,11 +4170,11 @@
     using B subset_ball by auto
   then have wout: "w \<in> outside (path_image \<gamma>)"
     using w by blast
-  moreover obtain k where "\<And>z. z \<in> outside (path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+  moreover have "winding_number \<gamma> constant_on outside (path_image \<gamma>)"
     using winding_number_constant [OF \<gamma> loop, of "outside(path_image \<gamma>)"] connected_outside
     by (metis DIM_complex bounded_path_image dual_order.refl \<gamma> outside_no_overlap)
   ultimately have "winding_number \<gamma> z = winding_number \<gamma> w"
-    using z by blast
+    by (metis (no_types, hide_lams) constant_on_def z)
   also have "... = 0"
   proof -
     have wnot: "w \<notin> path_image \<gamma>"  using wout by (simp add: outside_def)
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -127,7 +127,7 @@
       apply (rule Cauchy_inequality)
          using holf holomorphic_on_subset apply force
         using holf holomorphic_on_imp_continuous_on holomorphic_on_subset apply blast
-       using \<open>w \<noteq> 0\<close> apply (simp add:)
+       using \<open>w \<noteq> 0\<close> apply simp
        by (metis nof wgeA dist_0_norm dist_norm)
     also have "... = fact k * (B * 1 / cmod w ^ (k-n))"
       apply (simp only: mult_cancel_left times_divide_eq_right [symmetric])
@@ -327,7 +327,7 @@
     ultimately obtain w where w: "w \<in> frontier(cball \<xi> r)"
                           and now: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (f w) \<le> norm (f x)"
       apply (rule bexE [OF continuous_attains_inf [OF compact_frontier [OF compact_cball]]])
-      apply (simp add:)
+      apply simp
       done
     then have fw: "0 < norm (f w)"
       by (simp add: fnz')
@@ -336,7 +336,7 @@
     then obtain v where v: "v \<in> frontier(cball \<xi> r)"
                and nov: "\<And>x. x \<in> frontier(cball \<xi> r) \<Longrightarrow> norm (g v) \<ge> norm (g x)"
       apply (rule bexE [OF continuous_attains_sup [OF compact_frontier [OF compact_cball] froc]])
-      apply (simp add:)
+      apply simp
       done
     then have fv: "0 < norm (f v)"
       by (simp add: fnz')
@@ -628,7 +628,7 @@
       unfolding powf_def by (rule holomorphic_power_series [OF holfb w])
     moreover have "(\<Sum>i<n. powf i) = f \<xi>"
       apply (subst Groups_Big.comm_monoid_add_class.sum.setdiff_irrelevant [symmetric])
-      apply (simp add:)
+      apply simp
       apply (simp only: dfz sing)
       apply (simp add: powf_def)
       done
@@ -640,7 +640,7 @@
     have "summable (\<lambda>i. (deriv ^^ (i + n)) f \<xi> * (w - \<xi>) ^ i / fact (i + n))"
     proof (cases "w=\<xi>")
       case False then show ?thesis
-        using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by (simp add:)
+        using summable_mult [OF *, of "1 / (w - \<xi>) ^ n"] by simp
     next
       case True then show ?thesis
         by (auto simp: Power.semiring_1_class.power_0_left intro!: summable_finite [of "{0}"]
@@ -716,7 +716,7 @@
     apply (rule holomorphic_intros)+
     using h holomorphic_on_open apply blast
     apply (rule holomorphic_intros)+
-    using \<open>0 < n\<close> apply (simp add:)
+    using \<open>0 < n\<close> apply simp
     apply (rule holomorphic_intros)+
     done
   show ?thesis
@@ -924,7 +924,7 @@
         using \<open>0 < r\<close> by simp
       have "\<exists>B. 0<B \<and> eventually (\<lambda>z. cmod ((inverse \<circ> f \<circ> inverse) z) \<le> B) (at 0)"
         apply (rule exI [where x=1])
-        apply (simp add:)
+        apply simp
         using tendstoD [OF lim [unfolded lim_at_infinity_0] zero_less_one]
         apply (rule eventually_mono)
         apply (simp add: dist_norm)
@@ -969,8 +969,7 @@
       qed
       then show ?thesis
         apply (rule_tac a = "\<lambda>k. (deriv ^^ k) f 0 / (fact k)" and n=n in that)
-        apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf])
-        apply (simp add:)
+        apply (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf], simp)
         done
   next
     case False
@@ -1041,11 +1040,12 @@
   have "bounded {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
     using polyfun_extremal [where c=c and B="B+1", OF c]
     by (auto simp: bounded_pos eventually_at_infinity_pos *)
-  moreover have "closed {z. (\<Sum>i\<le>n. c i * z ^ i) \<in> K}"
-    apply (intro allI continuous_closed_preimage_univ continuous_intros)
+  moreover have "closed ((\<lambda>z. (\<Sum>i\<le>n. c i * z ^ i)) -` K)"
+    apply (intro allI continuous_closed_vimage continuous_intros)
     using \<open>compact K\<close> compact_eq_bounded_closed by blast
   ultimately show ?thesis
-    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed by blast
+    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed
+    by (auto simp add: vimage_def)
 qed
 
 corollary proper_map_polyfun_univ:
@@ -1095,7 +1095,7 @@
     fix e::real assume "0 < e"
     with compf [of "cball 0 (inverse e)"]
     show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
-      apply (simp add:)
+      apply simp
       apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
       apply (rule_tac x="b+1" in exI)
       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)
@@ -1134,7 +1134,7 @@
     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"
       apply (rule_tac x="min \<delta> \<epsilon>" in exI)
       apply (intro conjI allI impI Operator_Norm.onorm_le)
-      apply (simp add:)
+      apply simp
       apply (simp only: Rings.ring_class.left_diff_distrib [symmetric] norm_mult)
       apply (rule mult_right_mono [OF \<delta>])
       apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>)
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Connected.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -395,29 +395,6 @@
     by (simp add: th0 th1)
 qed
 
-lemma connected_continuous_image:
-  assumes "continuous_on s f"
-    and "connected s"
-  shows "connected(f ` s)"
-proof -
-  {
-    fix T
-    assume as:
-      "T \<noteq> {}"
-      "T \<noteq> f ` s"
-      "openin (subtopology euclidean (f ` s)) T"
-      "closedin (subtopology euclidean (f ` s)) T"
-    have "{x \<in> s. f x \<in> T} = {} \<or> {x \<in> s. f x \<in> T} = s"
-      using assms(1)[unfolded continuous_on_open, THEN spec[where x=T]]
-      using assms(1)[unfolded continuous_on_closed, THEN spec[where x=T]]
-      using assms(2)[unfolded connected_clopen, THEN spec[where x="{x \<in> s. f x \<in> T}"]] as(3,4) by auto
-    then have False using as(1,2)
-      using as(4)[unfolded closedin_def topspace_euclidean_subtopology] by auto
-  }
-  then show ?thesis
-    unfolding connected_clopen by auto
-qed
-
 lemma connected_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "linear f" and "connected s"
@@ -1442,13 +1419,13 @@
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on s f \<Longrightarrow> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
-  using continuous_closedin_preimage[of s f "{a}"] by auto
+  shows "continuous_on S f \<Longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x = a}"
+  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
 
 lemma continuous_closed_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
-  shows "continuous_on s f \<Longrightarrow> closed s \<Longrightarrow> closed {x \<in> s. f x = a}"
-  using continuous_closed_preimage[of s f "{a}"] by auto
+  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
+  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
 
 lemma continuous_constant_on_closure:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -1462,17 +1439,17 @@
     by auto
 
 lemma image_closure_subset:
-  assumes "continuous_on (closure s) f"
-    and "closed t"
-    and "(f ` s) \<subseteq> t"
-  shows "f ` (closure s) \<subseteq> t"
+  assumes contf: "continuous_on (closure S) f"
+    and "closed T"
+    and "(f ` S) \<subseteq> T"
+  shows "f ` (closure S) \<subseteq> T"
 proof -
-  have "s \<subseteq> {x \<in> closure s. f x \<in> t}"
+  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
     using assms(3) closure_subset by auto
-  moreover have "closed {x \<in> closure s. f x \<in> t}"
-    using continuous_closed_preimage[OF assms(1)] and assms(2) by auto
-  ultimately have "closure s = {x \<in> closure s . f x \<in> t}"
-    using closure_minimal[of s "{x \<in> closure s. f x \<in> t}"] by auto
+  moreover have "closed (closure S \<inter> f -` T)"
+    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
+  ultimately have "closure S = (closure S \<inter> f -` T)"
+    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
   then show ?thesis by auto
 qed
 
@@ -1967,7 +1944,7 @@
 lemma bounded_uniformly_continuous_image:
   fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
   assumes "uniformly_continuous_on S f" "bounded S"
-  shows "bounded(image f S)"
+  shows "bounded(f ` S)"
   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)
 
 subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
@@ -2023,61 +2000,61 @@
 subsection\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open:
-  assumes t: "f ` s \<subseteq> t"
-      and ope: "\<And>u. u \<subseteq> t
-              \<Longrightarrow> (openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
-                   openin (subtopology euclidean t) u)"
-    shows "continuous_on s f"
+  assumes T: "f ` S \<subseteq> T"
+      and ope: "\<And>U. U \<subseteq> T
+              \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+                   openin (subtopology euclidean T) U)"
+    shows "continuous_on S f"
 proof -
-  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+  have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
-    using ope [OF t]
+    using ope [OF T]
     apply (simp add: continuous_on_open)
-    by (metis (no_types, lifting) "ope"  openin_imp_subset openin_trans)
+    by (meson ope openin_imp_subset openin_trans)
 qed
 
 lemma quotient_map_imp_continuous_closed:
-  assumes t: "f ` s \<subseteq> t"
-      and ope: "\<And>u. u \<subseteq> t
-                  \<Longrightarrow> (closedin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
-                       closedin (subtopology euclidean t) u)"
-    shows "continuous_on s f"
+  assumes T: "f ` S \<subseteq> T"
+      and ope: "\<And>U. U \<subseteq> T
+                  \<Longrightarrow> (closedin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+                       closedin (subtopology euclidean T) U)"
+    shows "continuous_on S f"
 proof -
-  have [simp]: "{x \<in> s. f x \<in> f ` s} = s" by auto
+  have [simp]: "S \<inter> f -` f ` S = S" by auto
   show ?thesis
-    using ope [OF t]
+    using ope [OF T]
     apply (simp add: continuous_on_closed)
-    by (metis (no_types, lifting) "ope" closedin_imp_subset closedin_subtopology_refl closedin_trans openin_subtopology_refl openin_subtopology_self)
+    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
 qed
 
 lemma open_map_imp_quotient_map:
-  assumes contf: "continuous_on s f"
-      and t: "t \<subseteq> f ` s"
-      and ope: "\<And>t. openin (subtopology euclidean s) t
-                   \<Longrightarrow> openin (subtopology euclidean (f ` s)) (f ` t)"
-    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} =
-           openin (subtopology euclidean (f ` s)) t"
+  assumes contf: "continuous_on S f"
+      and T: "T \<subseteq> f ` S"
+      and ope: "\<And>T. openin (subtopology euclidean S) T
+                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` T)"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` T) =
+           openin (subtopology euclidean (f ` S)) T"
 proof -
-  have "t = image f {x. x \<in> s \<and> f x \<in> t}"
-    using t by blast
+  have "T = f ` (S \<inter> f -` T)"
+    using T by blast
   then show ?thesis
-    using "ope" contf continuous_on_open by fastforce
+    using "ope" contf continuous_on_open by metis
 qed
 
 lemma closed_map_imp_quotient_map:
-  assumes contf: "continuous_on s f"
-      and t: "t \<subseteq> f ` s"
-      and ope: "\<And>t. closedin (subtopology euclidean s) t
-              \<Longrightarrow> closedin (subtopology euclidean (f ` s)) (f ` t)"
-    shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t} \<longleftrightarrow>
-           openin (subtopology euclidean (f ` s)) t"
+  assumes contf: "continuous_on S f"
+      and T: "T \<subseteq> f ` S"
+      and ope: "\<And>T. closedin (subtopology euclidean S) T
+              \<Longrightarrow> closedin (subtopology euclidean (f ` S)) (f ` T)"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
+           openin (subtopology euclidean (f ` S)) T"
           (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then have *: "closedin (subtopology euclidean s) (s - {x \<in> s. f x \<in> t})"
+  then have *: "closedin (subtopology euclidean S) (S - (S \<inter> f -` T))"
     using closedin_diff by fastforce
-  have [simp]: "(f ` s - f ` (s - {x \<in> s. f x \<in> t})) = t"
-    using t by blast
+  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
+    using T by blast
   show ?rhs
     using ope [OF *, unfolded closedin_def] by auto
 next
@@ -2087,51 +2064,50 @@
 qed
 
 lemma continuous_right_inverse_imp_quotient_map:
-  assumes contf: "continuous_on s f" and imf: "f ` s \<subseteq> t"
-      and contg: "continuous_on t g" and img: "g ` t \<subseteq> s"
-      and fg [simp]: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y"
-      and u: "u \<subseteq> t"
-    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
-           openin (subtopology euclidean t) u"
+  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
+      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
+      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+      and U: "U \<subseteq> T"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+           openin (subtopology euclidean T) U"
           (is "?lhs = ?rhs")
 proof -
-  have f: "\<And>z. openin (subtopology euclidean (f ` s)) z \<Longrightarrow>
-                openin (subtopology euclidean s) {x \<in> s. f x \<in> z}"
-  and  g: "\<And>z. openin (subtopology euclidean (g ` t)) z \<Longrightarrow>
-                openin (subtopology euclidean t) {x \<in> t. g x \<in> z}"
+  have f: "\<And>Z. openin (subtopology euclidean (f ` S)) Z \<Longrightarrow>
+                openin (subtopology euclidean S) (S \<inter> f -` Z)"
+  and  g: "\<And>Z. openin (subtopology euclidean (g ` T)) Z \<Longrightarrow>
+                openin (subtopology euclidean T) (T \<inter> g -` Z)"
     using contf contg by (auto simp: continuous_on_open)
   show ?thesis
   proof
-    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}"
+    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
       using imf img by blast
-    also have "... = u"
-      using u by auto
-    finally have [simp]: "{x \<in> t. g x \<in> g ` t \<and> g x \<in> s \<and> f (g x) \<in> u} = u" .
+    also have "... = U"
+      using U by auto
+    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
     assume ?lhs
-    then have *: "openin (subtopology euclidean (g ` t)) (g ` t \<inter> {x \<in> s. f x \<in> u})"
+    then have *: "openin (subtopology euclidean (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
       by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
     show ?rhs
-      using g [OF *] by simp
+      using g [OF *] eq by auto
   next
     assume rhs: ?rhs
     show ?lhs
-      apply (rule f)
-      by (metis fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
+      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
   qed
 qed
 
 lemma continuous_left_inverse_imp_quotient_map:
-  assumes "continuous_on s f"
-      and "continuous_on (f ` s) g"
-      and  "\<And>x. x \<in> s \<Longrightarrow> g(f x) = x"
-      and "u \<subseteq> f ` s"
-    shows "openin (subtopology euclidean s) {x. x \<in> s \<and> f x \<in> u} \<longleftrightarrow>
-           openin (subtopology euclidean (f ` s)) u"
+  assumes "continuous_on S f"
+      and "continuous_on (f ` S) g"
+      and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+      and "U \<subseteq> f ` S"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+           openin (subtopology euclidean (f ` S)) U"
 apply (rule continuous_right_inverse_imp_quotient_map)
-using assms
-apply force+
+using assms apply force+
 done
 
+
 text \<open>Proving a function is constant by proving that a level set is open\<close>
 
 lemma continuous_levelset_openin_cases:
@@ -3234,17 +3210,19 @@
       and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
     shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
 proof -
-  have s: "s = {t \<in> s. h t \<in> atMost a} \<union> {t \<in> s. h t \<in> atLeast a}"
+  have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
     by force
-  have 1: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atMost a}"
+  have 1: "closedin (subtopology euclidean s) (s \<inter> h -` atMost a)"
     by (rule continuous_closedin_preimage [OF h closed_atMost])
-  have 2: "closedin (subtopology euclidean s) {t \<in> s. h t \<in> atLeast a}"
+  have 2: "closedin (subtopology euclidean s) (s \<inter> h -` atLeast a)"
     by (rule continuous_closedin_preimage [OF h closed_atLeast])
+  have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
+    by auto
   show ?thesis
     apply (rule continuous_on_subset [of s, OF _ order_refl])
     apply (subst s)
     apply (rule continuous_on_cases_local)
-    using 1 2 s assms apply auto
+    using 1 2 s assms apply (auto simp: eq)
     done
 qed
 
@@ -3761,7 +3739,7 @@
 proof -
   from imf injf have gTS: "g ` T = S"
     by force
-  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
     by force
   show ?thesis
     by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
@@ -3776,7 +3754,7 @@
 proof -
   from imf injf have gTS: "g ` T = S"
     by force
-  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
     by force
   show ?thesis
     by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
@@ -3813,7 +3791,7 @@
     and oo: "openin (subtopology euclidean S) U"
   shows "openin (subtopology euclidean T) (f ` U)"
 proof -
-  from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
     using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   from hom have "continuous_on T g"
     unfolding homeomorphism_def by blast
@@ -3828,7 +3806,7 @@
     and oo: "closedin (subtopology euclidean S) U"
   shows "closedin (subtopology euclidean T) (f ` U)"
 proof -
-  from hom oo have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
     using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
   from hom have "continuous_on T g"
     unfolding homeomorphism_def by blast
@@ -4750,17 +4728,263 @@
 lemma continuous_imp_closed_map:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "closedin (subtopology euclidean S) U"
-          "continuous_on S f" "image f S = T" "compact S"
-    shows "closedin (subtopology euclidean T) (image f U)"
+          "continuous_on S f" "f ` S = T" "compact S"
+    shows "closedin (subtopology euclidean T) (f ` U)"
   by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
 
 lemma continuous_imp_quotient_map:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
-    shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
+  assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
+    shows "openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (subtopology euclidean T) U"
-  by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
-
+  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
+
+lemma open_map_restrict:
+  assumes opeU: "openin (subtopology euclidean (S \<inter> f -` T')) U"
+    and oo: "\<And>U. openin (subtopology euclidean S) U \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+    and "T' \<subseteq> T"
+  shows "openin (subtopology euclidean T') (f ` U)"
+proof -
+  obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
+    using opeU by (auto simp: openin_open)
+  with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+    by (fastforce simp add: openin_open)
+qed
+
+lemma closed_map_restrict:
+  assumes cloU: "closedin (subtopology euclidean (S \<inter> f -` T')) U"
+    and cc: "\<And>U. closedin (subtopology euclidean S) U \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+    and "T' \<subseteq> T"
+  shows "closedin (subtopology euclidean T') (f ` U)"
+proof -
+  obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
+    using cloU by (auto simp: closedin_closed)
+  with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
+    by (fastforce simp add: closedin_closed)
+qed
+
+lemma connected_monotone_quotient_preimage:
+  assumes "connected T"
+      and contf: "continuous_on S f" and fim: "f ` S = T"
+      and opT: "\<And>U. U \<subseteq> T
+                 \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U) \<longleftrightarrow>
+                     openin (subtopology euclidean T) U"
+      and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+    shows "connected S"
+proof (rule connectedI)
+  fix U V
+  assume "open U" and "open V" and "U \<inter> S \<noteq> {}" and "V \<inter> S \<noteq> {}"
+    and "U \<inter> V \<inter> S = {}" and "S \<subseteq> U \<union> V"
+  moreover
+  have disjoint: "f ` (S \<inter> U) \<inter> f ` (S \<inter> V) = {}"
+  proof -
+    have False if "y \<in> f ` (S \<inter> U) \<inter> f ` (S \<inter> V)" for y
+    proof -
+      have "y \<in> T"
+        using fim that by blast
+      show ?thesis
+        using connectedD [OF connT [OF \<open>y \<in> T\<close>] \<open>open U\<close> \<open>open V\<close>]
+              \<open>S \<subseteq> U \<union> V\<close> \<open>U \<inter> V \<inter> S = {}\<close> that by fastforce
+    qed
+    then show ?thesis by blast
+  qed
+  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"
+    by auto
+  have opeU: "openin (subtopology euclidean T) (f ` (S \<inter> U))"
+    by (metis UU \<open>open U\<close> fim image_Int_subset le_inf_iff opT openin_open_Int)
+  have opeV: "openin (subtopology euclidean T) (f ` (S \<inter> V))"
+    by (metis opT fim VV \<open>open V\<close> openin_open_Int image_Int_subset inf.bounded_iff)
+  have "T \<subseteq> f ` (S \<inter> U) \<union> f ` (S \<inter> V)"
+    using \<open>S \<subseteq> U \<union> V\<close> fim by auto
+  then show False
+    using \<open>connected T\<close> disjoint opeU opeV \<open>U \<inter> S \<noteq> {}\<close> \<open>V \<inter> S \<noteq> {}\<close>
+    by (auto simp: connected_openin)
+qed
+
+lemma connected_open_monotone_preimage:
+  assumes contf: "continuous_on S f" and fim: "f ` S = T"
+    and ST: "\<And>C. openin (subtopology euclidean S) C \<Longrightarrow> openin (subtopology euclidean T) (f ` C)"
+    and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+    and "connected C" "C \<subseteq> T"
+  shows "connected (S \<inter> f -` C)"
+proof -
+  have contf': "continuous_on (S \<inter> f -` C) f"
+    by (meson contf continuous_on_subset inf_le1)
+  have eqC: "f ` (S \<inter> f -` C) = C"
+    using \<open>C \<subseteq> T\<close> fim by blast
+  show ?thesis
+  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
+    show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
+    proof -
+      have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
+        using that by blast
+      moreover have "connected (S \<inter> f -` {y})"
+        using \<open>C \<subseteq> T\<close> connT that by blast
+      ultimately show ?thesis
+        by metis
+    qed
+    have "\<And>U. openin (subtopology euclidean (S \<inter> f -` C)) U
+               \<Longrightarrow> openin (subtopology euclidean C) (f ` U)"
+      using open_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
+    then show "\<And>D. D \<subseteq> C
+          \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
+              openin (subtopology euclidean C) D"
+      using open_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
+  qed
+qed
+
+
+lemma connected_closed_monotone_preimage:
+  assumes contf: "continuous_on S f" and fim: "f ` S = T"
+    and ST: "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
+    and connT: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+    and "connected C" "C \<subseteq> T"
+  shows "connected (S \<inter> f -` C)"
+proof -
+  have contf': "continuous_on (S \<inter> f -` C) f"
+    by (meson contf continuous_on_subset inf_le1)
+  have eqC: "f ` (S \<inter> f -` C) = C"
+    using \<open>C \<subseteq> T\<close> fim by blast
+  show ?thesis
+  proof (rule connected_monotone_quotient_preimage [OF \<open>connected C\<close> contf' eqC])
+    show "connected (S \<inter> f -` C \<inter> f -` {y})" if "y \<in> C" for y
+    proof -
+      have "S \<inter> f -` C \<inter> f -` {y} = S \<inter> f -` {y}"
+        using that by blast
+      moreover have "connected (S \<inter> f -` {y})"
+        using \<open>C \<subseteq> T\<close> connT that by blast
+      ultimately show ?thesis
+        by metis
+    qed
+    have "\<And>U. closedin (subtopology euclidean (S \<inter> f -` C)) U
+               \<Longrightarrow> closedin (subtopology euclidean C) (f ` U)"
+      using closed_map_restrict [OF _ ST \<open>C \<subseteq> T\<close>] by metis
+    then show "\<And>D. D \<subseteq> C
+          \<Longrightarrow> openin (subtopology euclidean (S \<inter> f -` C)) (S \<inter> f -` C \<inter> f -` D) =
+              openin (subtopology euclidean C) D"
+      using closed_map_imp_quotient_map [of "(S \<inter> f -` C)" f] contf' by (simp add: eqC)
+  qed
+qed
+
+
+
+subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
+
+
+lemma connected_Un_clopen_in_complement:
+  fixes S U :: "'a::metric_space set"
+  assumes "connected S" "connected U" "S \<subseteq> U" 
+      and opeT: "openin (subtopology euclidean (U - S)) T" 
+      and cloT: "closedin (subtopology euclidean (U - S)) T"
+    shows "connected (S \<union> T)"
+proof -
+  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;
+            \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> ~(\<exists>x y. (P x y))" for P
+    by metis
+  show ?thesis
+    unfolding connected_closedin_eq
+  proof (rule *)
+    fix H1 H2
+    assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and> 
+               closedin (subtopology euclidean (S \<union> T)) H2 \<and>
+               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}"
+    then have clo: "closedin (subtopology euclidean S) (S \<inter> H1)"
+                   "closedin (subtopology euclidean S) (S \<inter> H2)"
+      by (metis Un_upper1 closedin_closed_subset inf_commute)+
+    have Seq: "S \<inter> (H1 \<union> H2) = S"
+      by (simp add: H)
+    have "S \<inter> ((S \<union> T) \<inter> H1) \<union> S \<inter> ((S \<union> T) \<inter> H2) = S"
+      using Seq by auto
+    moreover have "H1 \<inter> (S \<inter> ((S \<union> T) \<inter> H2)) = {}"
+      using H by blast
+    ultimately have "S \<inter> H1 = {} \<or> S \<inter> H2 = {}"
+      by (metis (no_types) H Int_assoc \<open>S \<inter> (H1 \<union> H2) = S\<close> \<open>connected S\<close>
+          clo Seq connected_closedin inf_bot_right inf_le1)
+    then show "S \<subseteq> H1 \<or> S \<subseteq> H2"
+      using H \<open>connected S\<close> unfolding connected_closedin by blast
+  next
+    fix H1 H2
+    assume H: "closedin (subtopology euclidean (S \<union> T)) H1 \<and>
+               closedin (subtopology euclidean (S \<union> T)) H2 \<and>
+               H1 \<union> H2 = S \<union> T \<and> H1 \<inter> H2 = {} \<and> H1 \<noteq> {} \<and> H2 \<noteq> {}" 
+       and "S \<subseteq> H1"
+    then have H2T: "H2 \<subseteq> T"
+      by auto
+    have "T \<subseteq> U"
+      using Diff_iff opeT openin_imp_subset by auto
+    with \<open>S \<subseteq> U\<close> have Ueq: "U = (U - S) \<union> (S \<union> T)" 
+      by auto
+    have "openin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
+    proof (rule openin_subtopology_Un)
+      show "openin (subtopology euclidean (S \<union> T)) H2"
+        using \<open>H2 \<subseteq> T\<close> apply (auto simp: openin_closedin_eq)
+        by (metis Diff_Diff_Int Diff_disjoint Diff_partition Diff_subset H Int_absorb1 Un_Diff)
+      then show "openin (subtopology euclidean (U - S)) H2"
+        by (meson H2T Un_upper2 opeT openin_subset_trans openin_trans)
+    qed
+    moreover have "closedin (subtopology euclidean ((U - S) \<union> (S \<union> T))) H2"
+    proof (rule closedin_subtopology_Un)
+      show "closedin (subtopology euclidean (U - S)) H2"
+        using H H2T cloT closedin_subset_trans 
+        by (blast intro: closedin_subtopology_Un closedin_trans)
+    qed (simp add: H)
+    ultimately
+    have H2: "H2 = {} \<or> H2 = U"
+      using Ueq \<open>connected U\<close> unfolding connected_clopen by metis   
+    then have "H2 \<subseteq> S"
+      by (metis Diff_partition H Un_Diff_cancel Un_subset_iff \<open>H2 \<subseteq> T\<close> assms(3) inf.orderE opeT openin_imp_subset)
+    moreover have "T \<subseteq> H2 - S"
+      by (metis (no_types) H2 H opeT openin_closedin_eq topspace_euclidean_subtopology)
+    ultimately show False
+      using H \<open>S \<subseteq> H1\<close> by blast
+  qed blast
+qed
+
+
+proposition component_complement_connected:
+  fixes S :: "'a::metric_space set"
+  assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
+  shows "connected(U - C)"
+  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+proof clarify
+  fix H3 H4 
+  assume clo3: "closedin (subtopology euclidean (U - C)) H3" 
+    and clo4: "closedin (subtopology euclidean (U - C)) H4" 
+    and "H3 \<union> H4 = U - C" and "H3 \<inter> H4 = {}" and "H3 \<noteq> {}" and "H4 \<noteq> {}"
+    and * [rule_format]:
+    "\<forall>H1 H2. \<not> closedin (subtopology euclidean S) H1 \<or>
+                      \<not> closedin (subtopology euclidean S) H2 \<or>
+                      H1 \<union> H2 \<noteq> S \<or> H1 \<inter> H2 \<noteq> {} \<or> \<not> H1 \<noteq> {} \<or> \<not> H2 \<noteq> {}"
+  then have "H3 \<subseteq> U-C" and ope3: "openin (subtopology euclidean (U - C)) (U - C - H3)"
+    and "H4 \<subseteq> U-C" and ope4: "openin (subtopology euclidean (U - C)) (U - C - H4)"
+    by (auto simp: closedin_def)
+  have "C \<noteq> {}" "C \<subseteq> U-S" "connected C"
+    using C in_components_nonempty in_components_subset in_components_maximal by blast+
+  have cCH3: "connected (C \<union> H3)"
+  proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo3])
+    show "openin (subtopology euclidean (U - C)) H3"
+      apply (simp add: openin_closedin_eq \<open>H3 \<subseteq> U - C\<close>)
+      apply (simp add: closedin_subtopology)
+      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)
+  qed (use clo3 \<open>C \<subseteq> U - S\<close> in auto)
+  have cCH4: "connected (C \<union> H4)"
+  proof (rule connected_Un_clopen_in_complement [OF \<open>connected C\<close> \<open>connected U\<close> _ _ clo4])
+    show "openin (subtopology euclidean (U - C)) H4"
+      apply (simp add: openin_closedin_eq \<open>H4 \<subseteq> U - C\<close>)
+      apply (simp add: closedin_subtopology)
+      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)
+  qed (use clo4 \<open>C \<subseteq> U - S\<close> in auto)
+  have "closedin (subtopology euclidean S) (S \<inter> H3)" "closedin (subtopology euclidean S) (S \<inter> H4)"
+    using clo3 clo4 \<open>S \<subseteq> U\<close> \<open>C \<subseteq> U - S\<close> by (auto simp: closedin_closed)
+  moreover have "S \<inter> H3 \<noteq> {}"      
+    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
+  moreover have "S \<inter> H4 \<noteq> {}"
+    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
+  ultimately show False
+    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> 
+    by auto
+qed
 
 subsection\<open> Finite intersection property\<close>
 
@@ -4952,15 +5176,12 @@
   assume "open U"
   have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
     using clo openin_imp_subset by blast
-  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
-    apply (auto simp: dest: S)
-      apply (metis (no_types, lifting) g mem_Collect_eq)
-    using clo f g openin_imp_subset by fastforce
-  show "openin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+    using S f g by fastforce
+  show "openin (subtopology euclidean S) (S \<inter> g -` U)"
     apply (subst *)
     apply (rule openin_Union, clarify)
-    apply (metis (full_types) \<open>open U\<close> cont clo openin_trans continuous_openin_preimage_gen)
-    done
+    using \<open>open U\<close> clo cont continuous_openin_preimage_gen openin_trans by blast
 qed
 
 lemma pasting_lemma_exists:
@@ -4996,13 +5217,11 @@
 proof (clarsimp simp: continuous_closedin_preimage_eq)
   fix U :: "'b set"
   assume "closed U"
-  have *: "{x \<in> S. g x \<in> U} = \<Union>{{x. x \<in> (T i) \<and> (f i x) \<in> U} |i. i \<in> I}"
-    apply auto
-    apply (metis (no_types, lifting) g mem_Collect_eq)
-    using clo closedin_closed apply blast
-    apply (metis Int_iff f g clo closedin_limpt inf.absorb_iff2)
-    done
-  show "closedin (subtopology euclidean S) {x \<in> S. g x \<in> U}"
+  have S: "\<And>i. i \<in> I \<Longrightarrow> (T i) \<subseteq> S"
+    using clo closedin_imp_subset by blast
+  have *: "(S \<inter> g -` U) = (\<Union>i \<in> I. T i \<inter> f i -` U)"
+    using S f g by fastforce
+  show "closedin (subtopology euclidean S) (S \<inter> g -` U)"
     apply (subst *)
     apply (rule closedin_Union)
     using \<open>finite I\<close> apply simp
@@ -5119,9 +5338,10 @@
       and conf: "continuous_on S f"
       and fim: "f ` S \<subseteq> t"
       and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
-    shows "\<exists>a. \<forall>x \<in> S. f x = a"
+    shows "f constant_on S"
 proof (cases "S = {}")
-  case True then show ?thesis by force
+  case True then show ?thesis
+    by (simp add: constant_on_def)
 next
   case False
   { fix x assume "x \<in> S"
@@ -5129,7 +5349,7 @@
     by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI S cct)
   }
   with False show ?thesis
-    by blast
+    unfolding constant_on_def by blast
 qed
 
 lemma discrete_subset_disconnected:
@@ -5195,7 +5415,7 @@
 text\<open>This proof requires the existence of two separate values of the range type.\<close>
 lemma finite_range_constant_imp_connected:
   assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> S. f x = a"
+              \<lbrakk>continuous_on S f; finite(f ` S)\<rbrakk> \<Longrightarrow> f constant_on S"
     shows "connected S"
 proof -
   { fix t u
@@ -5212,7 +5432,7 @@
       by (rule finite_subset [of _ "{0,1}"]) auto
     have "t = {} \<or> u = {}"
       using assms [OF conif fi] tus [symmetric]
-      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
+      by (auto simp: Ball_def constant_on_def) (metis IntI empty_iff one_neq_zero tue)
   }
   then show ?thesis
     by (simp add: connected_closedin_eq)
@@ -5222,18 +5442,18 @@
       "(connected S \<longleftrightarrow>
            (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
             \<forall>t. continuous_on S f \<and> f ` S \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
-            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis1)
+            \<longrightarrow> f constant_on S))" (is ?thesis1)
   and continuous_discrete_range_constant_eq:
       "(connected S \<longleftrightarrow>
          (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
           continuous_on S f \<and>
           (\<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)))
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis2)
+          \<longrightarrow> f constant_on S))" (is ?thesis2)
   and continuous_finite_range_constant_eq:
       "(connected S \<longleftrightarrow>
          (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
           continuous_on S f \<and> finite (f ` S)
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> S. f x = a)))" (is ?thesis3)
+          \<longrightarrow> f constant_on S))" (is ?thesis3)
 proof -
   have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
     \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
@@ -5255,18 +5475,16 @@
   assumes S: "connected S"
       and "continuous_on S f"
       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)"
-    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
-  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms
-  by blast
+    shows "f constant_on S"
+  using continuous_discrete_range_constant_eq [THEN iffD1, OF S] assms by blast
 
 lemma continuous_finite_range_constant:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   assumes "connected S"
       and "continuous_on S f"
       and "finite (f ` S)"
-    obtains a where "\<And>x. x \<in> S \<Longrightarrow> f x = a"
-  using assms continuous_finite_range_constant_eq
-  by blast
+    shows "f constant_on S"
+  using assms continuous_finite_range_constant_eq  by blast
 
 
 
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -281,10 +281,7 @@
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
           "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
-apply (rule Urysohn_local_strong [of UNIV S T])
-using assms
-apply (auto simp: closed_closedin)
-done
+using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
 
 proposition Urysohn:
   assumes US: "closed S"
@@ -295,10 +292,7 @@
           "\<And>x. f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
-apply (rule Urysohn_local [of UNIV S T a b])
-using assms
-apply (auto simp: closed_closedin)
-done
+using assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
 subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -1271,15 +1271,17 @@
     using g by (simp add: image_comp)
   have cgf: "closed (g ` f ` S)"
     by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
-  have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
-    using g by (simp add: o_def id_def image_def) metis
+  have [simp]: "(range f \<inter> g -` S) = f ` S"
+    using g unfolding o_def id_def image_def by auto metis+
   show ?thesis
-    apply (rule closedin_closed_trans [of "range f"])
-    apply (rule continuous_closedin_preimage [OF confg cgf, simplified])
-    apply (rule closed_injective_image_subspace)
-    using f
-    apply (auto simp: linear_linear linear_injective_0)
-    done
+  proof (rule closedin_closed_trans [of "range f"])
+    show "closedin (subtopology euclidean (range f)) (f ` S)"
+      using continuous_closedin_preimage [OF confg cgf] by simp
+    show "closed (range f)"
+      apply (rule closed_injective_image_subspace)
+      using f apply (auto simp: linear_linear linear_injective_0)
+      done
+  qed
 qed
 
 lemma closed_injective_linear_image_eq:
@@ -2374,16 +2376,13 @@
   by(simp add: convex_connected)
 
 proposition clopen:
-  fixes s :: "'a :: real_normed_vector set"
-  shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
-apply (rule iffI)
- apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
- apply (force simp add: closed_closedin, force)
-done
+  fixes S :: "'a :: real_normed_vector set"
+  shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
+    by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
 
 corollary compact_open:
-  fixes s :: "'a :: euclidean_space set"
-  shows "compact s \<and> open s \<longleftrightarrow> s = {}"
+  fixes S :: "'a :: euclidean_space set"
+  shows "compact S \<and> open S \<longleftrightarrow> S = {}"
   by (auto simp: compact_eq_bounded_closed clopen)
 
 corollary finite_imp_not_open:
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -2318,9 +2318,9 @@
 proof (clarsimp simp add: continuous_openin_preimage_eq)
   fix T :: "'a set"
   assume "open T"
-  have eq: "{x. x \<in> f ` S \<and> g x \<in> T} = f ` (S \<inter> T)"
+  have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
     by (auto simp: gf)
-  show "openin (subtopology euclidean (f ` S)) {x \<in> f ` S. g x \<in> T}"
+  show "openin (subtopology euclidean (f ` S)) (f ` S \<inter> g -` T)"
     apply (subst eq)
     apply (rule open_openin_trans)
       apply (rule invariance_of_domain_gen)
@@ -3173,7 +3173,7 @@
   have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
     using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
   have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
-               (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
+               (\<exists>v. \<Union>v = -{0} \<inter> (\<lambda>z. z ^ n) -` T \<and>
                     (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
                     pairwise disjnt v \<and>
                     (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
@@ -3216,8 +3216,6 @@
       by (intro continuous_intros)
     have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
       by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
-    have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
-      by (rule invariance_of_domain [OF cont open_ball inj])
     have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
                 if z': "z'^n = z^n" for z'
     proof -
@@ -3262,6 +3260,7 @@
       qed
       then show ?thesis by blast
     qed
+
     have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
                   if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
     proof -
@@ -3286,50 +3285,63 @@
         apply (simp add: dist_norm)
         done
     qed
-    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}"
-      apply (rule equalityI)
-       prefer 2 apply (force simp: ex_ball, clarsimp)
-      apply (subst im_eq [symmetric], assumption)
-      using assms
-      apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
-      done
-    have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
-    proof (clarsimp simp add: pairwise_def disjnt_iff)
-      fix \<xi> \<zeta> x
-      assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
-         and "dist \<xi> x < d" "dist \<zeta> x < d"
-      then have "dist \<xi> \<zeta> < d+d"
-        using dist_triangle_less_add by blast
-      then have "cmod (\<xi> - \<zeta>) < 2*d"
-        by (simp add: dist_norm)
-      also have "... \<le> e * cmod z"
-        using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
-      finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
-      with e have "\<xi> = \<zeta>"
-        by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
-      then show "False"
-        using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+
+    show ?thesis
+    proof (rule exI, intro conjI)
+      show "z ^ n \<in> (\<lambda>w. w ^ n) ` ball z d"
+        using \<open>d > 0\<close> by simp
+      show "open ((\<lambda>w. w ^ n) ` ball z d)"
+        by (rule invariance_of_domain [OF cont open_ball inj])
+      show "0 \<notin> (\<lambda>w. w ^ n) ` ball z d"
+        using \<open>z \<noteq> 0\<close> assms by (force simp: d_def)
+      show "\<exists>v. \<Union>v = - {0} \<inter> (\<lambda>z. z ^ n) -` (\<lambda>w. w ^ n) ` ball z d \<and>
+                (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
+                disjoint v \<and>
+                (\<forall>u\<in>v. Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n)))"
+      proof (rule exI, intro ballI conjI)
+        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")
+        proof 
+          show "?l \<subseteq> ?r"
+            apply auto
+             apply (simp add: assms d_def power_eq_imp_eq_norm that)
+            by (metis im_eq image_eqI mem_ball)
+          show "?r \<subseteq> ?l"
+            by auto (meson ex_ball)
+        qed
+        show "\<And>u. u \<in> {ball z' d |z'. z' ^ n = z ^ n} \<Longrightarrow> 0 \<notin> u"
+          by (force simp add: assms d_def power_eq_imp_eq_norm that)
+
+        show "disjoint {ball z' d |z'. z' ^ n = z ^ n}"
+        proof (clarsimp simp add: pairwise_def disjnt_iff)
+          fix \<xi> \<zeta> x
+          assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
+            and "dist \<xi> x < d" "dist \<zeta> x < d"
+          then have "dist \<xi> \<zeta> < d+d"
+            using dist_triangle_less_add by blast
+          then have "cmod (\<xi> - \<zeta>) < 2*d"
+            by (simp add: dist_norm)
+          also have "... \<le> e * cmod z"
+            using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
+          finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
+          with e have "\<xi> = \<zeta>"
+            by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
+          then show "False"
+            using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+        qed
+        show "Ex (homeomorphism u ((\<lambda>w. w ^ n) ` ball z d) (\<lambda>z. z ^ n))"
+          if "u \<in> {ball z' d |z'. z' ^ n = z ^ n}" for u
+        proof (rule invariance_of_domain_homeomorphism [of "u" "\<lambda>z. z^n"])
+          show "open u"
+            using that by auto
+          show "continuous_on u (\<lambda>z. z ^ n)"
+            by (intro continuous_intros)
+          show "inj_on (\<lambda>z. z ^ n) u"
+            using that by (auto simp: iff_x_eq_y inj_on_def)
+          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))"
+            using im_eq that by clarify metis
+        qed auto
+      qed auto
     qed
-    have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
-            if zeq: "z'^n = z^n" for z'
-    proof -
-      have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
-        by (meson iff_x_eq_y inj_onI zeq)
-      show ?thesis
-        apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
-          apply (rule open_ball continuous_intros order_refl inj)+
-        apply (force simp: im_eq [OF zeq])
-        done
-    qed
-    show ?thesis
-      apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
-      apply (intro conjI open_imball)
-        using \<open>d > 0\<close> apply simp
-       using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
-      apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
-      apply (intro conjI ball1 ball2)
-       apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
-      by (metis ball3)
   qed
   show ?thesis
     using assms
@@ -3353,7 +3365,7 @@
   show "range exp = - {0::complex}"
     by auto (metis exp_Ln range_eqI)
   show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
-             (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
+             (\<exists>v. \<Union>v = exp -` T \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
                   (\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
         if "z \<in> - {0::complex}" for z
   proof -
@@ -3374,8 +3386,8 @@
         using pi_ge_two by (simp add: ball_subset_ball_iff)
       ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
         by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
-      show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
-        by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
+      show "\<Union>\<V> = exp -` exp ` ball (Ln z) 1"
+        by (force simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
       show "\<forall>V\<in>\<V>. open V"
         by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
       have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
@@ -4314,7 +4326,7 @@
     qed
   next
     case False
-    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
     proof (rule continuous_discrete_range_constant [OF ST])
       show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
         apply (intro continuous_intros)
@@ -4338,7 +4350,9 @@
         then show ?thesis
           by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
       qed
-    qed blast
+    qed 
+    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+      by (auto simp: constant_on_def)
     with False have "exp a = 1"
       by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
     with a show ?thesis
@@ -4382,7 +4396,7 @@
     qed
   next
     case False
-    obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+    have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
     proof (rule continuous_discrete_range_constant [OF ST])
       show "continuous_on (S \<inter> T) (\<lambda>x. g x - h x)"
         apply (intro continuous_intros)
@@ -4406,7 +4420,9 @@
         then show ?thesis
           by (rule_tac x="2*pi" in exI) (fastforce simp add: algebra_simps)
       qed
-    qed blast
+    qed
+    then obtain a where a: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = a"
+      by (auto simp: constant_on_def)
     with False have "exp a = 1"
       by (metis IntI disjoint_iff_not_equal divide_self_if exp_diff exp_not_eq_zero fg fh)
     with a show ?thesis
@@ -4441,7 +4457,7 @@
     using fim by auto
   then obtain f' where f': "\<And>y. y \<in> T \<longrightarrow> f' y \<in> S \<and> f (f' y) = y"
     by metis
-  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
+  have *: "(\<lambda>x. h x - h(f' y)) constant_on {x. x \<in> S \<and> f x = y}" if "y \<in> T" for y
   proof (rule continuous_discrete_range_constant [OF conn [OF that], of "\<lambda>x. h x - h (f' y)"], simp_all add: algebra_simps)
     show "continuous_on {x \<in> S. f x = y} (\<lambda>x. h x - h (f' y))"
       by (intro continuous_intros continuous_on_subset [OF conth]) auto
@@ -4462,13 +4478,12 @@
     qed
   qed 
   have "h x = h (f' (f x))" if "x \<in> S" for x
-    using * [of "f x"] fim that apply clarsimp
-    by (metis f' imageI right_minus_eq)
+    using * [of "f x"] fim that unfolding constant_on_def by clarsimp (metis f' imageI right_minus_eq)
   moreover have "\<And>x. x \<in> T \<Longrightarrow> \<exists>u. u \<in> S \<and> x = f u \<and> h (f' x) = h u"
     using f' by fastforce
   ultimately
   have eq: "((\<lambda>x. (x, (h \<circ> f') x)) ` T) =
-            {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}}}"
+            {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})}"
     using fim by (auto simp: image_iff)
   show "\<exists>h. continuous_on T h \<and> (\<forall>x\<in>T. g x = exp (h x))"
   proof (intro exI conjI)
@@ -4513,9 +4528,10 @@
     proof (rule compact_continuous_image)
       show "continuous_on {x \<in> S. f x = y} h"
         by (rule continuous_on_subset [OF conth]) auto
-      have "compact {x \<in> S. f x \<in> {y}}"
+      have "compact (S \<inter> f -` {y})"
         by (rule proper_map_from_compact [OF contf _ \<open>compact S\<close>, of T]) (simp_all add: fim that)
-      then show "compact {x \<in> S. f x = y}" by simp
+      then show "compact {x \<in> S. f x = y}" 
+        by (auto simp: vimage_def Int_def)
     qed
     have 2: "h ` {x \<in> S. f x = y} \<noteq> {}"
       using fim that by auto
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -3187,17 +3187,15 @@
   proof -
     have "e * r > 0" using that \<open>0 < r\<close> by simp
     with intfi[unfolded has_integral]
-    obtain d where d: "gauge d"
-                   "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
+    obtain d where "gauge d"
+               and d: "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
                         \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e * r" 
       by metis
-    define d' where "d' x = {y. g y \<in> d (g x)}" for x
-    have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
-      unfolding d'_def ..
+    define d' where "d' x = g -` d (g x)" for x
     show ?thesis
     proof (rule_tac x=d' in exI, safe)
       show "gauge d'"
-        using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
+        using \<open>gauge d\<close> continuous_open_vimage[OF _ contg] by (auto simp: gauge_def d'_def)
     next
       fix p
       assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
@@ -3211,7 +3209,7 @@
         show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
           using ptag by auto
         show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
-          using finep unfolding fine_def d' by auto
+          using finep unfolding fine_def d'_def by auto
       next
         fix x k
         assume xk: "(x, k) \<in> p"
@@ -3259,7 +3257,7 @@
         using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
       finally have eq: "?l = ?r" .
       show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
-        using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
+        using d[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
     qed
   qed
   then show ?thesis
@@ -4229,7 +4227,7 @@
     and "x \<in> S"
   shows "f x = y"
 proof -
-  have xx: "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}" if "x \<in> S" for x
+  have "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})" if "x \<in> S" for x
   proof -
     obtain e where "0 < e" and e: "ball x e \<subseteq> S"
       using \<open>x \<in> S\<close> \<open>open S\<close> open_contains_ball by blast
@@ -4248,15 +4246,15 @@
           by (metis Diff_iff contra_subsetD derf e has_derivative_within_subset that)
       qed (use y e \<open>0 < e\<close> in auto)
     qed
-    then show "\<exists>e>0. ball x e \<subseteq> {xa \<in> S. f xa \<in> {f x}}"
+    then show "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})"
       using \<open>0 < e\<close> by blast
   qed
-  then have "openin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
+  then have "openin (subtopology euclidean S) (S \<inter> f -` {y})"
     by (auto intro!: open_openin_trans[OF \<open>open S\<close>] simp: open_contains_ball)
-  moreover have "closedin (subtopology euclidean S) {x \<in> S. f x \<in> {y}}"
+  moreover have "closedin (subtopology euclidean S) (S \<inter> f -` {y})"
     by (force intro!: continuous_closedin_preimage [OF contf])
-  ultimately have "{x \<in> S. f x \<in> {y}} = {} \<or> {x \<in> S. f x \<in> {y}} = S"
-    using \<open>connected S\<close> connected_clopen by blast
+  ultimately have "(S \<inter> f -` {y}) = {} \<or> (S \<inter> f -` {y}) = S"
+    using \<open>connected S\<close> by (simp add: connected_clopen)
   then show ?thesis
     using \<open>x \<in> S\<close> \<open>f c = y\<close> \<open>c \<in> S\<close> by auto
 qed
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -1089,14 +1089,14 @@
       by force
     have *: "r *\<^sub>R b = One \<Longrightarrow> b = (1 / r) *\<^sub>R One" for r and b::'b
       by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
-    have "f ` U = {z. (setdist {fst z} (- U) *\<^sub>R snd z) \<in> {One}}"
+    have "f ` U = (\<lambda>z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
       apply (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
       apply (rule_tac x=a in image_eqI)
       apply (auto simp: * setdist_eq_0_sing_1 dest: setdist1D)
       done
     then have clfU: "closed (f ` U)"
       apply (rule ssubst)
-      apply (rule continuous_closed_preimage_univ)
+      apply (rule continuous_closed_vimage)
       apply (auto intro: continuous_intros cont [unfolded o_def])
       done
     have "closed (f ` S)"
@@ -1278,7 +1278,7 @@
   "covering_space c p S \<equiv>
        continuous_on c p \<and> p ` c = S \<and>
        (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
-                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
+                    (\<exists>v. \<Union>v = c \<inter> p -` T \<and>
                         (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
                         pairwise disjnt v \<and>
                         (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
@@ -1302,16 +1302,16 @@
                       "homeomorphism T u p q"
 using assms
 apply (simp add: covering_space_def, clarify)
-apply (drule_tac x="p x" in bspec, force)
-by (metis (no_types, lifting) Union_iff mem_Collect_eq)
+  apply (drule_tac x="p x" in bspec, force)
+  by (metis IntI UnionE vimage_eq) 
 
 
 lemma covering_space_local_homeomorphism_alt:
   assumes p: "covering_space c p S" and "y \<in> S"
-  obtains x T u q where "p x = y"
+  obtains x T U q where "p x = y"
                         "x \<in> T" "openin (subtopology euclidean c) T"
-                        "y \<in> u" "openin (subtopology euclidean S) u"
-                          "homeomorphism T u p q"
+                        "y \<in> U" "openin (subtopology euclidean S) U"
+                          "homeomorphism T U p q"
 proof -
   obtain x where "p x = y" "x \<in> c"
     using assms covering_space_imp_surjective by blast
@@ -1329,7 +1329,7 @@
    and covs:
        "\<And>x. x \<in> S \<Longrightarrow>
             \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
-                  \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
+                  \<Union>VS = c \<inter> p -` X \<and>
                   (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
                   pairwise disjnt VS \<and>
                   (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
@@ -1340,7 +1340,7 @@
   proof -
     have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
     obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
-                  and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
+                  and VS: "\<Union>VS = c \<inter> p -` U"
                   and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
                   and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
       using covs [OF \<open>y \<in> S\<close>] by auto
@@ -1349,16 +1349,16 @@
       using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
     with VS obtain V where "x \<in> V" "V \<in> VS" by auto
     then obtain q where q: "homeomorphism V U p q" using homVS by blast
-    then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
+    then have ptV: "p ` (T \<inter> V) = U \<inter> q -` (T \<inter> V)"
       using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
     have ocv: "openin (subtopology euclidean c) V"
       by (simp add: \<open>V \<in> VS\<close> openVS)
-    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
+    have "openin (subtopology euclidean U) (U \<inter> q -` (T \<inter> V))"
       apply (rule continuous_on_open [THEN iffD1, rule_format])
        using homeomorphism_def q apply blast
       using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
       by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
-    then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
+    then have os: "openin (subtopology euclidean S) (U \<inter> q -` (T \<inter> V))"
       using openin_trans [of U] by (simp add: Collect_conj_eq U)
     show ?thesis
       apply (rule_tac x = "p ` (T \<inter> V)" in exI)
@@ -1400,20 +1400,19 @@
        using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
       done
     have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
-    have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
+    have gg: "U \<inter> g -` v = U \<inter> g -` (v \<inter> g ` U)" for g
       by auto
     have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
       using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
-    then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
+    then have 1: "openin (subtopology euclidean U) (U \<inter> g1 -` v)"
       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
     have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
       using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
-    then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
+    then have 2: "openin (subtopology euclidean U) (U \<inter> g2 -` v)"
       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
-    show "\<exists>T. openin (subtopology euclidean U) T \<and>
-              z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
+    show "\<exists>T. openin (subtopology euclidean U) T \<and> z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
       using z
-      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)
+      apply (rule_tac x = "(U \<inter> g1 -` v) \<inter> (U \<inter> g2 -` v)" in exI)
       apply (intro conjI)
       apply (rule openin_Int [OF 1 2])
       using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
@@ -1475,7 +1474,7 @@
       by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
     then obtain T \<V> where "p x \<in> T"
                       and opeT: "openin (subtopology euclidean S) T"
-                      and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}"
+                      and veq: "\<Union>\<V> = C \<inter> p -` T"
                       and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
                       and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
       using cov unfolding covering_space_def by (blast intro: that)
@@ -1583,7 +1582,7 @@
         if "y \<in> U" for y
   proof -
     obtain UU where UU: "\<And>s. s \<in> S \<Longrightarrow> s \<in> (UU s) \<and> openin (subtopology euclidean S) (UU s) \<and>
-                                        (\<exists>\<V>. \<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU s)} \<and>
+                                        (\<exists>\<V>. \<Union>\<V> = C \<inter> p -` UU s \<and>
                                             (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
                                             pairwise disjnt \<V> \<and>
                                             (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U (UU s) p q))"
@@ -1595,13 +1594,13 @@
     proof -
       have hinS: "h (t, y) \<in> S"
         using \<open>y \<in> U\<close> him that by blast
-      then have "(t,y) \<in> {z \<in> {0..1} \<times> U. h z \<in> UU (h (t, y))}"
+      then have "(t,y) \<in> ({0..1} \<times> U) \<inter> h -` UU(h(t, y))"
         using \<open>y \<in> U\<close> \<open>t \<in> {0..1}\<close>  by (auto simp: ope)
-      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))}"
+      moreover have ope_01U: "openin (subtopology euclidean ({0..1} \<times> U)) (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
         using hinS ope continuous_on_open_gen [OF him] conth by blast
       ultimately obtain V W where opeV: "open V" and "t \<in> {0..1} \<inter> V" "t \<in> {0..1} \<inter> V"
                               and opeW: "open W" and "y \<in> U" "y \<in> W"
-                              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))}"
+                              and VW: "({0..1} \<inter> V) \<times> (U \<inter> W)  \<subseteq> (({0..1} \<times> U) \<inter> h -` UU(h(t, y)))"
         by (rule Times_in_interior_subtopology) (auto simp: openin_open)
       then show ?thesis
         using hinS by blast
@@ -1677,7 +1676,7 @@
       qed blast
       have t01: "t \<in> {0..1}"
         using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
-      obtain \<V> where "\<Union>\<V> = {x. x \<in> C \<and> p x \<in> (UU (X t))}"
+      obtain \<V> where \<V>: "\<Union>\<V> = C \<inter> p -` UU (X t)"
                  and opeC: "\<And>U. U \<in> \<V> \<Longrightarrow> openin (subtopology euclidean C) U"
                  and "pairwise disjnt \<V>"
                  and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
@@ -1686,7 +1685,7 @@
         using N by (auto simp: divide_simps algebra_simps)
       with t have nN_in_kkt: "real n / real N \<in> K t"
         by blast
-      have "k (real n / real N, y) \<in> {x. x \<in> C \<and> p x \<in> (UU (X t))}"
+      have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
       proof (simp, rule conjI)
         show "k (real n / real N, y) \<in> C"
           using \<open>y \<in> V\<close> kim keq by force
@@ -1701,8 +1700,8 @@
           using him t01 by blast
         finally show "p (k (real n / real N, y)) \<in> UU (X t)" .
       qed
-      then have "k (real n / real N, y) \<in> \<Union>\<V>"
-        using \<open>\<Union>\<V> = {x \<in> C. p x \<in> UU (X t)}\<close> by blast
+      with \<V> have "k (real n / real N, y) \<in> \<Union>\<V>"
+        by blast
       then obtain W where W: "k (real n / real N, y) \<in> W" and "W \<in> \<V>"
         by blast
       then obtain p' where opeC': "openin (subtopology euclidean C) W"
@@ -1711,14 +1710,14 @@
       then have "W \<subseteq> C"
         using openin_imp_subset by blast
       define W' where "W' = UU(X t)"
-      have opeVW: "openin (subtopology euclidean V) {z \<in> V. (k \<circ> Pair (real n / real N)) z \<in> W}"
+      have opeVW: "openin (subtopology euclidean V) (V \<inter> (k \<circ> Pair (n / N)) -` W)"
         apply (rule continuous_openin_preimage [OF _ _ opeC'])
          apply (intro continuous_intros continuous_on_subset [OF contk])
         using kim apply (auto simp: \<open>y \<in> V\<close> W)
         done
       obtain N' where opeUN': "openin (subtopology euclidean U) N'"
                   and "y \<in> N'" and kimw: "k ` ({(real n / real N)} \<times> N') \<subseteq> W"
-        apply (rule_tac N' = "{z \<in> V. (k \<circ> Pair ((real n / real N))) z \<in> W}" in that)
+        apply (rule_tac N' = "(V \<inter> (k \<circ> Pair (n / N)) -` W)" in that)
         apply (fastforce simp:  \<open>y \<in> V\<close> W intro!: openin_trans [OF opeVW opeUV])+
         done
       obtain Q Q' where opeUQ: "openin (subtopology euclidean U) Q"
@@ -2283,7 +2282,7 @@
       using l [of "linepath z z" z "linepath a a"] by (auto simp: assms)
     show LC: "l ` U \<subseteq> C"
       by (clarify dest!: *) (metis (full_types) l pathfinish_in_path_image subsetCE)
-    have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> {x \<in> U. l x \<in> X}"
+    have "\<exists>T. openin (subtopology euclidean U) T \<and> y \<in> T \<and> T \<subseteq> U \<inter> l -` X"
          if X: "openin (subtopology euclidean C) X" and "y \<in> U" "l y \<in> X" for X y
     proof -
       have "X \<subseteq> C"
@@ -2292,7 +2291,7 @@
         using fim \<open>y \<in> U\<close> by blast
       then obtain W \<V>
               where WV: "f y \<in> W \<and> openin (subtopology euclidean S) W \<and>
-                         (\<Union>\<V> = {x. x \<in> C \<and> p x \<in> W} \<and>
+                         (\<Union>\<V> = C \<inter> p -` W \<and>
                           (\<forall>U \<in> \<V>. openin (subtopology euclidean C) U) \<and>
                           pairwise disjnt \<V> \<and>
                           (\<forall>U \<in> \<V>. \<exists>q. homeomorphism U W p q))"
@@ -2309,12 +2308,12 @@
       obtain V where "y \<in> V" "y \<in> U" and fimW: "f ` V \<subseteq> W" "V \<subseteq> U"
                  and "path_connected V" and opeUV: "openin (subtopology euclidean U) V"
       proof -
-        have "openin (subtopology euclidean U) {c \<in> U. f c \<in> W}"
+        have "openin (subtopology euclidean U) (U \<inter> f -` W)"
           using WV contf continuous_on_open_gen fim by auto
         then show ?thesis
           using U WV
           apply (auto simp: locally_path_connected)
-          apply (drule_tac x="{x. x \<in> U \<and> f x \<in> W}" in spec)
+          apply (drule_tac x="U \<inter> f -` W" in spec)
           apply (drule_tac x=y in spec)
           apply (auto simp: \<open>y \<in> U\<close> intro: that)
           done
@@ -2325,23 +2324,23 @@
         using homUW' homeomorphism_image2 by fastforce
       show ?thesis
       proof (intro exI conjI)
-        have "openin (subtopology euclidean S) {x \<in> W. p' x \<in> W' \<inter> X}"
+        have "openin (subtopology euclidean S) (W \<inter> p' -` (W' \<inter> X))"
         proof (rule openin_trans)
-          show "openin (subtopology euclidean W) {x \<in> W. p' x \<in> W' \<inter> X}"
+          show "openin (subtopology euclidean W) (W \<inter> p' -` (W' \<inter> X))"
             apply (rule continuous_openin_preimage [OF contp' p'im])
             using X \<open>W' \<subseteq> C\<close> apply (auto simp: openin_open)
             done
           show "openin (subtopology euclidean S) W"
             using WV by blast
         qed
-        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}})"
-          by (intro openin_Int opeUV continuous_openin_preimage [OF contf fim])
-        have "p' (f y) \<in> X"
+        then show "openin (subtopology euclidean U) (V \<inter> (U \<inter> (f -` (W \<inter> (p' -` (W' \<inter> X))))))"
+          by (blast intro: opeUV openin_subtopology_self continuous_openin_preimage [OF contf fim])
+         have "p' (f y) \<in> X"
           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
-        then show "y \<in> V \<inter> {x \<in> U. f x \<in> {x \<in> W. p' x \<in> W' \<inter> X}}"
+        then show "y \<in> V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X)))"
           using \<open>y \<in> U\<close> \<open>y \<in> V\<close> WV p'im by auto
-        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}"
-        proof clarsimp
+        show "V \<inter> (U \<inter> f -` (W \<inter> p' -` (W' \<inter> X))) \<subseteq> U \<inter> l -` X"
+        proof (intro subsetI IntI; clarify)
           fix y'
           assume y': "y' \<in> V" "y' \<in> U" "f y' \<in> W" "p' (f y') \<in> W'" "p' (f y') \<in> X"
           then obtain \<gamma> where "path \<gamma>" "path_image \<gamma> \<subseteq> V" "pathstart \<gamma> = y" "pathfinish \<gamma> = y'"
@@ -2354,7 +2353,7 @@
           have finW: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> f (\<gamma> x) \<in> W"
             using \<open>path_image \<gamma> \<subseteq> V\<close> by (auto simp: image_subset_iff path_image_def fimW [THEN subsetD])
           have "pathfinish (qq +++ (p' \<circ> f \<circ> \<gamma>)) = l y'"
-          proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)" ])
+          proof (rule l [of "pp +++ \<gamma>" y' "qq +++ (p' \<circ> f \<circ> \<gamma>)"])
             show "path (pp +++ \<gamma>)"
               by (simp add: \<open>path \<gamma>\<close> \<open>path pp\<close> \<open>pathfinish pp = y\<close> \<open>pathstart \<gamma> = y\<close>)
             show "path_image (pp +++ \<gamma>) \<subseteq> U"
@@ -2395,14 +2394,13 @@
                 using that \<xi> by auto
             qed
           qed
-          with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "l y' \<in> X"
+          with \<open>pathfinish \<gamma> = y'\<close>  \<open>p' (f y') \<in> X\<close> show "y' \<in> l -` X"
             unfolding pathfinish_join by (simp add: pathfinish_def)
         qed
       qed
     qed
     then show "continuous_on U l"
-      using openin_subopen continuous_on_open_gen [OF LC]
-      by (metis (no_types, lifting) mem_Collect_eq)
+      by (metis IntD1 IntD2 vimage_eq openin_subopen continuous_on_open_gen [OF LC])
   qed
 qed
 
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -88,8 +88,10 @@
       then show ?thesis
         by (rule_tac x="2*pi" in exI) auto
     qed
-    ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
+    ultimately have "(\<lambda>x. g x - h x) constant_on S \<inter> T"
       using continuous_discrete_range_constant [OF conST contgh] by blast
+    then obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
+      by (auto simp: constant_on_def)
     obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
       using disc z False
       by auto (metis diff_add_cancel g h of_real_add)
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -1546,7 +1546,7 @@
     by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl)
   ultimately show False
     using *[unfolded connected_local not_ex, rule_format,
-      of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"]
+      of "{0..1} \<inter> g -` e1" "{0..1} \<inter> g -` e2"]
     using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(1)]
     using continuous_openin_preimage_gen[OF g(1)[unfolded path_def] as(2)]
     by auto
@@ -4946,58 +4946,57 @@
 proposition homeomorphism_locally_imp:
   fixes S :: "'a::metric_space set" and t :: "'b::t2_space set"
   assumes S: "locally P S" and hom: "homeomorphism S t f g"
-      and Q: "\<And>S t. \<lbrakk>P S; homeomorphism S t f g\<rbrakk> \<Longrightarrow> Q t"
+      and Q: "\<And>S S'. \<lbrakk>P S; homeomorphism S S' f g\<rbrakk> \<Longrightarrow> Q S'"
     shows "locally Q t"
 proof (clarsimp simp: locally_def)
-  fix w y
-  assume "y \<in> w" and "openin (subtopology euclidean t) w"
-  then obtain T where T: "open T" "w = t \<inter> T"
+  fix W y
+  assume "y \<in> W" and "openin (subtopology euclidean t) W"
+  then obtain T where T: "open T" "W = t \<inter> T"
     by (force simp: openin_open)
-  then have "w \<subseteq> t" by auto
+  then have "W \<subseteq> t" by auto
   have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f"
    and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g"
     using hom by (auto simp: homeomorphism_def)
-  have gw: "g ` w = S \<inter> {x. f x \<in> w}"
-    using \<open>w \<subseteq> t\<close>
+  have gw: "g ` W = S \<inter> f -` W"
+    using \<open>W \<subseteq> t\<close>
     apply auto
-    using \<open>g ` t = S\<close> \<open>w \<subseteq> t\<close> apply blast
-    using g \<open>w \<subseteq> t\<close> apply auto[1]
+    using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
+    using g \<open>W \<subseteq> t\<close> apply auto[1]
     by (simp add: f rev_image_eqI)
-  have o: "openin (subtopology euclidean S) (g ` w)"
+  have o: "openin (subtopology euclidean S) (g ` W)"
   proof -
     have "continuous_on S f"
       using f(3) by blast
-    then show "openin (subtopology euclidean S) (g ` w)"
-      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) w\<close> continuous_on_open f(2))
+    then show "openin (subtopology euclidean S) (g ` W)"
+      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) W\<close> continuous_on_open f(2))
   qed
   then obtain u v
-    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` w"
-    using S [unfolded locally_def, rule_format, of "g ` w" "g y"] \<open>y \<in> w\<close> by force
+    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
+    using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
   have "v \<subseteq> S" using uv by (simp add: gw)
   have fv: "f ` v = t \<inter> {x. g x \<in> v}"
     using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto
-  have "f ` v \<subseteq> w"
+  have "f ` v \<subseteq> W"
     using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
   have contvf: "continuous_on v f"
     using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
   have contvg: "continuous_on (f ` v) g"
-    using \<open>f ` v \<subseteq> w\<close> \<open>w \<subseteq> t\<close> continuous_on_subset g(3) by blast
+    using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset g(3) by blast
   have homv: "homeomorphism v (f ` v) f g"
-    using \<open>v \<subseteq> S\<close> \<open>w \<subseteq> t\<close> f
+    using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
     apply (simp add: homeomorphism_def contvf contvg, auto)
     by (metis f(1) rev_image_eqI rev_subsetD)
-  have 1: "openin (subtopology euclidean t) {x \<in> t. g x \<in> u}"
+  have 1: "openin (subtopology euclidean t) (t \<inter> g -` u)"
     apply (rule continuous_on_open [THEN iffD1, rule_format])
     apply (rule \<open>continuous_on t g\<close>)
     using \<open>g ` t = S\<close> apply (simp add: osu)
     done
-  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"
+  have 2: "\<exists>V. Q V \<and> y \<in> (t \<inter> g -` u) \<and> (t \<inter> g -` u) \<subseteq> V \<and> V \<subseteq> W"
     apply (rule_tac x="f ` v" in exI)
     apply (intro conjI Q [OF \<open>P v\<close> homv])
-    using \<open>w \<subseteq> t\<close> \<open>y \<in> w\<close>  \<open>f ` v \<subseteq> w\<close>  uv  apply (auto simp: fv)
+    using \<open>W \<subseteq> t\<close> \<open>y \<in> W\<close>  \<open>f ` v \<subseteq> W\<close>  uv  apply (auto simp: fv)
     done
-  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)"
+  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)"
     by (meson 1 2)
 qed
 
@@ -5057,22 +5056,21 @@
       and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
     shows "locally Q (f ` S)"
 proof (clarsimp simp add: locally_def)
-  fix w y
-  assume oiw: "openin (subtopology euclidean (f ` S)) w" and "y \<in> w"
-  then have "w \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
-  have oivf: "openin (subtopology euclidean S) {x \<in> S. f x \<in> w}"
+  fix W y
+  assume oiw: "openin (subtopology euclidean (f ` S)) W" and "y \<in> W"
+  then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
+  have oivf: "openin (subtopology euclidean S) (S \<inter> f -` W)"
     by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
   then obtain x where "x \<in> S" "f x = y"
-    using \<open>w \<subseteq> f ` S\<close> \<open>y \<in> w\<close> by blast
-  then obtain u v
-    where "openin (subtopology euclidean S) u" "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> {x \<in> S. f x \<in> w}"
-    using P [unfolded locally_def, rule_format, of "{x. x \<in> S \<and> f x \<in> w}" x] oivf \<open>y \<in> w\<close>
+    using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
+  then obtain U V
+    where "openin (subtopology euclidean S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
+    using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
     by auto
-  then show "\<exists>u. openin (subtopology euclidean (f ` S)) u \<and>
-            (\<exists>v. Q v \<and> y \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
-    apply (rule_tac x="f ` u" in exI)
+  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)"
+    apply (rule_tac x="f ` U" in exI)
     apply (rule conjI, blast intro!: oo)
-    apply (rule_tac x="f ` v" in exI)
+    apply (rule_tac x="f ` V" in exI)
     apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q)
     done
 qed
@@ -6087,7 +6085,7 @@
 proposition locally_connected_quotient_image:
   assumes lcS: "locally connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
-                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
+                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
                     openin (subtopology euclidean (f ` S)) T"
     shows "locally connected (f ` S)"
 proof (clarsimp simp: locally_connected_open_component)
@@ -6096,53 +6094,53 @@
   then have "C \<subseteq> U" "U \<subseteq> f ` S"
     by (meson in_components_subset openin_imp_subset)+
   then have "openin (subtopology euclidean (f ` S)) C \<longleftrightarrow>
-             openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+             openin (subtopology euclidean S) (S \<inter> f -` C)"
     by (auto simp: oo)
-  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+  moreover have "openin (subtopology euclidean S) (S \<inter> f -` C)"
   proof (subst openin_subopen, clarify)
     fix x
     assume "x \<in> S" "f x \<in> C"
-    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> C}"
+    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` C)"
     proof (intro conjI exI)
-      show "openin (subtopology euclidean S) (connected_component_set {w \<in> S. f w \<in> U} x)"
+      show "openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
       proof (rule ccontr)
-        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set {a \<in> S. f a \<in> U} x)"
-        then have "x \<notin> {a \<in> S. f a \<in> U}"
+        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
+        then have "x \<notin> (S \<inter> f -` U)"
           using \<open>U \<subseteq> f ` S\<close> opefSU lcS locally_connected_2 oo by blast
         with ** show False
           by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen)
       qed
     next
-      show "x \<in> connected_component_set {w \<in> S. f w \<in> U} x"
+      show "x \<in> connected_component_set (S \<inter> f -` U) x"
         using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by auto
     next
       have contf: "continuous_on S f"
         by (simp add: continuous_on_open oo openin_imp_subset)
-      then have "continuous_on (connected_component_set {w \<in> S. f w \<in> U} x) f"
+      then have "continuous_on (connected_component_set (S \<inter> f -` U) x) f"
         apply (rule continuous_on_subset)
         using connected_component_subset apply blast
         done
-      then have "connected (f ` connected_component_set {w \<in> S. f w \<in> U} x)"
+      then have "connected (f ` connected_component_set (S \<inter> f -` U) x)"
         by (rule connected_continuous_image [OF _ connected_connected_component])
-      moreover have "f ` connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+      moreover have "f ` connected_component_set (S \<inter> f -` U) x \<subseteq> U"
         using connected_component_in by blast
-      moreover have "C \<inter> f ` connected_component_set {w \<in> S. f w \<in> U} x \<noteq> {}"
+      moreover have "C \<inter> f ` connected_component_set (S \<inter> f -` U) x \<noteq> {}"
         using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by fastforce
-      ultimately have fC: "f ` (connected_component_set {w \<in> S. f w \<in> U} x) \<subseteq> C"
+      ultimately have fC: "f ` (connected_component_set (S \<inter> f -` U) x) \<subseteq> C"
         by (rule components_maximal [OF \<open>C \<in> components U\<close>])
-      have cUC: "connected_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> C}"
+      have cUC: "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)"
         using connected_component_subset fC by blast
-      have "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> connected_component_set {w \<in> S. f w \<in> C} x"
+      have "connected_component_set (S \<inter> f -` U) x \<subseteq> connected_component_set (S \<inter> f -` C) x"
       proof -
-        { assume "x \<in> connected_component_set {a \<in> S. f a \<in> U} x"
+        { assume "x \<in> connected_component_set (S \<inter> f -` U) x"
           then have ?thesis
-            by (simp add: cUC connected_component_maximal) }
+            using cUC connected_component_idemp connected_component_mono by blast }
         then show ?thesis
           using connected_component_eq_empty by auto
       qed
-      also have "... \<subseteq> {w \<in> S. f w \<in> C}"
+      also have "... \<subseteq> (S \<inter> f -` C)"
         by (rule connected_component_subset)
-      finally show "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> C}" .
+      finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
     qed
   qed
   ultimately show "openin (subtopology euclidean (f ` S)) C"
@@ -6153,8 +6151,7 @@
 proposition locally_path_connected_quotient_image:
   assumes lcS: "locally path_connected S"
       and oo: "\<And>T. T \<subseteq> f ` S
-                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
-                    openin (subtopology euclidean (f ` S)) T"
+                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
     shows "locally path_connected (f ` S)"
 proof (clarsimp simp: locally_path_connected_open_path_component)
   fix U y
@@ -6162,62 +6159,62 @@
   then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
     by (meson path_component_subset openin_imp_subset)+
   then have "openin (subtopology euclidean (f ` S)) (path_component_set U y) \<longleftrightarrow>
-             openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+             openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
   proof -
     have "path_component_set U y \<subseteq> f ` S"
       using \<open>U \<subseteq> f ` S\<close> \<open>path_component_set U y \<subseteq> U\<close> by blast
     then show ?thesis
       using oo by blast
   qed
-  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+  moreover have "openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
   proof (subst openin_subopen, clarify)
     fix x
     assume "x \<in> S" and Uyfx: "path_component U y (f x)"
     then have "f x \<in> U"
       using path_component_mem by blast
-    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}"
+    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` path_component_set U y)"
     proof (intro conjI exI)
-      show "openin (subtopology euclidean S) (path_component_set {w \<in> S. f w \<in> U} x)"
+      show "openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
       proof (rule ccontr)
-        assume **: "\<not> openin (subtopology euclidean S) (path_component_set {a \<in> S. f a \<in> U} x)"
-        then have "x \<notin> {a \<in> S. f a \<in> U}"
+        assume **: "\<not> openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
+        then have "x \<notin> (S \<inter> f -` U)"
           by (metis (no_types, lifting) \<open>U \<subseteq> f ` S\<close> opefSU lcS oo locally_path_connected_open_path_component)
         then show False
           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
       qed
     next
-      show "x \<in> path_component_set {w \<in> S. f w \<in> U} x"
-        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)
+      show "x \<in> path_component_set (S \<inter> f -` U) x"
+        by (simp add: \<open>f x \<in> U\<close> \<open>x \<in> S\<close> path_component_refl)
     next
       have contf: "continuous_on S f"
         by (simp add: continuous_on_open oo openin_imp_subset)
-      then have "continuous_on (path_component_set {w \<in> S. f w \<in> U} x) f"
+      then have "continuous_on (path_component_set (S \<inter> f -` U) x) f"
         apply (rule continuous_on_subset)
         using path_component_subset apply blast
         done
-      then have "path_connected (f ` path_component_set {w \<in> S. f w \<in> U} x)"
-        by (simp add: path_connected_continuous_image path_connected_path_component)
-      moreover have "f ` path_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+      then have "path_connected (f ` path_component_set (S \<inter> f -` U) x)"
+        by (simp add: path_connected_continuous_image)
+      moreover have "f ` path_component_set (S \<inter> f -` U) x \<subseteq> U"
         using path_component_mem by fastforce
-      moreover have "f x \<in> f ` path_component_set {w \<in> S. f w \<in> U} x"
+      moreover have "f x \<in> f ` path_component_set (S \<inter> f -` U) x"
         by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
-      ultimately have "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U (f x)"
+      ultimately have "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U (f x)"
         by (meson path_component_maximal)
        also have  "... \<subseteq> path_component_set U y"
-        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym path_connected_path_component)
-      finally have fC: "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U y" .
-      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}"
+        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym)
+      finally have fC: "f ` (path_component_set (S \<inter> f -` U) x) \<subseteq> path_component_set U y" .
+      have cUC: "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)"
         using path_component_subset fC by blast
-      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"
+      have "path_component_set (S \<inter> f -` U) x \<subseteq> path_component_set (S \<inter> f -` path_component_set U y) x"
       proof -
-        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"
+        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"
           using cUC path_component_mono by blast
         then show ?thesis
           using path_component_path_component by blast
       qed
-      also have "... \<subseteq> {w \<in> S. f w \<in> path_component_set U y}"
+      also have "... \<subseteq> (S \<inter> f -` path_component_set U y)"
         by (rule path_component_subset)
-      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}" .
+      finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
     qed
   qed
   ultimately show "openin (subtopology euclidean (f ` S)) (path_component_set U y)"
@@ -6234,13 +6231,10 @@
 proof (clarsimp simp: continuous_openin_preimage_eq)
   fix t :: "'b set"
   assume "open t"
-  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}"
-    apply auto
-    apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
-    using Union_components by blast
-  then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
-    using \<open>open t\<close> assms
-    by (fastforce intro: openin_trans continuous_openin_preimage_gen)
+  have *: "S \<inter> f -` t = (\<Union>c \<in> components S. c \<inter> f -` t)"
+    by auto
+  show "openin (subtopology euclidean S) (S \<inter> f -` t)"
+    unfolding * using \<open>open t\<close> assms continuous_openin_preimage_gen openin_trans openin_Union by blast
 qed
 
 lemma continuous_on_components:
@@ -6308,11 +6302,9 @@
 proof -
   have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
     apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
-    using S apply (simp add: closed_closedin)
-    using c apply (simp add: Compl_eq_Diff_UNIV)
+    using S c apply (simp_all add: Compl_eq_Diff_UNIV)
     done
-  then show ?thesis
-    by (simp add: closed_closedin)
+  then show ?thesis by simp
 qed
 
 lemma closedin_Un_complement_component:
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -4973,10 +4973,16 @@
 
 lemma setdist_eq_0_closedin:
   fixes S :: "'a::euclidean_space set"
-  shows "\<lbrakk>closedin (subtopology euclidean u) S; x \<in> u\<rbrakk>
+  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U\<rbrakk>
          \<Longrightarrow> (setdist {x} S = 0 \<longleftrightarrow> S = {} \<or> x \<in> S)"
   by (auto simp: closedin_limpt setdist_eq_0_sing_1 closure_def)
 
+lemma setdist_gt_0_closedin:
+  fixes S :: "'a::euclidean_space set"
+  shows "\<lbrakk>closedin (subtopology euclidean U) S; x \<in> U; S \<noteq> {}; x \<notin> S\<rbrakk>
+         \<Longrightarrow> setdist {x} S > 0"
+  using less_eq_real_def setdist_eq_0_closedin by fastforce
+
 subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
 
 lemma hyperplane_eq_Ex:
@@ -5089,25 +5095,19 @@
   have contf: "continuous_on U f"
     unfolding f_def by (intro continuous_intros)
   show ?thesis
-  proof (rule_tac S' = "{x\<in>U. f x > 0}" and T' = "{x\<in>U. f x < 0}" in that)
-    show "{x \<in> U. 0 < f x} \<inter> {x \<in> U. f x < 0} = {}"
+  proof (rule_tac S' = "(U \<inter> f -` {0<..})" and T' = "(U \<inter> f -` {..<0})" in that)
+    show "(U \<inter> f -` {0<..}) \<inter> (U \<inter> f -` {..<0}) = {}"
       by auto
-    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {0<..}}"
-      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
-    then show "openin (subtopology euclidean U) {x \<in> U. 0 < f x}" by simp
-  next
-    have "openin (subtopology euclidean U) {x \<in> U. f x \<in> {..<0}}"
+    show "openin (subtopology euclidean U) (U \<inter> f -` {0<..})"
       by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
-    then show "openin (subtopology euclidean U) {x \<in> U. f x < 0}" by simp
+  next
+    show "openin (subtopology euclidean U) (U \<inter> f -` {..<0})"
+      by (rule continuous_openin_preimage [where T=UNIV]) (simp_all add: contf)
   next
-    show "S \<subseteq> {x \<in> U. 0 < f x}"
-      apply (clarsimp simp add: f_def setdist_sing_in_set)
-      using assms
-      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)
-    show "T \<subseteq> {x \<in> U. f x < 0}"
-      apply (clarsimp simp add: f_def setdist_sing_in_set)
-      using assms
-      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)
+    have "S \<subseteq> U" "T \<subseteq> U"
+      using closedin_imp_subset assms by blast+
+    then show "S \<subseteq> U \<inter> f -` {0<..}" "T \<subseteq> U \<inter> f -` {..<0}"
+      using assms False by (force simp add: f_def setdist_sing_in_set intro!: setdist_gt_0_closedin)+
   qed
 qed
 
@@ -5282,7 +5282,7 @@
 proposition proper_map:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   assumes "closedin (subtopology euclidean S) K"
-      and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact {x \<in> S. f x \<in> U}"
+      and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
       and "f ` S \<subseteq> T"
     shows "closedin (subtopology euclidean T) (f ` K)"
 proof -
@@ -5298,7 +5298,7 @@
       by metis
     then have fX: "\<And>n. f (X n) = h n"
       by metis
-    have "compact (C \<inter> {a \<in> S. f a \<in> insert y (range (\<lambda>i. f(X(n + i))))})" for n
+    have "compact (C \<inter> (S \<inter> f -` insert y (range (\<lambda>i. f(X(n + i))))))" for n
       apply (rule closed_Int_compact [OF \<open>closed C\<close>])
       apply (rule com)
        using X \<open>K \<subseteq> S\<close> \<open>f ` S \<subseteq> T\<close> \<open>y \<in> T\<close> apply blast
@@ -5350,16 +5350,16 @@
   assume RHS: ?rhs
   obtain g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     by (metis inv_into_f_f f)
-  then have *: "{x \<in> S. f x \<in> U} = g ` U" if "U \<subseteq> f ` S" for U
+  then have *: "(S \<inter> f -` U) = g ` U" if "U \<subseteq> f ` S" for U
     using that by fastforce
   have gfim: "g ` f ` S \<subseteq> S" using gf by auto
-  have **: "compact {x \<in> f ` S. g x \<in> C}" if C: "C \<subseteq> S" "compact C" for C
+  have **: "compact (f ` S \<inter> g -` C)" if C: "C \<subseteq> S" "compact C" for C
   proof -
-    obtain h :: "'a set \<Rightarrow> 'a" where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
+    obtain h where "h C \<in> C \<and> h C \<notin> S \<or> compact (f ` C)"
       by (force simp: C RHS)
-    moreover have "f ` C = {b \<in> f ` S. g b \<in> C}"
+    moreover have "f ` C = (f ` S \<inter> g -` C)"
       using C gf by auto
-    ultimately show "compact {b \<in> f ` S. g b \<in> C}"
+    ultimately show ?thesis
       using C by auto
   qed
   show ?lhs
@@ -5510,14 +5510,14 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
           "closedin (subtopology euclidean T) K"
-  shows "compact {x. x \<in> S \<and> f x \<in> K}"
+  shows "compact (S \<inter> f -` K)"
 by (rule closedin_compact [OF \<open>compact S\<close>] continuous_closedin_preimage_gen assms)+
 
 lemma proper_map_fst:
   assumes "compact T" "K \<subseteq> S" "compact K"
-    shows "compact {z \<in> S \<times> T. fst z \<in> K}"
-proof -
-  have "{z \<in> S \<times> T. fst z \<in> K} = K \<times> T"
+    shows "compact (S \<times> T \<inter> fst -` K)"
+proof -
+  have "(S \<times> T \<inter> fst -` K) = K \<times> T"
     using assms by auto
   then show ?thesis by (simp add: assms compact_Times)
 qed
@@ -5535,9 +5535,9 @@
 
 lemma proper_map_snd:
   assumes "compact S" "K \<subseteq> T" "compact K"
-    shows "compact {z \<in> S \<times> T. snd z \<in> K}"
-proof -
-  have "{z \<in> S \<times> T. snd z \<in> K} = S \<times> K"
+    shows "compact (S \<times> T \<inter> snd -` K)"
+proof -
+  have "(S \<times> T \<inter> snd -` K) = S \<times> K"
     using assms by auto
   then show ?thesis by (simp add: assms compact_Times)
 qed
@@ -7872,8 +7872,7 @@
                and "\<And>U. U \<in> \<C>' \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<C> \<and> U \<subseteq> T)"
                and "\<And>x. \<exists>V. open V \<and> x \<in> V \<and>
                                finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-using paracompact_closedin [of UNIV S \<C>] assms
-by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
+using paracompact_closedin [of UNIV S \<C>] assms by auto
 
   
 subsection\<open>Closed-graph characterization of continuity\<close>
@@ -7883,7 +7882,7 @@
   assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
     shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
 proof -
-  have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
+  have eq: "((\<lambda>x. Pair x (f x)) ` S) =(S \<times> T \<inter> (\<lambda>z. (f \<circ> fst)z - snd z) -` {0})"
     using fim by auto
   show ?thesis
     apply (subst eq)
@@ -7902,9 +7901,9 @@
   proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
     fix U
     assume U: "closedin (subtopology euclidean T) U"
-    have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
+    have eq: "(S \<inter> f -` U) = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
       by (force simp: image_iff)
-    show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+    show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
       by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
   qed
   with continuous_closed_graph_gen assms show ?thesis by blast
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -66,7 +66,7 @@
   shows "interior i \<subseteq> interior S"
 proof -
   have "box a b \<inter> cbox c d = {}"
-     using inter_interval_mixed_eq_empty[of c d a b] assms
+     using Int_interval_mixed_eq_empty[of c d a b] assms
      unfolding interior_cbox by auto
   moreover
   have "box a b \<subseteq> cbox c d \<union> S"
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -858,10 +858,15 @@
 by (simp add: closedin_def topspace_subtopology)
 
 lemma openin_subtopology_Un:
-    "openin (subtopology U T) S \<and> openin (subtopology U u) S
-     \<Longrightarrow> openin (subtopology U (T \<union> u)) S"
+    "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
+     \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
 by (simp add: openin_subtopology) blast
 
+lemma closedin_subtopology_Un:
+    "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
+     \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
+by (simp add: closedin_subtopology) blast
+
 
 subsubsection \<open>The standard Euclidean topology\<close>
 
@@ -886,6 +891,8 @@
 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
   by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
 
+declare closed_closedin [symmetric, simp]
+
 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
   using openI by auto
 
@@ -913,7 +920,7 @@
   by (auto simp: openin_open)
 
 lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
-  by (simp add: closedin_subtopology closed_closedin Int_ac)
+  by (simp add: closedin_subtopology Int_ac)
 
 lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
   by (metis closedin_closed)
@@ -965,7 +972,7 @@
        ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
                  openin (subtopology euclidean s) e2 \<and>
                  s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
-  apply (simp add: connected_def openin_open, safe)
+  apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   apply (simp_all, blast+)  (* SLOW *)
   done
 
@@ -1032,7 +1039,7 @@
 lemma closedin_trans[trans]:
   "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
     closedin (subtopology euclidean U) S"
-  by (auto simp: closedin_closed closed_closedin closed_Inter Int_assoc)
+  by (auto simp: closedin_closed closed_Inter Int_assoc)
 
 lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   by (auto simp: closedin_closed intro: closedin_trans)
@@ -5304,9 +5311,9 @@
 qed
 
 lemma continuous_on_open:
-  "continuous_on s f \<longleftrightarrow>
-    (\<forall>t. openin (subtopology euclidean (f ` s)) t \<longrightarrow>
-      openin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
+  "continuous_on S f \<longleftrightarrow>
+    (\<forall>T. openin (subtopology euclidean (f ` S)) T \<longrightarrow>
+      openin (subtopology euclidean S) (S \<inter> f -` T))"
   unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
@@ -5315,37 +5322,42 @@
   assumes "f ` S \<subseteq> T"
     shows "continuous_on S f \<longleftrightarrow>
              (\<forall>U. openin (subtopology euclidean T) U
-                  \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+                  \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
      (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then show ?rhs
-    apply (auto simp: openin_euclidean_subtopology_iff continuous_on_iff)
+    apply (clarsimp simp: openin_euclidean_subtopology_iff continuous_on_iff)
     by (metis assms image_subset_iff)
 next
   have ope: "openin (subtopology euclidean T) (ball y e \<inter> T)" for y e
     by (simp add: Int_commute openin_open_Int)
-  assume ?rhs
-  then show ?lhs
-    apply (clarsimp simp add: continuous_on_iff)
-    apply (drule_tac x = "ball (f x) e \<inter> T" in spec)
-    apply (clarsimp simp add: ope openin_euclidean_subtopology_iff [of S])
-    by (metis (no_types, hide_lams) assms dist_commute dist_self image_subset_iff)
+  assume R [rule_format]: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: continuous_on_iff)
+    fix x and e::real
+    assume "x \<in> S" and "0 < e"
+    then have x: "x \<in> S \<inter> (f -` ball (f x) e \<inter> f -` T)"
+      using assms by auto
+    show "\<exists>d>0. \<forall>x'\<in>S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+      using R [of "ball (f x) e \<inter> T"] x
+      by (fastforce simp add: ope openin_euclidean_subtopology_iff [of S] dist_commute)
+  qed
 qed
 
 lemma continuous_openin_preimage:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   shows
    "\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
-        \<Longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+        \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
 by (simp add: continuous_on_open_gen)
 
 text \<open>Similarly in terms of closed sets.\<close>
 
 lemma continuous_on_closed:
-  "continuous_on s f \<longleftrightarrow>
-    (\<forall>t. closedin (subtopology euclidean (f ` s)) t \<longrightarrow>
-      closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})"
+  "continuous_on S f \<longleftrightarrow>
+    (\<forall>T. closedin (subtopology euclidean (f ` S)) T \<longrightarrow>
+      closedin (subtopology euclidean S) (S \<inter> f -` T))"
   unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
@@ -5354,61 +5366,73 @@
   assumes "f ` S \<subseteq> T"
     shows "continuous_on S f \<longleftrightarrow>
              (\<forall>U. closedin (subtopology euclidean T) U
-                  \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<in> U})"
+                  \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
+     (is "?lhs = ?rhs")
 proof -
-  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
+  have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
     using assms by blast
   show ?thesis
-    apply (simp add: continuous_on_open_gen [OF assms], safe)
-    apply (drule_tac [!] x="T-U" in spec)
-    apply (force simp: closedin_def *)
-    apply (force simp: openin_closedin_eq *)
-    done
+  proof
+    assume L: ?lhs
+    show ?rhs
+    proof clarify
+      fix U
+      assume "closedin (subtopology euclidean T) U"
+      then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
+        using L unfolding continuous_on_open_gen [OF assms]
+        by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
+    qed
+  next
+    assume R [rule_format]: ?rhs
+    show ?lhs
+      unfolding continuous_on_open_gen [OF assms]
+      by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
+  qed
 qed
 
 lemma continuous_closedin_preimage_gen:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
-    shows "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+    shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
 using assms continuous_on_closed_gen by blast
 
 lemma continuous_on_imp_closedin:
   assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
-    shows "closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T}"
+    shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
 using assms continuous_on_closed by blast
 
 subsection \<open>Half-global and completely global cases.\<close>
 
 lemma continuous_openin_preimage_gen:
-  assumes "continuous_on s f"  "open t"
-  shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+  assumes "continuous_on S f"  "open T"
+  shows "openin (subtopology euclidean S) (S \<inter> f -` T)"
 proof -
-  have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
+  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
     by auto
-  have "openin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
-    using openin_open_Int[of t "f ` s", OF assms(2)] unfolding openin_open by auto
+  have "openin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
+    using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
   then show ?thesis
-    using assms(1)[unfolded continuous_on_open, THEN spec[where x="t \<inter> f ` s"]]
+    using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
     using * by auto
 qed
 
 lemma continuous_closedin_preimage:
-  assumes "continuous_on s f" and "closed t"
-  shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+  assumes "continuous_on S f" and "closed T"
+  shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
 proof -
-  have *: "\<forall>x. x \<in> s \<and> f x \<in> t \<longleftrightarrow> x \<in> s \<and> f x \<in> (t \<inter> f ` s)"
+  have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
     by auto
-  have "closedin (subtopology euclidean (f ` s)) (t \<inter> f ` s)"
-    using closedin_closed_Int[of t "f ` s", OF assms(2)]
+  have "closedin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
+    using closedin_closed_Int[of T "f ` S", OF assms(2)]
     by (simp add: Int_commute)
   then show ?thesis
-    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="t \<inter> f ` s"]]
+    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
     using * by auto
 qed
 
 lemma continuous_openin_preimage_eq:
    "continuous_on S f \<longleftrightarrow>
-    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+    (\<forall>T. open T \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T))"
 apply safe
 apply (simp add: continuous_openin_preimage_gen)
 apply (fastforce simp add: continuous_on_open openin_open)
@@ -5416,66 +5440,55 @@
 
 lemma continuous_closedin_preimage_eq:
    "continuous_on S f \<longleftrightarrow>
-    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+    (\<forall>T. closed T \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` T))"
 apply safe
 apply (simp add: continuous_closedin_preimage)
 apply (fastforce simp add: continuous_on_closed closedin_closed)
 done
 
 lemma continuous_open_preimage:
-  assumes "continuous_on s f"
-    and "open s"
-    and "open t"
-  shows "open {x \<in> s. f x \<in> t}"
+  assumes contf: "continuous_on S f" and "open S" "open T"
+  shows "open (S \<inter> f -` T)"
 proof-
-  obtain T where T: "open T" "{x \<in> s. f x \<in> t} = s \<inter> T"
-    using continuous_openin_preimage_gen[OF assms(1,3)] unfolding openin_open by auto
+  obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
+    using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
+    unfolding openin_open by auto
   then show ?thesis
-    using open_Int[of s T, OF assms(2)] by auto
+    using open_Int[of S U, OF \<open>open S\<close>] by auto
 qed
 
 lemma continuous_closed_preimage:
-  assumes "continuous_on s f"
-    and "closed s"
-    and "closed t"
-  shows "closed {x \<in> s. f x \<in> t}"
+  assumes contf: "continuous_on S f" and "closed S" "closed T"
+  shows "closed (S \<inter> f -` T)"
 proof-
-  obtain T where "closed T" "{x \<in> s. f x \<in> t} = s \<inter> T"
-    using continuous_closedin_preimage[OF assms(1,3)]
+  obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
+    using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
     unfolding closedin_closed by auto
-  then show ?thesis using closed_Int[of s T, OF assms(2)] by auto
+  then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
 qed
 
-lemma continuous_open_preimage_univ:
-  "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open {x. f x \<in> s}"
-  using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
-
-lemma continuous_closed_preimage_univ:
-  "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed {x. f x \<in> s}"
-  using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
-
-lemma continuous_open_vimage: "open s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` s)"
-  unfolding vimage_def by (rule continuous_open_preimage_univ)
-
-lemma continuous_closed_vimage: "closed s \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` s)"
-  unfolding vimage_def by (rule continuous_closed_preimage_univ)
+lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
+  by (metis continuous_on_eq_continuous_within open_vimage) 
+ 
+lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
+  by (simp add: closed_vimage continuous_on_eq_continuous_within)
 
 lemma interior_image_subset:
   assumes "inj f" "\<And>x. continuous (at x) f"
-  shows "interior (f ` s) \<subseteq> f ` (interior s)"
+  shows "interior (f ` S) \<subseteq> f ` (interior S)"
 proof
-  fix x assume "x \<in> interior (f ` s)"
-  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
-  then have "x \<in> f ` s" by auto
-  then obtain y where y: "y \<in> s" "x = f y" by auto
-  have "open (vimage f T)"
-    using assms \<open>open T\<close> by (metis continuous_open_vimage)
+  fix x assume "x \<in> interior (f ` S)"
+  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" ..
+  then have "x \<in> f ` S" by auto
+  then obtain y where y: "y \<in> S" "x = f y" by auto
+  have "open (f -` T)"
+    using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
   moreover have "y \<in> vimage f T"
     using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
-  moreover have "vimage f T \<subseteq> s"
-    using \<open>T \<subseteq> image f s\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
-  ultimately have "y \<in> interior s" ..
-  with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
+  moreover have "vimage f T \<subseteq> S"
+    using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
+  ultimately have "y \<in> interior S" ..
+  with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
 subsection \<open>Topological properties of linear functions.\<close>
@@ -5853,7 +5866,7 @@
     by auto
 qed
 
-lemma inter_interval_mixed_eq_empty:
+lemma Int_interval_mixed_eq_empty:
   fixes a :: "'a::euclidean_space"
    assumes "box c d \<noteq> {}"
   shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
diff -r ee874941dfb8 -r d3d508b23d1d src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Thu Oct 19 00:55:34 2017 +0200
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Thu Oct 19 17:16:13 2017 +0100
@@ -740,22 +740,20 @@
   case True
   have "path \<gamma>"
     by (simp add: assms simple_path_imp_path)
-  then obtain k where k: "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+  then have const: "winding_number \<gamma> constant_on inside(path_image \<gamma>)"
   proof (rule winding_number_constant)
     show "connected (inside(path_image \<gamma>))"
       by (simp add: Jordan_inside_outside True assms)
   qed (use inside_no_overlap True in auto)
   obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
     using simple_closed_path_wn3 [of \<gamma>] True assms by blast
-  with k have "winding_number \<gamma> z = k"
-    by blast
   have "winding_number \<gamma> z \<in> \<int>"
     using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
   with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
     apply (auto simp: Ints_def abs_if split: if_split_asm)
     by (metis of_int_1 of_int_eq_iff of_int_minus)
-  then show ?thesis
-    using that \<open>winding_number \<gamma> z = k\<close> k by auto
+  with that const zin show ?thesis
+    unfolding constant_on_def by metis
 next
   case False
   then show ?thesis