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