make (f -- a --> x) an abbreviation for (f ---> x) (at a)
authorhuffman
Tue May 04 10:42:47 2010 -0700 (2010-05-04)
changeset 366610a5b7b818d65
parent 36660 1cc4ab4b7ff7
child 36662 621122eeb138
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
src/HOL/Library/Product_Vector.thy
src/HOL/Lim.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue May 04 10:06:05 2010 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue May 04 10:42:47 2010 -0700
     1.3 @@ -312,18 +312,6 @@
     1.4         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
     1.5  qed
     1.6  
     1.7 -lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
     1.8 -unfolding LIM_conv_tendsto by (rule tendsto_fst)
     1.9 -
    1.10 -lemma LIM_snd: "f -- x --> a \<Longrightarrow> (\<lambda>x. snd (f x)) -- x --> snd a"
    1.11 -unfolding LIM_conv_tendsto by (rule tendsto_snd)
    1.12 -
    1.13 -lemma LIM_Pair:
    1.14 -  assumes "f -- x --> a" and "g -- x --> b"
    1.15 -  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
    1.16 -using assms unfolding LIM_conv_tendsto
    1.17 -by (rule tendsto_Pair)
    1.18 -
    1.19  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
    1.20  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
    1.21  
    1.22 @@ -348,7 +336,7 @@
    1.23  
    1.24  lemma isCont_Pair [simp]:
    1.25    "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
    1.26 -  unfolding isCont_def by (rule LIM_Pair)
    1.27 +  unfolding isCont_def by (rule tendsto_Pair)
    1.28  
    1.29  subsection {* Product is a complete metric space *}
    1.30  
     2.1 --- a/src/HOL/Lim.thy	Tue May 04 10:06:05 2010 -0700
     2.2 +++ b/src/HOL/Lim.thy	Tue May 04 10:42:47 2010 -0700
     2.3 @@ -12,12 +12,10 @@
     2.4  
     2.5  text{*Standard Definitions*}
     2.6  
     2.7 -definition
     2.8 +abbreviation
     2.9    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
    2.10          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    2.11 -  [code del]: "f -- a --> L =
    2.12 -     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    2.13 -        --> dist (f x) L < r)"
    2.14 +  "f -- a --> L \<equiv> (f ---> L) (at a)"
    2.15  
    2.16  definition
    2.17    isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
    2.18 @@ -29,8 +27,10 @@
    2.19  
    2.20  subsection {* Limits of Functions *}
    2.21  
    2.22 -lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
    2.23 -unfolding LIM_def tendsto_iff eventually_at ..
    2.24 +lemma LIM_def: "f -- a --> L =
    2.25 +     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    2.26 +        --> dist (f x) L < r)"
    2.27 +unfolding tendsto_iff eventually_at ..
    2.28  
    2.29  lemma metric_LIM_I:
    2.30    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    2.31 @@ -82,7 +82,7 @@
    2.32  by (drule_tac k="- a" in LIM_offset, simp)
    2.33  
    2.34  lemma LIM_const [simp]: "(%x. k) -- x --> k"
    2.35 -by (simp add: LIM_def)
    2.36 +by (rule tendsto_const)
    2.37  
    2.38  lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
    2.39  
    2.40 @@ -90,22 +90,17 @@
    2.41    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.42    assumes f: "f -- a --> L" and g: "g -- a --> M"
    2.43    shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
    2.44 -using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
    2.45 +using assms by (rule tendsto_add)
    2.46  
    2.47  lemma LIM_add_zero:
    2.48    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.49    shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
    2.50  by (drule (1) LIM_add, simp)
    2.51  
    2.52 -lemma minus_diff_minus:
    2.53 -  fixes a b :: "'a::ab_group_add"
    2.54 -  shows "(- a) - (- b) = - (a - b)"
    2.55 -by simp
    2.56 -
    2.57  lemma LIM_minus:
    2.58    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.59    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
    2.60 -unfolding LIM_conv_tendsto by (rule tendsto_minus)
    2.61 +by (rule tendsto_minus)
    2.62  
    2.63  (* TODO: delete *)
    2.64  lemma LIM_add_minus:
    2.65 @@ -116,7 +111,7 @@
    2.66  lemma LIM_diff:
    2.67    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.68    shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
    2.69 -unfolding LIM_conv_tendsto by (rule tendsto_diff)
    2.70 +by (rule tendsto_diff)
    2.71  
    2.72  lemma LIM_zero:
    2.73    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.74 @@ -156,7 +151,7 @@
    2.75  lemma LIM_norm:
    2.76    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.77    shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
    2.78 -unfolding LIM_conv_tendsto by (rule tendsto_norm)
    2.79 +by (rule tendsto_norm)
    2.80  
    2.81  lemma LIM_norm_zero:
    2.82    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    2.83 @@ -221,7 +216,7 @@
    2.84  done
    2.85  
    2.86  lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
    2.87 -by (auto simp add: LIM_def)
    2.88 +by (rule tendsto_ident_at)
    2.89  
    2.90  text{*Limits are equal for functions equal except at limit point*}
    2.91  lemma LIM_equal:
    2.92 @@ -349,7 +344,7 @@
    2.93  
    2.94  lemma (in bounded_linear) LIM:
    2.95    "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
    2.96 -unfolding LIM_conv_tendsto by (rule tendsto)
    2.97 +by (rule tendsto)
    2.98  
    2.99  lemma (in bounded_linear) cont: "f -- a --> f a"
   2.100  by (rule LIM [OF LIM_ident])
   2.101 @@ -362,7 +357,7 @@
   2.102  
   2.103  lemma (in bounded_bilinear) LIM:
   2.104    "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
   2.105 -unfolding LIM_conv_tendsto by (rule tendsto)
   2.106 +by (rule tendsto)
   2.107  
   2.108  lemma (in bounded_bilinear) LIM_prod_zero:
   2.109    fixes a :: "'d::metric_space"
   2.110 @@ -402,7 +397,6 @@
   2.111  lemma LIM_inverse:
   2.112    fixes L :: "'a::real_normed_div_algebra"
   2.113    shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
   2.114 -unfolding LIM_conv_tendsto
   2.115  by (rule tendsto_inverse)
   2.116  
   2.117  lemma LIM_inverse_fun:
     3.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue May 04 10:06:05 2010 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue May 04 10:42:47 2010 -0700
     3.3 @@ -313,10 +313,6 @@
     3.4  
     3.5  end
     3.6  
     3.7 -lemma LIM_Cart_nth:
     3.8 -  "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i"
     3.9 -unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
    3.10 -
    3.11  lemma Cauchy_Cart_nth:
    3.12    "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
    3.13  unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])