# HG changeset patch # User huffman # Date 1272994967 25200 # Node ID 0a5b7b818d65c375d25cc29cd0187fa67d41330d # Parent 1cc4ab4b7ff7ba740caecb5bc0661b73427739ac make (f -- a --> x) an abbreviation for (f ---> x) (at a) diff -r 1cc4ab4b7ff7 -r 0a5b7b818d65 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Tue May 04 10:06:05 2010 -0700 +++ b/src/HOL/Library/Product_Vector.thy Tue May 04 10:42:47 2010 -0700 @@ -312,18 +312,6 @@ (simp add: subsetD [OF `A \ B \ S`]) qed -lemma LIM_fst: "f -- x --> a \ (\x. fst (f x)) -- x --> fst a" -unfolding LIM_conv_tendsto by (rule tendsto_fst) - -lemma LIM_snd: "f -- x --> a \ (\x. snd (f x)) -- x --> snd a" -unfolding LIM_conv_tendsto by (rule tendsto_snd) - -lemma LIM_Pair: - assumes "f -- x --> a" and "g -- x --> b" - shows "(\x. (f x, g x)) -- x --> (a, b)" -using assms unfolding LIM_conv_tendsto -by (rule tendsto_Pair) - lemma Cauchy_fst: "Cauchy X \ Cauchy (\n. fst (X n))" unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) @@ -348,7 +336,7 @@ lemma isCont_Pair [simp]: "\isCont f x; isCont g x\ \ isCont (\x. (f x, g x)) x" - unfolding isCont_def by (rule LIM_Pair) + unfolding isCont_def by (rule tendsto_Pair) subsection {* Product is a complete metric space *} diff -r 1cc4ab4b7ff7 -r 0a5b7b818d65 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Tue May 04 10:06:05 2010 -0700 +++ b/src/HOL/Lim.thy Tue May 04 10:42:47 2010 -0700 @@ -12,12 +12,10 @@ text{*Standard Definitions*} -definition +abbreviation LIM :: "['a::metric_space \ 'b::metric_space, 'a, 'b] \ bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where - [code del]: "f -- a --> L = - (\r > 0. \s > 0. \x. x \ a & dist x a < s - --> dist (f x) L < r)" + "f -- a --> L \ (f ---> L) (at a)" definition isCont :: "['a::metric_space \ 'b::metric_space, 'a] \ bool" where @@ -29,8 +27,10 @@ subsection {* Limits of Functions *} -lemma LIM_conv_tendsto: "(f -- a --> L) \ (f ---> L) (at a)" -unfolding LIM_def tendsto_iff eventually_at .. +lemma LIM_def: "f -- a --> L = + (\r > 0. \s > 0. \x. x \ a & dist x a < s + --> dist (f x) L < r)" +unfolding tendsto_iff eventually_at .. lemma metric_LIM_I: "(\r. 0 < r \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r) @@ -82,7 +82,7 @@ by (drule_tac k="- a" in LIM_offset, simp) lemma LIM_const [simp]: "(%x. k) -- x --> k" -by (simp add: LIM_def) +by (rule tendsto_const) lemma LIM_cong_limit: "\ f -- x --> L ; K = L \ \ f -- x --> K" by simp @@ -90,22 +90,17 @@ fixes f g :: "'a::metric_space \ 'b::real_normed_vector" assumes f: "f -- a --> L" and g: "g -- a --> M" shows "(\x. f x + g x) -- a --> (L + M)" -using assms unfolding LIM_conv_tendsto by (rule tendsto_add) +using assms by (rule tendsto_add) lemma LIM_add_zero: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" shows "\f -- a --> 0; g -- a --> 0\ \ (\x. f x + g x) -- a --> 0" by (drule (1) LIM_add, simp) -lemma minus_diff_minus: - fixes a b :: "'a::ab_group_add" - shows "(- a) - (- b) = - (a - b)" -by simp - lemma LIM_minus: fixes f :: "'a::metric_space \ 'b::real_normed_vector" shows "f -- a --> L \ (\x. - f x) -- a --> - L" -unfolding LIM_conv_tendsto by (rule tendsto_minus) +by (rule tendsto_minus) (* TODO: delete *) lemma LIM_add_minus: @@ -116,7 +111,7 @@ lemma LIM_diff: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" shows "\f -- x --> l; g -- x --> m\ \ (\x. f x - g x) -- x --> l - m" -unfolding LIM_conv_tendsto by (rule tendsto_diff) +by (rule tendsto_diff) lemma LIM_zero: fixes f :: "'a::metric_space \ 'b::real_normed_vector" @@ -156,7 +151,7 @@ lemma LIM_norm: fixes f :: "'a::metric_space \ 'b::real_normed_vector" shows "f -- a --> l \ (\x. norm (f x)) -- a --> norm l" -unfolding LIM_conv_tendsto by (rule tendsto_norm) +by (rule tendsto_norm) lemma LIM_norm_zero: fixes f :: "'a::metric_space \ 'b::real_normed_vector" @@ -221,7 +216,7 @@ done lemma LIM_ident [simp]: "(\x. x) -- a --> a" -by (auto simp add: LIM_def) +by (rule tendsto_ident_at) text{*Limits are equal for functions equal except at limit point*} lemma LIM_equal: @@ -349,7 +344,7 @@ lemma (in bounded_linear) LIM: "g -- a --> l \ (\x. f (g x)) -- a --> f l" -unfolding LIM_conv_tendsto by (rule tendsto) +by (rule tendsto) lemma (in bounded_linear) cont: "f -- a --> f a" by (rule LIM [OF LIM_ident]) @@ -362,7 +357,7 @@ lemma (in bounded_bilinear) LIM: "\f -- a --> L; g -- a --> M\ \ (\x. f x ** g x) -- a --> L ** M" -unfolding LIM_conv_tendsto by (rule tendsto) +by (rule tendsto) lemma (in bounded_bilinear) LIM_prod_zero: fixes a :: "'d::metric_space" @@ -402,7 +397,6 @@ lemma LIM_inverse: fixes L :: "'a::real_normed_div_algebra" shows "\f -- a --> L; L \ 0\ \ (\x. inverse (f x)) -- a --> inverse L" -unfolding LIM_conv_tendsto by (rule tendsto_inverse) lemma LIM_inverse_fun: diff -r 1cc4ab4b7ff7 -r 0a5b7b818d65 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue May 04 10:06:05 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue May 04 10:42:47 2010 -0700 @@ -313,10 +313,6 @@ end -lemma LIM_Cart_nth: - "(f -- x --> y) \ (\x. f x $ i) -- x --> y $ i" -unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth) - lemma Cauchy_Cart_nth: "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)" unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])