# HG changeset patch # User wenzelm # Date 1459800827 -7200 # Node ID a8758f47f9e8adfc64e207553da4099e30899f92 # Parent 313d3b697c9a4724fc2e8d01ef6d021f6ed02b4a# Parent 3f97aa4580c67760c41ec02fe0f069f37738f54b merged diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Fun.thy --- 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: "(\x. f x = x) \ f = id" + by auto + code_printing constant id \ (Haskell) "id" diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Library/Disjoint_Sets.thy --- 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 \Set of Disjoint Sets\ -definition "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})" +abbreviation disjoint :: "'a set set \ bool" where "disjoint \ pairwise disjnt" + +lemma disjoint_def: "disjoint A \ (\a\A. \b\A. a \ b \ a \ b = {})" + unfolding pairwise_def disjnt_def by auto lemma disjointI: "(\a b. a \ A \ b \ A \ a \ b \ a \ b = {}) \ disjoint A" @@ -32,9 +35,6 @@ "disjoint A \ a \ A \ b \ A \ a \ b \ a \ b = {}" unfolding disjoint_def by auto -lemma disjoint_empty[iff]: "disjoint {}" - by (auto simp: disjoint_def) - lemma disjoint_INT: assumes *: "\i. i \ I \ disjoint (F i)" shows "disjoint {\i\I. X i | X. \i\I. X i \ 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 \ 'a set) \ 'i set \ bool" where diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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 \ t \ s \ continuous_on s r \ r ` s \ t \ (\x\t. r x = x)" -definition retract_of (infixl "retract'_of" 12) +definition retract_of (infixl "retract'_of" 50) where "(t retract_of s) \ (\r. retraction s t r)" lemma retraction_idempotent: "retraction s t r \ x \ s \ r (r x) = r x" diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- 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) (\n. {w \ 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 \ s" using openE [OF \open s\ \w \ s\] . then have holfb: "f holomorphic_on ball w e" using holf holomorphic_on_subset by blast diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- 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 \ 0 \ \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 \ 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 \ 0" "n \ 0" + obtains w where "w \ 0" "z = w ^ n" + by (metis exists_complex_root [of n z] assms power_0_left) + subsection\The Unwinding Number and the Ln-product Formula\ text\Note that in this special case the unwinding number is -1, 0 or 1.\ diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy --- 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 ` \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: "\X. \open X; X \ S; X \ {}\ \ ~ f constant_on X" shows "open (f ` U)" proof - - have "S = \(components S)" by (fact Union_components) + have "S = \(components S)" by simp with \U \ S\ have "U = (\C \ components S. C \ U)" by auto then have "f ` U = (\C \ components S. f ` (C \ U))" - by auto + using image_UN by fastforce moreover { fix C assume "C \ components S" with S \C \ components S\ open_components in_components_connected @@ -1028,7 +1030,7 @@ apply (rule allI continuous_closed_preimage_univ continuous_intros)+ using \compact K\ compact_eq_bounded_closed by blast ultimately show ?thesis - using closed_inter_compact [OF \closed S\] compact_eq_bounded_closed by blast + using closed_Int_compact [OF \closed S\] compact_eq_bounded_closed by blast qed corollary proper_map_polyfun_univ: diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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\0" "u \ b / norm x" "y = u *\<^sub>R x" "y \ ?A" "y \ s" "\z\?A \ s. dist 0 z \ 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 \ closure S = {} \ A \ 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" diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Determinants.thy --- 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: "(\x. f x = x) \ f = id" - by auto - lemma det_linear_rows_setsum_lemma: assumes fS: "finite S" and fT: "finite T" diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- 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 \ 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: diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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 \ path_connected s" by (simp add: convex_imp_path_connected is_interval_convex) -lemma linear_homeomorphic_image: - fixes f :: "'a::euclidean_space \ 'a" +lemma linear_homeomorphism_image: + fixes f :: "'a::euclidean_space \ '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 \ '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: "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" - apply (simp add: frontier_interiors connected_open_in, safe) + apply (simp add: frontier_interiors connected_openin, safe) apply (drule_tac x="s \ interior t" in spec, safe) apply (drule_tac [2] x="s \ 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 (\x. True) {} t f g" +lemma homotopic_on_empty [simp]: "homotopic_with (\x. True) {} t f g" by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff) diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 \ openin (topology U) = U" using topology_inverse[unfolded mem_Collect_eq] . lemma topology_inverse_iff: "istopology U \ 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 \ (\S. openin T1 S \ 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 \ openin U T \ openin U (S \ T)" - using openin_clauses by simp - -lemma openin_Union[intro]: "(\S \K. openin U S) \ openin U (\K)" - using openin_clauses by simp + by (rule openin_clauses) + +lemma openin_Union[intro]: "(\S. S \ K \ openin U S) \ openin U (\K)" + using openin_clauses by blast lemma openin_Un[intro]: "openin U S \ openin U T \ openin U (S \ 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 \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" (is "?lhs \ ?rhs") @@ -472,7 +472,7 @@ next assume H: ?rhs let ?t = "\{T. openin U T \ T \ 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 \ ~(\e1 e2. openin (subtopology euclidean s) e1 \ openin (subtopology euclidean s) e2 \ @@ -718,17 +718,17 @@ apply (simp_all, blast+) \\slow\ done -lemma connected_open_in_eq: +lemma connected_openin_eq: "connected s \ ~(\e1 e2. openin (subtopology euclidean s) e1 \ openin (subtopology euclidean s) e2 \ e1 \ e2 = s \ e1 \ e2 = {} \ e1 \ {} \ e2 \ {})" - 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 \ ~(\e1 e2. closedin (subtopology euclidean s) e1 \ @@ -759,14 +759,14 @@ done qed -lemma connected_closed_in_eq: +lemma connected_closedin_eq: "connected s \ ~(\e1 e2. closedin (subtopology euclidean s) e1 \ closedin (subtopology euclidean s) e2 \ e1 \ e2 = s \ e1 \ e2 = {} \ e1 \ {} \ e2 \ {})" - 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 \ closed T \ closed S" by (auto simp add: closedin_closed intro: closedin_trans) -lemma openin_subtopology_inter_subset: - "openin (subtopology euclidean u) (u \ s) \ v \ u \ openin (subtopology euclidean v) (v \ s)" +lemma openin_subtopology_Int_subset: + "\openin (subtopology euclidean u) (u \ S); v \ u\ \ openin (subtopology euclidean v) (v \ S)" by (auto simp: openin_subtopology) lemma openin_open_eq: "open s \ (openin (subtopology euclidean s) t \ open t \ t \ s)" @@ -900,6 +900,34 @@ lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" by (metis open_contains_ball subset_eq centre_in_ball) +lemma openin_contains_ball: + "openin (subtopology euclidean t) s \ + s \ t \ (\x \ s. \e. 0 < e \ ball x e \ t \ 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 \ + s \ t \ + (\x \ s. \e. 0 < e \ cball x e \ t \ 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 = {} \ e \ 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 \ (S \ closure T) = {} \ S \ 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 \ 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 \ 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 \ s \ t \ (\x. x islimpt s \ x \ t \ x \ s)" apply (simp add: closedin_closed, safe) apply (simp add: closed_limpt islimpt_subset) @@ -1856,7 +1884,7 @@ lemma closedin_closed_eq: "closed s \ (closedin (subtopology euclidean s) t \ closed t \ t \ 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 \ components u \ (\x. x \ u \ s = connected_component_set u x)" by (auto simp: components_def) -lemma Union_components: "u = \(components u)" +lemma Union_components [simp]: "\(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 (\X Y. X \ Y = {}) (components u)" apply (simp add: pairwise_def) @@ -2174,17 +2203,17 @@ have "A \ closure s \ {}" using Alap Int_absorb1 ts by blast then have Alaps: "A \ s \ {}" - by (simp add: A open_inter_closure_eq_empty) + by (simp add: A open_Int_closure_eq_empty) have "B \ closure s \ {}" using Blap Int_absorb1 ts by blast then have Blaps: "B \ s \ {}" - 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 \ \ 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 \ x islimpt (s \ t) \ x islimpt t" by (simp add: islimpt_Un islimpt_finite) @@ -3769,7 +3798,7 @@ then have "l' islimpt (f ` {.. 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 \ f ` {N..}" "y \ s" "y \ l'" using \l' \ s\ \open s\ by (rule islimptE) then obtain n where "N \ n" "f n \ s" "f n \ l'" @@ -3822,7 +3851,7 @@ text\In particular, some common special cases.\ -lemma compact_union [intro]: +lemma compact_Un [intro]: assumes "compact s" and "compact t" shows " compact (s \ t)" @@ -3845,19 +3874,19 @@ "finite A \ (\x. x \ A \ compact (B x)) \ compact (\x\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 \ 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 \ 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} \ 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 \ 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 \ {x. R x} \ {}" by (auto simp: Z_def) moreover assume "Ball S Q" "\x. Q x \ R x \ 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 \ t)" proof (rule seq_compactI) @@ -4104,7 +4133,7 @@ lemma seq_compact_closed_subset: assumes "closed s" and "s \ 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 \ t)" @@ -4937,7 +4966,7 @@ fixes s :: "'a::metric_space set" assumes "closed s" and "s \ 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 \Equality of continuous functions on closure and related results.\ -lemma continuous_closed_in_preimage_constant: +lemma continuous_closedin_preimage_constant: fixes f :: "_ \ 'b::t1_space" shows "continuous_on s f \ closedin (subtopology euclidean s) {x \ s. f x = a}" using continuous_closedin_preimage[of s f "{a}"] by auto @@ -6087,20 +6116,20 @@ text \Proving a function is constant by proving open-ness of level set.\ -lemma continuous_levelset_open_in_cases: +lemma continuous_levelset_openin_cases: fixes f :: "_ \ 'b::t1_space" shows "connected s \ continuous_on s f \ openin (subtopology euclidean s) {x \ s. f x = a} \ (\x \ s. f x \ a) \ (\x \ 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 :: "_ \ 'b::t1_space" shows "connected s \ continuous_on s f \ openin (subtopology euclidean s) {x \ s. f x = a} \ (\x \ s. f x = a) \ (\x \ 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 \ s. f x = a}" and "\x \ s. f x = a" shows "\x \ 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 \closed s\ compact_cball) + by (intro closed_Int_compact \closed s\ compact_cball) ultimately obtain x where "x \ ?B" "\y\?B. dist a x \ dist a y" by (metis continuous_attains_inf) with that show ?thesis by fastforce @@ -7172,11 +7201,11 @@ text \Continuity relative to a union.\ -lemma continuous_on_union_local: +lemma continuous_on_Un_local: "\closedin (subtopology euclidean (s \ t)) s; closedin (subtopology euclidean (s \ t)) t; continuous_on s f; continuous_on t f\ \ continuous_on (s \ 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; \x. \x \ s \ ~P x \ x \ t \ P x\ \ f x = g x\ \ continuous_on (s \ t) (\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 \ real" @@ -7588,7 +7617,7 @@ assumes "box c d \ {}" shows "box a b \ cbox c d = {} \ box a b \ 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 \ ?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 diff -r 3f97aa4580c6 -r a8758f47f9e8 src/HOL/Multivariate_Analysis/Weierstrass.thy --- 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: "\t. t \ s-U \ pf t ` s \ {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 "\t. t \ s-U \ \A. open A \ A \ s = {x\