src/HOL/NSA/HSEQ.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44568 e6f291cb5810
child 51474 1e9e68247ad1
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
huffman@27468
     1
(*  Title       : HSEQ.thy
huffman@27468
     2
    Author      : Jacques D. Fleuriot
huffman@27468
     3
    Copyright   : 1998  University of Cambridge
huffman@27468
     4
    Description : Convergence of sequences and series
huffman@27468
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
huffman@27468
     6
    Additional contributions by Jeremy Avigad and Brian Huffman
huffman@27468
     7
*)
huffman@27468
     8
huffman@27468
     9
header {* Sequences and Convergence (Nonstandard) *}
huffman@27468
    10
huffman@27468
    11
theory HSEQ
huffman@27468
    12
imports SEQ NatStar
huffman@27468
    13
begin
huffman@27468
    14
huffman@27468
    15
definition
huffman@27468
    16
  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
huffman@27468
    17
    ("((_)/ ----NS> (_))" [60, 60] 60) where
huffman@27468
    18
    --{*Nonstandard definition of convergence of sequence*}
haftmann@37765
    19
  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
huffman@27468
    20
huffman@27468
    21
definition
huffman@27468
    22
  nslim :: "(nat => 'a::real_normed_vector) => 'a" where
huffman@27468
    23
    --{*Nonstandard definition of limit using choice operator*}
huffman@27468
    24
  "nslim X = (THE L. X ----NS> L)"
huffman@27468
    25
huffman@27468
    26
definition
huffman@27468
    27
  NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
huffman@27468
    28
    --{*Nonstandard definition of convergence*}
huffman@27468
    29
  "NSconvergent X = (\<exists>L. X ----NS> L)"
huffman@27468
    30
huffman@27468
    31
definition
huffman@27468
    32
  NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
huffman@27468
    33
    --{*Nonstandard definition for bounded sequence*}
haftmann@37765
    34
  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
huffman@27468
    35
huffman@27468
    36
definition
huffman@27468
    37
  NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
huffman@27468
    38
    --{*Nonstandard definition*}
haftmann@37765
    39
  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
huffman@27468
    40
huffman@27468
    41
subsection {* Limits of Sequences *}
huffman@27468
    42
huffman@27468
    43
lemma NSLIMSEQ_iff:
huffman@27468
    44
    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
huffman@27468
    45
by (simp add: NSLIMSEQ_def)
huffman@27468
    46
huffman@27468
    47
lemma NSLIMSEQ_I:
huffman@27468
    48
  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L"
huffman@27468
    49
by (simp add: NSLIMSEQ_def)
huffman@27468
    50
huffman@27468
    51
lemma NSLIMSEQ_D:
huffman@27468
    52
  "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
huffman@27468
    53
by (simp add: NSLIMSEQ_def)
huffman@27468
    54
huffman@27468
    55
lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
huffman@27468
    56
by (simp add: NSLIMSEQ_def)
huffman@27468
    57
huffman@27468
    58
lemma NSLIMSEQ_add:
huffman@27468
    59
      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
huffman@27468
    60
by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
huffman@27468
    61
huffman@27468
    62
lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
huffman@27468
    63
by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
huffman@27468
    64
huffman@27468
    65
lemma NSLIMSEQ_mult:
huffman@27468
    66
  fixes a b :: "'a::real_normed_algebra"
huffman@27468
    67
  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
huffman@27468
    68
by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
huffman@27468
    69
huffman@27468
    70
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
huffman@27468
    71
by (auto simp add: NSLIMSEQ_def)
huffman@27468
    72
huffman@27468
    73
lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
huffman@27468
    74
by (drule NSLIMSEQ_minus, simp)
huffman@27468
    75
huffman@27468
    76
(* FIXME: delete *)
huffman@27468
    77
lemma NSLIMSEQ_add_minus:
huffman@27468
    78
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
huffman@27468
    79
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
huffman@27468
    80
huffman@27468
    81
lemma NSLIMSEQ_diff:
huffman@27468
    82
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
huffman@27468
    83
by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
huffman@27468
    84
huffman@27468
    85
lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
huffman@27468
    86
by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
huffman@27468
    87
huffman@27468
    88
lemma NSLIMSEQ_inverse:
huffman@27468
    89
  fixes a :: "'a::real_normed_div_algebra"
huffman@27468
    90
  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
huffman@27468
    91
by (simp add: NSLIMSEQ_def star_of_approx_inverse)
huffman@27468
    92
huffman@27468
    93
lemma NSLIMSEQ_mult_inverse:
huffman@27468
    94
  fixes a b :: "'a::real_normed_field"
huffman@27468
    95
  shows
huffman@27468
    96
     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
huffman@27468
    97
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
huffman@27468
    98
huffman@27468
    99
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
huffman@27468
   100
by transfer simp
huffman@27468
   101
huffman@27468
   102
lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
huffman@27468
   103
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
huffman@27468
   104
huffman@27468
   105
text{*Uniqueness of limit*}
huffman@27468
   106
lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
huffman@27468
   107
apply (simp add: NSLIMSEQ_def)
huffman@27468
   108
apply (drule HNatInfinite_whn [THEN [2] bspec])+
huffman@27468
   109
apply (auto dest: approx_trans3)
huffman@27468
   110
done
huffman@27468
   111
huffman@27468
   112
lemma NSLIMSEQ_pow [rule_format]:
haftmann@31017
   113
  fixes a :: "'a::{real_normed_algebra,power}"
huffman@27468
   114
  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
huffman@27468
   115
apply (induct "m")
huffman@27468
   116
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
huffman@27468
   117
done
huffman@27468
   118
huffman@27468
   119
text{*We can now try and derive a few properties of sequences,
huffman@27468
   120
     starting with the limit comparison property for sequences.*}
huffman@27468
   121
huffman@27468
   122
lemma NSLIMSEQ_le:
huffman@27468
   123
       "[| f ----NS> l; g ----NS> m;
huffman@27468
   124
           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
huffman@27468
   125
        |] ==> l \<le> (m::real)"
huffman@27468
   126
apply (simp add: NSLIMSEQ_def, safe)
huffman@27468
   127
apply (drule starfun_le_mono)
huffman@27468
   128
apply (drule HNatInfinite_whn [THEN [2] bspec])+
huffman@27468
   129
apply (drule_tac x = whn in spec)
huffman@27468
   130
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
huffman@27468
   131
apply clarify
huffman@27468
   132
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
huffman@27468
   133
done
huffman@27468
   134
huffman@27468
   135
lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
huffman@27468
   136
by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
huffman@27468
   137
huffman@27468
   138
lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
huffman@27468
   139
by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
huffman@27468
   140
huffman@27468
   141
text{*Shift a convergent series by 1:
huffman@27468
   142
  By the equivalence between Cauchiness and convergence and because
huffman@27468
   143
  the successor of an infinite hypernatural is also infinite.*}
huffman@27468
   144
huffman@27468
   145
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
huffman@27468
   146
apply (unfold NSLIMSEQ_def, safe)
huffman@27468
   147
apply (drule_tac x="N + 1" in bspec)
huffman@27468
   148
apply (erule HNatInfinite_add)
huffman@27468
   149
apply (simp add: starfun_shift_one)
huffman@27468
   150
done
huffman@27468
   151
huffman@27468
   152
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
huffman@27468
   153
apply (unfold NSLIMSEQ_def, safe)
huffman@27468
   154
apply (drule_tac x="N - 1" in bspec) 
huffman@27468
   155
apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
huffman@27468
   156
apply (simp add: starfun_shift_one one_le_HNatInfinite)
huffman@27468
   157
done
huffman@27468
   158
huffman@27468
   159
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
huffman@27468
   160
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
huffman@27468
   161
huffman@27468
   162
subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
huffman@27468
   163
huffman@27468
   164
lemma LIMSEQ_NSLIMSEQ:
huffman@27468
   165
  assumes X: "X ----> L" shows "X ----NS> L"
huffman@27468
   166
proof (rule NSLIMSEQ_I)
huffman@27468
   167
  fix N assume N: "N \<in> HNatInfinite"
huffman@27468
   168
  have "starfun X N - star_of L \<in> Infinitesimal"
huffman@27468
   169
  proof (rule InfinitesimalI2)
huffman@27468
   170
    fix r::real assume r: "0 < r"
huffman@27468
   171
    from LIMSEQ_D [OF X r]
huffman@27468
   172
    obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
huffman@27468
   173
    hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
huffman@27468
   174
      by transfer
huffman@27468
   175
    thus "hnorm (starfun X N - star_of L) < star_of r"
huffman@27468
   176
      using N by (simp add: star_of_le_HNatInfinite)
huffman@27468
   177
  qed
huffman@27468
   178
  thus "starfun X N \<approx> star_of L"
huffman@27468
   179
    by (unfold approx_def)
huffman@27468
   180
qed
huffman@27468
   181
huffman@27468
   182
lemma NSLIMSEQ_LIMSEQ:
huffman@27468
   183
  assumes X: "X ----NS> L" shows "X ----> L"
huffman@27468
   184
proof (rule LIMSEQ_I)
huffman@27468
   185
  fix r::real assume r: "0 < r"
huffman@27468
   186
  have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
huffman@27468
   187
  proof (intro exI allI impI)
huffman@27468
   188
    fix n assume "whn \<le> n"
huffman@27468
   189
    with HNatInfinite_whn have "n \<in> HNatInfinite"
huffman@27468
   190
      by (rule HNatInfinite_upward_closed)
huffman@27468
   191
    with X have "starfun X n \<approx> star_of L"
huffman@27468
   192
      by (rule NSLIMSEQ_D)
huffman@27468
   193
    hence "starfun X n - star_of L \<in> Infinitesimal"
huffman@27468
   194
      by (unfold approx_def)
huffman@27468
   195
    thus "hnorm (starfun X n - star_of L) < star_of r"
huffman@27468
   196
      using r by (rule InfinitesimalD2)
huffman@27468
   197
  qed
huffman@27468
   198
  thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
huffman@27468
   199
    by transfer
huffman@27468
   200
qed
huffman@27468
   201
huffman@27468
   202
theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
huffman@27468
   203
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
huffman@27468
   204
huffman@27468
   205
subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
huffman@27468
   206
huffman@27468
   207
text{*We prove the NS version from the standard one, since the NS proof
huffman@27468
   208
   seems more complicated than the standard one above!*}
huffman@27468
   209
lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)"
huffman@44568
   210
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
huffman@27468
   211
huffman@27468
   212
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
huffman@44568
   213
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
huffman@27468
   214
huffman@27468
   215
text{*Generalization to other limits*}
huffman@27468
   216
lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
huffman@27468
   217
apply (simp add: NSLIMSEQ_def)
huffman@27468
   218
apply (auto intro: approx_hrabs 
huffman@27468
   219
            simp add: starfun_abs)
huffman@27468
   220
done
huffman@27468
   221
huffman@27468
   222
lemma NSLIMSEQ_inverse_zero:
huffman@27468
   223
     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
huffman@27468
   224
      ==> (%n. inverse(f n)) ----NS> 0"
huffman@27468
   225
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
huffman@27468
   226
huffman@27468
   227
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
huffman@27468
   228
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
huffman@27468
   229
huffman@27468
   230
lemma NSLIMSEQ_inverse_real_of_nat_add:
huffman@27468
   231
     "(%n. r + inverse(real(Suc n))) ----NS> r"
huffman@27468
   232
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
huffman@27468
   233
huffman@27468
   234
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
huffman@27468
   235
     "(%n. r + -inverse(real(Suc n))) ----NS> r"
huffman@27468
   236
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
huffman@27468
   237
huffman@27468
   238
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
huffman@27468
   239
     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
huffman@27468
   240
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
huffman@27468
   241
huffman@27468
   242
huffman@27468
   243
subsection {* Convergence *}
huffman@27468
   244
huffman@27468
   245
lemma nslimI: "X ----NS> L ==> nslim X = L"
huffman@27468
   246
apply (simp add: nslim_def)
huffman@27468
   247
apply (blast intro: NSLIMSEQ_unique)
huffman@27468
   248
done
huffman@27468
   249
huffman@27468
   250
lemma lim_nslim_iff: "lim X = nslim X"
huffman@27468
   251
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
huffman@27468
   252
huffman@27468
   253
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
huffman@27468
   254
by (simp add: NSconvergent_def)
huffman@27468
   255
huffman@27468
   256
lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
huffman@27468
   257
by (auto simp add: NSconvergent_def)
huffman@27468
   258
huffman@27468
   259
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
huffman@27468
   260
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
huffman@27468
   261
huffman@27468
   262
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
huffman@27468
   263
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
huffman@27468
   264
huffman@27468
   265
huffman@27468
   266
subsection {* Bounded Monotonic Sequences *}
huffman@27468
   267
huffman@27468
   268
lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
huffman@27468
   269
by (simp add: NSBseq_def)
huffman@27468
   270
huffman@27468
   271
lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
huffman@27468
   272
unfolding Standard_def by auto
huffman@27468
   273
huffman@27468
   274
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
huffman@27468
   275
apply (cases "N \<in> HNatInfinite")
huffman@27468
   276
apply (erule (1) NSBseqD)
huffman@27468
   277
apply (rule subsetD [OF Standard_subset_HFinite])
huffman@27468
   278
apply (simp add: HNatInfinite_def Nats_eq_Standard)
huffman@27468
   279
done
huffman@27468
   280
huffman@27468
   281
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
huffman@27468
   282
by (simp add: NSBseq_def)
huffman@27468
   283
huffman@27468
   284
text{*The standard definition implies the nonstandard definition*}
huffman@27468
   285
huffman@27468
   286
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
huffman@27468
   287
proof (unfold NSBseq_def, safe)
huffman@27468
   288
  assume X: "Bseq X"
huffman@27468
   289
  fix N assume N: "N \<in> HNatInfinite"
huffman@27468
   290
  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
huffman@27468
   291
  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
huffman@27468
   292
  hence "hnorm (starfun X N) \<le> star_of K" by simp
huffman@27468
   293
  also have "star_of K < star_of (K + 1)" by simp
huffman@27468
   294
  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
huffman@27468
   295
  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
huffman@27468
   296
qed
huffman@27468
   297
huffman@27468
   298
text{*The nonstandard definition implies the standard definition*}
huffman@27468
   299
huffman@27468
   300
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
huffman@27468
   301
apply (insert HInfinite_omega)
huffman@27468
   302
apply (simp add: HInfinite_def)
huffman@27468
   303
apply (simp add: order_less_imp_le)
huffman@27468
   304
done
huffman@27468
   305
huffman@27468
   306
lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
huffman@27468
   307
proof (rule ccontr)
huffman@27468
   308
  let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
huffman@27468
   309
  assume "NSBseq X"
huffman@27468
   310
  hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
huffman@27468
   311
    by (rule NSBseqD2)
huffman@27468
   312
  assume "\<not> Bseq X"
huffman@27468
   313
  hence "\<forall>K>0. \<exists>n. K < norm (X n)"
huffman@27468
   314
    by (simp add: Bseq_def linorder_not_le)
huffman@27468
   315
  hence "\<forall>K>0. K < norm (X (?n K))"
huffman@27468
   316
    by (auto intro: LeastI_ex)
huffman@27468
   317
  hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
huffman@27468
   318
    by transfer
huffman@27468
   319
  hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
huffman@27468
   320
    by simp
huffman@27468
   321
  hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
huffman@27468
   322
    by (simp add: order_less_trans [OF SReal_less_omega])
huffman@27468
   323
  hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
huffman@27468
   324
    by (simp add: HInfinite_def)
huffman@27468
   325
  with finite show "False"
huffman@27468
   326
    by (simp add: HFinite_HInfinite_iff)
huffman@27468
   327
qed
huffman@27468
   328
huffman@27468
   329
text{* Equivalence of nonstandard and standard definitions
huffman@27468
   330
  for a bounded sequence*}
huffman@27468
   331
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
huffman@27468
   332
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
huffman@27468
   333
huffman@27468
   334
text{*A convergent sequence is bounded: 
huffman@27468
   335
 Boundedness as a necessary condition for convergence. 
huffman@27468
   336
 The nonstandard version has no existential, as usual *}
huffman@27468
   337
huffman@27468
   338
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
huffman@27468
   339
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
huffman@27468
   340
apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
huffman@27468
   341
done
huffman@27468
   342
huffman@27468
   343
text{*Standard Version: easily now proved using equivalence of NS and
huffman@27468
   344
 standard definitions *}
huffman@27468
   345
huffman@27468
   346
lemma convergent_Bseq: "convergent X ==> Bseq X"
huffman@27468
   347
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
huffman@27468
   348
huffman@27468
   349
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
huffman@27468
   350
huffman@27468
   351
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
huffman@27468
   352
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
huffman@27468
   353
huffman@27468
   354
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
huffman@27468
   355
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
huffman@27468
   356
huffman@27468
   357
subsubsection{*A Bounded and Monotonic Sequence Converges*}
huffman@27468
   358
huffman@27468
   359
text{* The best of both worlds: Easier to prove this result as a standard
huffman@27468
   360
   theorem and then use equivalence to "transfer" it into the
huffman@27468
   361
   equivalent nonstandard form if needed!*}
huffman@27468
   362
huffman@27468
   363
lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
huffman@27468
   364
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
huffman@27468
   365
huffman@27468
   366
lemma NSBseq_mono_NSconvergent:
huffman@27468
   367
     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
huffman@27468
   368
by (auto intro: Bseq_mono_convergent 
huffman@27468
   369
         simp add: convergent_NSconvergent_iff [symmetric] 
huffman@27468
   370
                   Bseq_NSBseq_iff [symmetric])
huffman@27468
   371
huffman@27468
   372
huffman@27468
   373
subsection {* Cauchy Sequences *}
huffman@27468
   374
huffman@27468
   375
lemma NSCauchyI:
huffman@27468
   376
  "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
huffman@27468
   377
   \<Longrightarrow> NSCauchy X"
huffman@27468
   378
by (simp add: NSCauchy_def)
huffman@27468
   379
huffman@27468
   380
lemma NSCauchyD:
huffman@27468
   381
  "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
huffman@27468
   382
   \<Longrightarrow> starfun X M \<approx> starfun X N"
huffman@27468
   383
by (simp add: NSCauchy_def)
huffman@27468
   384
huffman@27468
   385
subsubsection{*Equivalence Between NS and Standard*}
huffman@27468
   386
huffman@27468
   387
lemma Cauchy_NSCauchy:
huffman@27468
   388
  assumes X: "Cauchy X" shows "NSCauchy X"
huffman@27468
   389
proof (rule NSCauchyI)
huffman@27468
   390
  fix M assume M: "M \<in> HNatInfinite"
huffman@27468
   391
  fix N assume N: "N \<in> HNatInfinite"
huffman@27468
   392
  have "starfun X M - starfun X N \<in> Infinitesimal"
huffman@27468
   393
  proof (rule InfinitesimalI2)
huffman@27468
   394
    fix r :: real assume r: "0 < r"
huffman@27468
   395
    from CauchyD [OF X r]
huffman@27468
   396
    obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
huffman@27468
   397
    hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
huffman@27468
   398
           hnorm (starfun X m - starfun X n) < star_of r"
huffman@27468
   399
      by transfer
huffman@27468
   400
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@27468
   401
      using M N by (simp add: star_of_le_HNatInfinite)
huffman@27468
   402
  qed
huffman@27468
   403
  thus "starfun X M \<approx> starfun X N"
huffman@27468
   404
    by (unfold approx_def)
huffman@27468
   405
qed
huffman@27468
   406
huffman@27468
   407
lemma NSCauchy_Cauchy:
huffman@27468
   408
  assumes X: "NSCauchy X" shows "Cauchy X"
huffman@27468
   409
proof (rule CauchyI)
huffman@27468
   410
  fix r::real assume r: "0 < r"
huffman@27468
   411
  have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
huffman@27468
   412
  proof (intro exI allI impI)
huffman@27468
   413
    fix M assume "whn \<le> M"
huffman@27468
   414
    with HNatInfinite_whn have M: "M \<in> HNatInfinite"
huffman@27468
   415
      by (rule HNatInfinite_upward_closed)
huffman@27468
   416
    fix N assume "whn \<le> N"
huffman@27468
   417
    with HNatInfinite_whn have N: "N \<in> HNatInfinite"
huffman@27468
   418
      by (rule HNatInfinite_upward_closed)
huffman@27468
   419
    from X M N have "starfun X M \<approx> starfun X N"
huffman@27468
   420
      by (rule NSCauchyD)
huffman@27468
   421
    hence "starfun X M - starfun X N \<in> Infinitesimal"
huffman@27468
   422
      by (unfold approx_def)
huffman@27468
   423
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@27468
   424
      using r by (rule InfinitesimalD2)
huffman@27468
   425
  qed
huffman@27468
   426
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
huffman@27468
   427
    by transfer
huffman@27468
   428
qed
huffman@27468
   429
huffman@27468
   430
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
huffman@27468
   431
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
huffman@27468
   432
huffman@27468
   433
subsubsection {* Cauchy Sequences are Bounded *}
huffman@27468
   434
huffman@27468
   435
text{*A Cauchy sequence is bounded -- nonstandard version*}
huffman@27468
   436
huffman@27468
   437
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
huffman@27468
   438
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
huffman@27468
   439
huffman@27468
   440
subsubsection {* Cauchy Sequences are Convergent *}
huffman@27468
   441
huffman@27468
   442
text{*Equivalence of Cauchy criterion and convergence:
huffman@27468
   443
  We will prove this using our NS formulation which provides a
huffman@27468
   444
  much easier proof than using the standard definition. We do not
huffman@27468
   445
  need to use properties of subsequences such as boundedness,
huffman@27468
   446
  monotonicity etc... Compare with Harrison's corresponding proof
huffman@27468
   447
  in HOL which is much longer and more complicated. Of course, we do
huffman@27468
   448
  not have problems which he encountered with guessing the right
huffman@27468
   449
  instantiations for his 'espsilon-delta' proof(s) in this case
huffman@27468
   450
  since the NS formulations do not involve existential quantifiers.*}
huffman@27468
   451
huffman@27468
   452
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
huffman@27468
   453
apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
huffman@27468
   454
apply (auto intro: approx_trans2)
huffman@27468
   455
done
huffman@27468
   456
huffman@27468
   457
lemma real_NSCauchy_NSconvergent:
huffman@27468
   458
  fixes X :: "nat \<Rightarrow> real"
huffman@27468
   459
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@27468
   460
apply (simp add: NSconvergent_def NSLIMSEQ_def)
huffman@27468
   461
apply (frule NSCauchy_NSBseq)
huffman@27468
   462
apply (simp add: NSBseq_def NSCauchy_def)
huffman@27468
   463
apply (drule HNatInfinite_whn [THEN [2] bspec])
huffman@27468
   464
apply (drule HNatInfinite_whn [THEN [2] bspec])
huffman@27468
   465
apply (auto dest!: st_part_Ex simp add: SReal_iff)
huffman@27468
   466
apply (blast intro: approx_trans3)
huffman@27468
   467
done
huffman@27468
   468
huffman@27468
   469
lemma NSCauchy_NSconvergent:
huffman@27468
   470
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@27468
   471
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@27468
   472
apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
huffman@27468
   473
apply (erule convergent_NSconvergent_iff [THEN iffD1])
huffman@27468
   474
done
huffman@27468
   475
huffman@27468
   476
lemma NSCauchy_NSconvergent_iff:
huffman@27468
   477
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@27468
   478
  shows "NSCauchy X = NSconvergent X"
huffman@27468
   479
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
huffman@27468
   480
huffman@27468
   481
huffman@27468
   482
subsection {* Power Sequences *}
huffman@27468
   483
huffman@27468
   484
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
huffman@27468
   485
"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
huffman@27468
   486
  also fact that bounded and monotonic sequence converges.*}
huffman@27468
   487
huffman@27468
   488
text{* We now use NS criterion to bring proof of theorem through *}
huffman@27468
   489
huffman@27468
   490
lemma NSLIMSEQ_realpow_zero:
huffman@27468
   491
  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
huffman@27468
   492
apply (simp add: NSLIMSEQ_def)
huffman@27468
   493
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
huffman@27468
   494
apply (frule NSconvergentD)
huffman@27468
   495
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
huffman@27468
   496
apply (frule HNatInfinite_add_one)
huffman@27468
   497
apply (drule bspec, assumption)
huffman@27468
   498
apply (drule bspec, assumption)
huffman@27468
   499
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
huffman@27468
   500
apply (simp add: hyperpow_add)
huffman@27468
   501
apply (drule approx_mult_subst_star_of, assumption)
huffman@27468
   502
apply (drule approx_trans3, assumption)
huffman@27468
   503
apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
huffman@27468
   504
done
huffman@27468
   505
huffman@27468
   506
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
huffman@27468
   507
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
huffman@27468
   508
huffman@27468
   509
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
huffman@27468
   510
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
huffman@27468
   511
huffman@27468
   512
(***---------------------------------------------------------------
huffman@27468
   513
    Theorems proved by Harrison in HOL that we do not need
huffman@27468
   514
    in order to prove equivalence between Cauchy criterion
huffman@27468
   515
    and convergence:
huffman@27468
   516
 -- Show that every sequence contains a monotonic subsequence
huffman@27468
   517
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
huffman@27468
   518
 -- Show that a subsequence of a bounded sequence is bounded
huffman@27468
   519
Goal "Bseq X ==> Bseq (%n. X (f n))";
huffman@27468
   520
 -- Show we can take subsequential terms arbitrarily far
huffman@27468
   521
    up a sequence
huffman@27468
   522
Goal "subseq f ==> n \<le> f(n)";
huffman@27468
   523
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
huffman@27468
   524
 ---------------------------------------------------------------***)
huffman@27468
   525
huffman@27468
   526
end