src/HOL/NSA/HLim.thy
author huffman
Thu Jul 03 17:47:22 2008 +0200 (2008-07-03)
changeset 27468 0783dd1dc13d
child 28562 4e74209f113e
permissions -rw-r--r--
move nonstandard analysis theories to NSA directory
     1 (*  Title       : HLim.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6 *)
     7 
     8 header{* Limits and Continuity (Nonstandard) *}
     9 
    10 theory HLim
    11 imports Star Lim
    12 begin
    13 
    14 text{*Nonstandard Definitions*}
    15 
    16 definition
    17   NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
    18             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
    19   [code func del]: "f -- a --NS> L =
    20     (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    21 
    22 definition
    23   isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    24     --{*NS definition dispenses with limit notions*}
    25   [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
    26          ( *f* f) y @= star_of (f a))"
    27 
    28 definition
    29   isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    30   [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    31 
    32 
    33 subsection {* Limits of Functions *}
    34 
    35 lemma NSLIM_I:
    36   "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
    37    \<Longrightarrow> f -- a --NS> L"
    38 by (simp add: NSLIM_def)
    39 
    40 lemma NSLIM_D:
    41   "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
    42    \<Longrightarrow> starfun f x \<approx> star_of L"
    43 by (simp add: NSLIM_def)
    44 
    45 text{*Proving properties of limits using nonstandard definition.
    46       The properties hold for standard limits as well!*}
    47 
    48 lemma NSLIM_mult:
    49   fixes l m :: "'a::real_normed_algebra"
    50   shows "[| f -- x --NS> l; g -- x --NS> m |]
    51       ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
    52 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
    53 
    54 lemma starfun_scaleR [simp]:
    55   "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
    56 by transfer (rule refl)
    57 
    58 lemma NSLIM_scaleR:
    59   "[| f -- x --NS> l; g -- x --NS> m |]
    60       ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
    61 by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
    62 
    63 lemma NSLIM_add:
    64      "[| f -- x --NS> l; g -- x --NS> m |]
    65       ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
    66 by (auto simp add: NSLIM_def intro!: approx_add)
    67 
    68 lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
    69 by (simp add: NSLIM_def)
    70 
    71 lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
    72 by (simp add: NSLIM_def)
    73 
    74 lemma NSLIM_diff:
    75   "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
    76 by (simp only: diff_def NSLIM_add NSLIM_minus)
    77 
    78 lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
    79 by (simp only: NSLIM_add NSLIM_minus)
    80 
    81 lemma NSLIM_inverse:
    82   fixes L :: "'a::real_normed_div_algebra"
    83   shows "[| f -- a --NS> L;  L \<noteq> 0 |]
    84       ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
    85 apply (simp add: NSLIM_def, clarify)
    86 apply (drule spec)
    87 apply (auto simp add: star_of_approx_inverse)
    88 done
    89 
    90 lemma NSLIM_zero:
    91   assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
    92 proof -
    93   have "(\<lambda>x. f x - l) -- a --NS> l - l"
    94     by (rule NSLIM_diff [OF f NSLIM_const])
    95   thus ?thesis by simp
    96 qed
    97 
    98 lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
    99 apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   100 apply (auto simp add: diff_minus add_assoc)
   101 done
   102 
   103 lemma NSLIM_const_not_eq:
   104   fixes a :: "'a::real_normed_algebra_1"
   105   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
   106 apply (simp add: NSLIM_def)
   107 apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
   108 apply (simp add: hypreal_epsilon_not_zero approx_def)
   109 done
   110 
   111 lemma NSLIM_not_zero:
   112   fixes a :: "'a::real_normed_algebra_1"
   113   shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
   114 by (rule NSLIM_const_not_eq)
   115 
   116 lemma NSLIM_const_eq:
   117   fixes a :: "'a::real_normed_algebra_1"
   118   shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
   119 apply (rule ccontr)
   120 apply (blast dest: NSLIM_const_not_eq)
   121 done
   122 
   123 lemma NSLIM_unique:
   124   fixes a :: "'a::real_normed_algebra_1"
   125   shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
   126 apply (drule (1) NSLIM_diff)
   127 apply (auto dest!: NSLIM_const_eq)
   128 done
   129 
   130 lemma NSLIM_mult_zero:
   131   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   132   shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   133 by (drule NSLIM_mult, auto)
   134 
   135 lemma NSLIM_self: "(%x. x) -- a --NS> a"
   136 by (simp add: NSLIM_def)
   137 
   138 subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
   139 
   140 lemma LIM_NSLIM:
   141   assumes f: "f -- a --> L" shows "f -- a --NS> L"
   142 proof (rule NSLIM_I)
   143   fix x
   144   assume neq: "x \<noteq> star_of a"
   145   assume approx: "x \<approx> star_of a"
   146   have "starfun f x - star_of L \<in> Infinitesimal"
   147   proof (rule InfinitesimalI2)
   148     fix r::real assume r: "0 < r"
   149     from LIM_D [OF f r]
   150     obtain s where s: "0 < s" and
   151       less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
   152       by fast
   153     from less_r have less_r':
   154        "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
   155         \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   156       by transfer
   157     from approx have "x - star_of a \<in> Infinitesimal"
   158       by (unfold approx_def)
   159     hence "hnorm (x - star_of a) < star_of s"
   160       using s by (rule InfinitesimalD2)
   161     with neq show "hnorm (starfun f x - star_of L) < star_of r"
   162       by (rule less_r')
   163   qed
   164   thus "starfun f x \<approx> star_of L"
   165     by (unfold approx_def)
   166 qed
   167 
   168 lemma NSLIM_LIM:
   169   assumes f: "f -- a --NS> L" shows "f -- a --> L"
   170 proof (rule LIM_I)
   171   fix r::real assume r: "0 < r"
   172   have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
   173         \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
   174   proof (rule exI, safe)
   175     show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   176   next
   177     fix x assume neq: "x \<noteq> star_of a"
   178     assume "hnorm (x - star_of a) < epsilon"
   179     with Infinitesimal_epsilon
   180     have "x - star_of a \<in> Infinitesimal"
   181       by (rule hnorm_less_Infinitesimal)
   182     hence "x \<approx> star_of a"
   183       by (unfold approx_def)
   184     with f neq have "starfun f x \<approx> star_of L"
   185       by (rule NSLIM_D)
   186     hence "starfun f x - star_of L \<in> Infinitesimal"
   187       by (unfold approx_def)
   188     thus "hnorm (starfun f x - star_of L) < star_of r"
   189       using r by (rule InfinitesimalD2)
   190   qed
   191   thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
   192     by transfer
   193 qed
   194 
   195 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   196 by (blast intro: LIM_NSLIM NSLIM_LIM)
   197 
   198 
   199 subsection {* Continuity *}
   200 
   201 lemma isNSContD:
   202   "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
   203 by (simp add: isNSCont_def)
   204 
   205 lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
   206 by (simp add: isNSCont_def NSLIM_def)
   207 
   208 lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
   209 apply (simp add: isNSCont_def NSLIM_def, auto)
   210 apply (case_tac "y = star_of a", auto)
   211 done
   212 
   213 text{*NS continuity can be defined using NS Limit in
   214     similar fashion to standard def of continuity*}
   215 lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
   216 by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   217 
   218 text{*Hence, NS continuity can be given
   219   in terms of standard limit*}
   220 lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
   221 by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   222 
   223 text{*Moreover, it's trivial now that NS continuity
   224   is equivalent to standard continuity*}
   225 lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
   226 apply (simp add: isCont_def)
   227 apply (rule isNSCont_LIM_iff)
   228 done
   229 
   230 text{*Standard continuity ==> NS continuity*}
   231 lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
   232 by (erule isNSCont_isCont_iff [THEN iffD2])
   233 
   234 text{*NS continuity ==> Standard continuity*}
   235 lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
   236 by (erule isNSCont_isCont_iff [THEN iffD1])
   237 
   238 text{*Alternative definition of continuity*}
   239 
   240 (* Prove equivalence between NS limits - *)
   241 (* seems easier than using standard def  *)
   242 lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
   243 apply (simp add: NSLIM_def, auto)
   244 apply (drule_tac x = "star_of a + x" in spec)
   245 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   246 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   247 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
   248  prefer 2 apply (simp add: add_commute diff_def [symmetric])
   249 apply (rule_tac x = x in star_cases)
   250 apply (rule_tac [2] x = x in star_cases)
   251 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
   252 done
   253 
   254 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   255 by (rule NSLIM_h_iff)
   256 
   257 lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
   258 by (simp add: isNSCont_def)
   259 
   260 lemma isNSCont_inverse:
   261   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
   262   shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   263 by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   264 
   265 lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
   266 by (simp add: isNSCont_def)
   267 
   268 lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
   269 apply (simp add: isNSCont_def)
   270 apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
   271 done
   272 
   273 
   274 subsection {* Uniform Continuity *}
   275 
   276 lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
   277 by (simp add: isNSUCont_def)
   278 
   279 lemma isUCont_isNSUCont:
   280   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   281   assumes f: "isUCont f" shows "isNSUCont f"
   282 proof (unfold isNSUCont_def, safe)
   283   fix x y :: "'a star"
   284   assume approx: "x \<approx> y"
   285   have "starfun f x - starfun f y \<in> Infinitesimal"
   286   proof (rule InfinitesimalI2)
   287     fix r::real assume r: "0 < r"
   288     with f obtain s where s: "0 < s" and
   289       less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
   290       by (auto simp add: isUCont_def)
   291     from less_r have less_r':
   292        "\<And>x y. hnorm (x - y) < star_of s
   293         \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   294       by transfer
   295     from approx have "x - y \<in> Infinitesimal"
   296       by (unfold approx_def)
   297     hence "hnorm (x - y) < star_of s"
   298       using s by (rule InfinitesimalD2)
   299     thus "hnorm (starfun f x - starfun f y) < star_of r"
   300       by (rule less_r')
   301   qed
   302   thus "starfun f x \<approx> starfun f y"
   303     by (unfold approx_def)
   304 qed
   305 
   306 lemma isNSUCont_isUCont:
   307   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   308   assumes f: "isNSUCont f" shows "isUCont f"
   309 proof (unfold isUCont_def, safe)
   310   fix r::real assume r: "0 < r"
   311   have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
   312         \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   313   proof (rule exI, safe)
   314     show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
   315   next
   316     fix x y :: "'a star"
   317     assume "hnorm (x - y) < epsilon"
   318     with Infinitesimal_epsilon
   319     have "x - y \<in> Infinitesimal"
   320       by (rule hnorm_less_Infinitesimal)
   321     hence "x \<approx> y"
   322       by (unfold approx_def)
   323     with f have "starfun f x \<approx> starfun f y"
   324       by (simp add: isNSUCont_def)
   325     hence "starfun f x - starfun f y \<in> Infinitesimal"
   326       by (unfold approx_def)
   327     thus "hnorm (starfun f x - starfun f y) < star_of r"
   328       using r by (rule InfinitesimalD2)
   329   qed
   330   thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   331     by transfer
   332 qed
   333 
   334 end