Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
authorpaulson <>
Mon, 04 Apr 2016 16:52:56 +0100
changeset 62843 313d3b697c9a
parent 62842 db9f95ca2a8f
child 62857 a8758f47f9e8
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
--- a/src/HOL/Fun.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Fun.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -36,6 +36,9 @@
 lemma vimage_id [simp]: "vimage id = id"
   by (simp add: id_def fun_eq_iff)
+lemma eq_id_iff: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
+  by auto
   constant id \<rightharpoonup> (Haskell) "id"
--- a/src/HOL/Library/Disjoint_Sets.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -22,7 +22,10 @@
 subsection \<open>Set of Disjoint Sets\<close>
-definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+abbreviation disjoint :: "'a set set \<Rightarrow> bool" where "disjoint \<equiv> pairwise disjnt"
+lemma disjoint_def: "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
+  unfolding pairwise_def disjnt_def by auto
 lemma disjointI:
   "(\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}) \<Longrightarrow> disjoint A"
@@ -32,9 +35,6 @@
   "disjoint A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<inter> b = {}"
   unfolding disjoint_def by auto
-lemma disjoint_empty[iff]: "disjoint {}"
-  by (auto simp: disjoint_def)
 lemma disjoint_INT:
   assumes *: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)"
   shows "disjoint {\<Inter>i\<in>I. X i | X. \<forall>i\<in>I. X i \<in> F i}"
@@ -48,9 +48,6 @@
     by (auto simp: INT_Int_distrib[symmetric])
-lemma disjoint_singleton[simp]: "disjoint {A}"
-  by(simp add: disjoint_def)
 subsubsection "Family of Disjoint Sets"
 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -1781,7 +1781,7 @@
 definition "retraction s t r \<longleftrightarrow> t \<subseteq> s \<and> continuous_on s r \<and> r ` s \<subseteq> t \<and> (\<forall>x\<in>t. r x = x)"
-definition retract_of (infixl "retract'_of" 12)
+definition retract_of (infixl "retract'_of" 50)
   where "(t retract_of s) \<longleftrightarrow> (\<exists>r. retraction s t r)"
 lemma retraction_idempotent: "retraction s t r \<Longrightarrow> x \<in> s \<Longrightarrow>  r (r x) = r x"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -3388,7 +3388,7 @@
       by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
   then show ?thesis
-    by (simp add: connected_closed_in_eq)
+    by (simp add: connected_closedin_eq)
 lemma continuous_disconnected_range_constant_eq:
@@ -6814,7 +6814,7 @@
     using "*" by auto blast+
   have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
     using assms
-    by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
+    by (auto intro: continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
   obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] .
   then have holfb: "f holomorphic_on ball w e"
     using holf holomorphic_on_subset by blast
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -992,14 +992,21 @@
   using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
   by (metis Re_Ln complex_Re_le_cmod z)
-lemma exists_complex_root:
-  fixes a :: complex
-  shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
-  apply (cases "a=0", simp)
-  apply (rule_tac x= "exp(Ln(a) / n)" in exI)
-  apply (auto simp: exp_of_nat_mult [symmetric])
+proposition exists_complex_root:
+  fixes z :: complex
+  assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
+  apply (cases "z=0")
+  using assms apply (simp add: power_0_left)
+  apply (rule_tac w = "exp(Ln z / n)" in that)
+  apply (auto simp: assms exp_of_nat_mult [symmetric])
+corollary exists_complex_root_nonzero:
+  fixes z::complex
+  assumes "z \<noteq> 0" "n \<noteq> 0"
+  obtains w where "w \<noteq> 0" "z = w ^ n"
+  by (metis exists_complex_root [of n z] assms power_0_left)
 subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
 text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -441,8 +441,10 @@
     ultimately show ?thesis
       by (rule *)
+  then have "open (f ` \<Union>components U)"
+    by (metis (no_types, lifting) imageE image_Union open_Union)
   then show ?thesis
-    by (subst Union_components [of U]) (auto simp: image_Union)
+    by force
@@ -454,10 +456,10 @@
       and fnc: "\<And>X. \<lbrakk>open X; X \<subseteq> S; X \<noteq> {}\<rbrakk> \<Longrightarrow> ~ f constant_on X"
     shows "open (f ` U)"
 proof -
-  have "S = \<Union>(components S)" by (fact Union_components)
+  have "S = \<Union>(components S)" by simp
   with \<open>U \<subseteq> S\<close> have "U = (\<Union>C \<in> components S. C \<inter> U)" by auto
   then have "f ` U = (\<Union>C \<in> components S. f ` (C \<inter> U))"
-    by auto
+    using image_UN by fastforce
   { fix C assume "C \<in> components S"
     with S \<open>C \<in> components S\<close> open_components in_components_connected
@@ -1028,7 +1030,7 @@
     apply (rule allI continuous_closed_preimage_univ continuous_intros)+
     using \<open>compact K\<close> compact_eq_bounded_closed by blast
   ultimately show ?thesis
-    using closed_inter_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 blast
 corollary proper_map_polyfun_univ:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -5202,7 +5202,7 @@
   ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
     "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
-    using distance_attains_sup[OF compact_inter[OF _ assms(1), of ?A], of 0] by blast
+    using distance_attains_sup[OF compact_Int[OF _ assms(1), of ?A], of 0] by blast
   have "norm x > 0"
     using assms(3)[unfolded zero_less_norm_iff[symmetric]] by auto
@@ -7879,7 +7879,7 @@
   assumes "convex S"
     and "open A"
   shows "A \<inter> closure S = {} \<longleftrightarrow> A \<inter> rel_interior S = {}"
-  by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
+  by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty)
 lemma rel_interior_open_segment:
   fixes a :: "'a :: euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -577,9 +577,6 @@
-lemma eq_id_iff: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
-  by auto
 lemma det_linear_rows_setsum_lemma:
   assumes fS: "finite S"
     and fT: "finite T"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -23,7 +23,7 @@
 lemma compact_eq_closed:
   fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
   shows "compact S \<longleftrightarrow> closed S"
-  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed
+  using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed
   by auto
 lemma closed_contains_Sup_cl:
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -1712,16 +1712,22 @@
 lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
   by (simp add: convex_imp_path_connected is_interval_convex)
-lemma linear_homeomorphic_image:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+lemma linear_homeomorphism_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "inj f"
-    shows "s homeomorphic f ` s"
-    using assms unfolding homeomorphic_def homeomorphism_def
-    apply (rule_tac x=f in exI)
-    apply (rule_tac x="inv f" in exI)
-    using inj_linear_imp_inv_linear linear_continuous_on
-    apply (auto simp:  linear_conv_bounded_linear)
-    done
+    obtains g where "homeomorphism (f ` S) S g f"
+using linear_injective_left_inverse [OF assms]
+apply clarify
+apply (rule_tac g=g in that)
+using assms
+apply (auto simp: homeomorphism_def eq_id_iff [symmetric] image_comp comp_def linear_conv_bounded_linear linear_continuous_on)
+lemma linear_homeomorphic_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "inj f"
+    shows "S homeomorphic f ` S"
+by (meson homeomorphic_def homeomorphic_sym linear_homeomorphism_image [OF assms])
 lemma path_connected_Times:
   assumes "path_connected s" "path_connected t"
@@ -2329,7 +2335,7 @@
 lemma connected_Int_frontier:
      "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
-  apply (simp add: frontier_interiors connected_open_in, safe)
+  apply (simp add: frontier_interiors connected_openin, safe)
   apply (drule_tac x="s \<inter> interior t" in spec, safe)
    apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
    apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
@@ -2412,7 +2418,7 @@
 by (rule order_trans [OF frontier_Union_subset_closure])
    (auto simp: closure_subset_eq)
-lemma connected_component_UNIV:
+lemma connected_component_UNIV [simp]:
     fixes x :: "'a::real_normed_vector"
     shows "connected_component_set UNIV x = UNIV"
 using connected_iff_eq_connected_component_set [of "UNIV::'a set"] connected_UNIV
@@ -3146,7 +3152,7 @@
   apply (auto intro!: q [unfolded case_prod_unfold])
-lemma homotopic_on_empty: "homotopic_with (\<lambda>x. True) {} t f g"
+lemma homotopic_on_empty [simp]: "homotopic_with (\<lambda>x. True) {} t f g"
   by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -412,14 +412,14 @@
   morphisms "openin" "topology"
   unfolding istopology_def by blast
-lemma istopology_open_in[intro]: "istopology(openin U)"
+lemma istopology_openin[intro]: "istopology(openin U)"
   using openin[of U] by blast
 lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
   using topology_inverse[unfolded mem_Collect_eq] .
 lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
-  using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
+  using topology_inverse[of U] istopology_openin[of "topology U"] by auto
 lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
@@ -450,19 +450,19 @@
   unfolding topspace_def by blast
 lemma openin_empty[simp]: "openin U {}"
-  by (simp add: openin_clauses)
+  by (rule openin_clauses)
 lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
-  using openin_clauses by simp
-lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
-  using openin_clauses by simp
+  by (rule openin_clauses)
+lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
+  using openin_clauses by blast 
 lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
   using openin_Union[of "{S,T}" U] by auto
 lemma openin_topspace[intro, simp]: "openin U (topspace U)"
-  by (simp add: openin_Union topspace_def)
+  by (force simp add: openin_Union topspace_def)
 lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -472,7 +472,7 @@
   assume H: ?rhs
   let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
-  have "openin U ?t" by (simp add: openin_Union)
+  have "openin U ?t" by (force simp add: openin_Union)
   also have "?t = S" using H by auto
   finally show "openin U S" .
@@ -709,7 +709,7 @@
     unfolding openin_open open_dist by fast
-lemma connected_open_in:
+lemma connected_openin:
       "connected s \<longleftrightarrow>
        ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
                  openin (subtopology euclidean s) e2 \<and>
@@ -718,17 +718,17 @@
   apply (simp_all, blast+)  \<comment>\<open>slow\<close>
-lemma connected_open_in_eq:
+lemma connected_openin_eq:
       "connected s \<longleftrightarrow>
        ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
                  openin (subtopology euclidean s) e2 \<and>
                  e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
                  e1 \<noteq> {} \<and> e2 \<noteq> {})"
-  apply (simp add: connected_open_in, safe)
+  apply (simp add: connected_openin, safe)
   apply blast
   by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
-lemma connected_closed_in:
+lemma connected_closedin:
       "connected s \<longleftrightarrow>
        ~(\<exists>e1 e2.
              closedin (subtopology euclidean s) e1 \<and>
@@ -759,14 +759,14 @@
-lemma connected_closed_in_eq:
+lemma connected_closedin_eq:
       "connected s \<longleftrightarrow>
            ~(\<exists>e1 e2.
                  closedin (subtopology euclidean s) e1 \<and>
                  closedin (subtopology euclidean s) e2 \<and>
                  e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
                  e1 \<noteq> {} \<and> e2 \<noteq> {})"
-  apply (simp add: connected_closed_in, safe)
+  apply (simp add: connected_closedin, safe)
   apply blast
   by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
@@ -788,8 +788,8 @@
 lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   by (auto simp add: closedin_closed intro: closedin_trans)
-lemma openin_subtopology_inter_subset:
-   "openin (subtopology euclidean u) (u \<inter> s) \<and> v \<subseteq> u \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> s)"
+lemma openin_subtopology_Int_subset:
+   "\<lbrakk>openin (subtopology euclidean u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> S)"
   by (auto simp: openin_subtopology)
 lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
@@ -900,6 +900,34 @@
 lemma open_contains_ball_eq: "open S \<Longrightarrow> x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
   by (metis open_contains_ball subset_eq centre_in_ball)
+lemma openin_contains_ball:
+    "openin (subtopology euclidean t) s \<longleftrightarrow>
+     s \<subseteq> t \<and> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> ball x e \<inter> t \<subseteq> s)"
+    (is "?lhs = ?rhs")
+  assume ?lhs
+  then show ?rhs
+    apply (simp add: openin_open)
+    apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE)
+    done
+  assume ?rhs
+  then show ?lhs
+    apply (simp add: openin_euclidean_subtopology_iff)
+    by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball)
+lemma openin_contains_cball:
+   "openin (subtopology euclidean t) s \<longleftrightarrow>
+        s \<subseteq> t \<and>
+        (\<forall>x \<in> s. \<exists>e. 0 < e \<and> cball x e \<inter> t \<subseteq> s)"
+apply (simp add: openin_contains_ball)
+apply (rule iffI)
+apply (auto dest!: bspec)
+apply (rule_tac x="e/2" in exI)
+apply force+
 lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
   unfolding mem_ball set_eq_iff
   apply (simp add: not_less)
@@ -1763,7 +1791,7 @@
   using closure_eq[of S] closure_subset[of S]
   by simp
-lemma open_inter_closure_eq_empty:
+lemma open_Int_closure_eq_empty:
   "open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
   using open_subset_interior[of S "- T"]
   using interior_subset[of "- T"]
@@ -1824,7 +1852,7 @@
   unfolding closure_def using islimpt_punctured by blast
 lemma connected_imp_connected_closure: "connected s \<Longrightarrow> connected (closure s)"
-    by (rule connectedI) (meson closure_subset open_Int open_inter_closure_eq_empty subset_trans connectedD)
+    by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)
 lemma limpt_of_limpts:
       fixes x :: "'a::metric_space"
@@ -1845,7 +1873,7 @@
       shows "x islimpt closure s \<longleftrightarrow> x islimpt s"
   by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
-lemma closed_in_limpt:
+lemma closedin_limpt:
    "closedin (subtopology euclidean t) s \<longleftrightarrow> s \<subseteq> t \<and> (\<forall>x. x islimpt s \<and> x \<in> t \<longrightarrow> x \<in> s)"
   apply (simp add: closedin_closed, safe)
   apply (simp add: closed_limpt islimpt_subset)
@@ -1856,7 +1884,7 @@
 lemma closedin_closed_eq:
     "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
-  by (meson closed_in_limpt closed_subset closedin_closed_trans)
+  by (meson closedin_limpt closed_subset closedin_closed_trans)
 lemma bdd_below_closure:
   fixes A :: "real set"
@@ -2070,10 +2098,11 @@
 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   by (auto simp: components_def)
-lemma Union_components: "u = \<Union>(components u)"
+lemma Union_components [simp]: "\<Union>(components u) = u"
   apply (rule subset_antisym)
+  using Union_connected_component components_def apply fastforce
   apply (metis Union_connected_component components_def set_eq_subset)
-  using Union_connected_component components_def by fastforce
+  done
 lemma pairwise_disjoint_components: "pairwise (\<lambda>X Y. X \<inter> Y = {}) (components u)"
   apply (simp add: pairwise_def)
@@ -2174,17 +2203,17 @@
   have "A \<inter> closure s \<noteq> {}"
     using Alap Int_absorb1 ts by blast
   then have Alaps: "A \<inter> s \<noteq> {}"
-    by (simp add: A open_inter_closure_eq_empty)
+    by (simp add: A open_Int_closure_eq_empty)
   have "B \<inter> closure s \<noteq> {}"
     using Blap Int_absorb1 ts by blast
   then have Blaps: "B \<inter> s \<noteq> {}"
-    by (simp add: B open_inter_closure_eq_empty)
+    by (simp add: B open_Int_closure_eq_empty)
   then show False
     using cs [unfolded connected_def] A B disjs Alaps Blaps cover st
     by blast
-lemma closed_in_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)"
+lemma closedin_connected_component: "closedin (subtopology euclidean s) (connected_component_set s x)"
 proof (cases "connected_component_set s x = {}")
   case True then show ?thesis
     by (metis closedin_empty)
@@ -3715,7 +3744,7 @@
   shows "finite s \<Longrightarrow> \<not> x islimpt s"
   by (induct set: finite) (simp_all add: islimpt_insert)
-lemma islimpt_union_finite:
+lemma islimpt_Un_finite:
   fixes x :: "'a::t1_space"
   shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
   by (simp add: islimpt_Un islimpt_finite)
@@ -3769,7 +3798,7 @@
   then have "l' islimpt (f ` {..<N} \<union> f ` {N..})"
     by (simp add: image_Un)
   then have "l' islimpt (f ` {N..})"
-    by (simp add: islimpt_union_finite)
+    by (simp add: islimpt_Un_finite)
   then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
     using \<open>l' \<in> s\<close> \<open>open s\<close> by (rule islimptE)
   then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'"
@@ -3822,7 +3851,7 @@
 text\<open>In particular, some common special cases.\<close>
-lemma compact_union [intro]:
+lemma compact_Un [intro]:
   assumes "compact s"
     and "compact t"
   shows " compact (s \<union> t)"
@@ -3845,19 +3874,19 @@
   "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
   by (rule compact_Union) auto
-lemma closed_inter_compact [intro]:
+lemma closed_Int_compact [intro]:
   assumes "closed s"
     and "compact t"
   shows "compact (s \<inter> t)"
-  using compact_inter_closed [of t s] assms
+  using compact_Int_closed [of t s] assms
   by (simp add: Int_commute)
-lemma compact_inter [intro]:
+lemma compact_Int [intro]:
   fixes s t :: "'a :: t2_space set"
   assumes "compact s"
     and "compact t"
   shows "compact (s \<inter> t)"
-  using assms by (intro compact_inter_closed compact_imp_closed)
+  using assms by (intro compact_Int_closed compact_imp_closed)
 lemma compact_sing [simp]: "compact {a}"
   unfolding compact_eq_heine_borel by auto
@@ -3867,7 +3896,7 @@
   shows "compact (insert x s)"
 proof -
   have "compact ({x} \<union> s)"
-    using compact_sing assms by (rule compact_union)
+    using compact_sing assms by (rule compact_Un)
   then show ?thesis by simp
@@ -3935,7 +3964,7 @@
   proof safe
     fix P Q R S
     assume "eventually R F" "open S" "x \<in> S"
-    with open_inter_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"]
+    with open_Int_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"]
     have "S \<inter> {x. R x} \<noteq> {}" by (auto simp: Z_def)
     moreover assume "Ball S Q" "\<forall>x. Q x \<and> R x \<longrightarrow> bot x"
     ultimately show False by (auto simp: set_eq_iff)
@@ -4083,7 +4112,7 @@
     by simp
-lemma seq_compact_inter_closed:
+lemma seq_compact_Int_closed:
   assumes "seq_compact s" and "closed t"
   shows "seq_compact (s \<inter> t)"
 proof (rule seq_compactI)
@@ -4104,7 +4133,7 @@
 lemma seq_compact_closed_subset:
   assumes "closed s" and "s \<subseteq> t" and "seq_compact t"
   shows "seq_compact s"
-  using assms seq_compact_inter_closed [of t s] by (simp add: Int_absorb1)
+  using assms seq_compact_Int_closed [of t s] by (simp add: Int_absorb1)
 lemma seq_compact_imp_countably_compact:
   fixes U :: "'a :: first_countable_topology set"
@@ -4917,7 +4946,7 @@
     by simp
-lemma complete_inter_closed:
+lemma complete_Int_closed:
   fixes s :: "'a::metric_space set"
   assumes "complete s" and "closed t"
   shows "complete (s \<inter> t)"
@@ -4937,7 +4966,7 @@
   fixes s :: "'a::metric_space set"
   assumes "closed s" and "s \<subseteq> t" and "complete t"
   shows "complete s"
-  using assms complete_inter_closed [of t s] by (simp add: Int_absorb1)
+  using assms complete_Int_closed [of t s] by (simp add: Int_absorb1)
 lemma complete_eq_closed:
   fixes s :: "('a::complete_space) set"
@@ -5802,7 +5831,7 @@
 text \<open>Equality of continuous functions on closure and related results.\<close>
-lemma continuous_closed_in_preimage_constant:
+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
@@ -6087,20 +6116,20 @@
 text \<open>Proving a function is constant by proving open-ness of level set.\<close>
-lemma continuous_levelset_open_in_cases:
+lemma continuous_levelset_openin_cases:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a}
         \<Longrightarrow> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
   unfolding connected_clopen
-  using continuous_closed_in_preimage_constant by auto
-lemma continuous_levelset_open_in:
+  using continuous_closedin_preimage_constant by auto
+lemma continuous_levelset_openin:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
         (\<exists>x \<in> s. f x = a)  \<Longrightarrow> (\<forall>x \<in> s. f x = a)"
-  using continuous_levelset_open_in_cases[of s f ]
+  using continuous_levelset_openin_cases[of s f ]
   by meson
 lemma continuous_levelset_open:
@@ -6110,7 +6139,7 @@
     and "open {x \<in> s. f x = a}"
     and "\<exists>x \<in> s.  f x = a"
   shows "\<forall>x \<in> s. f x = a"
-  using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open]
+  using continuous_levelset_openin[OF assms(1,2), of a, unfolded openin_open]
   using assms (3,4)
   by fast
@@ -6511,7 +6540,7 @@
   moreover have "continuous_on ?B (dist a)"
     by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
   moreover have "compact ?B"
-    by (intro closed_inter_compact \<open>closed s\<close> compact_cball)
+    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
   ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
     by (metis continuous_attains_inf)
   with that show ?thesis by fastforce
@@ -7172,11 +7201,11 @@
 text \<open>Continuity relative to a union.\<close>
-lemma continuous_on_union_local:
+lemma continuous_on_Un_local:
     "\<lbrakk>closedin (subtopology euclidean (s \<union> t)) s; closedin (subtopology euclidean (s \<union> t)) t;
       continuous_on s f; continuous_on t f\<rbrakk>
      \<Longrightarrow> continuous_on (s \<union> t) f"
-  unfolding continuous_on closed_in_limpt
+  unfolding continuous_on closedin_limpt
   by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
 lemma continuous_on_cases_local:
@@ -7184,7 +7213,7 @@
        continuous_on s f; continuous_on t g;
        \<And>x. \<lbrakk>x \<in> s \<and> ~P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
       \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
-  by (rule continuous_on_union_local) (auto intro: continuous_on_eq)
+  by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
 lemma continuous_on_cases_le:
   fixes h :: "'a :: topological_space \<Rightarrow> real"
@@ -7588,7 +7617,7 @@
    assumes "box c d \<noteq> {}"
   shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   unfolding closure_box[OF assms, symmetric]
-  unfolding open_inter_closure_eq_empty[OF open_box] ..
+  unfolding open_Int_closure_eq_empty[OF open_box] ..
 lemma diameter_cbox:
   fixes a b::"'a::euclidean_space"
@@ -8079,7 +8108,7 @@
   then have "compact ?S''" by (metis compact_cball compact_frontier)
   moreover have "?S' = s \<inter> ?S''" by auto
   ultimately have "compact ?S'"
-    using closed_inter_compact[of s ?S''] using s(1) by auto
+    using closed_Int_compact[of s ?S''] using s(1) by auto
   moreover have *:"f ` ?S' = ?S" by auto
   ultimately have "compact ?S"
     using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -248,7 +248,7 @@
                    and pf01: "\<And>t. t \<in> s-U \<Longrightarrow> pf t ` s \<subseteq> {0..1}"
     by metis
   have com_sU: "compact (s-U)"
-    using compact closed_inter_compact U by (simp add: Diff_eq compact_inter_closed open_closed)
+    using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed)
   have "\<And>t. t \<in> s-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < pf t x}"
     apply (rule open_Collect_positive)
     by (metis pf continuous)
@@ -451,7 +451,7 @@
   then have setsum_max_0: "A \<subseteq> (\<Union>x \<in> A. Vf x)"
     by blast
   have com_A: "compact A" using A
-    by (metis compact compact_inter_closed inf.absorb_iff2)
+    by (metis compact compact_Int_closed inf.absorb_iff2)
   obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
     by (blast intro: that open_Vf compactE_image [OF com_A _ setsum_max_0])
   then have [simp]: "subA \<noteq> {}"
--- a/src/HOL/Set.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Set.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -833,6 +833,9 @@
 lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
   by fast
+lemma subset_singleton_iff: "X \<subseteq> {a} \<longleftrightarrow> X = {} \<or> X = {a}"
+  by blast
 lemma singleton_conv [simp]: "{x. x = a} = {a}"
   by blast
@@ -1564,6 +1567,8 @@
 lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
   by blast
+lemma subset_Compl_singleton [simp]: "A \<subseteq> - {b} \<longleftrightarrow> (b \<notin> A)"
+  by blast
 text \<open>\medskip Quantification over type @{typ bool}.\<close>
@@ -1897,6 +1902,14 @@
 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
+definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
+lemma pairwise_disjoint_empty [simp]: "pairwise disjnt {}"
+  by (simp add: pairwise_def disjnt_def)
+lemma pairwise_disjoint_singleton [simp]: "pairwise disjnt {A}"
+  by (simp add: pairwise_def disjnt_def)
 hide_const (open) member not_member
 lemmas equalityI = subset_antisym
--- a/src/HOL/Topological_Spaces.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -1540,10 +1540,10 @@
   shows "closed (f -` s)"
   using closed_vimage_Int [OF assms] by simp
-lemma continuous_on_empty: "continuous_on {} f"
+lemma continuous_on_empty [simp]: "continuous_on {} f"
   by (simp add: continuous_on_def)
-lemma continuous_on_sing: "continuous_on {x} f"
+lemma continuous_on_sing [simp]: "continuous_on {x} f"
   by (simp add: continuous_on_def at_within_def)
 lemma continuous_on_open_Union:
@@ -1780,7 +1780,7 @@
   using assms unfolding ball_simps [symmetric]
   by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
-lemma compact_inter_closed [intro]:
+lemma compact_Int_closed [intro]:
   assumes "compact s" and "closed t"
   shows "compact (s \<inter> t)"
 proof (rule compactI)
@@ -1911,7 +1911,7 @@
     by (rule continuous_on_subset)
   moreover have "compact (s - B)"
     using \<open>open B\<close> and \<open>compact s\<close>
-    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
+    unfolding Diff_eq by (intro compact_Int_closed closed_Compl)
   ultimately have "compact (f ` (s - B))"
     by (rule compact_continuous_image)
   hence "closed (f ` (s - B))"