--- 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 \<open>Encoding (almost) everything into natural numbers\<close>
theory Countable
-imports Old_Datatype Rat Nat_Bijection
+imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
begin
subsection \<open>The class of countable types\<close>
--- 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 \<Rightarrow> 'a cset \<Rightarrow> bool"
is subset_eq parametric subset_transfer .
@@ -81,7 +81,7 @@
where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (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 \<subset> 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 \<open>\<open>cimage\<close>\<close>
lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> 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 \<open>bounded quantification\<close>
lemma cBex_simps [simp, no_atp]:
- "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
+ "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
"\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)"
- "\<And>P. cBex cempty P = False"
+ "\<And>P. cBex cempty P = False"
"\<And>a B P. cBex (cinsert a B) P = (P a \<or> cBex B P)"
"\<And>A P f. cBex (cimage f A) P = cBex A (\<lambda>x. P (f x))"
"\<And>A P. (\<not> cBex A P) = cBall A (\<lambda>x. \<not> P x)"
@@ -498,7 +498,7 @@
lemma cInt_parametric [transfer_rule]:
"bi_unique A \<Longrightarrow> (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
--- 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]
--- 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 \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
proof (elim BseqE, intro bdd_aboveI2)
fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
@@ -152,7 +152,7 @@
lemma Bseq_eventually_mono:
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
- shows "Bseq f"
+ shows "Bseq f"
proof -
from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> 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 \<Rightarrow> 'a :: real_normed_vector)"
shows "Bseq (\<lambda>x. f x + c)"
proof -
@@ -260,12 +260,12 @@
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
-lemma Bseq_mult:
+lemma Bseq_mult:
assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
shows "Bseq (\<lambda>x. f x * g x)"
proof -
- from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
+ from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
unfolding Bseq_def by blast
hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
thus ?thesis by (rule BseqI')
@@ -794,7 +794,7 @@
lemma tendsto_add_const_iff:
"((\<lambda>x. c + f x :: 'a :: real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> 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 "\<lambda>x. c + f x" "c + d"] by auto
@@ -1001,11 +1001,11 @@
lemma not_tendsto_and_filterlim_at_infinity:
assumes "F \<noteq> bot"
- assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F"
+ assumes "(f \<longlongrightarrow> (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 (\<lambda>x. dist (f x) c < 1/2) F" by simp
moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
have "eventually (\<lambda>x. norm (f x) \<ge> 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 \<Rightarrow> '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 "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" by (rule tendsto_norm)
hence "eventually (\<lambda>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 (\<lambda>x. norm (g x) \<ge> 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 (\<lambda>x. norm (f x + g x) \<ge> r) F"
@@ -1506,7 +1506,7 @@
lemma eventually_at2:
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> 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 "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f \<longlongrightarrow> l) (at x within S)"
+ assumes "(f \<longlongrightarrow> l) (at x within S)"
+ and "0 < d"
+ and "\<And>x'. \<lbrakk>x'\<in>S; 0 < dist x' x; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
shows "(g \<longlongrightarrow> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>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 \<longlongrightarrow> l) (at x within S)" by fact
qed
-lemma Lim_transform_at:
- assumes "0 < d"
- and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f \<longlongrightarrow> l) (at x)"
- shows "(g \<longlongrightarrow> l) (at x)"
- using _ assms(3)
-proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>x. f x = g x) (at x)"
- unfolding eventually_at2
- using assms(1,2) by auto
-qed
-
text\<open>Common case assuming being away from some crucial point like 0.\<close>
lemma Lim_transform_away_within:
@@ -1574,15 +1562,15 @@
text\<open>Alternatively, within an open set.\<close>
lemma Lim_transform_within_open:
- assumes "open S" and "a \<in> S"
- and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
- and "(f \<longlongrightarrow> l) (at a)"
- shows "(g \<longlongrightarrow> l) (at a)"
+ assumes "(f \<longlongrightarrow> l) (at a within T)"
+ and "open s" and "a \<in> s"
+ and "\<And>x. \<lbrakk>x\<in>s; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "(g \<longlongrightarrow> l) (at a within T)"
proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>x. f x = g x) (at a)"
+ show "eventually (\<lambda>x. f x = g x) (at a within T)"
unfolding eventually_at_topological
- using assms(1,2,3) by auto
- show "(f \<longlongrightarrow> l) (at a)" by fact
+ using assms by auto
+ show "(f \<longlongrightarrow> l) (at a within T)" by fact
qed
text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
@@ -1642,7 +1630,7 @@
fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" 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: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
+ show "eventually (\<lambda>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 "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> 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 \<Longrightarrow> convergent (\<lambda>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 (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
proof
assume "convergent (\<lambda>n. c + f n)"
@@ -1752,11 +1740,11 @@
from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
qed
-lemma convergent_add_const_right_iff:
+lemma convergent_add_const_right_iff:
"convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> 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 (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
@@ -1772,7 +1760,7 @@
shows "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
proof
assume "convergent (\<lambda>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"
--- 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<..<c} - s", THEN iffD1], simp_all)
apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)
+ apply (force elim!: differentiable_subset)+
done
next
case ge show ?diff_fg
apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
using x ge 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 = "{c<..<b} - t", THEN iffD1], simp_all)
apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)
+ apply (force elim!: differentiable_subset)+
done
qed
}
@@ -351,11 +351,11 @@
have "(\<lambda>x. if x \<le> 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<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> 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<..<b} - insert c (s \<union> t))
(\<lambda>x. vector_derivative (\<lambda>x. if x \<le> 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: "\<forall>x\<in>{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 \<in> {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) (\<lambda>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))
((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))"
@@ -481,7 +484,7 @@
and g12D: "\<forall>x\<in>{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 \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
- apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at)
+ apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>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) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
apply (rule continuous_on_eq [OF _ vector_derivative_at])
- apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at)
+ apply (rule_tac f="g2 o (\<lambda>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: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 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 "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z - 1/2\<bar>"]])
apply (simp_all add: dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>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: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 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 "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x - 1))" and d = "\<bar>z - 1/2\<bar>"]])
apply (simp_all add: dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>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: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 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 "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z-1)/2\<bar>"]])
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def])
using s1
@@ -850,7 +853,7 @@
have g2: "\<lbrakk>0 < z; z < 1; z \<notin> s2\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 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 "\<bar>z/2\<bar>" _ "(\<lambda>x. g2(2*x-1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x-1))" and d = "\<bar>z/2\<bar>"]])
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2-1" 2 _ g2, simplified o_def])
using s2
@@ -916,7 +919,7 @@
have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a) ` s \<Longrightarrow>
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" _ "(\<lambda>x. g(a+x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>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 "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
@@ -929,7 +932,7 @@
have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a + 1) ` s \<Longrightarrow>
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" _ "(\<lambda>x. g(a+x-1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>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 "\<lambda>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: \<open>d>0\<close> \<open>e>0\<close> 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 \<open>pe>0\<close> \<open>L>0\<close>
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: \<open>d>0\<close> \<open>e>0\<close> 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 "\<lambda>w::complex. (f w - f z)/(w - z)"])
+ have "continuous (at x within s) (\<lambda>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 "\<lambda>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 \<open>finite k\<close> by blast
have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \<gamma>"
@@ -5485,7 +5491,7 @@
done
show ?thes2
apply (simp add: DERIV_within_iff del: power_Suc)
- apply (rule Lim_transform_at [OF \<open>0 < d\<close> _ tendsto_mult_left [OF *]])
+ apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
apply (simp add: \<open>k \<noteq> 0\<close> **)
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 \<in> ball z r"
+ { fix w assume w: "w \<in> ball z r"
have intf: "(\<lambda>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 * \<i>) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2))
@@ -5595,7 +5601,7 @@
by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
qed
-lemma holomorphic_deriv [holomorphic_intros]:
+lemma holomorphic_deriv [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (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 \<Longrightarrow> (deriv ^^ n) f analytic_on s"
unfolding analytic_on_def using holomorphic_higher_deriv by blast
-lemma has_field_derivative_higher_deriv:
- "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
+lemma has_field_derivative_higher_deriv:
+ "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
\<Longrightarrow> ((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 \<in> s"
- with assms obtain e a where
+ with assms obtain e a where
"0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
\<Longrightarrow> contour_integral (linepath a b) f +
@@ -5661,14 +5667,14 @@
shows "f analytic_on s"
proof -
{ fix z assume "z \<in> s"
- with assms obtain t where
+ with assms obtain t where
"open t" and z: "z \<in> t" and contf: "continuous_on t f"
and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
\<Longrightarrow> 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 \<subseteq> t"
+ then obtain e where "e>0" and e: "ball z e \<subseteq> 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:
- "\<lbrakk>continuous_on s f; open s;
+ "\<lbrakk>continuous_on s f; open s;
\<And>a b c. convex hull {a,b,c} \<subseteq> s
\<longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
@@ -5701,7 +5707,7 @@
subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
-lemma higher_deriv_linear [simp]:
+lemma higher_deriv_linear [simp]:
"(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>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:
"\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (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 \<in> s"
shows "(deriv ^^ n) (\<lambda>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 \<in> s"
shows "(deriv ^^ n) (\<lambda>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 \<in> s"
shows "(deriv ^^ n) (\<lambda>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 \<in> s"
- shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
+ shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
(\<Sum>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 *: "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
"\<And>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 "\<lambda>w. (\<Sum>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: "\<And>w. w \<in> s \<Longrightarrow> 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: "(\<lambda>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) (\<lambda>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) (\<lambda>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} \<Longrightarrow> (deriv ^^ n) (\<lambda>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) (\<lambda>w. f w * g w) z =
+ shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
(\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
proof -
have "f analytic_on {z} \<and> 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 \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
have "f complex_differentiable at z"
proof (cases "z \<in> k")
case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
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: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
by blast
- obtain e where "e>0" and e: "ball z e \<subseteq> s"
+ obtain e where "e>0" and e: "ball z e \<subseteq> s"
using s \<open>z \<in> s\<close> 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 "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
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: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> 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 \<le> r" and wz_eq: "norm(w - z) = r - k"
+ obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> 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 *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
+ have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
if "0 < e" for e
proof -
@@ -6111,7 +6117,7 @@
also have "... < e * k"
using \<open>0 < B\<close> N by (simp add: divide_simps)
also have "... \<le> e * norm (u - w)"
- using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm)
+ using r kle \<open>0 < e\<close> 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 "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>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 "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
+ then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
by (rule Series.sums_divide)
- then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
+ then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
sums f w"
by (simp add: field_simps)
then show ?thesis
@@ -6155,7 +6161,7 @@
text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
-lemma Liouville_weak_0:
+lemma Liouville_weak_0:
assumes holf: "f holomorphic_on UNIV" and inf: "(f \<longlongrightarrow> 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 \<longlongrightarrow> l) at_infinity"
shows "f z = l"
using Liouville_weak_0 [of "\<lambda>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: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
obtains z where "f z = 0"
proof -
@@ -6210,7 +6216,7 @@
text\<open> In particular we get the Fundamental Theorem of Algebra.\<close>
-theorem fundamental_theorem_of_algebra:
+theorem fundamental_theorem_of_algebra:
fixes a :: "nat \<Rightarrow> complex"
assumes "a 0 = 0 \<or> (\<exists>i \<in> {1..n}. a i \<noteq> 0)"
obtains z where "(\<Sum>i\<le>n. a i * z^i) = 0"
@@ -6257,7 +6263,7 @@
if w: "w \<in> ball z r" for w
proof -
def d \<equiv> "(r - norm(w - z))"
- have "0 < d" "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
+ have "0 < d" "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
have dle: "\<And>u. cmod (z - u) = r \<Longrightarrow> d \<le> cmod (u - w)"
unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
have ev_int: "\<forall>\<^sub>F n in F. (\<lambda>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 (\<lambda>n. continuous_on (cball z r) (f n) \<and>
+ assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
(\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> 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"
"\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> 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': "\<And>x. x \<in> ball z r \<Longrightarrow> (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': "((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F" if w: "w \<in> ball z r" for w
proof -
- have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
- if cont_fn: "continuous_on (cball z r) (f n)"
+ have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
+ if cont_fn: "continuous_on (cball z r) (f n)"
and fnd: "\<And>w. w \<in> ball z r \<Longrightarrow> (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 * \<i>) * ?conint (\<lambda>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 * \<i>) * ?conint (\<lambda>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: \<open>0 < d\<close>)
apply (force simp add: dist_norm dle intro: less_le_trans)
done
- have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
+ have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
\<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
--- 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 "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
- by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
+ by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
--- 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 \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
+ apply (rule Lim_transform_within_open [where s= "-{z. z \<in> \<real> & 0 \<le> Re z}" and f = "\<lambda>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
--- 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 \<in> s" using assms(1,3) by auto
assume "\<not> ?thesis"
then obtain y where "y\<in>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 \<le> 1" and u: "u < e / dist x y"
using real_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
@@ -3401,8 +3399,8 @@
also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
by (auto simp: continuous_on_closed_vimage)
hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
- finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
-qed
+ finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
+qed
lemma interior_real_semiline':
fixes a :: real
@@ -3434,7 +3432,7 @@
lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
proof-
have "{a..b} = {a..} \<inter> {..b}" by auto
- also have "interior ... = {a<..} \<inter> {..<b}"
+ also have "interior ... = {a<..} \<inter> {..<b}"
by (simp add: interior_real_semiline interior_real_semiline')
also have "... = {a<..<b}" by auto
finally show ?thesis .
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Jan 06 16:17:50 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jan 07 17:40:55 2016 +0000
@@ -165,36 +165,23 @@
subsubsection \<open>Limit transformation for derivatives\<close>
lemma has_derivative_transform_within:
- assumes "0 < d"
+ assumes "(f has_derivative f') (at x within s)"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f has_derivative f') (at x within s)"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> 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 "\<forall>x'. dist x' x < d \<longrightarrow> 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 \<in> s"
- and "\<forall>y\<in>s. f y = g y"
- and "(f has_derivative f') (at x)"
+ and "\<And>x. x\<in>s \<Longrightarrow> 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 \<open>Differentiability\<close>
@@ -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 \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
- assumes "f differentiable (at x within s)"
+ and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> 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 "\<forall>x'. dist x' x < d \<longrightarrow> 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 \<open>Frechet derivative and Jacobian matrix\<close>
@@ -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 "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
- by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
+ by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>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 \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> 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 "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> 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 "\<forall>x'. dist x' x < d \<longrightarrow> 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 \<in> s"
- and "\<forall>y\<in>s. f y = g y"
- and "(f has_vector_derivative f') (at x)"
+ and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
shows "(g has_vector_derivative f') (at x)"
using assms
unfolding has_vector_derivative_def
--- 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 \<open>path h\<close>])
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
--- 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 \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
by (fact tendsto_within_open)
+lemma Lim_within_open_NO_MATCH:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ shows "a \<in> S \<Longrightarrow> NO_MATCH UNIV S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
+using tendsto_within_open by blast
+
lemma continuous_on_union:
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> 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': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> 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 \<in> S" "z \<noteq> 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 \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> 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 \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> 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 \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> 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 \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {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 "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding distrib_right using \<open>x\<noteq>y\<close>[unfolded dist_nz, unfolded dist_norm]
- by auto
+ unfolding distrib_right using \<open>x\<noteq>y\<close> by auto
also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
by (auto simp add: dist_norm)
finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
@@ -3019,8 +3023,8 @@
apply (simp only: dist_norm [symmetric])
apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
apply (rule mult_strict_right_mono)
- apply (simp add: k_def zero_less_dist_iff \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
- apply (simp add: zero_less_dist_iff \<open>x \<noteq> y\<close>)
+ apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
+ apply (simp add: \<open>x \<noteq> y\<close>)
done
then have "z \<in> ball x (dist x y)"
by simp
@@ -3055,14 +3059,14 @@
shows "interior (cball x e) = ball x e"
proof (cases "e \<ge> 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 \<in> 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 \<in> 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 \<in> ball x e"
using \<open>x = y \<close> by simp
next
@@ -5165,7 +5167,6 @@
assume "y \<in> f ` (ball x d \<inter> s)"
then have "y \<in> 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 \<in> T"
with \<open>?lhs\<close> obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
- unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
+ unfolding continuous_within tendsto_def eventually_at by auto
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) \<open>d>0\<close> by simp
then have "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
proof eventually_elim
case (elim n)
then show ?case
- using d x(1) \<open>f a \<in> T\<close> unfolding dist_nz[symmetric] by auto
+ using d x(1) \<open>f a \<in> T\<close> by auto
qed
}
then show ?rhs
@@ -5414,30 +5413,15 @@
lemma continuous_transform_within:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
- assumes "0 < d"
+ assumes "continuous (at x within s) f"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
- and "continuous (at x within s) f"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> 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 "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- using assms(3) by auto
- have "f x = g x"
- using assms(1,2,3) by auto
- then show "(f \<longlongrightarrow> 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 \<Rightarrow> 'b::topological_space"
- assumes "0 < d"
- and "\<forall>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 \<open>Structural rules for pointwise continuity\<close>
@@ -5762,7 +5746,7 @@
done
qed
-lemma isCont_indicator:
+lemma isCont_indicator:
fixes x :: "'a::t2_space"
shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
proof auto
@@ -6243,7 +6227,6 @@
shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
unfolding continuous_at
unfolding Lim_at
- unfolding dist_nz[symmetric]
unfolding dist_norm
apply auto
apply (erule_tac x=e in allE)
--- 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 \<noteq> 0" show ?thesis
- by (rule continuous_transform_at [where d = "abs x" and f = "\<lambda>x. sin x / x"])
+ by (rule continuous_transform_within [where d = "abs x" and f = "\<lambda>x. sin x / x"])
(auto simp add: dist_real_def \<open>x \<noteq> 0\<close>)
qed
--- 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 \<noteq> y \<longleftrightarrow> 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 \<Longrightarrow> 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) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> 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"
--- 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 \<open>Diagonal: identity over a set\<close>
@@ -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
--- 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 \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
+ apply (simp add: sums_def)
+ apply (subst LIMSEQ_Suc_iff [symmetric])
+ apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
+ done
+
subsection \<open>Infinite summability on topological monoids\<close>
lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
@@ -674,7 +680,7 @@
text\<open>Relations among convergence and absolute convergence for power series.\<close>
-lemma abel_lemma:
+lemma Abel_lemma:
fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
shows "summable (\<lambda>n. norm (a n) * r^n)"
@@ -792,10 +798,10 @@
by (rule Cauchy_product_sums [THEN sums_unique])
lemma summable_Cauchy_product:
- assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
+ assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
"summable (\<lambda>k. norm (b k))"
shows "summable (\<lambda>k. \<Sum>i\<le>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 \<open>Series on @{typ real}s\<close>
--- 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} \<subseteq> B ==> A \<subseteq> insert x B"
+lemma Diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
+ by blast
+
+lemma subset_Diff_insert: "A \<subseteq> B - (insert x C) \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
by blast
lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"