src/HOL/Hyperreal/SEQ.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21139 c957e02e7a36
child 21810 b2d23672b003
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
paulson@10751
     1
(*  Title       : SEQ.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@10751
     4
    Description : Convergence of sequences and series
paulson@15082
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
avigad@16819
     6
    Additional contributions by Jeremy Avigad
paulson@15082
     7
*)
paulson@10751
     8
huffman@17439
     9
header {* Sequences and Series *}
huffman@17439
    10
nipkow@15131
    11
theory SEQ
nipkow@15236
    12
imports NatStar
nipkow@15131
    13
begin
paulson@10751
    14
wenzelm@19765
    15
definition
huffman@20552
    16
  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
wenzelm@21404
    17
    ("((_)/ ----> (_))" [60, 60] 60) where
paulson@15082
    18
    --{*Standard definition of convergence of sequence*}
huffman@20563
    19
  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
paulson@10751
    20
wenzelm@21404
    21
definition
huffman@20552
    22
  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
wenzelm@21404
    23
    ("((_)/ ----NS> (_))" [60, 60] 60) where
paulson@15082
    24
    --{*Nonstandard definition of convergence of sequence*}
huffman@20552
    25
  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
paulson@15082
    26
wenzelm@21404
    27
definition
wenzelm@21404
    28
  lim :: "(nat => 'a::real_normed_vector) => 'a" where
paulson@15082
    29
    --{*Standard definition of limit using choice operator*}
huffman@20682
    30
  "lim X = (THE L. X ----> L)"
paulson@10751
    31
wenzelm@21404
    32
definition
wenzelm@21404
    33
  nslim :: "(nat => 'a::real_normed_vector) => 'a" where
paulson@15082
    34
    --{*Nonstandard definition of limit using choice operator*}
huffman@20682
    35
  "nslim X = (THE L. X ----NS> L)"
paulson@10751
    36
wenzelm@21404
    37
definition
wenzelm@21404
    38
  convergent :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    39
    --{*Standard definition of convergence*}
huffman@20682
    40
  "convergent X = (\<exists>L. X ----> L)"
paulson@10751
    41
wenzelm@21404
    42
definition
wenzelm@21404
    43
  NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    44
    --{*Nonstandard definition of convergence*}
huffman@20682
    45
  "NSconvergent X = (\<exists>L. X ----NS> L)"
paulson@15082
    46
wenzelm@21404
    47
definition
wenzelm@21404
    48
  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    49
    --{*Standard definition for bounded sequence*}
huffman@20552
    50
  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
paulson@10751
    51
wenzelm@21404
    52
definition
wenzelm@21404
    53
  NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    54
    --{*Nonstandard definition for bounded sequence*}
wenzelm@19765
    55
  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
paulson@15082
    56
wenzelm@21404
    57
definition
wenzelm@21404
    58
  monoseq :: "(nat=>real)=>bool" where
paulson@15082
    59
    --{*Definition for monotonicity*}
wenzelm@19765
    60
  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
paulson@10751
    61
wenzelm@21404
    62
definition
wenzelm@21404
    63
  subseq :: "(nat => nat) => bool" where
paulson@15082
    64
    --{*Definition of subsequence*}
wenzelm@19765
    65
  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
paulson@10751
    66
wenzelm@21404
    67
definition
wenzelm@21404
    68
  Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    69
    --{*Standard definition of the Cauchy condition*}
huffman@20563
    70
  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
paulson@10751
    71
wenzelm@21404
    72
definition
wenzelm@21404
    73
  NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    74
    --{*Nonstandard definition*}
wenzelm@19765
    75
  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
paulson@15082
    76
paulson@15082
    77
huffman@20696
    78
subsection {* Limits of Sequences *}
huffman@20696
    79
huffman@20696
    80
subsubsection {* Purely standard proofs *}
paulson@15082
    81
paulson@15082
    82
lemma LIMSEQ_iff:
huffman@20563
    83
      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
paulson@15082
    84
by (simp add: LIMSEQ_def)
paulson@15082
    85
huffman@20751
    86
lemma LIMSEQ_I:
huffman@20751
    87
  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
huffman@20751
    88
by (simp add: LIMSEQ_def)
huffman@20751
    89
huffman@20751
    90
lemma LIMSEQ_D:
huffman@20751
    91
  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
huffman@20751
    92
by (simp add: LIMSEQ_def)
huffman@20751
    93
huffman@20696
    94
lemma LIMSEQ_const: "(%n. k) ----> k"
huffman@20696
    95
by (simp add: LIMSEQ_def)
huffman@20696
    96
huffman@20696
    97
lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
huffman@20696
    98
apply (simp add: LIMSEQ_def, safe)
huffman@20696
    99
apply (drule_tac x="r" in spec, safe)
huffman@20696
   100
apply (rule_tac x="no" in exI, safe)
huffman@20696
   101
apply (drule_tac x="n" in spec, safe)
huffman@20696
   102
apply (erule order_le_less_trans [OF norm_triangle_ineq3])
huffman@20696
   103
done
huffman@20696
   104
huffman@20696
   105
lemma LIMSEQ_ignore_initial_segment: "f ----> a 
huffman@20696
   106
  ==> (%n. f(n + k)) ----> a"
huffman@20696
   107
  apply (unfold LIMSEQ_def) 
huffman@20696
   108
  apply (clarify)
huffman@20696
   109
  apply (drule_tac x = r in spec)
huffman@20696
   110
  apply (clarify)
huffman@20696
   111
  apply (rule_tac x = "no + k" in exI)
huffman@20696
   112
  by auto
huffman@20696
   113
huffman@20696
   114
lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
huffman@20696
   115
    f ----> a"
huffman@20696
   116
  apply (unfold LIMSEQ_def)
huffman@20696
   117
  apply clarsimp
huffman@20696
   118
  apply (drule_tac x = r in spec)
huffman@20696
   119
  apply clarsimp
huffman@20696
   120
  apply (rule_tac x = "no + k" in exI)
huffman@20696
   121
  apply clarsimp
huffman@20696
   122
  apply (drule_tac x = "n - k" in spec)
huffman@20696
   123
  apply (frule mp)
huffman@20696
   124
  apply arith
huffman@20696
   125
  apply simp
huffman@20696
   126
done
huffman@20696
   127
huffman@20696
   128
subsubsection {* Purely nonstandard proofs *}
huffman@20696
   129
paulson@15082
   130
lemma NSLIMSEQ_iff:
huffman@20552
   131
    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
paulson@15082
   132
by (simp add: NSLIMSEQ_def)
paulson@15082
   133
huffman@20751
   134
lemma NSLIMSEQ_I:
huffman@20751
   135
  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L"
huffman@20751
   136
by (simp add: NSLIMSEQ_def)
huffman@20751
   137
huffman@20751
   138
lemma NSLIMSEQ_D:
huffman@20751
   139
  "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
huffman@20751
   140
by (simp add: NSLIMSEQ_def)
huffman@20751
   141
huffman@20696
   142
lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
huffman@20696
   143
by (simp add: NSLIMSEQ_def)
huffman@20696
   144
huffman@20696
   145
lemma NSLIMSEQ_add:
huffman@20696
   146
      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
huffman@20696
   147
by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
huffman@20696
   148
huffman@20696
   149
lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
huffman@20696
   150
by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
huffman@20696
   151
huffman@20696
   152
lemma NSLIMSEQ_mult:
huffman@20696
   153
  fixes a b :: "'a::real_normed_algebra"
huffman@20696
   154
  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
huffman@20696
   155
by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
huffman@20696
   156
huffman@20696
   157
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
huffman@20696
   158
by (auto simp add: NSLIMSEQ_def)
huffman@20696
   159
huffman@20696
   160
lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
huffman@20696
   161
by (drule NSLIMSEQ_minus, simp)
huffman@20696
   162
huffman@20696
   163
(* FIXME: delete *)
huffman@20696
   164
lemma NSLIMSEQ_add_minus:
huffman@20696
   165
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
huffman@20696
   166
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
huffman@20696
   167
huffman@20696
   168
lemma NSLIMSEQ_diff:
huffman@20696
   169
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
huffman@20696
   170
by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
huffman@20696
   171
huffman@20696
   172
lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
huffman@20696
   173
by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
huffman@20696
   174
huffman@20696
   175
lemma NSLIMSEQ_inverse:
huffman@20696
   176
  fixes a :: "'a::real_normed_div_algebra"
huffman@20696
   177
  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
huffman@20696
   178
by (simp add: NSLIMSEQ_def star_of_approx_inverse)
huffman@20696
   179
huffman@20696
   180
lemma NSLIMSEQ_mult_inverse:
huffman@20696
   181
  fixes a b :: "'a::real_normed_field"
huffman@20696
   182
  shows
huffman@20696
   183
     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
huffman@20696
   184
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
huffman@20696
   185
huffman@20696
   186
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
huffman@20696
   187
by transfer simp
huffman@20696
   188
huffman@20696
   189
lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
huffman@20696
   190
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
huffman@20696
   191
huffman@20696
   192
text{*Uniqueness of limit*}
huffman@20696
   193
lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
huffman@20696
   194
apply (simp add: NSLIMSEQ_def)
huffman@20696
   195
apply (drule HNatInfinite_whn [THEN [2] bspec])+
huffman@20696
   196
apply (auto dest: approx_trans3)
huffman@20696
   197
done
huffman@20696
   198
huffman@20696
   199
lemma NSLIMSEQ_pow [rule_format]:
huffman@20696
   200
  fixes a :: "'a::{real_normed_algebra,recpower}"
huffman@20696
   201
  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
huffman@20696
   202
apply (induct "m")
huffman@20696
   203
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
huffman@20696
   204
done
huffman@20696
   205
huffman@20696
   206
subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
paulson@15082
   207
paulson@15082
   208
lemma LIMSEQ_NSLIMSEQ:
huffman@20751
   209
  assumes X: "X ----> L" shows "X ----NS> L"
huffman@20751
   210
proof (rule NSLIMSEQ_I)
huffman@20751
   211
  fix N assume N: "N \<in> HNatInfinite"
huffman@20751
   212
  have "starfun X N - star_of L \<in> Infinitesimal"
huffman@20751
   213
  proof (rule InfinitesimalI2)
huffman@20751
   214
    fix r::real assume r: "0 < r"
huffman@20751
   215
    from LIMSEQ_D [OF X r]
huffman@20751
   216
    obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
huffman@20751
   217
    hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   218
      by transfer
huffman@20751
   219
    thus "hnorm (starfun X N - star_of L) < star_of r"
huffman@20751
   220
      using N by (simp add: star_of_le_HNatInfinite)
huffman@20751
   221
  qed
huffman@20751
   222
  thus "starfun X N \<approx> star_of L"
huffman@20751
   223
    by (unfold approx_def)
huffman@20751
   224
qed
paulson@15082
   225
huffman@20751
   226
lemma NSLIMSEQ_LIMSEQ:
huffman@20751
   227
  assumes X: "X ----NS> L" shows "X ----> L"
huffman@20751
   228
proof (rule LIMSEQ_I)
huffman@20751
   229
  fix r::real assume r: "0 < r"
huffman@20751
   230
  have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   231
  proof (intro exI allI impI)
huffman@20751
   232
    fix n assume "whn \<le> n"
huffman@20751
   233
    with HNatInfinite_whn have "n \<in> HNatInfinite"
huffman@20751
   234
      by (rule HNatInfinite_upward_closed)
huffman@20751
   235
    with X have "starfun X n \<approx> star_of L"
huffman@20751
   236
      by (rule NSLIMSEQ_D)
huffman@20751
   237
    hence "starfun X n - star_of L \<in> Infinitesimal"
huffman@20751
   238
      by (unfold approx_def)
huffman@20751
   239
    thus "hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   240
      using r by (rule InfinitesimalD2)
huffman@20751
   241
  qed
huffman@20751
   242
  thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
huffman@20751
   243
    by transfer
huffman@20751
   244
qed
paulson@15082
   245
huffman@20751
   246
theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
huffman@20751
   247
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
paulson@15082
   248
huffman@20751
   249
(* Used once by Integration/Rats.thy in AFP *)
paulson@15082
   250
lemma NSLIMSEQ_finite_set:
paulson@15082
   251
     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
huffman@20751
   252
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
paulson@15082
   253
huffman@20696
   254
subsubsection {* Derived theorems about @{term LIMSEQ} *}
paulson@15082
   255
paulson@15082
   256
lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
paulson@15082
   257
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
paulson@15082
   258
avigad@16819
   259
lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
huffman@20685
   260
by (simp add: LIMSEQ_add LIMSEQ_const)
avigad@16819
   261
huffman@20552
   262
lemma LIMSEQ_mult:
huffman@20552
   263
  fixes a b :: "'a::real_normed_algebra"
huffman@20552
   264
  shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
paulson@15082
   265
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
paulson@15082
   266
paulson@15082
   267
lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
paulson@15082
   268
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
paulson@15082
   269
paulson@15082
   270
lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
paulson@15082
   271
by (drule LIMSEQ_minus, simp)
paulson@15082
   272
huffman@20685
   273
(* FIXME: delete *)
paulson@15082
   274
lemma LIMSEQ_add_minus:
paulson@15082
   275
     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
paulson@15082
   276
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)
paulson@15082
   277
paulson@15082
   278
lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
huffman@20685
   279
by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
paulson@15082
   280
avigad@16819
   281
lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
huffman@20685
   282
by (simp add: LIMSEQ_diff LIMSEQ_const)
avigad@16819
   283
paulson@15082
   284
lemma LIMSEQ_inverse:
huffman@20653
   285
  fixes a :: "'a::real_normed_div_algebra"
huffman@20552
   286
  shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
paulson@15082
   287
by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   288
paulson@15082
   289
lemma LIMSEQ_divide:
huffman@20696
   290
  fixes a b :: "'a::real_normed_field"
huffman@20552
   291
  shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
paulson@15082
   292
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
paulson@15082
   293
paulson@15082
   294
lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
paulson@15082
   295
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
paulson@15082
   296
huffman@20696
   297
lemma LIMSEQ_pow:
huffman@20696
   298
  fixes a :: "'a::{real_normed_algebra,recpower}"
huffman@20696
   299
  shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
huffman@20696
   300
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
huffman@20696
   301
nipkow@15312
   302
lemma LIMSEQ_setsum:
nipkow@15312
   303
  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
nipkow@15312
   304
  shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
nipkow@15312
   305
proof (cases "finite S")
nipkow@15312
   306
  case True
nipkow@15312
   307
  thus ?thesis using n
nipkow@15312
   308
  proof (induct)
nipkow@15312
   309
    case empty
nipkow@15312
   310
    show ?case
nipkow@15312
   311
      by (simp add: LIMSEQ_const)
nipkow@15312
   312
  next
nipkow@15312
   313
    case insert
nipkow@15312
   314
    thus ?case
nipkow@15312
   315
      by (simp add: LIMSEQ_add)
nipkow@15312
   316
  qed
nipkow@15312
   317
next
nipkow@15312
   318
  case False
nipkow@15312
   319
  thus ?thesis
nipkow@15312
   320
    by (simp add: setsum_def LIMSEQ_const)
nipkow@15312
   321
qed
nipkow@15312
   322
avigad@16819
   323
lemma LIMSEQ_setprod:
huffman@20552
   324
  fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
avigad@16819
   325
  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
avigad@16819
   326
  shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
avigad@16819
   327
proof (cases "finite S")
avigad@16819
   328
  case True
avigad@16819
   329
  thus ?thesis using n
avigad@16819
   330
  proof (induct)
avigad@16819
   331
    case empty
avigad@16819
   332
    show ?case
avigad@16819
   333
      by (simp add: LIMSEQ_const)
avigad@16819
   334
  next
avigad@16819
   335
    case insert
avigad@16819
   336
    thus ?case
avigad@16819
   337
      by (simp add: LIMSEQ_mult)
avigad@16819
   338
  qed
avigad@16819
   339
next
avigad@16819
   340
  case False
avigad@16819
   341
  thus ?thesis
avigad@16819
   342
    by (simp add: setprod_def LIMSEQ_const)
avigad@16819
   343
qed
avigad@16819
   344
avigad@16819
   345
lemma LIMSEQ_diff_approach_zero: 
avigad@16819
   346
  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
avigad@16819
   347
     f ----> L"
avigad@16819
   348
  apply (drule LIMSEQ_add)
avigad@16819
   349
  apply assumption
avigad@16819
   350
  apply simp
avigad@16819
   351
done
avigad@16819
   352
avigad@16819
   353
lemma LIMSEQ_diff_approach_zero2: 
avigad@16819
   354
  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
avigad@16819
   355
     g ----> L";
avigad@16819
   356
  apply (drule LIMSEQ_diff)
avigad@16819
   357
  apply assumption
avigad@16819
   358
  apply simp
avigad@16819
   359
done
avigad@16819
   360
paulson@15082
   361
huffman@20696
   362
subsection {* Convergence *}
paulson@15082
   363
paulson@15082
   364
lemma limI: "X ----> L ==> lim X = L"
paulson@15082
   365
apply (simp add: lim_def)
paulson@15082
   366
apply (blast intro: LIMSEQ_unique)
paulson@15082
   367
done
paulson@15082
   368
paulson@15082
   369
lemma nslimI: "X ----NS> L ==> nslim X = L"
paulson@15082
   370
apply (simp add: nslim_def)
paulson@15082
   371
apply (blast intro: NSLIMSEQ_unique)
paulson@15082
   372
done
paulson@15082
   373
paulson@15082
   374
lemma lim_nslim_iff: "lim X = nslim X"
paulson@15082
   375
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   376
paulson@15082
   377
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
paulson@15082
   378
by (simp add: convergent_def)
paulson@15082
   379
paulson@15082
   380
lemma convergentI: "(X ----> L) ==> convergent X"
paulson@15082
   381
by (auto simp add: convergent_def)
paulson@15082
   382
paulson@15082
   383
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
paulson@15082
   384
by (simp add: NSconvergent_def)
paulson@15082
   385
paulson@15082
   386
lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
paulson@15082
   387
by (auto simp add: NSconvergent_def)
paulson@15082
   388
paulson@15082
   389
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
paulson@15082
   390
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   391
paulson@15082
   392
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
huffman@20682
   393
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
paulson@15082
   394
paulson@15082
   395
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
huffman@20682
   396
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
paulson@15082
   397
huffman@20696
   398
lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
huffman@20696
   399
apply (simp add: convergent_def)
huffman@20696
   400
apply (auto dest: LIMSEQ_minus)
huffman@20696
   401
apply (drule LIMSEQ_minus, auto)
huffman@20696
   402
done
huffman@20696
   403
huffman@20696
   404
huffman@20696
   405
subsection {* Bounded Monotonic Sequences *}
huffman@20696
   406
paulson@15082
   407
text{*Subsequence (alternative definition, (e.g. Hoskins)*}
paulson@15082
   408
paulson@15082
   409
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
paulson@15082
   410
apply (simp add: subseq_def)
paulson@15082
   411
apply (auto dest!: less_imp_Suc_add)
paulson@15082
   412
apply (induct_tac k)
paulson@15082
   413
apply (auto intro: less_trans)
paulson@15082
   414
done
paulson@15082
   415
paulson@15082
   416
lemma monoseq_Suc:
paulson@15082
   417
   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
paulson@15082
   418
                 | (\<forall>n. X (Suc n) \<le> X n))"
paulson@15082
   419
apply (simp add: monoseq_def)
paulson@15082
   420
apply (auto dest!: le_imp_less_or_eq)
paulson@15082
   421
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
paulson@15082
   422
apply (induct_tac "ka")
paulson@15082
   423
apply (auto intro: order_trans)
wenzelm@18585
   424
apply (erule contrapos_np)
paulson@15082
   425
apply (induct_tac "k")
paulson@15082
   426
apply (auto intro: order_trans)
paulson@15082
   427
done
paulson@15082
   428
nipkow@15360
   429
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
paulson@15082
   430
by (simp add: monoseq_def)
paulson@15082
   431
nipkow@15360
   432
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
paulson@15082
   433
by (simp add: monoseq_def)
paulson@15082
   434
paulson@15082
   435
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
paulson@15082
   436
by (simp add: monoseq_Suc)
paulson@15082
   437
paulson@15082
   438
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
paulson@15082
   439
by (simp add: monoseq_Suc)
paulson@15082
   440
huffman@20696
   441
text{*Bounded Sequence*}
paulson@15082
   442
huffman@20552
   443
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
paulson@15082
   444
by (simp add: Bseq_def)
paulson@15082
   445
huffman@20552
   446
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
paulson@15082
   447
by (auto simp add: Bseq_def)
paulson@15082
   448
paulson@15082
   449
lemma lemma_NBseq_def:
huffman@20552
   450
     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
huffman@20552
   451
      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
paulson@15082
   452
apply auto
paulson@15082
   453
 prefer 2 apply force
paulson@15082
   454
apply (cut_tac x = K in reals_Archimedean2, clarify)
paulson@15082
   455
apply (rule_tac x = n in exI, clarify)
paulson@15082
   456
apply (drule_tac x = na in spec)
paulson@15082
   457
apply (auto simp add: real_of_nat_Suc)
paulson@15082
   458
done
paulson@15082
   459
paulson@15082
   460
text{* alternative definition for Bseq *}
huffman@20552
   461
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
paulson@15082
   462
apply (simp add: Bseq_def)
paulson@15082
   463
apply (simp (no_asm) add: lemma_NBseq_def)
paulson@15082
   464
done
paulson@15082
   465
paulson@15082
   466
lemma lemma_NBseq_def2:
huffman@20552
   467
     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
paulson@15082
   468
apply (subst lemma_NBseq_def, auto)
paulson@15082
   469
apply (rule_tac x = "Suc N" in exI)
paulson@15082
   470
apply (rule_tac [2] x = N in exI)
paulson@15082
   471
apply (auto simp add: real_of_nat_Suc)
paulson@15082
   472
 prefer 2 apply (blast intro: order_less_imp_le)
paulson@15082
   473
apply (drule_tac x = n in spec, simp)
paulson@15082
   474
done
paulson@15082
   475
paulson@15082
   476
(* yet another definition for Bseq *)
huffman@20552
   477
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
paulson@15082
   478
by (simp add: Bseq_def lemma_NBseq_def2)
paulson@15082
   479
huffman@17318
   480
lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
paulson@15082
   481
by (simp add: NSBseq_def)
paulson@15082
   482
huffman@17318
   483
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
paulson@15082
   484
by (simp add: NSBseq_def)
paulson@15082
   485
paulson@15082
   486
text{*The standard definition implies the nonstandard definition*}
paulson@15082
   487
huffman@20552
   488
lemma lemma_Bseq: "\<forall>n. norm (X n) \<le> K ==> \<forall>n. norm(X((f::nat=>nat) n)) \<le> K"
paulson@15082
   489
by auto
paulson@15082
   490
paulson@15082
   491
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
huffman@21139
   492
proof (unfold NSBseq_def, safe)
huffman@21139
   493
  assume X: "Bseq X"
huffman@21139
   494
  fix N assume N: "N \<in> HNatInfinite"
huffman@21139
   495
  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
huffman@21139
   496
  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
huffman@21139
   497
  hence "hnorm (starfun X N) \<le> star_of K" by simp
huffman@21139
   498
  also have "star_of K < star_of (K + 1)" by simp
huffman@21139
   499
  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
huffman@21139
   500
  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
huffman@21139
   501
qed
paulson@15082
   502
paulson@15082
   503
text{*The nonstandard definition implies the standard definition*}
paulson@15082
   504
paulson@15082
   505
(* similar to NSLIM proof in REALTOPOS *)
paulson@15082
   506
paulson@15082
   507
text{* We need to get rid of the real variable and do so by proving the
paulson@15082
   508
   following, which relies on the Archimedean property of the reals.
paulson@15082
   509
   When we skolemize we then get the required function @{term "f::nat=>nat"}.
paulson@15082
   510
   Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
paulson@15082
   511
   which woulid be useless.*}
paulson@15082
   512
paulson@15082
   513
lemma lemmaNSBseq:
huffman@20552
   514
     "\<forall>K > 0. \<exists>n. K < norm (X n)
huffman@20552
   515
      ==> \<forall>N. \<exists>n. real(Suc N) < norm (X n)"
paulson@15082
   516
apply safe
paulson@15082
   517
apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
paulson@15082
   518
done
paulson@15082
   519
huffman@20552
   520
lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n::nat. K < norm (X n)
huffman@20552
   521
                     ==> \<exists>f. \<forall>N. real(Suc N) < norm (X (f N))"
paulson@15082
   522
apply (drule lemmaNSBseq)
huffman@20552
   523
apply (drule no_choice, blast)
paulson@15082
   524
done
paulson@15082
   525
paulson@15082
   526
lemma real_seq_to_hypreal_HInfinite:
huffman@20552
   527
     "\<forall>N. real(Suc N) < norm (X (f N))
huffman@17318
   528
      ==>  star_n (X o f) : HInfinite"
paulson@15082
   529
apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
paulson@15082
   530
apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
paulson@15082
   531
apply (drule FreeUltrafilterNat_all)
paulson@15082
   532
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
paulson@15082
   533
apply (auto simp add: real_of_nat_Suc)
paulson@15082
   534
done
paulson@15082
   535
paulson@15082
   536
text{* Now prove that we can get out an infinite hypernatural as well
paulson@15082
   537
     defined using the skolem function  @{term "f::nat=>nat"} above*}
paulson@15082
   538
paulson@15082
   539
lemma lemma_finite_NSBseq:
huffman@20552
   540
     "{n. f n \<le> Suc u & real(Suc n) < norm (X (f n))} \<le>
huffman@20552
   541
      {n. f n \<le> u & real(Suc n) < norm (X (f n))} Un
huffman@20552
   542
      {n. real(Suc n) < norm (X (Suc u))}"
paulson@15082
   543
by (auto dest!: le_imp_less_or_eq)
paulson@15082
   544
paulson@15082
   545
lemma lemma_finite_NSBseq2:
huffman@20552
   546
     "finite {n. f n \<le> (u::nat) &  real(Suc n) < norm (X(f n))}"
paulson@15251
   547
apply (induct "u")
paulson@15082
   548
apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
huffman@20552
   549
apply (rule_tac B = "{n. real (Suc n) < norm (X 0) }" in finite_subset)
paulson@15082
   550
apply (auto intro: finite_real_of_nat_less_real 
paulson@15082
   551
            simp add: real_of_nat_Suc less_diff_eq [symmetric])
paulson@15082
   552
done
paulson@15082
   553
paulson@15082
   554
lemma HNatInfinite_skolem_f:
huffman@20552
   555
     "\<forall>N. real(Suc N) < norm (X (f N))
huffman@17318
   556
      ==> star_n f : HNatInfinite"
paulson@15082
   557
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
paulson@15082
   558
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
paulson@15082
   559
apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
huffman@20552
   560
apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < norm (X (f n))} =
huffman@20552
   561
                    {n. f n \<le> u} \<inter> {N. real (Suc N) < norm (X (f N))}")
paulson@15082
   562
apply (erule ssubst) 
paulson@15082
   563
 apply (auto simp add: linorder_not_less Compl_def)
paulson@15082
   564
done
paulson@15082
   565
paulson@15082
   566
lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
paulson@15082
   567
apply (simp add: Bseq_def NSBseq_def)
paulson@15082
   568
apply (rule ccontr)
paulson@15082
   569
apply (auto simp add: linorder_not_less [symmetric])
paulson@15082
   570
apply (drule lemmaNSBseq2, safe)
paulson@15082
   571
apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
paulson@15082
   572
apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
huffman@17318
   573
apply (auto simp add: starfun o_def HFinite_HInfinite_iff)
paulson@15082
   574
done
paulson@15082
   575
paulson@15082
   576
text{* Equivalence of nonstandard and standard definitions
paulson@15082
   577
  for a bounded sequence*}
paulson@15082
   578
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
paulson@15082
   579
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
paulson@15082
   580
paulson@15082
   581
text{*A convergent sequence is bounded: 
paulson@15082
   582
 Boundedness as a necessary condition for convergence. 
paulson@15082
   583
 The nonstandard version has no existential, as usual *}
paulson@15082
   584
paulson@15082
   585
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
paulson@15082
   586
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
huffman@20552
   587
apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
paulson@15082
   588
done
paulson@15082
   589
paulson@15082
   590
text{*Standard Version: easily now proved using equivalence of NS and
paulson@15082
   591
 standard definitions *}
paulson@15082
   592
lemma convergent_Bseq: "convergent X ==> Bseq X"
paulson@15082
   593
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
paulson@15082
   594
huffman@20696
   595
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
paulson@15082
   596
paulson@15082
   597
lemma Bseq_isUb:
paulson@15082
   598
  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
paulson@15082
   599
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
paulson@15082
   600
paulson@15082
   601
paulson@15082
   602
text{* Use completeness of reals (supremum property)
paulson@15082
   603
   to show that any bounded sequence has a least upper bound*}
paulson@15082
   604
paulson@15082
   605
lemma Bseq_isLub:
paulson@15082
   606
  "!!(X::nat=>real). Bseq X ==>
paulson@15082
   607
   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
paulson@15082
   608
by (blast intro: reals_complete Bseq_isUb)
paulson@15082
   609
huffman@20552
   610
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
paulson@15082
   611
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
paulson@15082
   612
huffman@20552
   613
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
paulson@15082
   614
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
paulson@15082
   615
paulson@15082
   616
huffman@20696
   617
subsubsection{*A Bounded and Monotonic Sequence Converges*}
paulson@15082
   618
paulson@15082
   619
lemma lemma_converg1:
nipkow@15360
   620
     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
paulson@15082
   621
                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
nipkow@15360
   622
               |] ==> \<forall>n \<ge> ma. X n = X ma"
paulson@15082
   623
apply safe
paulson@15082
   624
apply (drule_tac y = "X n" in isLubD2)
paulson@15082
   625
apply (blast dest: order_antisym)+
paulson@15082
   626
done
paulson@15082
   627
paulson@15082
   628
text{* The best of both worlds: Easier to prove this result as a standard
paulson@15082
   629
   theorem and then use equivalence to "transfer" it into the
paulson@15082
   630
   equivalent nonstandard form if needed!*}
paulson@15082
   631
paulson@15082
   632
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
paulson@15082
   633
apply (simp add: LIMSEQ_def)
paulson@15082
   634
apply (rule_tac x = "X m" in exI, safe)
paulson@15082
   635
apply (rule_tac x = m in exI, safe)
paulson@15082
   636
apply (drule spec, erule impE, auto)
paulson@15082
   637
done
paulson@15082
   638
paulson@15082
   639
text{*Now, the same theorem in terms of NS limit *}
nipkow@15360
   640
lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
paulson@15082
   641
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   642
paulson@15082
   643
lemma lemma_converg2:
paulson@15082
   644
   "!!(X::nat=>real).
paulson@15082
   645
    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
paulson@15082
   646
apply safe
paulson@15082
   647
apply (drule_tac y = "X m" in isLubD2)
paulson@15082
   648
apply (auto dest!: order_le_imp_less_or_eq)
paulson@15082
   649
done
paulson@15082
   650
paulson@15082
   651
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
paulson@15082
   652
by (rule setleI [THEN isUbI], auto)
paulson@15082
   653
paulson@15082
   654
text{* FIXME: @{term "U - T < U"} is redundant *}
paulson@15082
   655
lemma lemma_converg4: "!!(X::nat=> real).
paulson@15082
   656
               [| \<forall>m. X m ~= U;
paulson@15082
   657
                  isLub UNIV {x. \<exists>n. X n = x} U;
paulson@15082
   658
                  0 < T;
paulson@15082
   659
                  U + - T < U
paulson@15082
   660
               |] ==> \<exists>m. U + -T < X m & X m < U"
paulson@15082
   661
apply (drule lemma_converg2, assumption)
paulson@15082
   662
apply (rule ccontr, simp)
paulson@15082
   663
apply (simp add: linorder_not_less)
paulson@15082
   664
apply (drule lemma_converg3)
paulson@15082
   665
apply (drule isLub_le_isUb, assumption)
paulson@15082
   666
apply (auto dest: order_less_le_trans)
paulson@15082
   667
done
paulson@15082
   668
paulson@15082
   669
text{*A standard proof of the theorem for monotone increasing sequence*}
paulson@15082
   670
paulson@15082
   671
lemma Bseq_mono_convergent:
huffman@20552
   672
     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
paulson@15082
   673
apply (simp add: convergent_def)
paulson@15082
   674
apply (frule Bseq_isLub, safe)
paulson@15082
   675
apply (case_tac "\<exists>m. X m = U", auto)
paulson@15082
   676
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
paulson@15082
   677
(* second case *)
paulson@15082
   678
apply (rule_tac x = U in exI)
paulson@15082
   679
apply (subst LIMSEQ_iff, safe)
paulson@15082
   680
apply (frule lemma_converg2, assumption)
paulson@15082
   681
apply (drule lemma_converg4, auto)
paulson@15082
   682
apply (rule_tac x = m in exI, safe)
paulson@15082
   683
apply (subgoal_tac "X m \<le> X n")
paulson@15082
   684
 prefer 2 apply blast
paulson@15082
   685
apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
paulson@15082
   686
done
paulson@15082
   687
paulson@15082
   688
text{*Nonstandard version of the theorem*}
paulson@15082
   689
paulson@15082
   690
lemma NSBseq_mono_NSconvergent:
huffman@20552
   691
     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
paulson@15082
   692
by (auto intro: Bseq_mono_convergent 
paulson@15082
   693
         simp add: convergent_NSconvergent_iff [symmetric] 
paulson@15082
   694
                   Bseq_NSBseq_iff [symmetric])
paulson@15082
   695
paulson@15082
   696
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
paulson@15082
   697
by (simp add: Bseq_def)
paulson@15082
   698
paulson@15082
   699
text{*Main monotonicity theorem*}
paulson@15082
   700
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
paulson@15082
   701
apply (simp add: monoseq_def, safe)
paulson@15082
   702
apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
paulson@15082
   703
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
paulson@15082
   704
apply (auto intro!: Bseq_mono_convergent)
paulson@15082
   705
done
paulson@15082
   706
huffman@20696
   707
subsubsection{*A Few More Equivalence Theorems for Boundedness*}
paulson@15082
   708
paulson@15082
   709
text{*alternative formulation for boundedness*}
huffman@20552
   710
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
paulson@15082
   711
apply (unfold Bseq_def, safe)
huffman@20552
   712
apply (rule_tac [2] x = "k + norm x" in exI)
nipkow@15360
   713
apply (rule_tac x = K in exI, simp)
paulson@15221
   714
apply (rule exI [where x = 0], auto)
huffman@20552
   715
apply (erule order_less_le_trans, simp)
huffman@20552
   716
apply (drule_tac x=n in spec, fold diff_def)
huffman@20552
   717
apply (drule order_trans [OF norm_triangle_ineq2])
huffman@20552
   718
apply simp
paulson@15082
   719
done
paulson@15082
   720
paulson@15082
   721
text{*alternative formulation for boundedness*}
huffman@20552
   722
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
paulson@15082
   723
apply safe
paulson@15082
   724
apply (simp add: Bseq_def, safe)
huffman@20552
   725
apply (rule_tac x = "K + norm (X N)" in exI)
paulson@15082
   726
apply auto
huffman@20552
   727
apply (erule order_less_le_trans, simp)
paulson@15082
   728
apply (rule_tac x = N in exI, safe)
huffman@20552
   729
apply (drule_tac x = n in spec)
huffman@20552
   730
apply (rule order_trans [OF norm_triangle_ineq], simp)
paulson@15082
   731
apply (auto simp add: Bseq_iff2)
paulson@15082
   732
done
paulson@15082
   733
huffman@20552
   734
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
paulson@15082
   735
apply (simp add: Bseq_def)
paulson@15221
   736
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
webertj@20217
   737
apply (drule_tac x = n in spec, arith)
paulson@15082
   738
done
paulson@15082
   739
paulson@15082
   740
huffman@20696
   741
subsection {* Cauchy Sequences *}
paulson@15082
   742
huffman@20751
   743
lemma CauchyI:
huffman@20751
   744
  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
huffman@20751
   745
by (simp add: Cauchy_def)
huffman@20751
   746
huffman@20751
   747
lemma CauchyD:
huffman@20751
   748
  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
huffman@20751
   749
by (simp add: Cauchy_def)
huffman@20751
   750
huffman@20751
   751
lemma NSCauchyI:
huffman@20751
   752
  "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
huffman@20751
   753
   \<Longrightarrow> NSCauchy X"
huffman@20751
   754
by (simp add: NSCauchy_def)
huffman@20751
   755
huffman@20751
   756
lemma NSCauchyD:
huffman@20751
   757
  "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
huffman@20751
   758
   \<Longrightarrow> starfun X M \<approx> starfun X N"
huffman@20751
   759
by (simp add: NSCauchy_def)
huffman@20751
   760
huffman@20696
   761
subsubsection{*Equivalence Between NS and Standard*}
huffman@20696
   762
huffman@20751
   763
lemma Cauchy_NSCauchy:
huffman@20751
   764
  assumes X: "Cauchy X" shows "NSCauchy X"
huffman@20751
   765
proof (rule NSCauchyI)
huffman@20751
   766
  fix M assume M: "M \<in> HNatInfinite"
huffman@20751
   767
  fix N assume N: "N \<in> HNatInfinite"
huffman@20751
   768
  have "starfun X M - starfun X N \<in> Infinitesimal"
huffman@20751
   769
  proof (rule InfinitesimalI2)
huffman@20751
   770
    fix r :: real assume r: "0 < r"
huffman@20751
   771
    from CauchyD [OF X r]
huffman@20751
   772
    obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
huffman@20751
   773
    hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
huffman@20751
   774
           hnorm (starfun X m - starfun X n) < star_of r"
huffman@20751
   775
      by transfer
huffman@20751
   776
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@20751
   777
      using M N by (simp add: star_of_le_HNatInfinite)
huffman@20751
   778
  qed
huffman@20751
   779
  thus "starfun X M \<approx> starfun X N"
huffman@20751
   780
    by (unfold approx_def)
huffman@20751
   781
qed
paulson@15082
   782
huffman@20751
   783
lemma NSCauchy_Cauchy:
huffman@20751
   784
  assumes X: "NSCauchy X" shows "Cauchy X"
huffman@20751
   785
proof (rule CauchyI)
huffman@20751
   786
  fix r::real assume r: "0 < r"
huffman@20751
   787
  have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
huffman@20751
   788
  proof (intro exI allI impI)
huffman@20751
   789
    fix M assume "whn \<le> M"
huffman@20751
   790
    with HNatInfinite_whn have M: "M \<in> HNatInfinite"
huffman@20751
   791
      by (rule HNatInfinite_upward_closed)
huffman@20751
   792
    fix N assume "whn \<le> N"
huffman@20751
   793
    with HNatInfinite_whn have N: "N \<in> HNatInfinite"
huffman@20751
   794
      by (rule HNatInfinite_upward_closed)
huffman@20751
   795
    from X M N have "starfun X M \<approx> starfun X N"
huffman@20751
   796
      by (rule NSCauchyD)
huffman@20751
   797
    hence "starfun X M - starfun X N \<in> Infinitesimal"
huffman@20751
   798
      by (unfold approx_def)
huffman@20751
   799
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@20751
   800
      using r by (rule InfinitesimalD2)
huffman@20751
   801
  qed
huffman@20751
   802
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
huffman@20751
   803
    by transfer
huffman@20751
   804
qed
paulson@15082
   805
paulson@15082
   806
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
paulson@15082
   807
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
paulson@15082
   808
huffman@20696
   809
subsubsection {* Cauchy Sequences are Bounded *}
huffman@20696
   810
paulson@15082
   811
text{*A Cauchy sequence is bounded -- this is the standard
paulson@15082
   812
  proof mechanization rather than the nonstandard proof*}
paulson@15082
   813
huffman@20563
   814
lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
huffman@20552
   815
          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
huffman@20552
   816
apply (clarify, drule spec, drule (1) mp)
huffman@20563
   817
apply (simp only: norm_minus_commute)
huffman@20552
   818
apply (drule order_le_less_trans [OF norm_triangle_ineq2])
huffman@20552
   819
apply simp
huffman@20552
   820
done
paulson@15082
   821
huffman@20552
   822
lemma Bseq_Suc_imp_Bseq: "Bseq (\<lambda>n. X (Suc n)) \<Longrightarrow> Bseq X"
huffman@20552
   823
apply (unfold Bseq_def, clarify)
huffman@20552
   824
apply (rule_tac x="max K (norm (X 0))" in exI)
huffman@20552
   825
apply (simp add: order_less_le_trans [OF _ le_maxI1])
huffman@20552
   826
apply (clarify, case_tac "n", simp)
huffman@20552
   827
apply (simp add: order_trans [OF _ le_maxI1])
huffman@20552
   828
done
huffman@20552
   829
huffman@20552
   830
lemma Bseq_shift_imp_Bseq: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
huffman@20552
   831
apply (induct k, simp_all)
huffman@20552
   832
apply (subgoal_tac "Bseq (\<lambda>n. X (n + k))", simp)
huffman@20552
   833
apply (rule Bseq_Suc_imp_Bseq, simp)
huffman@20552
   834
done
huffman@20552
   835
paulson@15082
   836
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
huffman@20552
   837
apply (simp add: Cauchy_def)
huffman@20552
   838
apply (drule spec, drule mp, rule zero_less_one, safe)
huffman@20552
   839
apply (drule_tac x="M" in spec, simp)
paulson@15082
   840
apply (drule lemmaCauchy)
huffman@20552
   841
apply (rule_tac k="M" in Bseq_shift_imp_Bseq)
huffman@20552
   842
apply (simp add: Bseq_def)
huffman@20552
   843
apply (rule_tac x="1 + norm (X M)" in exI)
huffman@20552
   844
apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
huffman@20552
   845
apply (simp add: order_less_imp_le)
paulson@15082
   846
done
paulson@15082
   847
paulson@15082
   848
text{*A Cauchy sequence is bounded -- nonstandard version*}
paulson@15082
   849
paulson@15082
   850
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
paulson@15082
   851
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
paulson@15082
   852
huffman@20696
   853
subsubsection {* Cauchy Sequences are Convergent *}
paulson@15082
   854
huffman@20830
   855
axclass banach \<subseteq> real_normed_vector
huffman@20830
   856
  Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
huffman@20830
   857
paulson@15082
   858
text{*Equivalence of Cauchy criterion and convergence:
paulson@15082
   859
  We will prove this using our NS formulation which provides a
paulson@15082
   860
  much easier proof than using the standard definition. We do not
paulson@15082
   861
  need to use properties of subsequences such as boundedness,
paulson@15082
   862
  monotonicity etc... Compare with Harrison's corresponding proof
paulson@15082
   863
  in HOL which is much longer and more complicated. Of course, we do
paulson@15082
   864
  not have problems which he encountered with guessing the right
paulson@15082
   865
  instantiations for his 'espsilon-delta' proof(s) in this case
paulson@15082
   866
  since the NS formulations do not involve existential quantifiers.*}
paulson@15082
   867
huffman@20691
   868
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
huffman@20691
   869
apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
huffman@20691
   870
apply (auto intro: approx_trans2)
huffman@20691
   871
done
huffman@20691
   872
huffman@20691
   873
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
huffman@20691
   874
apply (rule NSconvergent_NSCauchy [THEN NSCauchy_Cauchy])
huffman@20691
   875
apply (simp add: convergent_NSconvergent_iff)
huffman@20691
   876
done
huffman@20691
   877
huffman@20830
   878
lemma real_NSCauchy_NSconvergent:
huffman@20830
   879
  fixes X :: "nat \<Rightarrow> real"
huffman@20830
   880
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@20830
   881
apply (simp add: NSconvergent_def NSLIMSEQ_def)
paulson@15082
   882
apply (frule NSCauchy_NSBseq)
huffman@20830
   883
apply (simp add: NSBseq_def NSCauchy_def)
paulson@15082
   884
apply (drule HNatInfinite_whn [THEN [2] bspec])
paulson@15082
   885
apply (drule HNatInfinite_whn [THEN [2] bspec])
paulson@15082
   886
apply (auto dest!: st_part_Ex simp add: SReal_iff)
paulson@15082
   887
apply (blast intro: approx_trans3)
paulson@15082
   888
done
paulson@15082
   889
paulson@15082
   890
text{*Standard proof for free*}
huffman@20830
   891
lemma real_Cauchy_convergent:
huffman@20830
   892
  fixes X :: "nat \<Rightarrow> real"
huffman@20830
   893
  shows "Cauchy X \<Longrightarrow> convergent X"
huffman@20830
   894
apply (drule Cauchy_NSCauchy [THEN real_NSCauchy_NSconvergent])
huffman@20830
   895
apply (erule convergent_NSconvergent_iff [THEN iffD2])
huffman@20830
   896
done
huffman@20830
   897
huffman@20830
   898
instance real :: banach
huffman@20830
   899
by intro_classes (rule real_Cauchy_convergent)
huffman@20830
   900
huffman@20830
   901
lemma NSCauchy_NSconvergent:
huffman@20830
   902
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
   903
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@20830
   904
apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
huffman@20830
   905
apply (erule convergent_NSconvergent_iff [THEN iffD1])
huffman@20830
   906
done
huffman@20830
   907
huffman@20830
   908
lemma NSCauchy_NSconvergent_iff:
huffman@20830
   909
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
   910
  shows "NSCauchy X = NSconvergent X"
huffman@20830
   911
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
huffman@20830
   912
huffman@20830
   913
lemma Cauchy_convergent_iff:
huffman@20830
   914
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
   915
  shows "Cauchy X = convergent X"
huffman@20830
   916
by (fast intro: Cauchy_convergent convergent_Cauchy)
paulson@15082
   917
paulson@15082
   918
huffman@20696
   919
subsection {* More Properties of Sequences *}
huffman@20696
   920
paulson@15082
   921
text{*We can now try and derive a few properties of sequences,
paulson@15082
   922
     starting with the limit comparison property for sequences.*}
paulson@15082
   923
paulson@15082
   924
lemma NSLIMSEQ_le:
paulson@15082
   925
       "[| f ----NS> l; g ----NS> m;
nipkow@15360
   926
           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
huffman@20552
   927
        |] ==> l \<le> (m::real)"
paulson@15082
   928
apply (simp add: NSLIMSEQ_def, safe)
paulson@15082
   929
apply (drule starfun_le_mono)
paulson@15082
   930
apply (drule HNatInfinite_whn [THEN [2] bspec])+
paulson@15082
   931
apply (drule_tac x = whn in spec)
paulson@15082
   932
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
paulson@15082
   933
apply clarify
paulson@15082
   934
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
paulson@15082
   935
done
paulson@15082
   936
paulson@15082
   937
(* standard version *)
paulson@15082
   938
lemma LIMSEQ_le:
nipkow@15360
   939
     "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
huffman@20552
   940
      ==> l \<le> (m::real)"
paulson@15082
   941
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
paulson@15082
   942
huffman@20552
   943
lemma LIMSEQ_le_const: "[| X ----> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
paulson@15082
   944
apply (rule LIMSEQ_le)
paulson@15082
   945
apply (rule LIMSEQ_const, auto)
paulson@15082
   946
done
paulson@15082
   947
huffman@20552
   948
lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
paulson@15082
   949
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
paulson@15082
   950
huffman@20552
   951
lemma LIMSEQ_le_const2: "[| X ----> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
paulson@15082
   952
apply (rule LIMSEQ_le)
paulson@15082
   953
apply (rule_tac [2] LIMSEQ_const, auto)
paulson@15082
   954
done
paulson@15082
   955
huffman@20552
   956
lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
paulson@15082
   957
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
paulson@15082
   958
paulson@15082
   959
text{*Shift a convergent series by 1:
paulson@15082
   960
  By the equivalence between Cauchiness and convergence and because
paulson@15082
   961
  the successor of an infinite hypernatural is also infinite.*}
paulson@15082
   962
paulson@15082
   963
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
huffman@20552
   964
apply (unfold NSLIMSEQ_def, safe)
huffman@20552
   965
apply (drule_tac x="N + 1" in bspec)
huffman@20740
   966
apply (erule HNatInfinite_add)
huffman@20552
   967
apply (simp add: starfun_shift_one)
paulson@15082
   968
done
paulson@15082
   969
paulson@15082
   970
text{* standard version *}
paulson@15082
   971
lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
paulson@15082
   972
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
paulson@15082
   973
paulson@15082
   974
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
huffman@20552
   975
apply (unfold NSLIMSEQ_def, safe)
paulson@15082
   976
apply (drule_tac x="N - 1" in bspec) 
huffman@20740
   977
apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
huffman@20740
   978
apply (simp add: starfun_shift_one one_le_HNatInfinite)
paulson@15082
   979
done
paulson@15082
   980
paulson@15082
   981
lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
paulson@15082
   982
apply (simp add: LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   983
apply (erule NSLIMSEQ_imp_Suc)
paulson@15082
   984
done
paulson@15082
   985
paulson@15082
   986
lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
paulson@15082
   987
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
paulson@15082
   988
paulson@15082
   989
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
paulson@15082
   990
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
paulson@15082
   991
paulson@15082
   992
text{*A sequence tends to zero iff its abs does*}
huffman@20685
   993
lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)"
huffman@20685
   994
by (simp add: LIMSEQ_def)
huffman@20685
   995
huffman@20552
   996
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
paulson@15082
   997
by (simp add: LIMSEQ_def)
paulson@15082
   998
paulson@15082
   999
text{*We prove the NS version from the standard one, since the NS proof
paulson@15082
  1000
   seems more complicated than the standard one above!*}
huffman@20685
  1001
lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)"
huffman@20685
  1002
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero)
huffman@20685
  1003
huffman@20552
  1004
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
paulson@15082
  1005
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
paulson@15082
  1006
paulson@15082
  1007
text{*Generalization to other limits*}
huffman@20552
  1008
lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
paulson@15082
  1009
apply (simp add: NSLIMSEQ_def)
paulson@15082
  1010
apply (auto intro: approx_hrabs 
huffman@17318
  1011
            simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
paulson@15082
  1012
done
paulson@15082
  1013
paulson@15082
  1014
text{* standard version *}
huffman@20552
  1015
lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
paulson@15082
  1016
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
paulson@15082
  1017
paulson@15082
  1018
text{*An unbounded sequence's inverse tends to 0*}
paulson@15082
  1019
paulson@15082
  1020
text{* standard proof seems easier *}
paulson@15082
  1021
lemma LIMSEQ_inverse_zero:
huffman@20552
  1022
      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
paulson@15082
  1023
apply (simp add: LIMSEQ_def, safe)
paulson@15082
  1024
apply (drule_tac x = "inverse r" in spec, safe)
paulson@15082
  1025
apply (rule_tac x = N in exI, safe)
paulson@15082
  1026
apply (drule spec, auto)
paulson@15082
  1027
apply (frule positive_imp_inverse_positive)
paulson@15082
  1028
apply (frule order_less_trans, assumption)
paulson@15082
  1029
apply (frule_tac a = "f n" in positive_imp_inverse_positive)
paulson@15082
  1030
apply (simp add: abs_if) 
paulson@15082
  1031
apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
paulson@15082
  1032
apply (auto intro: inverse_less_iff_less [THEN iffD2]
paulson@15082
  1033
            simp del: inverse_inverse_eq)
paulson@15082
  1034
done
paulson@15082
  1035
paulson@15082
  1036
lemma NSLIMSEQ_inverse_zero:
huffman@20552
  1037
     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
paulson@15082
  1038
      ==> (%n. inverse(f n)) ----NS> 0"
paulson@15082
  1039
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
paulson@15082
  1040
paulson@15082
  1041
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
paulson@15082
  1042
paulson@15082
  1043
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
paulson@15082
  1044
apply (rule LIMSEQ_inverse_zero, safe)
paulson@15082
  1045
apply (cut_tac x = y in reals_Archimedean2)
paulson@15082
  1046
apply (safe, rule_tac x = n in exI)
paulson@15082
  1047
apply (auto simp add: real_of_nat_Suc)
paulson@15082
  1048
done
paulson@15082
  1049
paulson@15082
  1050
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
paulson@15082
  1051
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
paulson@15082
  1052
paulson@15082
  1053
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
paulson@15082
  1054
infinity is now easily proved*}
paulson@15082
  1055
paulson@15082
  1056
lemma LIMSEQ_inverse_real_of_nat_add:
paulson@15082
  1057
     "(%n. r + inverse(real(Suc n))) ----> r"
paulson@15082
  1058
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
paulson@15082
  1059
paulson@15082
  1060
lemma NSLIMSEQ_inverse_real_of_nat_add:
paulson@15082
  1061
     "(%n. r + inverse(real(Suc n))) ----NS> r"
paulson@15082
  1062
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
paulson@15082
  1063
paulson@15082
  1064
lemma LIMSEQ_inverse_real_of_nat_add_minus:
paulson@15082
  1065
     "(%n. r + -inverse(real(Suc n))) ----> r"
paulson@15082
  1066
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
paulson@15082
  1067
paulson@15082
  1068
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
paulson@15082
  1069
     "(%n. r + -inverse(real(Suc n))) ----NS> r"
paulson@15082
  1070
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
paulson@15082
  1071
paulson@15082
  1072
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
paulson@15082
  1073
     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
paulson@15082
  1074
by (cut_tac b=1 in
paulson@15082
  1075
        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
paulson@15082
  1076
paulson@15082
  1077
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
paulson@15082
  1078
     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
paulson@15082
  1079
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
paulson@15082
  1080
paulson@15082
  1081
huffman@20696
  1082
subsection {* Power Sequences *}
paulson@15082
  1083
paulson@15082
  1084
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
paulson@15082
  1085
"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
paulson@15082
  1086
  also fact that bounded and monotonic sequence converges.*}
paulson@15082
  1087
huffman@20552
  1088
lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
paulson@15082
  1089
apply (simp add: Bseq_def)
paulson@15082
  1090
apply (rule_tac x = 1 in exI)
paulson@15082
  1091
apply (simp add: power_abs)
paulson@15082
  1092
apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
paulson@15082
  1093
done
paulson@15082
  1094
paulson@15082
  1095
lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
paulson@15082
  1096
apply (clarify intro!: mono_SucI2)
paulson@15082
  1097
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
paulson@15082
  1098
done
paulson@15082
  1099
huffman@20552
  1100
lemma convergent_realpow:
huffman@20552
  1101
  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
paulson@15082
  1102
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
paulson@15082
  1103
paulson@15082
  1104
text{* We now use NS criterion to bring proof of theorem through *}
paulson@15082
  1105
huffman@20552
  1106
lemma NSLIMSEQ_realpow_zero:
huffman@20552
  1107
  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
paulson@15082
  1108
apply (simp add: NSLIMSEQ_def)
paulson@15082
  1109
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
paulson@15082
  1110
apply (frule NSconvergentD)
huffman@17318
  1111
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
paulson@15082
  1112
apply (frule HNatInfinite_add_one)
paulson@15082
  1113
apply (drule bspec, assumption)
paulson@15082
  1114
apply (drule bspec, assumption)
paulson@15082
  1115
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
paulson@15082
  1116
apply (simp add: hyperpow_add)
paulson@15082
  1117
apply (drule approx_mult_subst_SReal, assumption)
paulson@15082
  1118
apply (drule approx_trans3, assumption)
huffman@17318
  1119
apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
paulson@15082
  1120
done
paulson@15082
  1121
paulson@15082
  1122
text{* standard version *}
huffman@20552
  1123
lemma LIMSEQ_realpow_zero:
huffman@20552
  1124
  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0"
paulson@15082
  1125
by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
paulson@15082
  1126
huffman@20685
  1127
lemma LIMSEQ_power_zero:
huffman@20685
  1128
  fixes x :: "'a::{real_normed_div_algebra,recpower}"
huffman@20685
  1129
  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
huffman@20685
  1130
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
huffman@20685
  1131
apply (simp add: norm_power [symmetric] LIMSEQ_norm_zero)
huffman@20685
  1132
done
huffman@20685
  1133
huffman@20552
  1134
lemma LIMSEQ_divide_realpow_zero:
huffman@20552
  1135
  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
paulson@15082
  1136
apply (cut_tac a = a and x1 = "inverse x" in
paulson@15082
  1137
        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
paulson@15082
  1138
apply (auto simp add: divide_inverse power_inverse)
paulson@15082
  1139
apply (simp add: inverse_eq_divide pos_divide_less_eq)
paulson@15082
  1140
done
paulson@15082
  1141
paulson@15102
  1142
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
paulson@15082
  1143
huffman@20552
  1144
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
huffman@20685
  1145
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
paulson@15082
  1146
huffman@20552
  1147
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
paulson@15082
  1148
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
paulson@15082
  1149
huffman@20552
  1150
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
paulson@15082
  1151
apply (rule LIMSEQ_rabs_zero [THEN iffD1])
paulson@15082
  1152
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
paulson@15082
  1153
done
paulson@15082
  1154
huffman@20552
  1155
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
paulson@15082
  1156
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
paulson@15082
  1157
paulson@15082
  1158
subsection{*Hyperreals and Sequences*}
paulson@15082
  1159
paulson@15082
  1160
text{*A bounded sequence is a finite hyperreal*}
huffman@17318
  1161
lemma NSBseq_HFinite_hypreal: "NSBseq X ==> star_n X : HFinite"
huffman@17298
  1162
by (auto intro!: bexI lemma_starrel_refl 
paulson@15082
  1163
            intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
paulson@15082
  1164
            simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
paulson@15082
  1165
                      Bseq_iff1a)
paulson@15082
  1166
paulson@15082
  1167
text{*A sequence converging to zero defines an infinitesimal*}
paulson@15082
  1168
lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
huffman@17318
  1169
      "X ----NS> 0 ==> star_n X : Infinitesimal"
paulson@15082
  1170
apply (simp add: NSLIMSEQ_def)
paulson@15082
  1171
apply (drule_tac x = whn in bspec)
paulson@15082
  1172
apply (simp add: HNatInfinite_whn)
huffman@17318
  1173
apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfun)
paulson@15082
  1174
done
paulson@15082
  1175
paulson@15082
  1176
(***---------------------------------------------------------------
paulson@15082
  1177
    Theorems proved by Harrison in HOL that we do not need
paulson@15082
  1178
    in order to prove equivalence between Cauchy criterion
paulson@15082
  1179
    and convergence:
paulson@15082
  1180
 -- Show that every sequence contains a monotonic subsequence
paulson@15082
  1181
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
paulson@15082
  1182
 -- Show that a subsequence of a bounded sequence is bounded
paulson@15082
  1183
Goal "Bseq X ==> Bseq (%n. X (f n))";
paulson@15082
  1184
 -- Show we can take subsequential terms arbitrarily far
paulson@15082
  1185
    up a sequence
paulson@15082
  1186
Goal "subseq f ==> n \<le> f(n)";
paulson@15082
  1187
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
paulson@15082
  1188
 ---------------------------------------------------------------***)
paulson@15082
  1189
paulson@10751
  1190
end