# HG changeset patch # User paulson # Date 1452188455 0 # Node ID 44841d07ef1d81a08c943ea30b65322f5f9c892c # Parent 969119292e25360defb6e70e14f0fba1d246ff72 revisions to limits and derivatives, plus new lemmas diff -r 969119292e25 -r 44841d07ef1d src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Library/Countable.thy Thu Jan 07 17:40:55 2016 +0000 @@ -7,7 +7,7 @@ section \Encoding (almost) everything into natural numbers\ theory Countable -imports Old_Datatype Rat Nat_Bijection +imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection begin subsection \The class of countable types\ diff -r 969119292e25 -r 44841d07ef1d src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Library/Countable_Set_Type.thy Thu Jan 07 17:40:55 2016 +0000 @@ -72,7 +72,7 @@ interpretation lifting_syntax . -lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp +lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp lift_definition less_eq_cset :: "'a cset \ 'a cset \ bool" is subset_eq parametric subset_transfer . @@ -81,7 +81,7 @@ where "xs < ys \ xs \ ys \ xs \ (ys::'a cset)" lemma less_cset_transfer[transfer_rule]: - assumes [transfer_rule]: "bi_unique A" + assumes [transfer_rule]: "bi_unique A" shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \ op <" unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover @@ -201,7 +201,7 @@ lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred] -lemmas cDiff_single_cinsert = diff_single_insert[Transfer.transferred] +lemmas cDiff_single_cinsert = Diff_single_insert[Transfer.transferred] lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred] lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred] @@ -389,14 +389,14 @@ subsubsection \\cimage\\ lemma subset_cimage_iff: "csubset_eq B (cimage f A) \ (\AA. csubset_eq AA A \ B = cimage f AA)" -by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) +by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) subsubsection \bounded quantification\ lemma cBex_simps [simp, no_atp]: - "\A P Q. cBex A (\x. P x \ Q) = (cBex A P \ Q)" + "\A P Q. cBex A (\x. P x \ Q) = (cBex A P \ Q)" "\A P Q. cBex A (\x. P \ Q x) = (P \ cBex A Q)" - "\P. cBex cempty P = False" + "\P. cBex cempty P = False" "\a B P. cBex (cinsert a B) P = (P a \ cBex B P)" "\A P f. cBex (cimage f A) P = cBex A (\x. P (f x))" "\A P. (\ cBex A P) = cBall A (\x. \ P x)" @@ -498,7 +498,7 @@ lemma cInt_parametric [transfer_rule]: "bi_unique A \ (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt" -unfolding rel_fun_def +unfolding rel_fun_def using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast diff -r 969119292e25 -r 44841d07ef1d src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Library/FSet.thy Thu Jan 07 17:40:55 2016 +0000 @@ -286,7 +286,7 @@ lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred] -lemmas fminus_single_finsert = diff_single_insert[Transfer.transferred] +lemmas fminus_single_finsert = Diff_single_insert[Transfer.transferred] lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred] lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred] diff -r 969119292e25 -r 44841d07ef1d src/HOL/Limits.thy --- a/src/HOL/Limits.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Limits.thy Thu Jan 07 17:40:55 2016 +0000 @@ -137,7 +137,7 @@ by (auto elim!: allE[of _ n]) qed -lemma Bseq_bdd_above': +lemma Bseq_bdd_above': "Bseq (X::nat \ 'a :: real_normed_vector) \ bdd_above (range (\n. norm (X n)))" proof (elim BseqE, intro bdd_aboveI2) fix K n assume "0 < K" "\n. norm (X n) \ K" then show "norm (X n) \ K" @@ -152,7 +152,7 @@ lemma Bseq_eventually_mono: assumes "eventually (\n. norm (f n) \ norm (g n)) sequentially" "Bseq g" - shows "Bseq f" + shows "Bseq f" proof - from assms(1) obtain N where N: "\n. n \ N \ norm (f n) \ norm (g n)" by (auto simp: eventually_at_top_linorder) @@ -162,7 +162,7 @@ apply (rule max.coboundedI2, rule Max.coboundedI, auto) [] apply (rule max.coboundedI1, force intro: order.trans[OF N K]) done - thus ?thesis by (blast intro: BseqI') + thus ?thesis by (blast intro: BseqI') qed lemma lemma_NBseq_def: @@ -243,7 +243,7 @@ lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X" by (simp add: Bseq_def) -lemma Bseq_add: +lemma Bseq_add: assumes "Bseq (f :: nat \ 'a :: real_normed_vector)" shows "Bseq (\x. f x + c)" proof - @@ -260,12 +260,12 @@ lemma Bseq_add_iff: "Bseq (\x. f x + c) \ Bseq (f :: nat \ 'a :: real_normed_vector)" using Bseq_add[of f c] Bseq_add[of "\x. f x + c" "-c"] by auto -lemma Bseq_mult: +lemma Bseq_mult: assumes "Bseq (f :: nat \ 'a :: real_normed_field)" assumes "Bseq (g :: nat \ 'a :: real_normed_field)" shows "Bseq (\x. f x * g x)" proof - - from assms obtain K1 K2 where K: "\x. norm (f x) \ K1" "K1 > 0" "\x. norm (g x) \ K2" "K2 > 0" + from assms obtain K1 K2 where K: "\x. norm (f x) \ K1" "K1 > 0" "\x. norm (g x) \ K2" "K2 > 0" unfolding Bseq_def by blast hence "\x. norm (f x * g x) \ K1 * K2" by (auto simp: norm_mult intro!: mult_mono) thus ?thesis by (rule BseqI') @@ -794,7 +794,7 @@ lemma tendsto_add_const_iff: "((\x. c + f x :: 'a :: real_normed_vector) \ c + d) F \ (f \ d) F" - using tendsto_add[OF tendsto_const[of c], of f d] + using tendsto_add[OF tendsto_const[of c], of f d] tendsto_add[OF tendsto_const[of "-c"], of "\x. c + f x" "c + d"] by auto @@ -1001,11 +1001,11 @@ lemma not_tendsto_and_filterlim_at_infinity: assumes "F \ bot" - assumes "(f \ (c :: 'a :: real_normed_vector)) F" + assumes "(f \ (c :: 'a :: real_normed_vector)) F" assumes "filterlim f at_infinity F" shows False proof - - from tendstoD[OF assms(2), of "1/2"] + from tendstoD[OF assms(2), of "1/2"] have "eventually (\x. dist (f x) c < 1/2) F" by simp moreover from filterlim_at_infinity[of "norm c" f F] assms(3) have "eventually (\x. norm (f x) \ norm c + 1) F" by simp @@ -1037,7 +1037,7 @@ thus ?thesis by eventually_elim auto qed -lemma tendsto_of_nat [tendsto_intros]: +lemma tendsto_of_nat [tendsto_intros]: "filterlim (of_nat :: nat \ 'a :: real_normed_algebra_1) at_infinity sequentially" proof (subst filterlim_at_infinity[OF order.refl], intro allI impI) fix r :: real assume r: "r > 0" @@ -1164,7 +1164,7 @@ fix r :: real assume r: "r > 0" from assms(1) have "((\x. norm (f x)) \ norm c) F" by (rule tendsto_norm) hence "eventually (\x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all - moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all + moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all with assms(2) have "eventually (\x. norm (g x) \ r + norm c + 1) F" unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all ultimately show "eventually (\x. norm (f x + g x) \ r) F" @@ -1506,7 +1506,7 @@ lemma eventually_at2: "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" - unfolding eventually_at dist_nz by auto + unfolding eventually_at by auto lemma Lim_transform: fixes a b :: "'a::real_normed_vector" @@ -1526,28 +1526,16 @@ done lemma Lim_transform_within: - assumes "0 < d" - and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f \ l) (at x within S)" + assumes "(f \ l) (at x within S)" + and "0 < d" + and "\x'. \x'\S; 0 < dist x' x; dist x' x < d\ \ f x' = g x'" shows "(g \ l) (at x within S)" proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at x within S)" - using assms(1,2) by (auto simp: dist_nz eventually_at) + using assms by (auto simp: eventually_at) show "(f \ l) (at x within S)" by fact qed -lemma Lim_transform_at: - assumes "0 < d" - and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - and "(f \ l) (at x)" - shows "(g \ l) (at x)" - using _ assms(3) -proof (rule Lim_transform_eventually) - show "eventually (\x. f x = g x) (at x)" - unfolding eventually_at2 - using assms(1,2) by auto -qed - text\Common case assuming being away from some crucial point like 0.\ lemma Lim_transform_away_within: @@ -1574,15 +1562,15 @@ text\Alternatively, within an open set.\ lemma Lim_transform_within_open: - assumes "open S" and "a \ S" - and "\x\S. x \ a \ f x = g x" - and "(f \ l) (at a)" - shows "(g \ l) (at a)" + assumes "(f \ l) (at a within T)" + and "open s" and "a \ s" + and "\x. \x\s; x \ a\ \ f x = g x" + shows "(g \ l) (at a within T)" proof (rule Lim_transform_eventually) - show "eventually (\x. f x = g x) (at a)" + show "eventually (\x. f x = g x) (at a within T)" unfolding eventually_at_topological - using assms(1,2,3) by auto - show "(f \ l) (at a)" by fact + using assms by auto + show "(f \ l) (at a within T)" by fact qed text\A congruence rule allowing us to transform limits assuming not at point.\ @@ -1642,7 +1630,7 @@ fix n :: nat assume n: "n \ nat \inverse e + 1\" have "inverse e < of_nat (nat \inverse e + 1\)" by linarith also note n - finally show "dist (1 / of_nat n :: 'a) 0 < e" using e + finally show "dist (1 / of_nat n :: 'a) 0 < e" using e by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide) qed @@ -1660,9 +1648,9 @@ lemma LIMSEQ_n_over_Suc_n: "(\n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \ 1" proof (rule Lim_transform_eventually) - show "eventually (\n. inverse (of_nat (Suc n) / of_nat n :: 'a) = + show "eventually (\n. inverse (of_nat (Suc n) / of_nat n :: 'a) = of_nat n / of_nat (Suc n)) sequentially" - using eventually_gt_at_top[of "0::nat"] + using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: field_simps del: of_nat_Suc) have "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \ inverse 1" by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all @@ -1738,11 +1726,11 @@ thus ?thesis by (auto simp: convergent_def) qed -lemma convergent_of_real: +lemma convergent_of_real: "convergent f \ convergent (\n. of_real (f n) :: 'a :: real_normed_algebra_1)" unfolding convergent_def by (blast intro!: tendsto_of_real) -lemma convergent_add_const_iff: +lemma convergent_add_const_iff: "convergent (\n. c + f n :: 'a :: real_normed_vector) \ convergent f" proof assume "convergent (\n. c + f n)" @@ -1752,11 +1740,11 @@ from convergent_add[OF convergent_const[of c] this] show "convergent (\n. c + f n)" by simp qed -lemma convergent_add_const_right_iff: +lemma convergent_add_const_right_iff: "convergent (\n. f n + c :: 'a :: real_normed_vector) \ convergent f" using convergent_add_const_iff[of c f] by (simp add: add_ac) -lemma convergent_diff_const_right_iff: +lemma convergent_diff_const_right_iff: "convergent (\n. f n - c :: 'a :: real_normed_vector) \ convergent f" using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac) @@ -1772,7 +1760,7 @@ shows "convergent (\n. c * f n :: 'a :: real_normed_field) \ convergent f" proof assume "convergent (\n. c * f n)" - from assms convergent_mult[OF this convergent_const[of "inverse c"]] + from assms convergent_mult[OF this convergent_const[of "inverse c"]] show "convergent f" by (simp add: field_simps) next assume "convergent f" diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Jan 07 17:40:55 2016 +0000 @@ -99,21 +99,21 @@ case le show ?diff_fg apply (rule differentiable_transform_within [where d = "dist x c" and f = f]) using x le st - apply (simp_all add: dist_real_def dist_nz [symmetric]) + apply (simp_all add: dist_real_def) apply (rule differentiable_at_withinI) apply (rule differentiable_within_open [where s = "{a<..x. if x \ c then f x else g x) differentiable at x" (is "?diff_fg") proof (cases x c rule: le_cases) case le show ?diff_fg - apply (rule differentiable_transform_at [of "dist x c" _ f]) + apply (rule differentiable_transform_within [where f=f and d = "dist x c"]) using x dist_real_def le st by (auto simp: C1_differentiable_on_eq) next case ge show ?diff_fg - apply (rule differentiable_transform_at [of "dist x c" _ g]) + apply (rule differentiable_transform_within [where f=g and d = "dist x c"]) using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq) qed } @@ -370,18 +370,20 @@ apply (rule continuous_on_eq [OF fcon]) apply (simp add:) apply (rule vector_derivative_at [symmetric]) - apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at) + apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within) apply (simp_all add: dist_norm vector_derivative_works [symmetric]) - using f_diff - by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1)) + apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1)) + apply auto + done moreover have "continuous_on ({c<..x. vector_derivative (\x. if x \ c then f x else g x) (at x))" apply (rule continuous_on_eq [OF gcon]) apply (simp add:) apply (rule vector_derivative_at [symmetric]) - apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at) + apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within) apply (simp_all add: dist_norm vector_derivative_works [symmetric]) - using g_diff - by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2)) + apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2)) + apply auto + done ultimately have "continuous_on ({a<.. t)) (\x. vector_derivative (\x. if x \ c then f x else g x) (at x))" apply (rule continuous_on_subset [OF continuous_on_open_Un], auto) @@ -435,7 +437,7 @@ and g12D: "\x\{0..1} - s. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) then have g1D: "g1 differentiable at x" if "x \ {0..1} - insert 1 (op * 2 ` s)" for x - apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at) + apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_within) using that apply (simp_all add: dist_real_def joinpaths_def) apply (rule differentiable_chain_at derivative_intros | force)+ @@ -450,9 +452,10 @@ using co12 by (rule continuous_on_subset) force then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\x. vector_derivative (g1 o op*2) (at x))" apply (rule continuous_on_eq [OF _ vector_derivative_at]) - apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at) + apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_within) apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric]) apply (force intro: g1D differentiable_chain_at) + apply auto done have "continuous_on ({0..1} - insert 1 (op * 2 ` s)) ((\x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))" @@ -481,7 +484,7 @@ and g12D: "\x\{0..1} - s. g1 +++ g2 differentiable at x" using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq) then have g2D: "g2 differentiable at x" if "x \ {0..1} - insert 0 ((\x. 2*x-1) ` s)" for x - apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\x. (x+1)/2)" in differentiable_transform_at) + apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\x. (x+1)/2)" in differentiable_transform_within) using that apply (simp_all add: dist_real_def joinpaths_def) apply (auto simp: dist_real_def joinpaths_def field_simps) @@ -496,7 +499,7 @@ using co12 by (rule continuous_on_subset) force then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\x. vector_derivative (g2 o (\x. 2*x-1)) (at x))" apply (rule continuous_on_eq [OF _ vector_derivative_at]) - apply (rule_tac f="g2 o (\x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at) + apply (rule_tac f="g2 o (\x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within) apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric] intro!: g2D differentiable_chain_at) done @@ -755,7 +758,7 @@ have g1: "\0 \ z; z*2 < 1; z*2 \ s1\ \ vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = 2 *\<^sub>R vector_derivative g1 (at (z*2))" for z - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z - 1/2\" _ "(\x. g1(2*x))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g1(2*x))" and d = "\z - 1/2\"]]) apply (simp_all add: dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. 2*x" 2 _ g1, simplified o_def]) apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) @@ -765,7 +768,7 @@ have g2: "\1 < z*2; z \ 1; z*2 - 1 \ s2\ \ vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) = 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z - 1/2\" _ "(\x. g2 (2*x - 1))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g2 (2*x - 1))" and d = "\z - 1/2\"]]) apply (simp_all add: dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. 2*x - 1" 2 _ g2, simplified o_def]) apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left) @@ -816,7 +819,7 @@ have g1: "\0 < z; z < 1; z \ s1\ \ vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) = 2 *\<^sub>R vector_derivative g1 (at z)" for z - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\(z-1)/2\" _ "(\x. g1(2*x))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g1(2*x))" and d = "\(z-1)/2\"]]) apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. x*2" 2 _ g1, simplified o_def]) using s1 @@ -850,7 +853,7 @@ have g2: "\0 < z; z < 1; z \ s2\ \ vector_derivative (\x. if x*2 \ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) = 2 *\<^sub>R vector_derivative g2 (at z)" for z - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\z/2\" _ "(\x. g2(2*x-1))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g2(2*x-1))" and d = "\z/2\"]]) apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. x*2-1" 2 _ g2, simplified o_def]) using s2 @@ -916,7 +919,7 @@ have "0 \ x \ x + a < 1 \ x \ (\x. x - a) ` s \ vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))" unfolding shiftpath_def - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1-a) x" _ "(\x. g(a+x))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g(a+x))" and d = "dist(1-a) x"]]) apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. x+a" 1 _ g, simplified o_def scaleR_one]) apply (intro derivative_eq_intros | simp)+ @@ -929,7 +932,7 @@ have "1 < x + a \ x \ 1 \ x \ (\x. x - a + 1) ` s \ vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))" unfolding shiftpath_def - apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1-a) x" _ "(\x. g(a+x-1))"]]) + apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\x. g(a+x-1))" and d = "dist (1-a) x"]]) apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm) apply (rule vector_diff_chain_at [of "\x. x+a-1" 1 _ g, simplified o_def scaleR_one]) apply (intro derivative_eq_intros | simp)+ @@ -986,12 +989,12 @@ vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})" apply (rule vector_derivative_at_within_ivl [OF has_vector_derivative_transform_within_open - [of "{0<..<1}-s" _ "(shiftpath (1 - a) (shiftpath a g))"]]) + [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]]) using s g assms x apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath vector_derivative_within_interior vector_derivative_works [symmetric]) - apply (rule Derivative.differentiable_transform_at [of "min x (1-x)", OF _ _ gx]) - apply (auto simp: dist_real_def shiftpath_shiftpath abs_if) + apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"]) + apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: split_if_asm) done } note vd = this have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))" @@ -4041,14 +4044,16 @@ using pi_ge_two e by (force simp: winding_number_valid_path p field_simps norm_divide norm_mult intro: less_le_trans) } note cmod_wn_diff = this - show ?thesis - apply (rule continuous_transform_at [of "min d e / 2" _ "winding_number p"]) - apply (auto simp: \d>0\ \e>0\ dist_norm wnwn simp del: less_divide_eq_numeral1) + then have "isCont (winding_number p) z" apply (simp add: continuous_at_eps_delta, clarify) apply (rule_tac x="min (pe/4) (e/2*pe^2/L/4)" in exI) using \pe>0\ \L>0\ apply (simp add: dist_norm cmod_wn_diff) done + then show ?thesis + apply (rule continuous_transform_within [where d = "min d e / 2"]) + apply (auto simp: \d>0\ \e>0\ dist_norm wnwn) + done qed corollary continuous_on_winding_number: @@ -4393,14 +4398,15 @@ done next case False - then have dxz: "dist x z > 0" using dist_nz by blast + then have dxz: "dist x z > 0" by auto have cf: "continuous (at x within s) f" using conf continuous_on_eq_continuous_within that by blast - show ?thesis - apply (rule continuous_transform_within [OF dxz that, of "\w::complex. (f w - f z)/(w - z)"]) + have "continuous (at x within s) (\w. (f w - f z) / (w - z))" + by (rule cf continuous_intros | simp add: False)+ + then show ?thesis + apply (rule continuous_transform_within [OF _ dxz that, of "\w::complex. (f w - f z)/(w - z)"]) apply (force simp: dist_commute) - apply (rule cf continuous_intros)+ - using False by auto + done qed have fink': "finite (insert z k)" using \finite k\ by blast have *: "((\w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \" @@ -5485,7 +5491,7 @@ done show ?thes2 apply (simp add: DERIV_within_iff del: power_Suc) - apply (rule Lim_transform_at [OF \0 < d\ _ tendsto_mult_left [OF *]]) + apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \0 < d\ ]) apply (simp add: \k \ 0\ **) done qed @@ -5566,7 +5572,7 @@ by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset) have holf_ball: "f holomorphic_on ball z r" using holf_cball using ball_subset_cball holomorphic_on_subset by blast - { fix w assume w: "w \ ball z r" + { fix w assume w: "w \ ball z r" have intf: "(\u. f u / (u - w)\<^sup>2) contour_integrable_on circlepath z r" by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball]) have fder': "(f has_field_derivative 1 / (2 * of_real pi * \) * contour_integral (circlepath z r) (\u. f u / (u - w)\<^sup>2)) @@ -5595,7 +5601,7 @@ by (simp add: holomorphic_on_open [OF \open s\] *) qed -lemma holomorphic_deriv [holomorphic_intros]: +lemma holomorphic_deriv [holomorphic_intros]: "\f holomorphic_on s; open s\ \ (deriv f) holomorphic_on s" by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def) @@ -5608,10 +5614,10 @@ lemma analytic_higher_deriv: "f analytic_on s \ (deriv ^^ n) f analytic_on s" unfolding analytic_on_def using holomorphic_higher_deriv by blast -lemma has_field_derivative_higher_deriv: - "\f holomorphic_on s; open s; x \ s\ +lemma has_field_derivative_higher_deriv: + "\f holomorphic_on s; open s; x \ s\ \ ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)" -by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply +by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def) @@ -5627,7 +5633,7 @@ shows "f analytic_on s" proof - { fix z assume "z \ s" - with assms obtain e a where + with assms obtain e a where "0 < e" and z: "z \ ball a e" and contf: "continuous_on (ball a e) f" and 0: "\b c. closed_segment b c \ ball a e \ contour_integral (linepath a b) f + @@ -5661,14 +5667,14 @@ shows "f analytic_on s" proof - { fix z assume "z \ s" - with assms obtain t where + with assms obtain t where "open t" and z: "z \ t" and contf: "continuous_on t f" and 0: "\a b c. convex hull {a,b,c} \ t \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" by force - then obtain e where "e>0" and e: "ball z e \ t" + then obtain e where "e>0" and e: "ball z e \ t" using open_contains_ball by blast have [simp]: "continuous_on (ball z e) f" using contf using continuous_on_subset e by blast @@ -5689,7 +5695,7 @@ qed proposition Morera_triangle: - "\continuous_on s f; open s; + "\continuous_on s f; open s; \a b c. convex hull {a,b,c} \ s \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + @@ -5701,7 +5707,7 @@ subsection\ Combining theorems for higher derivatives including Leibniz rule.\ -lemma higher_deriv_linear [simp]: +lemma higher_deriv_linear [simp]: "(deriv ^^ n) (\w. c*w) = (\z. if n = 0 then c*z else if n = 1 then c else 0)" by (induction n) (auto simp: deriv_const deriv_linear) @@ -5718,21 +5724,21 @@ "(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)" by (simp add: id_def) -lemma has_complex_derivative_funpow_1: +lemma has_complex_derivative_funpow_1: "\(f has_field_derivative 1) (at z); f z = z\ \ (f^^n has_field_derivative 1) (at z)" apply (induction n) apply auto apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one) by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral) -proposition higher_deriv_uminus: +proposition higher_deriv_uminus: assumes "f holomorphic_on s" "open s" and z: "z \ s" shows "(deriv ^^ n) (\w. -(f w)) z = - ((deriv ^^ n) f z)" using z proof (induction n arbitrary: z) case 0 then show ?case by simp next - case (Suc n z) + case (Suc n z) have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)" using Suc.prems assms has_field_derivative_higher_deriv by auto show ?case @@ -5744,7 +5750,7 @@ done qed -proposition higher_deriv_add: +proposition higher_deriv_add: fixes z::complex assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \ s" shows "(deriv ^^ n) (\w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z" @@ -5752,7 +5758,7 @@ proof (induction n arbitrary: z) case 0 then show ?case by simp next - case (Suc n z) + case (Suc n z) have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)" "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)" using Suc.prems assms has_field_derivative_higher_deriv by auto @@ -5765,7 +5771,7 @@ done qed -corollary higher_deriv_diff: +corollary higher_deriv_diff: fixes z::complex assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \ s" shows "(deriv ^^ n) (\w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z" @@ -5781,13 +5787,13 @@ proposition higher_deriv_mult: fixes z::complex assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \ s" - shows "(deriv ^^ n) (\w. f w * g w) z = + shows "(deriv ^^ n) (\w. f w * g w) z = (\i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)" using z proof (induction n arbitrary: z) case 0 then show ?case by simp next - case (Suc n z) + case (Suc n z) have *: "\n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)" "\n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)" using Suc.prems assms has_field_derivative_higher_deriv by auto @@ -5801,7 +5807,7 @@ show ?case apply (simp only: funpow.simps o_apply) apply (rule DERIV_imp_deriv) - apply (rule DERIV_transform_within_open + apply (rule DERIV_transform_within_open [of "\w. (\i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"]) apply (simp add: algebra_simps) apply (rule DERIV_cong [OF DERIV_setsum]) @@ -5817,7 +5823,7 @@ and fg: "\w. w \ s \ f w = g w" shows "(deriv ^^ i) f z = (deriv ^^ i) g z" using z -by (induction i arbitrary: z) +by (induction i arbitrary: z) (auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms) proposition higher_deriv_compose_linear: @@ -5829,7 +5835,7 @@ proof (induction n arbitrary: z) case 0 then show ?case by simp next - case (Suc n z) + case (Suc n z) have holo0: "f holomorphic_on op * u ` s" by (meson fg f holomorphic_on_subset image_subset_iff) have holo1: "(\w. f (u * w)) holomorphic_on s" @@ -5867,7 +5873,7 @@ by simp qed -lemma higher_deriv_add_at: +lemma higher_deriv_add_at: assumes "f analytic_on {z}" "g analytic_on {z}" shows "(deriv ^^ n) (\w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z" proof - @@ -5877,7 +5883,7 @@ by (auto simp: analytic_at_two) qed -lemma higher_deriv_diff_at: +lemma higher_deriv_diff_at: assumes "f analytic_on {z}" "g analytic_on {z}" shows "(deriv ^^ n) (\w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z" proof - @@ -5887,14 +5893,14 @@ by (auto simp: analytic_at_two) qed -lemma higher_deriv_uminus_at: +lemma higher_deriv_uminus_at: "f analytic_on {z} \ (deriv ^^ n) (\w. -(f w)) z = - ((deriv ^^ n) f z)" using higher_deriv_uminus by (auto simp: analytic_at) -lemma higher_deriv_mult_at: +lemma higher_deriv_mult_at: assumes "f analytic_on {z}" "g analytic_on {z}" - shows "(deriv ^^ n) (\w. f w * g w) z = + shows "(deriv ^^ n) (\w. f w * g w) z = (\i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)" proof - have "f analytic_on {z} \ g analytic_on {z}" @@ -5911,17 +5917,17 @@ assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k" shows "f holomorphic_on s" proof - - { fix z + { fix z assume "z \ s" and cdf: "\x. x\s - k \ f complex_differentiable at x" have "f complex_differentiable at z" proof (cases "z \ k") case False then show ?thesis by (blast intro: cdf \z \ s\) next case True - with finite_set_avoid [OF k, of z] + with finite_set_avoid [OF k, of z] obtain d where "d>0" and d: "\x. \x\k; x \ z\ \ d \ dist z x" by blast - obtain e where "e>0" and e: "ball z e \ s" + obtain e where "e>0" and e: "ball z e \ s" using s \z \ s\ by (force simp add: open_contains_ball) have fde: "continuous_on (ball z (min d e)) f" by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI) @@ -5930,7 +5936,7 @@ apply (rule Cauchy_theorem_triangle_cofinite [OF _ k]) apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset) apply (rule cdf) - apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset + apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset interior_mono interior_subset subset_hull) done then have "f holomorphic_on ball z (min d e)" @@ -5952,8 +5958,8 @@ shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf]) apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def) - using no_isolated_singularity [where s = "interior s"] - apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset + using no_isolated_singularity [where s = "interior s"] + apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset has_field_derivative_at_within holomorphic_on_def interior_subset open_interior) using assms apply auto @@ -6021,7 +6027,7 @@ by simp show ?thes1 using * using contour_integrable_on_def by blast - show ?thes2 + show ?thes2 unfolding contour_integral_unique [OF *] by (simp add: divide_simps) qed @@ -6065,13 +6071,13 @@ done obtain B where "0 < B" and B: "\u. u \ cball z r \ norm(f u) \ B" by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI) - obtain k where k: "0 < k" "k \ r" and wz_eq: "norm(w - z) = r - k" + obtain k where k: "0 < k" "k \ r" and wz_eq: "norm(w - z) = r - k" and kle: "\u. norm(u - z) = r \ k \ norm(u - w)" apply (rule_tac k = "r - dist z w" in that) using w apply (auto simp: dist_norm norm_minus_commute) by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute) - have *: "\\<^sub>F n in sequentially. \x\path_image (circlepath z r). + have *: "\\<^sub>F n in sequentially. \x\path_image (circlepath z r). norm ((\k0 < B\ N by (simp add: divide_simps) also have "... \ e * norm (u - w)" - using r kle \0 < e\ by (simp add: dist_commute dist_norm) + using r kle \0 < e\ by (simp add: dist_commute dist_norm) finally show ?thesis by (simp add: divide_simps norm_divide del: power_Suc) qed @@ -6140,10 +6146,10 @@ then have "(\k. contour_integral (circlepath z r) (\u. f u/(u - z)^(Suc k)) * (w - z)^k) sums (2 * of_real pi * ii * f w)" using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]]) - then have "(\k. contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc k) * (w - z)^k / (\ * (of_real pi * 2))) + then have "(\k. contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc k) * (w - z)^k / (\ * (of_real pi * 2))) sums ((2 * of_real pi * ii * f w) / (\ * (complex_of_real pi * 2)))" by (rule Series.sums_divide) - then have "(\n. (w - z) ^ n * contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc n) / (\ * (of_real pi * 2))) + then have "(\n. (w - z) ^ n * contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc n) / (\ * (of_real pi * 2))) sums f w" by (simp add: field_simps) then show ?thesis @@ -6155,7 +6161,7 @@ text\ These weak Liouville versions don't even need the derivative formula.\ -lemma Liouville_weak_0: +lemma Liouville_weak_0: assumes holf: "f holomorphic_on UNIV" and inf: "(f \ 0) at_infinity" shows "f z = 0" proof (rule ccontr) @@ -6181,14 +6187,14 @@ by (auto simp: norm_mult norm_divide divide_simps) qed -proposition Liouville_weak: +proposition Liouville_weak: assumes "f holomorphic_on UNIV" and "(f \ l) at_infinity" shows "f z = l" using Liouville_weak_0 [of "\z. f z - l"] by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero) -proposition Liouville_weak_inverse: +proposition Liouville_weak_inverse: assumes "f holomorphic_on UNIV" and unbounded: "\B. eventually (\x. norm (f x) \ B) at_infinity" obtains z where "f z = 0" proof - @@ -6210,7 +6216,7 @@ text\ In particular we get the Fundamental Theorem of Algebra.\ -theorem fundamental_theorem_of_algebra: +theorem fundamental_theorem_of_algebra: fixes a :: "nat \ complex" assumes "a 0 = 0 \ (\i \ {1..n}. a i \ 0)" obtains z where "(\i\n. a i * z^i) = 0" @@ -6257,7 +6263,7 @@ if w: "w \ ball z r" for w proof - def d \ "(r - norm(w - z))" - have "0 < d" "d \ r" using w by (auto simp: norm_minus_commute d_def dist_norm) + have "0 < d" "d \ r" using w by (auto simp: norm_minus_commute d_def dist_norm) have dle: "\u. cmod (z - u) = r \ d \ cmod (u - w)" unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute) have ev_int: "\\<^sub>F n in F. (\u. f n u / (u - w)) contour_integrable_on circlepath z r" @@ -6308,17 +6314,17 @@ proposition has_complex_derivative_uniform_limit: fixes z::complex - assumes cont: "eventually (\n. continuous_on (cball z r) (f n) \ + assumes cont: "eventually (\n. continuous_on (cball z r) (f n) \ (\w \ ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F" and lim: "\e. 0 < e \ eventually (\n. \x \ cball z r. norm(f n x - g x) < e) F" and F: "~ trivial_limit F" and "0 < r" obtains g' where - "continuous_on (cball z r) g" + "continuous_on (cball z r) g" "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) \ g' w) F" proof - let ?conint = "contour_integral (circlepath z r)" have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r" - by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; + by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; auto simp: holomorphic_on_open complex_differentiable_def)+ then obtain g' where g': "\x. x \ ball z r \ (g has_field_derivative g' x) (at x)" using DERIV_deriv_iff_has_field_derivative @@ -6327,8 +6333,8 @@ by (simp add: DERIV_imp_deriv) have tends_f'n_g': "((\n. f' n w) \ g' w) F" if w: "w \ ball z r" for w proof - - have eq_f': "?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \)" - if cont_fn: "continuous_on (cball z r) (f n)" + have eq_f': "?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \)" + if cont_fn: "continuous_on (cball z r) (f n)" and fnd: "\w. w \ ball z r \ (f n has_field_derivative f' n w) (at w)" for n proof - have hol_fn: "f n holomorphic_on ball z r" @@ -6336,7 +6342,7 @@ have "(f n has_field_derivative 1 / (2 * of_real pi * \) * ?conint (\u. f n u / (u - w)\<^sup>2)) (at w)" by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w]) then have f': "f' n w = 1 / (2 * of_real pi * \) * ?conint (\u. f n u / (u - w)\<^sup>2)" - using DERIV_unique [OF fnd] w by blast + using DERIV_unique [OF fnd] w by blast show ?thesis by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps) qed @@ -6358,7 +6364,7 @@ apply (simp add: \0 < d\) apply (force simp add: dist_norm dle intro: less_le_trans) done - have "((\n. contour_integral (circlepath z r) (\x. f n x / (x - w)\<^sup>2)) + have "((\n. contour_integral (circlepath z r) (\x. f n x / (x - w)\<^sup>2)) \ contour_integral (circlepath z r) ((\x. g x / (x - w)\<^sup>2))) F" by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \0 < r\]) then have tendsto_0: "((\n. 1 / (2 * of_real pi * \) * (?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2))) \ 0) F" diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Jan 07 17:40:55 2016 +0000 @@ -907,7 +907,7 @@ from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)" by (simp add: has_field_derivative_def s) have "((\x. \n. f n x) has_derivative op * (g' x)) (at x)" - by (rule has_derivative_transform_within_open[OF \open s\ x _ g']) + by (rule has_derivative_transform_within_open[OF g' \open s\ x]) (insert g, auto simp: sums_iff) thus "(\x. \n. f n x) complex_differentiable (at x)" unfolding differentiable_def by (auto simp: summable_def complex_differentiable_def has_field_derivative_def) diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Jan 07 17:40:55 2016 +0000 @@ -1345,9 +1345,9 @@ by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+ then show ?thesis apply (simp add: continuous_at) - apply (rule Lim_transform_within_open [of "-{z. z \ \ & 0 \ Re z}" _ "\z. Im(Ln(-z)) + pi"]) + apply (rule Lim_transform_within_open [where s= "-{z. z \ \ & 0 \ Re z}" and f = "\z. Im(Ln(-z)) + pi"]) + apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0]) apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge) - apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0]) done qed diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 17:40:55 2016 +0000 @@ -1368,9 +1368,7 @@ have "x \ s" using assms(1,3) by auto assume "\ ?thesis" then obtain y where "y\s" and y: "f x > f y" by auto - then have xy: "0 < dist x y" - by (auto simp add: dist_nz[symmetric]) - + then have xy: "0 < dist x y" by auto then obtain u where "0 < u" "u \ 1" and u: "u < e / dist x y" using real_lbound_gt_zero[of 1 "e / dist x y"] xy \e>0\ by auto then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \ (1-u) * f x + u * f y" @@ -3401,8 +3399,8 @@ also from assms(1) have "closed (g -` {a..} \ {c..d})" by (auto simp: continuous_on_closed_vimage) hence "closure (g -` {a..} \ {c..d}) = g -` {a..} \ {c..d}" by simp - finally show ?thesis using \x \ {c..d}\ by auto -qed + finally show ?thesis using \x \ {c..d}\ by auto +qed lemma interior_real_semiline': fixes a :: real @@ -3434,7 +3432,7 @@ lemma interior_atLeastAtMost_real: "interior {a..b} = {a<.. {..b}" by auto - also have "interior ... = {a<..} \ {.. {..Limit transformation for derivatives\ lemma has_derivative_transform_within: - assumes "0 < d" + assumes "(f has_derivative f') (at x within s)" + and "0 < d" and "x \ s" - and "\x'\s. dist x' x < d \ f x' = g x'" - and "(f has_derivative f') (at x within s)" + and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" shows "(g has_derivative f') (at x within s)" using assms - unfolding has_derivative_within - apply clarify - apply (rule Lim_transform_within, auto) - done - -lemma has_derivative_transform_at: - assumes "0 < d" - and "\x'. dist x' x < d \ f x' = g x'" - and "(f has_derivative f') (at x)" - shows "(g has_derivative f') (at x)" - using has_derivative_transform_within [of d x UNIV f g f'] assms - by simp + unfolding has_derivative_within + by (force simp add: intro: Lim_transform_within) lemma has_derivative_transform_within_open: - assumes "open s" + assumes "(f has_derivative f') (at x)" + and "open s" and "x \ s" - and "\y\s. f y = g y" - and "(f has_derivative f') (at x)" + and "\x. x\s \ f x = g x" shows "(g has_derivative f') (at x)" - using assms - unfolding has_derivative_at - apply clarify - apply (rule Lim_transform_within_open[OF assms(1,2)], auto) - done + using assms unfolding has_derivative_at + by (force simp add: intro: Lim_transform_within_open) subsection \Differentiability\ @@ -234,24 +221,13 @@ by (metis at_within_interior interior_open) lemma differentiable_transform_within: - assumes "0 < d" + assumes "f differentiable (at x within s)" + and "0 < d" and "x \ s" - and "\x'\s. dist x' x < d \ f x' = g x'" - assumes "f differentiable (at x within s)" + and "\x'. \x'\s; dist x' x < d\ \ f x' = g x'" shows "g differentiable (at x within s)" - using assms(4) - unfolding differentiable_def - by (auto intro!: has_derivative_transform_within[OF assms(1-3)]) - -lemma differentiable_transform_at: - assumes "0 < d" - and "\x'. dist x' x < d \ f x' = g x'" - and "f differentiable at x" - shows "g differentiable at x" - using assms(3) - unfolding differentiable_def - using has_derivative_transform_at[OF assms(1-2)] - by auto + using assms has_derivative_transform_within unfolding differentiable_def + by blast subsection \Frechet derivative and Jacobian matrix\ @@ -2263,7 +2239,7 @@ from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)" by (simp add: has_field_derivative_def s) have "((\x. \n. f n x) has_derivative op * (g' x)) (at x)" - by (rule has_derivative_transform_within_open[OF \open s\ x _ g']) + by (rule has_derivative_transform_within_open[OF g' \open s\ x]) (insert g, auto simp: sums_iff) thus "(\x. \n. f n x) differentiable (at x)" unfolding differentiable_def by (auto simp: summable_def differentiable_def has_field_derivative_def) @@ -2475,29 +2451,20 @@ qed lemma has_vector_derivative_transform_within: - assumes "0 < d" + assumes "(f has_vector_derivative f') (at x within s)" + and "0 < d" and "x \ s" - and "\x'\s. dist x' x < d \ f x' = g x'" - assumes "(f has_vector_derivative f') (at x within s)" - shows "(g has_vector_derivative f') (at x within s)" + and "\x'. \x'\s; dist x' x < d\ \ f x' = g x'" + shows "(g has_vector_derivative f') (at x within s)" using assms unfolding has_vector_derivative_def by (rule has_derivative_transform_within) -lemma has_vector_derivative_transform_at: - assumes "0 < d" - and "\x'. dist x' x < d \ f x' = g x'" - and "(f has_vector_derivative f') (at x)" - shows "(g has_vector_derivative f') (at x)" - using assms - unfolding has_vector_derivative_def - by (rule has_derivative_transform_at) - lemma has_vector_derivative_transform_within_open: - assumes "open s" + assumes "(f has_vector_derivative f') (at x)" + and "open s" and "x \ s" - and "\y\s. f y = g y" - and "(f has_vector_derivative f') (at x)" + and "\y. y\s \ f y = g y" shows "(g has_vector_derivative f') (at x)" using assms unfolding has_vector_derivative_def diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Jan 07 17:40:55 2016 +0000 @@ -843,7 +843,7 @@ apply (rule that [OF \path h\]) using assms h apply auto - apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) + apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) done qed diff -r 969119292e25 -r 44841d07ef1d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 07 17:40:55 2016 +0000 @@ -13,7 +13,7 @@ "~~/src/HOL/Library/FuncSet" Linear_Algebra Norm_Arith - + begin lemma image_affinity_interval: @@ -51,6 +51,11 @@ shows "a \ S \ open S \ (f \ l)(at a within S) \ (f \ l)(at a)" by (fact tendsto_within_open) +lemma Lim_within_open_NO_MATCH: + fixes f :: "'a::topological_space \ 'b::topological_space" + shows "a \ S \ NO_MATCH UNIV S \ open S \ (f \ l)(at a within S) \ (f \ l)(at a)" +using tendsto_within_open by blast + lemma continuous_on_union: "closed s \ closed t \ continuous_on s f \ continuous_on t f \ continuous_on (s \ t) f" by (fact continuous_on_closed_Un) @@ -1486,7 +1491,7 @@ case False let ?d = "min d (dist a x)" have dp: "?d > 0" - using False d(1) using dist_nz by auto + using False d(1) by auto from d have d': "\x\F. x \ a \ ?d \ dist a x" by auto with dp False show ?thesis @@ -1511,7 +1516,7 @@ by blast let ?m = "min (e/2) (dist x y) " from e2 y(2) have mp: "?m > 0" - by (simp add: dist_nz[symmetric]) + by simp from C[rule_format, OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m" by blast have th: "dist z y < e" using z y @@ -2312,11 +2317,11 @@ lemma Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_at_le dist_nz) + by (auto simp add: tendsto_iff eventually_at_le) lemma Lim_within: "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_at dist_nz) + by (auto simp add: tendsto_iff eventually_at) 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)" @@ -2665,9 +2670,9 @@ by (metis closure_contains_Inf closure_minimal subset_eq) lemma atLeastAtMost_subset_contains_Inf: - fixes A :: "real set" and a b :: real + fixes A :: "real set" and a b :: real shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" - by (rule closed_subset_contains_Inf) + by (rule closed_subset_contains_Inf) (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) lemma not_trivial_limit_within_ball: @@ -2940,8 +2945,7 @@ by (auto simp add: norm_minus_commute) also have "\ = \- norm (x - y) + d / 2\" unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]] - unfolding distrib_right using \x\y\[unfolded dist_nz, unfolded dist_norm] - by auto + unfolding distrib_right using \x\y\ by auto also have "\ \ e - d/2" using \d \ dist x y\ and \d>0\ and \?rhs\ by (auto simp add: dist_norm) finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \ ball x e" using \d>0\ @@ -3019,8 +3023,8 @@ apply (simp only: dist_norm [symmetric]) apply (subgoal_tac "\1 - k\ * dist x y < 1 * dist x y", simp) apply (rule mult_strict_right_mono) - apply (simp add: k_def zero_less_dist_iff \0 < r\ \x \ y\) - apply (simp add: zero_less_dist_iff \x \ y\) + apply (simp add: k_def \0 < r\ \x \ y\) + apply (simp add: \x \ y\) done then have "z \ ball x (dist x y)" by simp @@ -3055,14 +3059,14 @@ shows "interior (cball x e) = ball x e" proof (cases "e \ 0") case False note cs = this - from cs have "ball x e = {}" + from cs have null: "ball x e = {}" using ball_empty[of e x] by auto moreover { fix y assume "y \ cball x e" then have False - unfolding mem_cball using dist_nz[of x y] cs by auto + by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball) } then have "cball x e = {}" by auto then have "interior (cball x e) = {}" @@ -3088,9 +3092,7 @@ then have "y \ ball x e" proof (cases "x = y") case True - then have "e > 0" - using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] - by (auto simp add: dist_commute) + then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce then show "y \ ball x e" using \x = y \ by simp next @@ -5165,7 +5167,6 @@ assume "y \ f ` (ball x d \ s)" then have "y \ ball (f x) e" using d(2) - unfolding dist_nz[symmetric] apply (auto simp add: dist_commute) apply (erule_tac x=xa in ballE) apply auto @@ -5200,9 +5201,7 @@ apply (rule_tac x=d in exI) apply auto apply (erule_tac x=xa in allE) - apply (auto simp add: dist_commute dist_nz) - unfolding dist_nz[symmetric] - apply auto + apply (auto simp add: dist_commute) done next assume ?rhs @@ -5214,7 +5213,7 @@ apply (rule_tac x=d in exI) apply auto apply (erule_tac x="f xa" in allE) - apply (auto simp add: dist_commute dist_nz) + apply (auto simp add: dist_commute) done qed @@ -5285,14 +5284,14 @@ fix T :: "'b set" assume "open T" and "f a \ T" with \?lhs\ obtain d where "d>0" and d:"\x\s. 0 < dist x a \ dist x a < d \ f x \ T" - unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz) + unfolding continuous_within tendsto_def eventually_at by auto have "eventually (\n. dist (x n) a < d) sequentially" using x(2) \d>0\ by simp then have "eventually (\n. (f \ x) n \ T) sequentially" proof eventually_elim case (elim n) then show ?case - using d x(1) \f a \ T\ unfolding dist_nz[symmetric] by auto + using d x(1) \f a \ T\ by auto qed } then show ?rhs @@ -5414,30 +5413,15 @@ lemma continuous_transform_within: fixes f g :: "'a::metric_space \ 'b::topological_space" - assumes "0 < d" + assumes "continuous (at x within s) f" + and "0 < d" and "x \ s" - and "\x' \ s. dist x' x < d --> f x' = g x'" - and "continuous (at x within s) f" + and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" shows "continuous (at x within s) g" + using assms unfolding continuous_within -proof (rule Lim_transform_within) - show "0 < d" by fact - show "\x'\s. 0 < dist x' x \ dist x' x < d \ f x' = g x'" - using assms(3) by auto - have "f x = g x" - using assms(1,2,3) by auto - then show "(f \ g x) (at x within s)" - using assms(4) unfolding continuous_within by simp -qed - -lemma continuous_transform_at: - fixes f g :: "'a::metric_space \ 'b::topological_space" - assumes "0 < d" - and "\x'. dist x' x < d --> f x' = g x'" - and "continuous (at x) f" - shows "continuous (at x) g" - using continuous_transform_within [of d x UNIV f g] assms by simp - + by (force simp add: intro: Lim_transform_within) + subsubsection \Structural rules for pointwise continuity\ @@ -5762,7 +5746,7 @@ done qed -lemma isCont_indicator: +lemma isCont_indicator: fixes x :: "'a::t2_space" shows "isCont (indicator A :: 'a \ real) x = (x \ frontier A)" proof auto @@ -6243,7 +6227,6 @@ shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> \f x' - f x\ < e)" unfolding continuous_at unfolding Lim_at - unfolding dist_nz[symmetric] unfolding dist_norm apply auto apply (erule_tac x=e in allE) diff -r 969119292e25 -r 44841d07ef1d src/HOL/Probability/Sinc_Integral.thy --- a/src/HOL/Probability/Sinc_Integral.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Probability/Sinc_Integral.thy Thu Jan 07 17:40:55 2016 +0000 @@ -126,7 +126,7 @@ by (auto simp: isCont_def sinc_at_0) next assume "x \ 0" show ?thesis - by (rule continuous_transform_at [where d = "abs x" and f = "\x. sin x / x"]) + by (rule continuous_transform_within [where d = "abs x" and f = "\x. sin x / x"]) (auto simp add: dist_real_def \x \ 0\) qed diff -r 969119292e25 -r 44841d07ef1d src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Thu Jan 07 17:40:55 2016 +0000 @@ -1056,6 +1056,8 @@ shows "x \ y \ 0 < dist x y" by (simp add: zero_less_dist_iff) +declare dist_nz [symmetric, simp] + lemma dist_triangle_le: shows "dist x z + dist y z <= e \ dist x y <= e" by (rule order_trans [OF dist_triangle2]) @@ -1673,7 +1675,7 @@ lemma eventually_at: fixes a :: "'a :: metric_space" shows "eventually P (at a within S) \ (\d>0. \x\S. x \ a \ dist x a < d \ P x)" - unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz) + unfolding eventually_at_filter eventually_nhds_metric by auto lemma eventually_at_le: fixes a :: "'a::metric_space" diff -r 969119292e25 -r 44841d07ef1d src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Relation.thy Thu Jan 07 17:40:55 2016 +0000 @@ -515,6 +515,8 @@ lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r" by (simp add: total_on_def) +lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}" + by force subsubsection \Diagonal: identity over a set\ @@ -873,6 +875,12 @@ lemma snd_eq_Range: "snd ` R = Range R" by force +lemma range_fst [simp]: "range fst = UNIV" + by (auto simp: fst_eq_Domain) + +lemma range_snd [simp]: "range snd = UNIV" + by (auto simp: snd_eq_Range) + lemma Domain_empty [simp]: "Domain {} = {}" by auto diff -r 969119292e25 -r 44841d07ef1d src/HOL/Series.thy --- a/src/HOL/Series.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Series.thy Thu Jan 07 17:40:55 2016 +0000 @@ -30,6 +30,12 @@ where "suminf f = (THE s. f sums s)" +lemma sums_def': "f sums s \ (\n. \i = 0..n. f i) \ s" + apply (simp add: sums_def) + apply (subst LIMSEQ_Suc_iff [symmetric]) + apply (simp only: lessThan_Suc_atMost atLeast0AtMost) + done + subsection \Infinite summability on topological monoids\ lemma sums_subst[trans]: "f = g \ g sums z \ f sums z" @@ -674,7 +680,7 @@ text\Relations among convergence and absolute convergence for power series.\ -lemma abel_lemma: +lemma Abel_lemma: fixes a :: "nat \ 'a::real_normed_vector" assumes r: "0 \ r" and r0: "r < r0" and M: "\n. norm (a n) * r0^n \ M" shows "summable (\n. norm (a n) * r^n)" @@ -792,10 +798,10 @@ by (rule Cauchy_product_sums [THEN sums_unique]) lemma summable_Cauchy_product: - assumes "summable (\k. norm (a k :: 'a :: {real_normed_algebra,banach}))" + assumes "summable (\k. norm (a k :: 'a :: {real_normed_algebra,banach}))" "summable (\k. norm (b k))" shows "summable (\k. \i\k. a i * b (k - i))" - using Cauchy_product_sums[OF assms] by (simp add: sums_iff) + using Cauchy_product_sums[OF assms] by (simp add: sums_iff) subsection \Series on @{typ real}s\ diff -r 969119292e25 -r 44841d07ef1d src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Jan 06 16:17:50 2016 +0100 +++ b/src/HOL/Set.thy Thu Jan 07 17:40:55 2016 +0000 @@ -846,7 +846,10 @@ lemma singleton_conv2 [simp]: "{x. a = x} = {a}" by blast -lemma diff_single_insert: "A - {x} \ B ==> A \ insert x B" +lemma Diff_single_insert: "A - {x} \ B ==> A \ insert x B" + by blast + +lemma subset_Diff_insert: "A \ B - (insert x C) \ A \ B - C \ x \ A" by blast lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"