--- a/src/HOL/Fun.thy Mon Apr 04 22:13:08 2016 +0200
+++ b/src/HOL/Fun.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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
+
code_printing
constant id \<rightharpoonup> (Haskell) "id"
--- a/src/HOL/Library/Disjoint_Sets.thy Mon Apr 04 22:13:08 2016 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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])
qed
-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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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)
qed
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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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])
done
+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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Apr 04 22:13:47 2016 +0200
@@ -441,8 +441,10 @@
ultimately show ?thesis
by (rule *)
qed
+ 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
qed
@@ -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
moreover
{ 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
qed
corollary proper_map_polyfun_univ:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 04 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 04 22:13:47 2016 +0200
@@ -5202,7 +5202,7 @@
done
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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 04 22:13:47 2016 +0200
@@ -577,9 +577,6 @@
qed
-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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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)
+done
+
+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])
done
-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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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)"
proof
@@ -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 @@
next
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" .
qed
@@ -709,7 +709,7 @@
unfolding openin_open open_dist by fast
qed
-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>
done
-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 @@
done
qed
-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")
+proof
+ 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
+next
+ 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)
+qed
+
+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+
+done
+
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
qed
-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
qed
@@ -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
qed
-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
qed
-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 22:13:08 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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 22:13:08 2016 +0200
+++ b/src/HOL/Set.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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 22:13:08 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Apr 04 22:13:47 2016 +0200
@@ -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))"