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