# HG changeset patch # User paulson # Date 1449506666 0 # Node ID d2e62ae01cd896866fbbb12048dc24cef550328a # Parent 4cf66f21b764ee433875f9829ffe965a6ddc0165 Cauchy's integral formula for circles. Starting to fix eventually_mono. diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Filter.thy Mon Dec 07 16:44:26 2015 +0000 @@ -71,6 +71,11 @@ unfolding eventually_def by (rule is_filter.mono [OF is_filter_Rep_filter]) +lemma eventually_mono': + "\eventually P F; \x. P x \ Q x\ \ eventually Q F" + unfolding eventually_def + by (blast intro: is_filter.mono [OF is_filter_Rep_filter]) + lemma eventually_conj: assumes P: "eventually (\x. P x) F" assumes Q: "eventually (\x. Q x) F" @@ -82,10 +87,11 @@ assumes "eventually (\x. P x \ Q x) F" assumes "eventually (\x. P x) F" shows "eventually (\x. Q x) F" -proof (rule eventually_mono) - show "\x. (P x \ Q x) \ P x \ Q x" by simp - show "eventually (\x. (P x \ Q x) \ P x) F" +proof - + have "eventually (\x. (P x \ Q x) \ P x) F" using assms by (rule eventually_conj) + then show ?thesis + by (blast intro: eventually_mono') qed lemma eventually_rev_mp: @@ -172,7 +178,7 @@ lemma frequently_mp: assumes ev: "\\<^sub>Fx in F. P x \ Q x" and P: "\\<^sub>Fx in F. P x" shows "\\<^sub>Fx in F. Q x" -proof - +proof - from ev have "eventually (\x. \ Q x \ \ P x) F" by (rule eventually_rev_mp) (auto intro!: always_eventually) from eventually_mp[OF this] P show ?thesis @@ -225,7 +231,7 @@ "(\\<^sub>Fx in F. C \ P x) \ (C \ (\\<^sub>Fx in F. P x))" by (cases C; simp add: not_frequently)+ -lemmas eventually_frequently_simps = +lemmas eventually_frequently_simps = eventually_frequently_const_simps not_eventually eventually_conj_iff @@ -340,7 +346,7 @@ unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } { assume "F \ F'" and "F \ F''" thus "F \ inf F' F''" unfolding le_filter_def eventually_inf - by (auto elim!: eventually_mono intro: eventually_conj) } + by (auto intro: eventually_mono' [OF eventually_conj]) } { show "F \ sup F F'" and "F' \ sup F F'" unfolding le_filter_def eventually_sup by simp_all } { assume "F \ F''" and "F' \ F''" thus "sup F F' \ F''" @@ -404,10 +410,13 @@ lemma trivial_limit_def: "trivial_limit F \ eventually (\x. False) F" by (rule eventually_False [symmetric]) +lemma False_imp_not_eventually: "(\x. \ P x ) \ \ trivial_limit net \ \ eventually (\x. P x) net" + by (simp add: eventually_False) + lemma eventually_Inf: "eventually P (Inf B) \ (\X\B. finite X \ eventually P (Inf X))" proof - let ?F = "\P. \X\B. finite X \ eventually P (Inf X)" - + { fix P have "eventually P (Abs_filter ?F) \ ?F P" proof (rule eventually_Abs_filter is_filter.intro)+ show "?F (\x. True)" @@ -605,7 +614,7 @@ have "eventually P (INF k. principal {k <..}) \ (\N::'a. \n>N. P n)" by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2) also have "(INF k. principal {k::'a <..}) = at_top" - unfolding at_top_def + unfolding at_top_def by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex) finally show ?thesis . qed @@ -645,7 +654,7 @@ have "eventually P (INF k. principal {..< k}) \ (\N::'a. \nm x. m \ J \ i m \ I) \ (\m x. m \ J \ x \ F (i m) \ f x \ G m) \ + "(\m x. m \ J \ i m \ I) \ (\m x. m \ J \ x \ F (i m) \ f x \ G m) \ LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))" by (force intro!: filterlim_INF_INF simp: image_subset_iff) -lemma filterlim_base_iff: +lemma filterlim_base_iff: assumes "I \ {}" and chain: "\i j. i \ I \ j \ I \ F i \ F j \ F j \ F i" shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \ (\j\J. \i\I. \x\F i. f x \ G j)" @@ -912,7 +921,7 @@ shows "(LIM x F. f x :> at_top) \ (\Z>c. eventually (\x. Z \ f x) F)" by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge) -lemma filterlim_at_bot: +lemma filterlim_at_bot: fixes f :: "'a \ ('b::linorder)" shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x \ Z) F)" by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1) @@ -926,12 +935,12 @@ assume "\Z. eventually (\x. f x \ Z) F" hence "eventually (\x. f x \ Z') F" by auto thus "eventually (\x. f x < Z) F" - apply (rule eventually_mono[rotated]) + apply (rule eventually_mono') using 1 by auto - next - fix Z :: 'b + next + fix Z :: 'b show "\Z. eventually (\x. f x < Z) F \ eventually (\x. f x \ Z) F" - by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le) + by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le) qed lemma filterlim_at_bot_le: @@ -958,7 +967,7 @@ where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)" lemma rel_filter_eventually: - "rel_filter R F G \ + "rel_filter R F G \ ((R ===> op =) ===> op =) (\P. eventually P F) (\P. eventually P G)" by(simp add: rel_filter_def eventually_def) @@ -984,7 +993,7 @@ from Q have *: "\x. T (Rep x) x" unfolding Quotient_alt_def by blast fix F - show "rel_filter T (filtermap Rep F) F" + show "rel_filter T (filtermap Rep F) F" by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\P. eventually P F"] rel_funI del: iffI simp add: eventually_filtermap rel_filter_eventually) qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually @@ -1063,7 +1072,7 @@ proof(rule left_totalI) fix F :: "'a filter" from bi_total_fun[OF bi_unique_fun[OF \bi_total A\ bi_unique_eq] bi_total_eq] - obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\P. eventually P F) G" + obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\P. eventually P F) G" unfolding bi_total_def by blast moreover have "is_filter (\P. eventually P F) \ is_filter G" by transfer_prover hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter) @@ -1094,7 +1103,7 @@ fix P :: "'a \ bool" obtain P' where [transfer_rule]: "(A ===> op =) P P'" using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast - have "eventually P F = eventually P' G" + have "eventually P F = eventually P' G" and "eventually P F' = eventually P' G" by transfer_prover+ thus "eventually P F = eventually P F'" by simp qed @@ -1139,7 +1148,7 @@ context fixes A :: "'a \ 'b \ bool" - assumes [transfer_rule]: "bi_unique A" + assumes [transfer_rule]: "bi_unique A" begin lemma le_filter_parametric [transfer_rule]: @@ -1173,4 +1182,4 @@ end -end \ No newline at end of file +end diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Library/Extended_Real.thy Mon Dec 07 16:44:26 2015 +0000 @@ -2443,11 +2443,8 @@ assume "open S" and "x \ S" then have S: "open S" "ereal x \ ereal ` S" by (simp_all add: inj_image_mem_iff) - have "\x. f x \ ereal ` S \ real_of_ereal (f x) \ S" - by auto - from this lim[THEN topological_tendstoD, OF open_ereal, OF S] show "eventually (\x. real_of_ereal (f x) \ S) net" - by (rule eventually_mono) + by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]]) qed lemma lim_ereal[simp]: "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Library/Liminf_Limsup.thy Mon Dec 07 16:44:26 2015 +0000 @@ -100,7 +100,7 @@ lemma Liminf_eq: assumes "eventually (\x. f x = g x) F" shows "Liminf F f = Liminf F g" - by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto + by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto lemma Limsup_mono: assumes ev: "eventually (\x. f x \ g x) F" @@ -116,7 +116,7 @@ lemma Limsup_eq: assumes "eventually (\x. f x = g x) net" shows "Limsup net f = Limsup net g" - by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto + by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto lemma Liminf_le_Limsup: assumes ntriv: "\ trivial_limit F" diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Limits.thy Mon Dec 07 16:44:26 2015 +0000 @@ -661,6 +661,10 @@ subsubsection \Linear operators and multiplication\ +lemma linear_times: + fixes c::"'a::real_algebra" shows "linear (\x. c * x)" + by (auto simp: linearI distrib_left) + lemma (in bounded_linear) tendsto: "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) @@ -713,6 +717,16 @@ lemmas tendsto_mult [tendsto_intros] = bounded_bilinear.tendsto [OF bounded_bilinear_mult] +lemma tendsto_mult_left: + fixes c::"'a::real_normed_algebra" + shows "(f ---> l) F \ ((\x. c * (f x)) ---> c * l) F" +by (rule tendsto_mult [OF tendsto_const]) + +lemma tendsto_mult_right: + fixes c::"'a::real_normed_algebra" + shows "(f ---> l) F \ ((\x. (f x) * c) ---> l * c) F" +by (rule tendsto_mult [OF _ tendsto_const]) + lemmas continuous_of_real [continuous_intros] = bounded_linear.continuous [OF bounded_linear_of_real] diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Dec 07 16:44:26 2015 +0000 @@ -1508,7 +1508,7 @@ apply (auto simp: has_contour_integral_integral) done -lemma contour_integral_0: "contour_integral g (\x. 0) = 0" +lemma contour_integral_0 [simp]: "contour_integral g (\x. 0) = 0" by (simp add: contour_integral_unique has_contour_integral_0) lemma contour_integral_setsum: @@ -4728,4 +4728,472 @@ \ winding_number h z = winding_number g z" by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq) + +proposition winding_number_subpath_combine: + "\path g; z \ path_image g; + u \ {0..1}; v \ {0..1}; w \ {0..1}\ + \ winding_number (subpath u v g) z + winding_number (subpath v w g) z = + winding_number (subpath u w g) z" +apply (rule trans [OF winding_number_join [THEN sym] + winding_number_homotopic_paths [OF homotopic_join_subpaths]]) +apply (auto dest: path_image_subpath_subset) +done + + +subsection\Partial circle path\ + +definition part_circlepath :: "[complex, real, real, real, real] \ complex" + where "part_circlepath z r s t \ \x. z + of_real r * exp (ii * of_real (linepath s t x))" + +lemma pathstart_part_circlepath [simp]: + "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)" +by (metis part_circlepath_def pathstart_def pathstart_linepath) + +lemma pathfinish_part_circlepath [simp]: + "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)" +by (metis part_circlepath_def pathfinish_def pathfinish_linepath) + +proposition has_vector_derivative_part_circlepath [derivative_intros]: + "((part_circlepath z r s t) has_vector_derivative + (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x))) + (at x within X)" + apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real) + apply (rule has_vector_derivative_real_complex) + apply (rule derivative_eq_intros | simp)+ + done + +corollary vector_derivative_part_circlepath: + "vector_derivative (part_circlepath z r s t) (at x) = + ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)" + using has_vector_derivative_part_circlepath vector_derivative_at by blast + +corollary vector_derivative_part_circlepath01: + "\0 \ x; x \ 1\ + \ vector_derivative (part_circlepath z r s t) (at x within {0..1}) = + ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)" + using has_vector_derivative_part_circlepath + by (auto simp: vector_derivative_at_within_ivl) + +lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)" + apply (simp add: valid_path_def) + apply (rule C1_differentiable_imp_piecewise) + apply (auto simp: C1_differentiable_on_eq vector_derivative_works vector_derivative_part_circlepath has_vector_derivative_part_circlepath + intro!: continuous_intros) + done + +lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)" + by (simp add: valid_path_imp_path) + +proposition path_image_part_circlepath: + assumes "s \ t" + shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \ x \ x \ t}" +proof - + { fix z::real + assume "0 \ z" "z \ 1" + with \s \ t\ have "\x. (exp (\ * linepath s t z) = exp (\ * of_real x)) \ s \ x \ x \ t" + apply (rule_tac x="(1 - z) * s + z * t" in exI) + apply (simp add: linepath_def scaleR_conv_of_real algebra_simps) + apply (rule conjI) + using mult_right_mono apply blast + using affine_ineq by (metis "mult.commute") + } + moreover + { fix z + assume "s \ z" "z \ t" + then have "z + of_real r * exp (\ * of_real z) \ (\x. z + of_real r * exp (\ * linepath s t x)) ` {0..1}" + apply (rule_tac x="(z - s)/(t - s)" in image_eqI) + apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq) + apply (auto simp: algebra_simps divide_simps) + done + } + ultimately show ?thesis + by (fastforce simp add: path_image_def part_circlepath_def) +qed + +corollary path_image_part_circlepath_subset: + "\s \ t; 0 \ r\ \ path_image(part_circlepath z r s t) \ sphere z r" +by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult) + +proposition in_path_image_part_circlepath: + assumes "w \ path_image(part_circlepath z r s t)" "s \ t" "0 \ r" + shows "norm(w - z) = r" +proof - + have "w \ {c. dist z c = r}" + by (metis (no_types) path_image_part_circlepath_subset sphere_def subset_eq assms) + thus ?thesis + by (simp add: dist_norm norm_minus_commute) +qed + +proposition finite_bounded_log: "finite {z::complex. norm z \ b \ exp z = w}" +proof (cases "w = 0") + case True then show ?thesis by auto +next + case False + have *: "finite {x. cmod (complex_of_real (2 * real_of_int x * pi) * \) \ b + cmod (Ln w)}" + apply (simp add: norm_mult finite_int_iff_bounded_le) + apply (rule_tac x="floor ((b + cmod (Ln w)) / (2*pi))" in exI) + apply (auto simp: divide_simps le_floor_iff) + done + have [simp]: "\P f. {z. P z \ (\n. z = f n)} = f ` {n. P (f n)}" + by blast + show ?thesis + apply (subst exp_Ln [OF False, symmetric]) + apply (simp add: exp_eq) + using norm_add_leD apply (fastforce intro: finite_subset [OF _ *]) + done +qed + +lemma finite_bounded_log2: + fixes a::complex + assumes "a \ 0" + shows "finite {z. norm z \ b \ exp(a*z) = w}" +proof - + have *: "finite ((\z. z / a) ` {z. cmod z \ b * cmod a \ exp z = w})" + by (rule finite_imageI [OF finite_bounded_log]) + show ?thesis + by (rule finite_subset [OF _ *]) (force simp: assms norm_mult) +qed + +proposition has_contour_integral_bound_part_circlepath_strong: + assumes fi: "(f has_contour_integral i) (part_circlepath z r s t)" + and "finite k" and le: "0 \ B" "0 < r" "s \ t" + and B: "\x. x \ path_image(part_circlepath z r s t) - k \ norm(f x) \ B" + shows "cmod i \ B * r * (t - s)" +proof - + consider "s = t" | "s < t" using \s \ t\ by linarith + then show ?thesis + proof cases + case 1 with fi [unfolded has_contour_integral] + have "i = 0" by (simp add: vector_derivative_part_circlepath) + with assms show ?thesis by simp + next + case 2 + have [simp]: "abs r = r" using \r > 0\ by linarith + have [simp]: "cmod (complex_of_real t - complex_of_real s) = t-s" + by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff) + have "finite (part_circlepath z r s t -` {y} \ {0..1})" if "y \ k" for y + proof - + def w \ "(y - z)/of_real r / exp(ii * of_real s)" + have fin: "finite (of_real -` {z. cmod z \ 1 \ exp (\ * complex_of_real (t - s) * z) = w})" + apply (rule finite_vimageI [OF finite_bounded_log2]) + using \s < t\ apply (auto simp: inj_of_real) + done + show ?thesis + apply (simp add: part_circlepath_def linepath_def vimage_def) + apply (rule finite_subset [OF _ fin]) + using le + apply (auto simp: w_def algebra_simps scaleR_conv_of_real exp_add exp_diff) + done + qed + then have fin01: "finite ((part_circlepath z r s t) -` k \ {0..1})" + by (rule finite_finite_vimage_IntI [OF \finite k\]) + have **: "((\x. if (part_circlepath z r s t x) \ k then 0 + else f(part_circlepath z r s t x) * + vector_derivative (part_circlepath z r s t) (at x)) has_integral i) {0..1}" + apply (rule has_integral_spike + [where f = "\x. f(part_circlepath z r s t x) * vector_derivative (part_circlepath z r s t) (at x)"]) + apply (rule negligible_finite [OF fin01]) + using fi has_contour_integral + apply auto + done + have *: "\x. \0 \ x; x \ 1; part_circlepath z r s t x \ k\ \ cmod (f (part_circlepath z r s t x)) \ B" + by (auto intro!: B [unfolded path_image_def image_def, simplified]) + show ?thesis + apply (rule has_integral_bound [where 'a=real, simplified, OF _ **, simplified]) + using assms apply force + apply (simp add: norm_mult vector_derivative_part_circlepath) + using le * "2" \r > 0\ by auto + qed +qed + +corollary has_contour_integral_bound_part_circlepath: + "\(f has_contour_integral i) (part_circlepath z r s t); + 0 \ B; 0 < r; s \ t; + \x. x \ path_image(part_circlepath z r s t) \ norm(f x) \ B\ + \ norm i \ B*r*(t - s)" + by (auto intro: has_contour_integral_bound_part_circlepath_strong) + +proposition contour_integrable_continuous_part_circlepath: + "continuous_on (path_image (part_circlepath z r s t)) f + \ f contour_integrable_on (part_circlepath z r s t)" + apply (simp add: contour_integrable_on has_contour_integral_def vector_derivative_part_circlepath path_image_def) + apply (rule integrable_continuous_real) + apply (fast intro: path_part_circlepath [unfolded path_def] continuous_intros continuous_on_compose2 [where g=f, OF _ _ order_refl]) + done + +proposition winding_number_part_circlepath_pos_less: + assumes "s < t" and no: "norm(w - z) < r" + shows "0 < Re (winding_number(part_circlepath z r s t) w)" +proof - + have "0 < r" by (meson no norm_not_less_zero not_le order.strict_trans2) + note valid_path_part_circlepath + moreover have " w \ path_image (part_circlepath z r s t)" + using assms by (auto simp: path_image_def image_def part_circlepath_def norm_mult linepath_def) + moreover have "0 < r * (t - s) * (r - cmod (w - z))" + using assms by (metis \0 < r\ diff_gt_0_iff_gt mult_pos_pos) + ultimately show ?thesis + apply (rule winding_number_pos_lt [where e = "r*(t - s)*(r - norm(w - z))"]) + apply (simp add: vector_derivative_part_circlepath right_diff_distrib [symmetric] mult_ac) + apply (rule mult_left_mono)+ + using Re_Im_le_cmod [of "w-z" "linepath s t x" for x] + apply (simp add: exp_Euler cos_of_real sin_of_real part_circlepath_def algebra_simps cos_squared_eq [unfolded power2_eq_square]) + using assms \0 < r\ by auto +qed + +proposition simple_path_part_circlepath: + "simple_path(part_circlepath z r s t) \ (r \ 0 \ s \ t \ abs(s - t) \ 2*pi)" +proof (cases "r = 0 \ s = t") + case True + then show ?thesis + apply (rule disjE) + apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+ + done +next + case False then have "r \ 0" "s \ t" by auto + have *: "\x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z \ ii*(x - y) * (t - s) = z" + by (simp add: algebra_simps) + have abs01: "\x y::real. 0 \ x \ x \ 1 \ 0 \ y \ y \ 1 + \ (x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0 \ abs(x - y) \ {0,1})" + by auto + have abs_away: "\P. (\x\{0..1}. \y\{0..1}. P(abs(x - y))) \ (\x::real. 0 \ x \ x \ 1 \ P x)" + by force + have **: "\x y. (\n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \ + (\n. abs(x - y) * (t - s) = 2 * (of_int n * pi))" + by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real] + intro: exI [where x = "-n" for n]) + have 1: "\x. 0 \ x \ x \ 1 \ (\n. x * (t - s) = 2 * (real_of_int n * pi)) \ x = 0 \ x = 1 \ \s - t\ \ 2 * pi" + apply (rule ccontr) + apply (drule_tac x="2*pi / abs(t-s)" in spec) + using False + apply (simp add: abs_minus_commute divide_simps) + apply (frule_tac x=1 in spec) + apply (drule_tac x="-1" in spec) + apply (simp add:) + done + have 2: "\s - t\ = \2 * (real_of_int n * pi) / x\" if "x \ 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n + proof - + have "t-s = 2 * (real_of_int n * pi)/x" + using that by (simp add: field_simps) + then show ?thesis by (metis abs_minus_commute) + qed + show ?thesis using False + apply (simp add: simple_path_def path_part_circlepath) + apply (simp add: part_circlepath_def linepath_def exp_eq * ** abs01 del: Set.insert_iff) + apply (subst abs_away) + apply (auto simp: 1) + apply (rule ccontr) + apply (auto simp: 2 divide_simps abs_mult dest: of_int_leD) + done +qed + +proposition arc_part_circlepath: + assumes "r \ 0" "s \ t" "abs(s - t) < 2*pi" + shows "arc (part_circlepath z r s t)" +proof - + have *: "x = y" if eq: "\ * (linepath s t x) = \ * (linepath s t y) + 2 * of_int n * complex_of_real pi * \" + and x: "x \ {0..1}" and y: "y \ {0..1}" for x y n + proof - + have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi" + by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq) + then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))" + by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re]) + then have st: "x \ y \ (s-t) = (of_int n * (pi * 2) / (y-x))" + by (force simp: field_simps) + show ?thesis + apply (rule ccontr) + using assms x y + apply (simp add: st abs_mult field_simps) + using st + apply (auto simp: dest: of_int_lessD) + done + qed + show ?thesis + using assms + apply (simp add: arc_def) + apply (simp add: part_circlepath_def inj_on_def exp_eq) + apply (blast intro: *) + done +qed + + +subsection\Special case of one complete circle\ + +definition circlepath :: "[complex, real, real] \ complex" + where "circlepath z r \ part_circlepath z r 0 (2*pi)" + +lemma circlepath: "circlepath z r = (\x. z + r * exp(2 * of_real pi * ii * of_real x))" + by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps) + +lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r" + by (simp add: circlepath_def) + +lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r" + by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute) + +proposition has_vector_derivative_circlepath [derivative_intros]: + "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x))) + (at x within X)" + apply (simp add: circlepath_def scaleR_conv_of_real) + apply (rule derivative_eq_intros) + apply (simp add: algebra_simps) + done + +corollary vector_derivative_circlepath: + "vector_derivative (circlepath z r) (at x) = + 2 * pi * ii * r * exp(2 * of_real pi * ii * x)" +using has_vector_derivative_circlepath vector_derivative_at by blast + +corollary vector_derivative_circlepath01: + "\0 \ x; x \ 1\ + \ vector_derivative (circlepath z r) (at x within {0..1}) = + 2 * pi * ii * r * exp(2 * of_real pi * ii * x)" + using has_vector_derivative_circlepath + by (auto simp: vector_derivative_at_within_ivl) + +lemma valid_path_circlepath [simp]: "valid_path (circlepath z r)" + by (simp add: circlepath_def) + +lemma path_circlepath [simp]: "path (circlepath z r)" + by (simp add: valid_path_imp_path) + +proposition path_image_circlepath [simp]: + assumes "0 \ r" shows "path_image (circlepath z r) = sphere z r" +proof - + have *: "x \ (\u. z + (cmod (x - z)) * exp (\ * (of_real u * (of_real pi * 2)))) ` {0..1}" for x + proof (cases "x = z") + case True then show ?thesis by force + next + case False + def w \ "x - z" + then have "w \ 0" by (simp add: False) + have **: "\t. \Re w = cos t * cmod w; Im w = sin t * cmod w\ \ w = of_real (cmod w) * exp (\ * t)" + using cis_conv_exp complex_eq_iff by auto + show ?thesis + apply (rule sincos_total_2pi [of "Re(w/of_real(norm w))" "Im(w/of_real(norm w))"]) + apply (simp add: divide_simps \w \ 0\ cmod_power2 [symmetric]) + apply (rule_tac x="t / (2*pi)" in image_eqI) + apply (simp add: divide_simps \w \ 0\) + using False ** + apply (auto simp: w_def) + done + qed + show ?thesis + unfolding circlepath path_image_def sphere_def dist_norm + by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *) +qed + +lemma has_contour_integral_bound_circlepath_strong: + "\(f has_contour_integral i) (circlepath z r); + finite k; 0 \ B; 0 < r; + \x. \norm(x - z) = r; x \ k\ \ norm(f x) \ B\ + \ norm i \ B*(2*pi*r)" + unfolding circlepath_def + by (auto simp: algebra_simps in_path_image_part_circlepath dest!: has_contour_integral_bound_part_circlepath_strong) + +corollary has_contour_integral_bound_circlepath: + "\(f has_contour_integral i) (circlepath z r); + 0 \ B; 0 < r; \x. norm(x - z) = r \ norm(f x) \ B\ + \ norm i \ B*(2*pi*r)" + by (auto intro: has_contour_integral_bound_circlepath_strong) + +proposition contour_integrable_continuous_circlepath: + "continuous_on (path_image (circlepath z r)) f + \ f contour_integrable_on (circlepath z r)" + by (simp add: circlepath_def contour_integrable_continuous_part_circlepath) + +lemma simple_path_circlepath: "simple_path(circlepath z r) \ (r \ 0)" + by (simp add: circlepath_def simple_path_part_circlepath) + +lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r \ w \ path_image (circlepath z r)" + apply (subst path_image_circlepath) + apply (meson le_cases less_le_trans norm_not_less_zero) + apply (simp add: sphere_def dist_norm norm_minus_commute) + done + +proposition contour_integral_circlepath: + "0 < r \ contour_integral (circlepath z r) (\w. 1 / (w - z)) = 2 * complex_of_real pi * \" + apply (rule contour_integral_unique) + apply (simp add: has_contour_integral_def) + apply (subst has_integral_cong) + apply (simp add: vector_derivative_circlepath01) + using has_integral_const_real [of _ 0 1] + apply (force simp: circlepath) + done + +lemma winding_number_circlepath_centre: "0 < r \ winding_number (circlepath z r) z = 1" + apply (rule winding_number_unique_loop) + apply (simp_all add: sphere_def valid_path_imp_path) + apply (rule_tac x="circlepath z r" in exI) + apply (simp add: sphere_def contour_integral_circlepath) + done + +proposition winding_number_circlepath: + assumes "norm(w - z) < r" shows "winding_number(circlepath z r) w = 1" +proof (cases "w = z") + case True then show ?thesis + using assms winding_number_circlepath_centre by auto +next + case False + have [simp]: "r > 0" + using assms le_less_trans norm_ge_zero by blast + def r' \ "norm(w - z)" + have "r' < r" + by (simp add: assms r'_def) + have disjo: "cball z r' \ sphere z r = {}" + using \r' < r\ by (force simp: cball_def sphere_def) + have "winding_number(circlepath z r) w = winding_number(circlepath z r) z" + apply (rule winding_number_around_inside [where s = "cball z r'"]) + apply (simp_all add: disjo order.strict_implies_order winding_number_circlepath_centre) + apply (simp_all add: False r'_def dist_norm norm_minus_commute) + done + also have "... = 1" + by (simp add: winding_number_circlepath_centre) + finally show ?thesis . +qed + + +text\ Hence the Cauchy formula for points inside a circle.\ + +theorem Cauchy_integral_circlepath: + assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r" + shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w)) + (circlepath z r)" +proof - + have "r > 0" + using assms le_less_trans norm_ge_zero by blast + have "((\u. f u / (u - w)) has_contour_integral (2 * pi) * \ * winding_number (circlepath z r) w * f w) + (circlepath z r)" + apply (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"]) + using assms \r > 0\ + apply (simp_all add: dist_norm norm_minus_commute) + apply (metis at_within_interior dist_norm holomorphic_on_def interior_ball mem_ball norm_minus_commute) + apply (simp add: cball_def sphere_def dist_norm, clarify) + apply (simp add:) + by (metis dist_commute dist_norm less_irrefl) + then show ?thesis + by (simp add: winding_number_circlepath assms) +qed + +corollary Cauchy_integral_circlepath_simple: + assumes "f holomorphic_on cball z r" "norm(w - z) < r" + shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w)) + (circlepath z r)" +using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath) + + +lemma no_bounded_connected_component_imp_winding_number_zero: + assumes g: "path g" "path_image g \ s" "pathfinish g = pathstart g" "z \ s" + and nb: "\z. bounded (connected_component_set (- s) z) \ z \ s" + shows "winding_number g z = 0" +apply (rule winding_number_zero_in_outside) +apply (simp_all add: assms) +by (metis nb [of z] \path_image g \ s\ \z \ s\ contra_subsetD mem_Collect_eq outside outside_mono) + +lemma no_bounded_path_component_imp_winding_number_zero: + assumes g: "path g" "path_image g \ s" "pathfinish g = pathstart g" "z \ s" + and nb: "\z. bounded (path_component_set (- s) z) \ z \ s" + shows "winding_number g z = 0" +apply (rule no_bounded_connected_component_imp_winding_number_zero [OF g]) +by (simp add: bounded_subset nb path_component_subset_connected_component) + end diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Dec 07 16:44:26 2015 +0000 @@ -24,8 +24,8 @@ using bounded_linear.has_derivative[OF bounded_linear_of_real] . lemma has_vector_derivative_real_complex: - "DERIV f (of_real a) :> f' \ ((\x. f (of_real x)) has_vector_derivative f') (at a)" - using has_derivative_compose[of of_real of_real a UNIV f "op * f'"] + "DERIV f (of_real a) :> f' \ ((\x. f (of_real x)) has_vector_derivative f') (at a within s)" + using has_derivative_compose[of of_real of_real a _ f "op * f'"] by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def) lemma fact_cancel: @@ -33,10 +33,6 @@ shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps) -lemma linear_times: - fixes c::"'a::real_algebra" shows "linear (\x. c * x)" - by (auto simp: linearI distrib_left) - lemma bilinear_times: fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)" by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) @@ -44,16 +40,6 @@ lemma linear_cnj: "linear cnj" using bounded_linear.linear[OF bounded_linear_cnj] . -lemma tendsto_mult_left: - fixes c::"'a::real_normed_algebra" - shows "(f ---> l) F \ ((\x. c * (f x)) ---> c * l) F" -by (rule tendsto_mult [OF tendsto_const]) - -lemma tendsto_mult_right: - fixes c::"'a::real_normed_algebra" - shows "(f ---> l) F \ ((\x. (f x) * c) ---> l * c) F" -by (rule tendsto_mult [OF _ tendsto_const]) - lemma tendsto_Re_upper: assumes "~ (trivial_limit F)" "(f ---> l) F" diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Dec 07 16:44:26 2015 +0000 @@ -854,6 +854,13 @@ obtains r a::real where "z = complex_of_real r * (cos a + \ * sin a)" "0 \ r" "0 \ a" "a < 2*pi" using Arg cis.ctr cis_conv_exp by fastforce +lemma Re_Im_le_cmod: "Im w * sin \ + Re w * cos \ \ cmod w" +proof (cases w rule: complex_split_polar) + case (1 r a) with sin_cos_le1 [of a \] show ?thesis + apply (simp add: norm_mult cmod_unit_one) + by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le) +qed + subsection\Analytic properties of tangent function\ lemma cnj_tan: "cnj(tan z) = tan(cnj z)" diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 07 16:44:26 2015 +0000 @@ -2622,7 +2622,7 @@ lemma integral_neg: "f integrable_on s \ integral s (\x. - f x) = - integral s f" by (rule integral_unique) (metis integrable_integral has_integral_neg) -lemma integral_sub: "f integrable_on s \ g integrable_on s \ +lemma integral_diff: "f integrable_on s \ g integrable_on s \ integral s (\x. f x - g x) = integral s f - integral s g" by (rule integral_unique) (metis integrable_integral has_integral_sub) @@ -2645,7 +2645,7 @@ lemma integrable_neg: "f integrable_on s \ (\x. -f(x)) integrable_on s" unfolding integrable_on_def by(auto intro: has_integral_neg) -lemma integrable_sub: +lemma integrable_diff: "f integrable_on s \ g integrable_on s \ (\x. f x - g x) integrable_on s" unfolding integrable_on_def by(auto intro: has_integral_sub) @@ -4623,6 +4623,8 @@ qed qed +lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified] + subsection \Negligible sets.\ @@ -8933,19 +8935,19 @@ have *: "\x f g. (if x \ s then f x else 0) - (if x \ s then g x else 0) = (if x \ s then f x - g x else (0::real))" by auto - note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]] + note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_diff, OF h g]] show "norm (integral (cbox a b) (\x. if x \ s then h x else 0) - integral (cbox a b) (\x. if x \ s then g x else 0)) \ norm (integral (cbox c d) (\x. if x \ s then h x else 0) - integral (cbox c d) (\x. if x \ s then g x else 0))" - unfolding integral_sub[OF h g,symmetric] real_norm_def + unfolding integral_diff[OF h g,symmetric] real_norm_def apply (subst **) defer apply (subst **) defer apply (rule has_integral_subset_le) defer - apply (rule integrable_integral integrable_sub h g)+ + apply (rule integrable_integral integrable_diff h g)+ proof safe fix x assume "x \ cbox a b" @@ -10123,7 +10125,7 @@ qed have sub: "\k. integral s (\x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" - apply (subst integral_sub) + apply (subst integral_diff) apply (rule assms(1)[rule_format])+ apply rule done @@ -10144,7 +10146,7 @@ next case (2 k) then show ?case - apply (rule integrable_sub) + apply (rule integrable_diff) using assms(1) apply auto done @@ -10182,7 +10184,7 @@ apply - apply rule defer - apply (subst(asm) integral_sub) + apply (subst(asm) integral_diff) using assms(1) apply auto apply (rule LIMSEQ_imp_Suc) @@ -11653,11 +11655,11 @@ "J = integral (cbox a b) g" using I[of n] J by (simp_all add: integral_unique) then have "dist (I n) J = norm (integral (cbox a b) (\x. f n x - g x))" - by (simp add: integral_sub dist_norm) + by (simp add: integral_diff dist_norm) also have "\ \ integral (cbox a b) (\x. (e' / content (cbox a b)))" using elim by (intro integral_norm_bound_integral) - (auto intro!: integrable_sub absolutely_integrable_onI) + (auto intro!: integrable_diff absolutely_integrable_onI) also have "\ < e" using \0 < e\ by (simp add: e'_def) @@ -12029,12 +12031,12 @@ apply clarify apply (rule le_less_trans [OF _ e2_less]) apply (rule integrable_bound) - apply (auto intro: integrable_sub continuous_on_imp_integrable_on_Pair1) + apply (auto intro: integrable_diff continuous_on_imp_integrable_on_Pair1) done } note * = this show ?thesis apply (rule integrable_continuous) - apply (simp add: * continuous_on_iff dist_norm integral_sub [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms]) + apply (simp add: * continuous_on_iff dist_norm integral_diff [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms]) done qed @@ -12217,10 +12219,10 @@ by (blast intro: continuous_on_imp_integrable_on_Pair1) have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\x. f (t1,t2))) \ e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" - apply (simp only: integral_sub [symmetric] f_int_uwvz integrable_const) + apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const) apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]]) using cbp e' nf' - apply (auto simp: integrable_sub f_int_uwvz integrable_const) + apply (auto simp: integrable_diff f_int_uwvz integrable_const) done have int_integrable: "(\x. integral (cbox w z) (\y. f (x, y))) integrable_on cbox u v" using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast @@ -12228,24 +12230,24 @@ "\x. x \ cbox u v \ norm (integral (cbox w z) (\y. f (x, y)) - integral (cbox w z) (\y. f (t1, t2))) \ e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2" - apply (simp only: integral_sub [symmetric] f_int_uv integrable_const) + apply (simp only: integral_diff [symmetric] f_int_uv integrable_const) apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]]) using cbp e' nf' - apply (auto simp: integrable_sub f_int_uv integrable_const) + apply (auto simp: integrable_diff f_int_uv integrable_const) done have "norm (integral (cbox u v) (\x. integral (cbox w z) (\y. f (x,y)) - integral (cbox w z) (\y. f (t1,t2)))) \ e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)" apply (rule integrable_bound [OF _ _ normint_wz]) using cbp e' - apply (auto simp: divide_simps content_pos_le integrable_sub int_integrable integrable_const) + apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const) done also have "... \ e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" by (simp add: content_Pair divide_simps) finally have 2: "norm (integral (cbox u v) (\x. integral (cbox w z) (\y. f (x,y))) - integral (cbox u v) (\x. integral (cbox w z) (\y. f (t1,t2)))) \ e * content (cbox (u,w) (v,z)) / content ?CBOX / 2" - by (simp only: integral_sub [symmetric] int_integrable integrable_const) + by (simp only: integral_diff [symmetric] int_integrable integrable_const) have norm_xx: "\x' = y'; norm(x - x') \ e/2; norm(y - y') \ e/2\ \ norm(x - y) \ e" for x::'c and y x' y' e using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves by (simp add: norm_minus_commute) diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Dec 07 16:44:26 2015 +0000 @@ -1,5 +1,5 @@ (* Title: HOL/Multivariate_Analysis/Path_Connected.thy - Author: Robert Himmelmann, TU Muenchen, and LC Paulson with material from HOL Light + Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light *) section \Continuous paths and path-connected sets\ diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 07 16:44:26 2015 +0000 @@ -2282,15 +2282,6 @@ lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)" by (simp add: filter_eq_iff) -text\Combining theorems for "eventually"\ - -lemma eventually_rev_mono: - "eventually P net \ (\x. P x \ Q x) \ eventually Q net" - using eventually_mono [of P Q] by fast - -lemma not_eventually: "(\x. \ P x ) \ \ trivial_limit net \ \ eventually (\x. P x) net" - by (simp add: eventually_False) - subsection \Limits\ @@ -2319,7 +2310,7 @@ by (auto simp add: tendsto_iff eventually_at_infinity) lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" - by (rule topological_tendstoI, auto elim: eventually_rev_mono) + by (rule topological_tendstoI, auto elim: eventually_mono') text\The expected monotonicity property.\ @@ -2998,7 +2989,7 @@ by fast qed -lemma closure_ball: +lemma closure_ball [simp]: fixes x :: "'a::real_normed_vector" shows "0 < e \ closure (ball x e) = cball x e" apply (rule equalityI) @@ -3016,7 +3007,7 @@ done (* In a trivial vector space, this fails for e = 0. *) -lemma interior_cball: +lemma interior_cball [simp]: fixes x :: "'a::{real_normed_vector, perfect_space}" shows "interior (cball x e) = ball x e" proof (cases "e \ 0") @@ -3108,12 +3099,12 @@ apply arith done -lemma cball_eq_empty: "cball x e = {} \ e < 0" +lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0" apply (simp add: set_eq_iff not_le) apply (metis zero_le_dist dist_self order_less_le_trans) done -lemma cball_empty: "e < 0 \ cball x e = {}" +lemma cball_empty [simp]: "e < 0 \ cball x e = {}" by (simp add: cball_eq_empty) lemma cball_eq_sing: @@ -3133,6 +3124,26 @@ shows "e = 0 \ cball x e = {x}" by (auto simp add: set_eq_iff) +lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e" + apply (cases "e \ 0") + apply (simp add: ball_empty divide_simps) + apply (rule subset_ball) + apply (simp add: divide_simps) + done + +lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e" + using ball_divide_subset one_le_numeral by blast + +lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e" + apply (cases "e < 0") + apply (simp add: divide_simps) + apply (rule subset_cball) + apply (metis divide_1 frac_le not_le order_refl zero_less_one) + done + +lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e" + using cball_divide_subset one_le_numeral by blast + subsection \Boundedness\ @@ -5723,7 +5734,7 @@ using \open U\ and \f x \ U\ unfolding tendsto_def by fast then have "eventually (\y. f y \ a) (at x within s)" - using \a \ U\ by (fast elim: eventually_mono [rotated]) + using \a \ U\ by (fast elim: eventually_mono') then show ?thesis using \f x \ a\ by (auto simp: dist_commute zero_less_dist_iff eventually_at) qed @@ -8206,9 +8217,8 @@ qed next assume ?rhs then show ?lhs - apply (auto simp: ball_def dist_norm ) + apply (auto simp: ball_def dist_norm) apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans) - using le_less_trans apply fastforce done qed @@ -8249,7 +8259,6 @@ assume ?rhs then show ?lhs apply (auto simp: ball_def dist_norm ) apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans) - using le_less_trans apply fastforce done qed @@ -8361,8 +8370,7 @@ using \?lhs\ ball_eq_empty cball_eq_empty apply blast+ done next - assume ?rhs then show ?lhs - by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff) + assume ?rhs then show ?lhs by auto qed lemma cball_eq_ball_iff: @@ -8377,8 +8385,7 @@ using \?lhs\ ball_eq_empty cball_eq_empty apply blast+ done next - assume ?rhs then show ?lhs - by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff) + assume ?rhs then show ?lhs using ball_eq_cball_iff by blast qed no_notation diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Multivariate_Analysis/Uniform_Limit.thy --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 16:44:26 2015 +0000 @@ -477,9 +477,7 @@ lemma uniform_limit_on_subset: "uniform_limit J f g F \ I \ J \ uniform_limit I f g F" - by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono) - - + by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono') lemma uniformly_convergent_add: "uniformly_convergent_on A f \ uniformly_convergent_on A g\ diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/NSA/HyperDef.thy Mon Dec 07 16:44:26 2015 +0000 @@ -231,7 +231,7 @@ text{*A few lemmas first*} -lemma lemma_omega_empty_singleton_disj: +lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} \ (\y. {n::nat. x = real n} = {y})" by force @@ -243,8 +243,7 @@ apply (simp add: omega_def star_of_def star_n_eq_iff) apply clarify apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE]) -apply (rule eventually_mono) -prefer 2 apply assumption +apply (erule eventually_mono') apply auto done diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/NSA/NSA.thy Mon Dec 07 16:44:26 2015 +0000 @@ -2106,7 +2106,7 @@ apply (simp add: omega_def) apply (rule FreeUltrafilterNat_HInfinite) apply clarify -apply (rule_tac u1 = "u-1" in eventually_mono [OF _ FreeUltrafilterNat_nat_gt_real]) +apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real]) apply auto done diff -r 4cf66f21b764 -r d2e62ae01cd8 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Mon Dec 07 10:38:04 2015 +0100 +++ b/src/HOL/Topological_Spaces.thy Mon Dec 07 16:44:26 2015 +0000 @@ -1758,7 +1758,7 @@ with \finite D\ have "eventually (\y. y \ \D) (nhds y)" by (simp add: eventually_ball_finite) with \s \ \D\ have "eventually (\y. y \ s) (nhds y)" - by (auto elim!: eventually_mono [rotated]) + by (auto elim!: eventually_mono') thus "\t. open t \ y \ t \ t \ - s" by (simp add: eventually_nhds subset_eq) qed