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