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