# HG changeset patch # User nipkow # Date 1456247071 -3600 # Node ID a620a8756b7ce7411653d773bc916be439139ea0 # Parent 7891843d79bb9ca1282f4b2af9ac06d9cfb4582a# Parent 747d36865c2c2387a69f0219785a6c3c8b08ebd4 resolved conflict diff -r 747d36865c2c -r a620a8756b7c src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Feb 23 18:04:31 2016 +0100 @@ -342,7 +342,7 @@ text \ The @{command datatype} command introduces various constants in addition to the constructors. With each datatype are associated set functions, a map -function,, a predicator, a relator, discriminators, and selectors, all of which can be given +function, a predicator, a relator, discriminators, and selectors, all of which can be given custom names. In the example below, the familiar names @{text null}, @{text hd}, @{text tl}, @{text set}, @{text map}, and @{text list_all2} override the default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2}, @@ -916,6 +916,10 @@ \item[@{text "t."}\hthm{map_sel}\rm:] ~ \\ @{thm list.map_sel[no_vars]} +\item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\ +@{thm list.pred_inject(1)[no_vars]} \\ +@{thm list.pred_inject(2)[no_vars]} + \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\ @{thm list.rel_inject(1)[no_vars]} \\ @{thm list.rel_inject(2)[no_vars]} @@ -1475,7 +1479,8 @@ \ primrec increasing_tree :: "int \ int tree\<^sub>f\<^sub>f \ bool" where - "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \ n \ m \ list_all (increasing_tree (n + 1)) ts" + "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \ + n \ m \ list_all (increasing_tree (n + 1)) ts" subsubsection \ Nested-as-Mutual Recursion @@ -1512,7 +1517,7 @@ @{thm [source] at\<^sub>f\<^sub>f.induct}, @{thm [source] ats\<^sub>f\<^sub>f.induct}, and @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The -induction rules and the underlying recursors are generated on a per-need basis +induction rules and the underlying recursors are generated dynamically and are kept in a cache to speed up subsequent definitions. Here is a second example: @@ -2352,7 +2357,7 @@ @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct} and analogously for @{text coinduct_strong}. These rules and the -underlying corecursors are generated on a per-need basis and are kept in a cache +underlying corecursors are generated dynamically and are kept in a cache to speed up subsequent definitions. \ @@ -2986,7 +2991,7 @@ @@{command bnf} target? (name ':')? type \ 'map:' term ('sets:' (term +))? 'bd:' term \ ('wits:' (term +))? ('rel:' term)? \ - @{syntax plugins}? + ('pred:' term)? @{syntax plugins}? \} \medskip @@ -3404,11 +3409,6 @@ \item[@{text "t."}\hthm{Domainp_rel} @{text "[relator_domain]"}\rm:] ~ \\ @{thm list.Domainp_rel[no_vars]} -\item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\ -@{thm list.pred_inject(1)[no_vars]} \\ -@{thm list.pred_inject(2)[no_vars]} \\ -This property is generated only for (co)datatypes. - \item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\ @{thm list.left_total_rel[no_vars]} diff -r 747d36865c2c -r a620a8756b7c src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Limits.thy Tue Feb 23 18:04:31 2016 +0100 @@ -1534,10 +1534,6 @@ text\Transformation of limit.\ -lemma eventually_at2: - "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" - unfolding eventually_at by auto - lemma Lim_transform: fixes a b :: "'a::real_normed_vector" shows "\(g \ a) F; ((\x. f x - g x) \ 0) F\ \ (f \ a) F" diff -r 747d36865c2c -r a620a8756b7c src/HOL/Meson.thy --- a/src/HOL/Meson.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Meson.thy Tue Feb 23 18:04:31 2016 +0100 @@ -93,7 +93,7 @@ subsection \Lemmas for Forward Proof\ -text\There is a similarity to congruence rules\ +text\There is a similarity to congruence rules. They are also useful in ordinary proofs.\ (*NOTE: could handle conjunctions (faster?) by nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) @@ -103,6 +103,9 @@ lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" by blast +lemma imp_forward: "[| P' \ Q'; P ==> P'; Q' ==> Q |] ==> P \ Q" +by blast + (*Version of @{text disj_forward} for removal of duplicate literals*) lemma disj_forward2: "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 18:04:31 2016 +0100 @@ -1998,7 +1998,7 @@ apply (rule retract_fixpoint_property[OF *, of "\x. scaleR 2 a - x"]) apply (blast intro: brouwer_ball[OF assms]) apply (intro continuous_intros) - unfolding frontier_cball subset_eq Ball_def image_iff dist_norm + unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def apply (auto simp add: ** norm_minus_commute) done then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 18:04:31 2016 +0100 @@ -74,7 +74,7 @@ shows "continuous_on s exp" by (simp add: continuous_on_exp continuous_on_id) -lemma holomorphic_on_exp: "exp holomorphic_on s" +lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s" by (simp add: complex_differentiable_within_exp holomorphic_on_def) subsection\Euler and de Moivre formulas.\ diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 18:04:31 2016 +0100 @@ -324,10 +324,24 @@ unfolding one_add_one [symmetric] scaleR_left_distrib by simp lemma vector_choose_size: - "0 \ c \ \x::'a::euclidean_space. norm x = c" - apply (rule exI [where x="c *\<^sub>R (SOME i. i \ Basis)"]) - apply (auto simp: SOME_Basis) - done + assumes "0 \ c" + obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c" +proof - + obtain a::'a where "a \ 0" + using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce + then show ?thesis + by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms) +qed + +lemma vector_choose_dist: + assumes "0 \ c" + obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c" +by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size) + +lemma sphere_eq_empty [simp]: + fixes a :: "'a::{real_normed_vector, perfect_space}" + shows "sphere a r = {} \ r < 0" +by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) lemma setsum_delta_notmem: assumes "x \ s" @@ -4300,8 +4314,7 @@ and "\y\s. dist a (closest_point s a) \ dist a y" unfolding closest_point_def apply(rule_tac[!] someI2_ex) - using distance_attains_inf[OF assms(1,2), of a] - apply auto + apply (auto intro: distance_attains_inf[OF assms(1,2), of a]) done lemma closest_point_in_set: "closed s \ s \ {} \ closest_point s a \ s" @@ -4446,9 +4459,8 @@ and "z \ s" shows "\a b. \y\s. inner a z < b \ inner a y = b \ (\x\s. inner a x \ b)" proof - - from distance_attains_inf[OF assms(2-3)] obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" - by auto + by (metis distance_attains_inf[OF assms(2-3)]) show ?thesis apply (rule_tac x="y - z" in exI) apply (rule_tac x="inner (y - z) y" in exI) @@ -4497,7 +4509,7 @@ next case False obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" - using distance_attains_inf[OF assms(2) False] by auto + by (metis distance_attains_inf[OF assms(2) False]) show ?thesis apply (rule_tac x="y - z" in exI) apply (rule_tac x="inner (y - z) z + (norm (y - z))\<^sup>2 / 2" in exI) @@ -4657,16 +4669,8 @@ shows "\a. a \ 0 \ (\x\s. 0 \ inner a x)" proof - let ?k = "\c. {x::'a. 0 \ inner c x}" - have "frontier (cball 0 1) \ (\(?k ` s)) \ {}" - apply (rule compact_imp_fip) - apply (rule compact_frontier[OF compact_cball]) - defer - apply rule - apply rule - apply (erule conjE) + have *: "frontier (cball 0 1) \ \f \ {}" if as: "f \ ?k ` s" "finite f" for f proof - - fix f - assume as: "f \ ?k ` s" "finite f" obtain c where c: "f = ?k ` c" "c \ s" "finite c" using finite_subset_image[OF as(2,1)] by auto then obtain a b where ab: "a \ 0" "0 < b" "\x\convex hull c. b < inner a x" @@ -4680,14 +4684,17 @@ unfolding subset_eq and inner_scaleR by (auto simp add: inner_commute del: ballE elim!: ballE) then show "frontier (cball 0 1) \ \f \ {}" - unfolding c(1) frontier_cball dist_norm by auto - qed (insert closed_halfspace_ge, auto) + unfolding c(1) frontier_cball sphere_def dist_norm by auto + qed + have "frontier (cball 0 1) \ (\(?k ` s)) \ {}" + apply (rule compact_imp_fip) + apply (rule compact_frontier[OF compact_cball]) + using * closed_halfspace_ge + by auto then obtain x where "norm x = 1" "\y\s. x\?k y" - unfolding frontier_cball dist_norm by auto + unfolding frontier_cball dist_norm sphere_def by auto then show ?thesis - apply (rule_tac x=x in exI) - apply (auto simp add: inner_commute) - done + by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one) qed lemma separating_hyperplane_sets: @@ -9928,8 +9935,9 @@ using assms by blast then have "\x \ s. \y \ t. dist x y \ setdist s t" - using distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms - apply (clarsimp simp: dist_norm le_setdist_iff, blast) + apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]]) + apply (simp add: dist_norm le_setdist_iff) + apply blast done then show ?thesis by (blast intro!: antisym [OF _ setdist_le_dist] ) @@ -10009,5 +10017,4 @@ lemma setdist_le_sing: "x \ s ==> setdist s t \ setdist {x} t" using setdist_subset_left by auto - end diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 18:04:31 2016 +0100 @@ -1697,15 +1697,15 @@ also continuous. So if we know for some other reason that the inverse function exists, it's OK.\ -lemma has_derivative_locally_injective: +proposition has_derivative_locally_injective: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes "a \ s" - and "open s" - and "bounded_linear g'" - and "g' \ f' a = id" - and "\x\s. (f has_derivative f' x) (at x)" - and "\e>0. \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e" - obtains t where "a \ t" "open t" "\x\t. \x'\t. f x' = f x \ x' = x" + and "open s" + and "bounded_linear g'" + and "g' \ f' a = id" + and "\x. x \ s \ (f has_derivative f' x) (at x)" + and "\e. e > 0 \ \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e" + obtains r where "r > 0" "ball a r \ s" "inj_on f (ball a r)" proof - interpret bounded_linear g' using assms by auto @@ -1738,9 +1738,11 @@ using real_lbound_gt_zero[OF d1(1) d2(1)] by blast show ?thesis proof - show "a \ ball a d" - using d by auto - show "\x\ball a d. \x'\ball a d. f x' = f x \ x' = x" + show "0 < d" by (fact d) + show "ball a d \ s" + using \d < d2\ \ball a d2 \ s\ by auto + show "inj_on f (ball a d)" + unfolding inj_on_def proof (intro strip) fix x y assume as: "x \ ball a d" "y \ ball a d" "f x = f y" @@ -1749,7 +1751,7 @@ unfolding ph_def o_def unfolding diff using f'g' - by (auto simp add: algebra_simps) + by (auto simp: algebra_simps) have "norm (ph x - ph y) \ (1 / 2) * norm (x - y)" apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\x v. v - g'(f' x v)"]) apply (rule_tac[!] ballI) @@ -1788,7 +1790,7 @@ using d1(2)[of u] using onorm_neg[where f="\x. f' u x - f' a x"] using d and u and onorm_pos_le[OF assms(3)] - apply (auto simp add: algebra_simps) + apply (auto simp: algebra_simps) done also have "\ \ 1 / 2" unfolding k_def by auto @@ -1804,7 +1806,7 @@ ultimately show "x = y" unfolding norm_minus_commute by auto qed - qed auto + qed qed diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 18:04:31 2016 +0100 @@ -1019,7 +1019,7 @@ shows "\e > 0. ball z e \ path_image g = {}" proof - obtain a where "a \ path_image g" "\y \ path_image g. dist z a \ dist z y" - using distance_attains_inf[OF _ path_image_nonempty, of g z] + apply (rule distance_attains_inf[OF _ path_image_nonempty, of g z]) using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto then show ?thesis apply (rule_tac x="dist z a" in exI) @@ -1661,6 +1661,50 @@ apply (auto simp: cball_diff_eq_sphere dist_norm) done +proposition connected_open_delete: + assumes "open S" "connected S" and 2: "2 \ DIM('N::euclidean_space)" + shows "connected(S - {a::'N})" +proof (cases "a \ S") + case True + with \open S\ obtain \ where "\ > 0" and \: "cball a \ \ S" + using open_contains_cball_eq by blast + have "dist a (a + \ *\<^sub>R (SOME i. i \ Basis)) = \" + by (simp add: dist_norm SOME_Basis \0 < \\ less_imp_le) + with \ have "\{S - ball a r |r. 0 < r \ r < \} \ {} \ False" + apply (drule_tac c="a + scaleR (\) ((SOME i. i \ Basis))" in subsetD) + by auto + then have nonemp: "(\{S - ball a r |r. 0 < r \ r < \}) = {} \ False" + by auto + have con: "\r. r < \ \ connected (S - ball a r)" + using \ by (force intro: connected_diff_ball [OF \connected S\ _ 2]) + have "x \ \{S - ball a r |r. 0 < r \ r < \}" if "x \ S - {a}" for x + apply (rule UnionI [of "S - ball a (min \ (dist a x) / 2)"]) + using that \0 < \\ apply (simp_all add:) + apply (rule_tac x="min \ (dist a x) / 2" in exI) + apply auto + done + then have "S - {a} = \{S - ball a r | r. 0 < r \ r < \}" + by auto + then show ?thesis + by (auto intro: connected_Union con dest!: nonemp) +next + case False then show ?thesis + by (simp add: \connected S\) +qed + +corollary path_connected_open_delete: + assumes "open S" "connected S" and 2: "2 \ DIM('N::euclidean_space)" + shows "path_connected(S - {a::'N})" +by (simp add: assms connected_open_delete connected_open_path_connected open_delete) + +corollary path_connected_punctured_ball: + "2 \ DIM('N::euclidean_space) \ path_connected(ball a r - {a::'N})" +by (simp add: path_connected_open_delete) + +lemma connected_punctured_ball: + "2 \ DIM('N::euclidean_space) \ connected(ball a r - {a::'N})" +by (simp add: connected_open_delete) + subsection\Relations between components and path components\ lemma open_connected_component: @@ -1961,7 +2005,10 @@ lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)" by (simp add: Int_commute frontier_def interior_closure) -lemma connected_inter_frontier: +lemma frontier_interior_subset: "frontier(interior S) \ frontier S" + by (simp add: Diff_mono frontier_interiors interior_mono interior_subset) + +lemma connected_Int_frontier: "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" apply (simp add: frontier_interiors connected_open_in, safe) apply (drule_tac x="s \ interior t" in spec, safe) @@ -1969,6 +2016,44 @@ apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) done +lemma frontier_not_empty: + fixes S :: "'a :: real_normed_vector set" + shows "\S \ {}; S \ UNIV\ \ frontier S \ {}" + using connected_Int_frontier [of UNIV S] by auto + +lemma frontier_eq_empty: + fixes S :: "'a :: real_normed_vector set" + shows "frontier S = {} \ S = {} \ S = UNIV" +using frontier_UNIV frontier_empty frontier_not_empty by blast + +lemma frontier_of_connected_component_subset: + fixes S :: "'a::real_normed_vector set" + shows "frontier(connected_component_set S x) \ frontier S" +proof - + { fix y + assume y1: "y \ closure (connected_component_set S x)" + and y2: "y \ interior (connected_component_set S x)" + have 1: "y \ closure S" + using y1 closure_mono connected_component_subset by blast + have "z \ interior (connected_component_set S x)" + if "0 < e" "ball y e \ interior S" "dist y z < e" for e z + proof - + have "ball y e \ connected_component_set S y" + apply (rule connected_component_maximal) + using that interior_subset mem_ball apply auto + done + then show ?thesis + using y1 apply (simp add: closure_approachable open_contains_ball_eq [OF open_interior]) + by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in subsetD + dist_commute mem_Collect_eq mem_ball mem_interior \0 < e\ y2) + qed + then have 2: "y \ interior S" + using y2 by (force simp: open_contains_ball_eq [OF open_interior]) + note 1 2 + } + then show ?thesis by (auto simp: frontier_def) +qed + lemma connected_component_UNIV: fixes x :: "'a::real_normed_vector" shows "connected_component_set UNIV x = UNIV" @@ -1992,7 +2077,7 @@ assume x: "x \ interior s" and y: "y \ s" and cc: "connected_component (- frontier s) x y" have "connected_component_set (- frontier s) x \ frontier s \ {}" - apply (rule connected_inter_frontier, simp) + apply (rule connected_Int_frontier, simp) apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x) using y cc by blast diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Summation.thy --- a/src/HOL/Multivariate_Analysis/Summation.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Summation.thy Tue Feb 23 18:04:31 2016 +0100 @@ -583,7 +583,6 @@ "conv_radius f = liminf (\n. inverse (ereal (root n (norm (f n)))))" by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def) - lemma abs_summable_in_conv_radius: fixes f :: "nat \ 'a :: {banach, real_normed_div_algebra}" assumes "ereal (norm z) < conv_radius f" @@ -905,7 +904,16 @@ from r have "summable (\n. (\i\n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))" by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all thus "summable (\n. (\i\n. f i * g (n - i)) * of_real r ^ n)" - by (simp add: algebra_simps of_real_def scaleR_power power_add [symmetric] scaleR_setsum_right) + by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_setsum_right) qed +lemma le_conv_radius_iff: + fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}" + shows "r \ conv_radius a \ (\x. norm (x-\) < r \ summable (\i. a i * (x - \) ^ i))" +apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex) +apply (meson less_ereal.simps(1) not_le order_trans) +apply (rule_tac x="of_real ra" in exI, simp) +apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real) +done + end diff -r 747d36865c2c -r a620a8756b7c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Feb 23 17:47:23 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Feb 23 18:04:31 2016 +0100 @@ -897,12 +897,15 @@ lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. +lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" + by (auto simp: open_contains_ball) + lemma openE[elim?]: assumes "open S" "x\S" obtains e where "e>0" "ball x e \ S" using assms unfolding open_contains_ball by auto -lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ S)" +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 ball_eq_empty[simp]: "ball x e = {} \ e \ 0" @@ -2251,6 +2254,9 @@ using frontier_complement frontier_subset_eq[of "- S"] unfolding open_closed by auto +lemma frontier_UNIV [simp]: "frontier UNIV = {}" + using frontier_complement frontier_empty by fastforce + subsection \Filters and the ``eventually true'' quantifier\ @@ -2339,7 +2345,7 @@ lemma Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_at2) + by (auto simp add: tendsto_iff eventually_at) lemma Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" @@ -2355,6 +2361,23 @@ lemma Lim_eventually: "eventually (\x. f x = l) net \ (f \ l) net" by (rule topological_tendstoI, auto elim: eventually_mono) +lemma Lim_transform_within_set: + fixes a l :: "'a::real_normed_vector" + shows "\(f \ l) (at a within s); eventually (\x. x \ s \ x \ t) (at a)\ + \ (f \ l) (at a within t)" +apply (clarsimp simp: eventually_at Lim_within) +apply (drule_tac x=e in spec, clarify) +apply (rename_tac k) +apply (rule_tac x="min d k" in exI) +apply (simp add:) +done + +lemma Lim_transform_within_set_eq: + fixes a l :: "'a::real_normed_vector" + shows "eventually (\x. x \ s \ x \ t) (at a) + \ ((f \ l) (at a within s) \ (f \ l) (at a within t))" +by (force intro: Lim_transform_within_set elim: eventually_mono) + text\The expected monotonicity property.\ lemma Lim_Un: @@ -2514,6 +2537,36 @@ using assms(1) tendsto_norm_zero [OF assms(2)] by (rule Lim_null_comparison) +lemma lim_null_mult_right_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes f: "(f \ 0) F" and g: "eventually (\x. norm(g x) \ B) F" + shows "((\z. f z * g z) \ 0) F" +proof - + have *: "((\x. norm (f x) * B) \ 0) F" + by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) + have "((\x. norm (f x) * norm (g x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_left_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + +lemma lim_null_mult_left_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes g: "eventually (\x. norm(g x) \ B) F" and f: "(f \ 0) F" + shows "((\z. g z * f z) \ 0) F" +proof - + have *: "((\x. B * norm (f x)) \ 0) F" + by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) + have "((\x. norm (g x) * norm (f x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_right_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + text\Deducing things about the limit from the elements.\ lemma Lim_in_closed_set: @@ -3149,21 +3202,18 @@ by auto qed -lemma frontier_ball: +lemma interior_ball [simp]: "interior (ball x e) = ball x e" + by (simp add: interior_open) + +lemma frontier_ball [simp]: fixes a :: "'a::real_normed_vector" - shows "0 < e \ frontier(ball a e) = {x. dist a x = e}" - apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) - apply (simp add: set_eq_iff) - apply arith - done - -lemma frontier_cball: + shows "0 < e \ frontier (ball a e) = sphere a e" + by (force simp: frontier_def) + +lemma frontier_cball [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" - shows "frontier (cball a e) = {x. dist a x = e}" - apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) - apply (simp add: set_eq_iff) - apply arith - done + shows "frontier (cball a e) = sphere a e" + by (force simp: frontier_def) lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0" apply (simp add: set_eq_iff not_le) @@ -3340,7 +3390,7 @@ lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" by (metis Diff_subset bounded_subset) -lemma not_bounded_UNIV[simp, intro]: +lemma not_bounded_UNIV[simp]: "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" proof (auto simp add: bounded_pos not_le) obtain x :: 'a where "x \ 0" @@ -4446,6 +4496,11 @@ shows "\compact s; c \ components s\ \ compact c" by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed) +lemma not_compact_UNIV[simp]: + fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" + shows "~ compact (UNIV::'a set)" + by (simp add: compact_eq_bounded_closed) + (* TODO: is this lemma necessary? *) lemma bounded_increasing_convergent: fixes s :: "nat \ real" @@ -4927,12 +4982,17 @@ using compact_eq_bounded_closed compact_frontier_bounded by blast +corollary compact_sphere: + fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" + shows "compact (sphere a r)" +using compact_frontier [of "cball a r"] by simp + lemma frontier_subset_compact: fixes s :: "'a::heine_borel set" shows "compact s \ frontier s \ s" using frontier_subset_closed compact_eq_bounded_closed by blast - + subsection\Relations among convergence and absolute convergence for power series.\ lemma summable_imp_bounded: @@ -5757,11 +5817,12 @@ lemma continuous_constant_on_closure: fixes f :: "_ \ 'b::t1_space" - assumes "continuous_on (closure s) f" - and "\x \ s. f x = a" - shows "\x \ (closure s). f x = a" - using continuous_closed_preimage_constant[of "closure s" f a] - assms closure_minimal[of s "{x \ closure s. f x = a}"] closure_subset + assumes "continuous_on (closure S) f" + and "\x. x \ S \ f x = a" + and "x \ closure S" + shows "f x = a" + using continuous_closed_preimage_constant[of "closure S" f a] + assms closure_minimal[of S "{x \ closure S. f x = a}"] closure_subset unfolding subset_eq by auto @@ -5851,6 +5912,27 @@ qed qed +subsection \A function constant on a set\ + +definition constant_on (infixl "(constant'_on)" 50) + where "f constant_on A \ \y. \x\A. f x = y" + +lemma constant_on_subset: "\f constant_on A; B \ A\ \ f constant_on B" + unfolding constant_on_def by blast + +lemma injective_not_constant: + fixes S :: "'a::{perfect_space} set" + shows "\open S; inj_on f S; f constant_on S\ \ S = {}" +unfolding constant_on_def +by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) + +lemma constant_on_closureI: + fixes f :: "_ \ 'b::t1_space" + assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f" + shows "f constant_on (closure S)" +using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def +by metis + text \Making a continuous function avoid some value in a neighbourhood.\ lemma continuous_within_avoid: @@ -6317,25 +6399,24 @@ lemma distance_attains_inf: fixes a :: "'a::heine_borel" - assumes "closed s" - and "s \ {}" - shows "\x\s. \y\s. dist a x \ dist a y" + assumes "closed s" and "s \