src/HOL/NSA/HLim.thy
changeset 27468 0783dd1dc13d
child 28562 4e74209f113e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NSA/HLim.thy	Thu Jul 03 17:47:22 2008 +0200
     1.3 @@ -0,0 +1,334 @@
     1.4 +(*  Title       : HLim.thy
     1.5 +    ID          : $Id$
     1.6 +    Author      : Jacques D. Fleuriot
     1.7 +    Copyright   : 1998  University of Cambridge
     1.8 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.9 +*)
    1.10 +
    1.11 +header{* Limits and Continuity (Nonstandard) *}
    1.12 +
    1.13 +theory HLim
    1.14 +imports Star Lim
    1.15 +begin
    1.16 +
    1.17 +text{*Nonstandard Definitions*}
    1.18 +
    1.19 +definition
    1.20 +  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    1.21 +            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
    1.22 +  [code func del]: "f -- a --NS> L =
    1.23 +    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    1.24 +
    1.25 +definition
    1.26 +  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    1.27 +    --{*NS definition dispenses with limit notions*}
    1.28 +  [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
    1.29 +         ( *f* f) y @= star_of (f a))"
    1.30 +
    1.31 +definition
    1.32 +  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    1.33 +  [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    1.34 +
    1.35 +
    1.36 +subsection {* Limits of Functions *}
    1.37 +
    1.38 +lemma NSLIM_I:
    1.39 +  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
    1.40 +   \<Longrightarrow> f -- a --NS> L"
    1.41 +by (simp add: NSLIM_def)
    1.42 +
    1.43 +lemma NSLIM_D:
    1.44 +  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
    1.45 +   \<Longrightarrow> starfun f x \<approx> star_of L"
    1.46 +by (simp add: NSLIM_def)
    1.47 +
    1.48 +text{*Proving properties of limits using nonstandard definition.
    1.49 +      The properties hold for standard limits as well!*}
    1.50 +
    1.51 +lemma NSLIM_mult:
    1.52 +  fixes l m :: "'a::real_normed_algebra"
    1.53 +  shows "[| f -- x --NS> l; g -- x --NS> m |]
    1.54 +      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
    1.55 +by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
    1.56 +
    1.57 +lemma starfun_scaleR [simp]:
    1.58 +  "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
    1.59 +by transfer (rule refl)
    1.60 +
    1.61 +lemma NSLIM_scaleR:
    1.62 +  "[| f -- x --NS> l; g -- x --NS> m |]
    1.63 +      ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
    1.64 +by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
    1.65 +
    1.66 +lemma NSLIM_add:
    1.67 +     "[| f -- x --NS> l; g -- x --NS> m |]
    1.68 +      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
    1.69 +by (auto simp add: NSLIM_def intro!: approx_add)
    1.70 +
    1.71 +lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
    1.72 +by (simp add: NSLIM_def)
    1.73 +
    1.74 +lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
    1.75 +by (simp add: NSLIM_def)
    1.76 +
    1.77 +lemma NSLIM_diff:
    1.78 +  "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
    1.79 +by (simp only: diff_def NSLIM_add NSLIM_minus)
    1.80 +
    1.81 +lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
    1.82 +by (simp only: NSLIM_add NSLIM_minus)
    1.83 +
    1.84 +lemma NSLIM_inverse:
    1.85 +  fixes L :: "'a::real_normed_div_algebra"
    1.86 +  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
    1.87 +      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
    1.88 +apply (simp add: NSLIM_def, clarify)
    1.89 +apply (drule spec)
    1.90 +apply (auto simp add: star_of_approx_inverse)
    1.91 +done
    1.92 +
    1.93 +lemma NSLIM_zero:
    1.94 +  assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
    1.95 +proof -
    1.96 +  have "(\<lambda>x. f x - l) -- a --NS> l - l"
    1.97 +    by (rule NSLIM_diff [OF f NSLIM_const])
    1.98 +  thus ?thesis by simp
    1.99 +qed
   1.100 +
   1.101 +lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
   1.102 +apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   1.103 +apply (auto simp add: diff_minus add_assoc)
   1.104 +done
   1.105 +
   1.106 +lemma NSLIM_const_not_eq:
   1.107 +  fixes a :: "'a::real_normed_algebra_1"
   1.108 +  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
   1.109 +apply (simp add: NSLIM_def)
   1.110 +apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
   1.111 +apply (simp add: hypreal_epsilon_not_zero approx_def)
   1.112 +done
   1.113 +
   1.114 +lemma NSLIM_not_zero:
   1.115 +  fixes a :: "'a::real_normed_algebra_1"
   1.116 +  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
   1.117 +by (rule NSLIM_const_not_eq)
   1.118 +
   1.119 +lemma NSLIM_const_eq:
   1.120 +  fixes a :: "'a::real_normed_algebra_1"
   1.121 +  shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
   1.122 +apply (rule ccontr)
   1.123 +apply (blast dest: NSLIM_const_not_eq)
   1.124 +done
   1.125 +
   1.126 +lemma NSLIM_unique:
   1.127 +  fixes a :: "'a::real_normed_algebra_1"
   1.128 +  shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
   1.129 +apply (drule (1) NSLIM_diff)
   1.130 +apply (auto dest!: NSLIM_const_eq)
   1.131 +done
   1.132 +
   1.133 +lemma NSLIM_mult_zero:
   1.134 +  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   1.135 +  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   1.136 +by (drule NSLIM_mult, auto)
   1.137 +
   1.138 +lemma NSLIM_self: "(%x. x) -- a --NS> a"
   1.139 +by (simp add: NSLIM_def)
   1.140 +
   1.141 +subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
   1.142 +
   1.143 +lemma LIM_NSLIM:
   1.144 +  assumes f: "f -- a --> L" shows "f -- a --NS> L"
   1.145 +proof (rule NSLIM_I)
   1.146 +  fix x
   1.147 +  assume neq: "x \<noteq> star_of a"
   1.148 +  assume approx: "x \<approx> star_of a"
   1.149 +  have "starfun f x - star_of L \<in> Infinitesimal"
   1.150 +  proof (rule InfinitesimalI2)
   1.151 +    fix r::real assume r: "0 < r"
   1.152 +    from LIM_D [OF f r]
   1.153 +    obtain s where s: "0 < s" and
   1.154 +      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
   1.155 +      by fast
   1.156 +    from less_r have less_r':
   1.157 +       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
   1.158 +        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   1.159 +      by transfer
   1.160 +    from approx have "x - star_of a \<in> Infinitesimal"
   1.161 +      by (unfold approx_def)
   1.162 +    hence "hnorm (x - star_of a) < star_of s"
   1.163 +      using s by (rule InfinitesimalD2)
   1.164 +    with neq show "hnorm (starfun f x - star_of L) < star_of r"
   1.165 +      by (rule less_r')
   1.166 +  qed
   1.167 +  thus "starfun f x \<approx> star_of L"
   1.168 +    by (unfold approx_def)
   1.169 +qed
   1.170 +
   1.171 +lemma NSLIM_LIM:
   1.172 +  assumes f: "f -- a --NS> L" shows "f -- a --> L"
   1.173 +proof (rule LIM_I)
   1.174 +  fix r::real assume r: "0 < r"
   1.175 +  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
   1.176 +        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   1.177 +  proof (rule exI, safe)
   1.178 +    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   1.179 +  next
   1.180 +    fix x assume neq: "x \<noteq> star_of a"
   1.181 +    assume "hnorm (x - star_of a) < epsilon"
   1.182 +    with Infinitesimal_epsilon
   1.183 +    have "x - star_of a \<in> Infinitesimal"
   1.184 +      by (rule hnorm_less_Infinitesimal)
   1.185 +    hence "x \<approx> star_of a"
   1.186 +      by (unfold approx_def)
   1.187 +    with f neq have "starfun f x \<approx> star_of L"
   1.188 +      by (rule NSLIM_D)
   1.189 +    hence "starfun f x - star_of L \<in> Infinitesimal"
   1.190 +      by (unfold approx_def)
   1.191 +    thus "hnorm (starfun f x - star_of L) < star_of r"
   1.192 +      using r by (rule InfinitesimalD2)
   1.193 +  qed
   1.194 +  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
   1.195 +    by transfer
   1.196 +qed
   1.197 +
   1.198 +theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   1.199 +by (blast intro: LIM_NSLIM NSLIM_LIM)
   1.200 +
   1.201 +
   1.202 +subsection {* Continuity *}
   1.203 +
   1.204 +lemma isNSContD:
   1.205 +  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
   1.206 +by (simp add: isNSCont_def)
   1.207 +
   1.208 +lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
   1.209 +by (simp add: isNSCont_def NSLIM_def)
   1.210 +
   1.211 +lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
   1.212 +apply (simp add: isNSCont_def NSLIM_def, auto)
   1.213 +apply (case_tac "y = star_of a", auto)
   1.214 +done
   1.215 +
   1.216 +text{*NS continuity can be defined using NS Limit in
   1.217 +    similar fashion to standard def of continuity*}
   1.218 +lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
   1.219 +by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   1.220 +
   1.221 +text{*Hence, NS continuity can be given
   1.222 +  in terms of standard limit*}
   1.223 +lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
   1.224 +by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   1.225 +
   1.226 +text{*Moreover, it's trivial now that NS continuity
   1.227 +  is equivalent to standard continuity*}
   1.228 +lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
   1.229 +apply (simp add: isCont_def)
   1.230 +apply (rule isNSCont_LIM_iff)
   1.231 +done
   1.232 +
   1.233 +text{*Standard continuity ==> NS continuity*}
   1.234 +lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
   1.235 +by (erule isNSCont_isCont_iff [THEN iffD2])
   1.236 +
   1.237 +text{*NS continuity ==> Standard continuity*}
   1.238 +lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
   1.239 +by (erule isNSCont_isCont_iff [THEN iffD1])
   1.240 +
   1.241 +text{*Alternative definition of continuity*}
   1.242 +
   1.243 +(* Prove equivalence between NS limits - *)
   1.244 +(* seems easier than using standard def  *)
   1.245 +lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
   1.246 +apply (simp add: NSLIM_def, auto)
   1.247 +apply (drule_tac x = "star_of a + x" in spec)
   1.248 +apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   1.249 +apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   1.250 +apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   1.251 + prefer 2 apply (simp add: add_commute diff_def [symmetric])
   1.252 +apply (rule_tac x = x in star_cases)
   1.253 +apply (rule_tac [2] x = x in star_cases)
   1.254 +apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
   1.255 +done
   1.256 +
   1.257 +lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   1.258 +by (rule NSLIM_h_iff)
   1.259 +
   1.260 +lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
   1.261 +by (simp add: isNSCont_def)
   1.262 +
   1.263 +lemma isNSCont_inverse:
   1.264 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   1.265 +  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   1.266 +by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   1.267 +
   1.268 +lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
   1.269 +by (simp add: isNSCont_def)
   1.270 +
   1.271 +lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
   1.272 +apply (simp add: isNSCont_def)
   1.273 +apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
   1.274 +done
   1.275 +
   1.276 +
   1.277 +subsection {* Uniform Continuity *}
   1.278 +
   1.279 +lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
   1.280 +by (simp add: isNSUCont_def)
   1.281 +
   1.282 +lemma isUCont_isNSUCont:
   1.283 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   1.284 +  assumes f: "isUCont f" shows "isNSUCont f"
   1.285 +proof (unfold isNSUCont_def, safe)
   1.286 +  fix x y :: "'a star"
   1.287 +  assume approx: "x \<approx> y"
   1.288 +  have "starfun f x - starfun f y \<in> Infinitesimal"
   1.289 +  proof (rule InfinitesimalI2)
   1.290 +    fix r::real assume r: "0 < r"
   1.291 +    with f obtain s where s: "0 < s" and
   1.292 +      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
   1.293 +      by (auto simp add: isUCont_def)
   1.294 +    from less_r have less_r':
   1.295 +       "\<And>x y. hnorm (x - y) < star_of s
   1.296 +        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   1.297 +      by transfer
   1.298 +    from approx have "x - y \<in> Infinitesimal"
   1.299 +      by (unfold approx_def)
   1.300 +    hence "hnorm (x - y) < star_of s"
   1.301 +      using s by (rule InfinitesimalD2)
   1.302 +    thus "hnorm (starfun f x - starfun f y) < star_of r"
   1.303 +      by (rule less_r')
   1.304 +  qed
   1.305 +  thus "starfun f x \<approx> starfun f y"
   1.306 +    by (unfold approx_def)
   1.307 +qed
   1.308 +
   1.309 +lemma isNSUCont_isUCont:
   1.310 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   1.311 +  assumes f: "isNSUCont f" shows "isUCont f"
   1.312 +proof (unfold isUCont_def, safe)
   1.313 +  fix r::real assume r: "0 < r"
   1.314 +  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
   1.315 +        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   1.316 +  proof (rule exI, safe)
   1.317 +    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   1.318 +  next
   1.319 +    fix x y :: "'a star"
   1.320 +    assume "hnorm (x - y) < epsilon"
   1.321 +    with Infinitesimal_epsilon
   1.322 +    have "x - y \<in> Infinitesimal"
   1.323 +      by (rule hnorm_less_Infinitesimal)
   1.324 +    hence "x \<approx> y"
   1.325 +      by (unfold approx_def)
   1.326 +    with f have "starfun f x \<approx> starfun f y"
   1.327 +      by (simp add: isNSUCont_def)
   1.328 +    hence "starfun f x - starfun f y \<in> Infinitesimal"
   1.329 +      by (unfold approx_def)
   1.330 +    thus "hnorm (starfun f x - starfun f y) < star_of r"
   1.331 +      using r by (rule InfinitesimalD2)
   1.332 +  qed
   1.333 +  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   1.334 +    by transfer
   1.335 +qed
   1.336 +
   1.337 +end