# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1474473591 -3600
# Node ID d81fb5b46a5c01c2eb35a8524a0229f1c9c3c565
# Parent  0efb482beb84e427fdfa37efb3df6fc3bf23fcbb
new material about topological concepts, etc

diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -2794,6 +2794,14 @@
   using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
 by (metis clo closed_closedin open_openin subtopology_UNIV)
 
+corollary neighbourhood_extension_into_ANR:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
+  obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
+                    "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+  using ANR_imp_absolute_neighbourhood_extensor [OF  \<open>ANR T\<close> contf fim]
+  by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
+
 lemma absolute_neighbourhood_extensor_imp_ANR:
   fixes S :: "'a::euclidean_space set"
   assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
@@ -3739,8 +3747,9 @@
     apply (rule homeomorphic_closedin_convex [of S])
     using aff_dim_le_DIM [of S] apply auto
     done
-  have "locally path_connected T"
-    by (meson ANR_imp_absolute_neighbourhood_retract \<open>S homeomorphic T\<close> \<open>closedin (subtopology euclidean U) T\<close> \<open>convex U\<close> assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
+  then have "locally path_connected T"
+    by (meson ANR_imp_absolute_neighbourhood_retract
+        assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
   then have S: "locally path_connected S"
       if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
     using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -5420,10 +5420,6 @@
 
 subsection\<open> General stepping result for derivative formulas.\<close>
 
-lemma sum_sqs_eq:
-  fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
-  by algebra
-
 proposition Cauchy_next_derivative:
   assumes "continuous_on (path_image \<gamma>) f'"
       and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -1027,7 +1027,7 @@
     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 (rule allI continuous_closed_preimage_univ continuous_intros)+
+    apply (intro allI continuous_closed_preimage_univ 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
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -5554,6 +5554,31 @@
   apply auto
   done
 
+text\<open>A non-singleton connected set is perfect (i.e. has no isolated points). \<close>
+lemma connected_imp_perfect:
+  fixes a :: "'a::metric_space"
+  assumes "connected S" "a \<in> S" and S: "\<And>x. S \<noteq> {x}"
+  shows "a islimpt S"
+proof -
+  have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T
+  proof -
+    obtain e where "e > 0" and e: "cball a e \<subseteq> T"
+      using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball)
+    have "openin (subtopology euclidean S) {a}"
+      unfolding openin_open using that \<open>a \<in> S\<close> by blast
+    moreover have "closedin (subtopology euclidean S) {a}"
+      by (simp add: assms)
+    ultimately show "False"
+      using \<open>connected S\<close> connected_clopen S by blast
+  qed
+  then show ?thesis
+    unfolding islimpt_def by blast
+qed
+
+lemma connected_imp_perfect_aff_dim:
+     "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
+  using aff_dim_sing connected_imp_perfect by blast
+
 subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
 
 lemma is_interval_1:
@@ -10406,7 +10431,7 @@
 
 lemma collinear_3_expand:
    "collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
-proof -
+proof -                          
   have "collinear{a,b,c} = collinear{a,c,b}"
     by (simp add: insert_commute)
   also have "... = collinear {0, a - c, b - c}"
@@ -10418,6 +10443,27 @@
   finally show ?thesis .
 qed
 
+lemma collinear_aff_dim: "collinear S \<longleftrightarrow> aff_dim S \<le> 1"
+proof
+  assume "collinear S"
+  then obtain u and v :: "'a" where "aff_dim S \<le> aff_dim {u,v}"
+    by (metis \<open>collinear S\<close> aff_dim_affine_hull aff_dim_subset collinear_affine_hull)
+  then show "aff_dim S \<le> 1"
+    using order_trans by fastforce
+next
+  assume "aff_dim S \<le> 1"
+  then have le1: "aff_dim (affine hull S) \<le> 1"
+    by simp
+  obtain B where "B \<subseteq> S" and B: "\<not> affine_dependent B" "affine hull S = affine hull B"
+    using affine_basis_exists [of S] by auto
+  then have "finite B" "card B \<le> 2"
+    using B le1 by (auto simp: affine_independent_iff_card)
+  then have "collinear B"
+    by (rule collinear_small)
+  then show "collinear S"
+    by (metis \<open>affine hull S = affine hull B\<close> collinear_affine_hull_collinear)
+qed
+
 lemma collinear_midpoint: "collinear{a,midpoint a b,b}"
   apply (auto simp: collinear_3 collinear_lemma)
   apply (drule_tac x="-1" in spec)
@@ -10443,6 +10489,35 @@
   ultimately show ?thesis by blast
 qed
 
+lemma between_imp_collinear:
+  fixes x :: "'a :: euclidean_space"
+  assumes "between (a,b) x"
+    shows "collinear {a,x,b}"
+proof (cases "x = a \<or> x = b \<or> a = b")
+  case True with assms show ?thesis
+    by (auto simp: dist_commute)
+next
+  case False with assms show ?thesis
+    apply (auto simp: collinear_3 collinear_lemma between_norm)
+    apply (drule_tac x="-(norm(b - x) / norm(x - a))" in spec)
+    apply (simp add: vector_add_divide_simps eq_vector_fraction_iff real_vector.scale_minus_right [symmetric])
+    done
+qed
+
+lemma midpoint_between:
+  fixes a b :: "'a::euclidean_space"
+  shows "b = midpoint a c \<longleftrightarrow> between (a,c) b \<and> dist a b = dist b c"
+proof (cases "a = c")
+  case True then show ?thesis
+    by (auto simp: dist_commute)
+next
+  case False
+  show ?thesis
+    apply (rule iffI)
+    apply (simp add: between_midpoint(1) dist_midpoint)
+    using False between_imp_collinear midpoint_collinear by blast
+qed
+
 lemma collinear_triples:
   assumes "a \<noteq> b"
     shows "collinear(insert a (insert b S)) \<longleftrightarrow> (\<forall>x \<in> S. collinear{a,b,x})"
@@ -11157,7 +11232,7 @@
 using assms unfolding openin_open
 by (metis affine_hull_convex_Int_open hull_subset inf.orderE inf_assoc)
 
-corollary affine_hull_open_in:
+corollary affine_hull_openin:
   fixes S :: "'a::real_normed_vector set"
   assumes "openin (subtopology euclidean (affine hull T)) S" "S \<noteq> {}"
     shows "affine hull S = affine hull T"
@@ -11180,6 +11255,19 @@
   shows "\<lbrakk>convex S; open T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow>  aff_dim(S \<inter> T) = aff_dim S"
 using aff_dim_convex_Int_nonempty_interior interior_eq by blast
 
+lemma affine_hull_Diff:
+  fixes S:: "'a::real_normed_vector set"
+  assumes ope: "openin (subtopology euclidean (affine hull S)) S" and "finite F" "F \<subset> S"
+    shows "affine hull (S - F) = affine hull S"
+proof -
+  have clo: "closedin (subtopology euclidean S) F"
+    using assms finite_imp_closedin by auto
+  moreover have "S - F \<noteq> {}"
+    using assms by auto
+  ultimately show ?thesis
+    by (metis ope closedin_def topspace_euclidean_subtopology affine_hull_openin openin_trans)
+qed
+
 lemma affine_hull_halfspace_lt:
   fixes a :: "'a::euclidean_space"
   shows "affine hull {x. a \<bullet> x < r} = (if a = 0 \<and> r \<le> 0 then {} else UNIV)"
@@ -11963,6 +12051,44 @@
   using in_convex_hull_exchange_unique assms apply blast
   by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
 
+lemma Int_closed_segment:
+  fixes b :: "'a::euclidean_space"
+  assumes "b \<in> closed_segment a c \<or> ~collinear{a,b,c}"
+    shows "closed_segment a b \<inter> closed_segment b c = {b}"
+proof (cases "c = a")
+  case True
+  then show ?thesis
+    using assms collinear_3_eq_affine_dependent by fastforce
+next
+  case False
+  from assms show ?thesis
+  proof
+    assume "b \<in> closed_segment a c"
+    moreover have "\<not> affine_dependent {a, c}"
+      by (simp add: affine_independent_2)
+    ultimately show ?thesis
+      using False convex_hull_exchange_Int [of "{a,c}" b "{a}" "{c}"]
+      by (simp add: segment_convex_hull insert_commute)
+  next
+    assume ncoll: "\<not> collinear {a, b, c}"
+    have False if "closed_segment a b \<inter> closed_segment b c \<noteq> {b}"
+    proof -
+      have "b \<in> closed_segment a b" and "b \<in> closed_segment b c"
+        by auto
+      with that obtain d where "b \<noteq> d" "d \<in> closed_segment a b" "d \<in> closed_segment b c"
+        by force
+      then have d: "collinear {a, d, b}"  "collinear {b, d, c}"
+        by (auto simp:  between_mem_segment between_imp_collinear)
+      have "collinear {a, b, c}"
+        apply (rule collinear_3_trans [OF _ _ \<open>b \<noteq> d\<close>])
+        using d  by (auto simp: insert_commute)
+      with ncoll show False ..
+    qed
+    then show ?thesis
+      by blast
+  qed
+qed
+
 lemma affine_hull_finite_intersection_hyperplanes:
   fixes s :: "'a::euclidean_space set"
   obtains f where
@@ -12812,6 +12938,7 @@
   finally show "aff_dim S \<le> aff_dim (f ` S)" .
 qed
 
+
 text\<open>Choosing a subspace of a given dimension\<close>
 proposition choose_subspace_of_subspace:
   fixes S :: "'n::euclidean_space set"
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -5894,7 +5894,7 @@
   assumes "0 < r"
     and "\<forall>x. h(g x) = x"
     and "\<forall>x. g(h x) = x"
-    and "\<forall>x. continuous (at x) g"
+    and contg: "\<And>x. continuous (at x) g"
     and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
     and "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
     and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
@@ -5947,7 +5947,7 @@
       show "gauge d'"
         using d(1)
         unfolding gauge_def d'
-        using continuous_open_preimage_univ[OF assms(4)]
+        using continuous_open_preimage_univ[OF _ contg]
         by auto
       fix p
       assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
@@ -5985,7 +5985,7 @@
         proof -
           assume as: "interior k \<inter> interior k' = {}"
           have "z \<in> g ` (interior k \<inter> interior k')"
-            using interior_image_subset[OF assms(4) inj(1)] z
+            using interior_image_subset[OF \<open>inj g\<close> contg] z
             unfolding image_Int[OF inj(1)] by blast
           then show False
             using as by blast
@@ -6178,20 +6178,13 @@
   assumes "(f has_integral i) (cbox a b)"
     and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
-    ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
-  apply (rule has_integral_twiddle[where f=f])
-  unfolding zero_less_abs_iff content_image_stretch_interval
-  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
-  using assms
-proof -
-  show "\<forall>y::'a. continuous (at y) (\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k))"
-    apply rule
-    apply (rule linear_continuous_at)
-    unfolding linear_linear
-    unfolding linear_iff inner_simps euclidean_eq_iff[where 'a='a]
-    apply (auto simp add: field_simps)
-    done
-qed auto
+         ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+apply (rule has_integral_twiddle[where f=f])
+unfolding zero_less_abs_iff content_image_stretch_interval
+unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+using assms
+by auto
+ 
 
 lemma integrable_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -6199,14 +6192,9 @@
     and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
     ((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` cbox a b)"
-  using assms
-  unfolding integrable_on_def
-  apply -
-  apply (erule exE)
-  apply (drule has_integral_stretch)
-  apply assumption
-  apply auto
-  done
+  using assms unfolding integrable_on_def
+  by (force dest: has_integral_stretch)
+
 
 subsection \<open>even more special cases.\<close>
 
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -8,6 +8,11 @@
 imports "~~/src/HOL/Library/Sum_of_Squares"
 begin
 
+(* FIXME: move elsewhere *)
+lemma sum_sqs_eq:
+  fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
+  by algebra
+
 lemma norm_cmul_rule_thm:
   fixes x :: "'a::real_normed_vector"
   shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -4746,19 +4746,17 @@
 lemma connected_equivalence_relation:
   assumes "connected S"
       and etc: "a \<in> S" "b \<in> S"
-      and sym: "\<And>x y z. R x y \<Longrightarrow> R y x"
-      and trans: "\<And>x y z. R x y \<and> R y z \<Longrightarrow> R x z"
-      and opI: "\<And>a. a \<in> S
-             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
+      and sym: "\<And>x y. \<lbrakk>R x y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> R y x"
+      and trans: "\<And>x y z. \<lbrakk>R x y; R y z; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> R x z"
+      and opI: "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
     shows "R a b"
 proof -
   have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
     apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
-    by (meson local.sym local.trans opI)
+    by (meson local.sym local.trans opI openin_imp_subset subsetCE)
   then show ?thesis by (metis etc opI)
 qed
 
-
 lemma locally_constant_imp_constant:
   assumes "connected S"
       and opI: "\<And>a. a \<in> S
@@ -5270,6 +5268,12 @@
 apply (force simp: convex_Int convex_imp_path_connected)
 done
 
+lemma convex_imp_locally_connected:
+  fixes S :: "'a:: real_normed_vector set"
+  shows "convex S \<Longrightarrow> locally connected S"
+  by (simp add: locally_path_connected_imp_locally_connected convex_imp_locally_path_connected)
+
+
 subsection\<open>Relations between components and path components\<close>
 
 lemma path_component_eq_connected_component:
@@ -5741,7 +5745,7 @@
     done
 qed
 
-lemma isometry_subspaces:
+corollary isometry_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
   assumes S: "subspace S"
@@ -5751,6 +5755,14 @@
 using isometries_subspaces [OF assms]
 by metis
 
+corollary isomorphisms_UNIV_UNIV:
+  assumes "DIM('M) = DIM('N)"
+  obtains f::"'M::euclidean_space \<Rightarrow>'N::euclidean_space" and g
+  where "linear f" "linear g"
+                    "\<And>x. norm(f x) = norm x" "\<And>y. norm(g y) = norm y"
+                    "\<And>x. g(f x) = x" "\<And>y. f(g y) = y"
+  using assms by (auto simp: dim_UNIV intro: isometries_subspaces [of "UNIV::'M set" "UNIV::'N set"])
+
 lemma homeomorphic_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -17,6 +17,7 @@
 
 
 (* FIXME: move elsewhere *)
+
 definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set"
 where
   "support_on s f = {x\<in>s. f x \<noteq> 0}"
@@ -766,6 +767,11 @@
 lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   by (auto simp add: closedin_closed)
 
+lemma finite_imp_closedin:
+  fixes S :: "'a::t1_space set"
+  shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"
+    by (simp add: finite_imp_closed closed_subset)
+
 lemma closedin_singleton [simp]:
   fixes a :: "'a::t1_space"
   shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U"
@@ -3611,6 +3617,9 @@
     unfolding bounded_def by auto
 qed
 
+lemma bounded_closure_image: "bounded (f ` closure S) \<Longrightarrow> bounded (f ` S)"
+  by (simp add: bounded_subset closure_subset image_mono)
+
 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
   apply (simp add: bounded_def)
   apply (rule_tac x=x in exI)
@@ -3749,7 +3758,8 @@
   shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
 
-text\<open>Some theorems on sups and infs using the notion "bounded".\<close>
+
+subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
 
 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
   by (simp add: bounded_iff)
@@ -6122,22 +6132,21 @@
 qed
 
 lemma continuous_open_preimage_univ:
-  "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+  "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:
-  "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s \<Longrightarrow> closed {x. f x \<in> s}"
+  "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: "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+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: "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+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 interior_image_subset:
-  assumes "\<forall>x. continuous (at x) f"
-    and "inj f"
+  assumes "inj f" "\<And>x. continuous (at x) f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
 proof
   fix x assume "x \<in> interior (f ` s)"
@@ -6145,7 +6154,7 @@
   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(1) \<open>open T\<close> by (rule continuous_open_vimage)
+    using assms \<open>open T\<close> by (metis continuous_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"
@@ -6774,53 +6783,53 @@
   by (auto intro!: image_eqI [where f="\<lambda>x. - x"])
 
 lemma open_negations:
-  fixes s :: "'a::real_normed_vector set"
-  shows "open s \<Longrightarrow> open ((\<lambda>x. - x) ` s)"
-  using open_scaling [of "- 1" s] by simp
+  fixes S :: "'a::real_normed_vector set"
+  shows "open S \<Longrightarrow> open ((\<lambda>x. - x) ` S)"
+  using open_scaling [of "- 1" S] by simp
 
 lemma open_translation:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "open s"
-  shows "open((\<lambda>x. a + x) ` s)"
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"
+  shows "open((\<lambda>x. a + x) ` S)"
 proof -
   {
     fix x
     have "continuous (at x) (\<lambda>x. x - a)"
       by (intro continuous_diff continuous_ident continuous_const)
   }
-  moreover have "{x. x - a \<in> s} = op + a ` s"
+  moreover have "{x. x - a \<in> S} = op + a ` S"
     by force
-  ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s]
-    using assms by auto
+  ultimately show ?thesis
+    by (metis assms continuous_open_vimage vimage_def)
 qed
 
 lemma open_affinity:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "open s"  "c \<noteq> 0"
-  shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"  "c \<noteq> 0"
+  shows "open ((\<lambda>x. a + c *\<^sub>R x) ` S)"
 proof -
   have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
     unfolding o_def ..
-  have "op + a ` op *\<^sub>R c ` s = (op + a \<circ> op *\<^sub>R c) ` s"
+  have "op + a ` op *\<^sub>R c ` S = (op + a \<circ> op *\<^sub>R c) ` S"
     by auto
   then show ?thesis
-    using assms open_translation[of "op *\<^sub>R c ` s" a]
+    using assms open_translation[of "op *\<^sub>R c ` S" a]
     unfolding *
     by auto
 qed
 
 lemma interior_translation:
-  fixes s :: "'a::real_normed_vector set"
-  shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
+  fixes S :: "'a::real_normed_vector set"
+  shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)"
 proof (rule set_eqI, rule)
   fix x
-  assume "x \<in> interior (op + a ` s)"
-  then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` s"
+  assume "x \<in> interior (op + a ` S)"
+  then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` S"
     unfolding mem_interior by auto
-  then have "ball (x - a) e \<subseteq> s"
+  then have "ball (x - a) e \<subseteq> S"
     unfolding subset_eq Ball_def mem_ball dist_norm
     by (auto simp add: diff_diff_eq)
-  then show "x \<in> op + a ` interior s"
+  then show "x \<in> op + a ` interior S"
     unfolding image_iff
     apply (rule_tac x="x - a" in bexI)
     unfolding mem_interior
@@ -6829,27 +6838,27 @@
     done
 next
   fix x
-  assume "x \<in> op + a ` interior s"
-  then obtain y e where "e > 0" and e: "ball y e \<subseteq> s" and y: "x = a + y"
+  assume "x \<in> op + a ` interior S"
+  then obtain y e where "e > 0" and e: "ball y e \<subseteq> S" and y: "x = a + y"
     unfolding image_iff Bex_def mem_interior by auto
   {
     fix z
     have *: "a + y - z = y + a - z" by auto
     assume "z \<in> ball x e"
-    then have "z - a \<in> s"
+    then have "z - a \<in> S"
       using e[unfolded subset_eq, THEN bspec[where x="z - a"]]
       unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 *
       by auto
-    then have "z \<in> op + a ` s"
+    then have "z \<in> op + a ` S"
       unfolding image_iff by (auto intro!: bexI[where x="z - a"])
   }
-  then have "ball x e \<subseteq> op + a ` s"
+  then have "ball x e \<subseteq> op + a ` S"
     unfolding subset_eq by auto
-  then show "x \<in> interior (op + a ` s)"
+  then show "x \<in> interior (op + a ` S)"
     unfolding mem_interior using \<open>e > 0\<close> by auto
 qed
 
-text \<open>Topological properties of linear functions.\<close>
+subsection \<open>Topological properties of linear functions.\<close>
 
 lemma linear_lim_0:
   assumes "bounded_linear f"
@@ -6877,6 +6886,73 @@
   "bounded_linear f \<Longrightarrow> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
+subsubsection\<open>Relating linear images to open/closed/interior/closure.\<close>
+
+proposition open_surjective_linear_image:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "open A" "linear f" "surj f"
+    shows "open(f ` A)"
+unfolding open_dist
+proof clarify
+  fix x
+  assume "x \<in> A"
+  have "bounded (inv f ` Basis)"
+    by (simp add: finite_imp_bounded)
+  with bounded_pos obtain B where "B > 0" and B: "\<And>x. x \<in> inv f ` Basis \<Longrightarrow> norm x \<le> B"
+    by metis
+  obtain e where "e > 0" and e: "\<And>z. dist z x < e \<Longrightarrow> z \<in> A"
+    by (metis open_dist \<open>x \<in> A\<close> \<open>open A\<close>)
+  define \<delta> where "\<delta> \<equiv> e / B / DIM('b)"
+  show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
+  proof (intro exI conjI)
+    show "\<delta> > 0"
+      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps) (simp add: mult_less_0_iff)
+    have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
+    proof -
+      define u where "u \<equiv> y - f x"
+      show ?thesis
+      proof (rule image_eqI)
+        show "y = f (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i))"
+          apply (simp add: linear_add linear_setsum linear.scaleR \<open>linear f\<close> surj_f_inv_f \<open>surj f\<close>)
+          apply (simp add: euclidean_representation u_def)
+          done
+        have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
+          by (simp add: dist_norm setsum_norm_le)
+        also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
+          by (simp add: )
+        also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
+          by (simp add: B setsum_distrib_right setsum_mono mult_left_mono)
+        also have "... \<le> DIM('b) * dist y (f x) * B"
+          apply (rule mult_right_mono [OF setsum_bounded_above])
+          using \<open>0 < B\<close> by (auto simp add: Basis_le_norm dist_norm u_def)
+        also have "... < e"
+          by (metis mult.commute mult.left_commute that)
+        finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
+          by (rule e)
+      qed
+    qed
+    then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
+      using \<open>e > 0\<close> \<open>B > 0\<close>
+      by (auto simp: \<delta>_def divide_simps mult_less_0_iff)
+  qed
+qed
+
+corollary open_bijective_linear_image_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "bij f"
+    shows "open(f ` A) \<longleftrightarrow> open A"
+proof
+  assume "open(f ` A)"
+  then have "open(f -` (f ` A))"
+    using assms by (force simp add: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
+  then show "open A"
+    by (simp add: assms bij_is_inj inj_vimage_image_eq)
+next
+  assume "open A"
+  then show "open(f ` A)"
+    by (simp add: assms bij_is_surj open_surjective_linear_image)
+qed
+
 text \<open>Also bilinear functions, in composition form.\<close>
 
 lemma bilinear_continuous_at_compose:
@@ -7957,7 +8033,7 @@
   then show "?L \<subseteq> ?R" ..
 qed
 
-lemma bounded_cbox:
+lemma bounded_cbox [simp]:
   fixes a :: "'a::euclidean_space"
   shows "bounded (cbox a b)"
 proof -
@@ -8384,11 +8460,27 @@
   (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
   (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
 
+lemma homeomorphismI [intro?]:
+  assumes "continuous_on S f" "continuous_on T g"
+          "f ` S \<subseteq> T" "g ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
+    shows "homeomorphism S T f g"
+  using assms by (force simp: homeomorphism_def)
+
 lemma homeomorphism_translation:
   fixes a :: "'a :: real_normed_vector"
   shows "homeomorphism (op + a ` S) S (op + (- a)) (op + a)"
 unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
 
+lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
+  by (rule homeomorphismI) (auto simp: continuous_on_id)
+
+lemma homeomorphism_compose:
+  assumes "homeomorphism S T f g" "homeomorphism T U h k"
+    shows "homeomorphism S U (h o f) (g o k)"
+  using assms
+  unfolding homeomorphism_def
+  by (intro conjI ballI continuous_on_compose) (auto simp: image_comp [symmetric])
+
 lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
   by (simp add: homeomorphism_def)
 
@@ -8416,47 +8508,12 @@
   by blast
 
 lemma homeomorphic_trans [trans]:
-  assumes "s homeomorphic t"
-      and "t homeomorphic u"
-    shows "s homeomorphic u"
-proof -
-  obtain f1 g1 where fg1: "\<forall>x\<in>s. g1 (f1 x) = x"  "f1 ` s = t"
-    "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"
-    using assms(1) unfolding homeomorphic_def homeomorphism_def by auto
-  obtain f2 g2 where fg2: "\<forall>x\<in>t. g2 (f2 x) = x"  "f2 ` t = u" "continuous_on t f2"
-    "\<forall>y\<in>u. f2 (g2 y) = y" "g2 ` u = t" "continuous_on u g2"
-    using assms(2) unfolding homeomorphic_def homeomorphism_def by auto
-  {
-    fix x
-    assume "x\<in>s"
-    then have "(g1 \<circ> g2) ((f2 \<circ> f1) x) = x"
-      using fg1(1)[THEN bspec[where x=x]] and fg2(1)[THEN bspec[where x="f1 x"]] and fg1(2)
-      by auto
-  }
-  moreover have "(f2 \<circ> f1) ` s = u"
-    using fg1(2) fg2(2) by auto
-  moreover have "continuous_on s (f2 \<circ> f1)"
-    using continuous_on_compose[OF fg1(3)] and fg2(3) unfolding fg1(2) by auto
-  moreover
-  {
-    fix y
-    assume "y\<in>u"
-    then have "(f2 \<circ> f1) ((g1 \<circ> g2) y) = y"
-      using fg2(4)[THEN bspec[where x=y]] and fg1(4)[THEN bspec[where x="g2 y"]] and fg2(5)
-      by auto
-  }
-  moreover have "(g1 \<circ> g2) ` u = s" using fg1(5) fg2(5) by auto
-  moreover have "continuous_on u (g1 \<circ> g2)"
-    using continuous_on_compose[OF fg2(6)] and fg1(6)
-    unfolding fg2(5)
-    by auto
-  ultimately show ?thesis
-    unfolding homeomorphic_def homeomorphism_def
-    apply (rule_tac x="f2 \<circ> f1" in exI)
-    apply (rule_tac x="g1 \<circ> g2" in exI)
-    apply auto
-    done
-qed
+  assumes "S homeomorphic T"
+      and "T homeomorphic U"
+    shows "S homeomorphic U"
+  using assms
+  unfolding homeomorphic_def
+by (metis homeomorphism_compose)
 
 lemma homeomorphic_minimal:
   "s homeomorphic t \<longleftrightarrow>
diff -r 0efb482beb84 -r d81fb5b46a5c src/HOL/Library/Disjoint_Sets.thy
--- a/src/HOL/Library/Disjoint_Sets.thy	Wed Sep 21 14:20:07 2016 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Wed Sep 21 16:59:51 2016 +0100
@@ -65,6 +65,26 @@
 
 abbreviation "disjoint_family A \<equiv> disjoint_family_on A UNIV"
 
+lemma disjoint_family_elem_disjnt:
+  assumes "infinite A" "finite C"
+      and df: "disjoint_family_on B A"
+  obtains x where "x \<in> A" "disjnt C (B x)"
+proof -
+  have "False" if *: "\<forall>x \<in> A. \<exists>y. y \<in> C \<and> y \<in> B x"
+  proof -
+    obtain g where g: "\<forall>x \<in> A. g x \<in> C \<and> g x \<in> B x"
+      using * by metis
+    with df have "inj_on g A"
+      by (fastforce simp add: inj_on_def disjoint_family_on_def)
+    then have "infinite (g ` A)"
+      using \<open>infinite A\<close> finite_image_iff by blast
+    then show False
+      by (meson \<open>finite C\<close> finite_subset g image_subset_iff)
+  qed
+  then show ?thesis
+    by (force simp: disjnt_iff intro: that)
+qed
+
 lemma disjoint_family_onD:
   "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   by (auto simp: disjoint_family_on_def)