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