src/HOL/Hyperreal/SEQ.thy
author huffman
Tue Apr 10 22:02:43 2007 +0200 (2007-04-10)
changeset 22628 0e5ac9503d7e
parent 22615 d650e51b5970
child 22629 73771f454861
permissions -rw-r--r--
new standard proof of LIMSEQ_realpow_zero
paulson@10751
     1
(*  Title       : SEQ.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@10751
     4
    Description : Convergence of sequences and series
paulson@15082
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
huffman@22608
     6
    Additional contributions by Jeremy Avigad and Brian Huffman
paulson@15082
     7
*)
paulson@10751
     8
huffman@17439
     9
header {* Sequences and Series *}
huffman@17439
    10
nipkow@15131
    11
theory SEQ
nipkow@15236
    12
imports NatStar
nipkow@15131
    13
begin
paulson@10751
    14
wenzelm@19765
    15
definition
huffman@22608
    16
  Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
huffman@22608
    17
    --{*Standard definition of sequence converging to zero*}
huffman@22608
    18
  "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
huffman@22608
    19
huffman@22608
    20
definition
huffman@20552
    21
  LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
wenzelm@21404
    22
    ("((_)/ ----> (_))" [60, 60] 60) where
paulson@15082
    23
    --{*Standard definition of convergence of sequence*}
huffman@20563
    24
  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
paulson@10751
    25
wenzelm@21404
    26
definition
huffman@20552
    27
  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
wenzelm@21404
    28
    ("((_)/ ----NS> (_))" [60, 60] 60) where
paulson@15082
    29
    --{*Nonstandard definition of convergence of sequence*}
huffman@20552
    30
  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
paulson@15082
    31
wenzelm@21404
    32
definition
wenzelm@21404
    33
  lim :: "(nat => 'a::real_normed_vector) => 'a" where
paulson@15082
    34
    --{*Standard definition of limit using choice operator*}
huffman@20682
    35
  "lim X = (THE L. X ----> L)"
paulson@10751
    36
wenzelm@21404
    37
definition
wenzelm@21404
    38
  nslim :: "(nat => 'a::real_normed_vector) => 'a" where
paulson@15082
    39
    --{*Nonstandard definition of limit using choice operator*}
huffman@20682
    40
  "nslim X = (THE L. X ----NS> L)"
paulson@10751
    41
wenzelm@21404
    42
definition
wenzelm@21404
    43
  convergent :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    44
    --{*Standard definition of convergence*}
huffman@20682
    45
  "convergent X = (\<exists>L. X ----> L)"
paulson@10751
    46
wenzelm@21404
    47
definition
wenzelm@21404
    48
  NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    49
    --{*Nonstandard definition of convergence*}
huffman@20682
    50
  "NSconvergent X = (\<exists>L. X ----NS> L)"
paulson@15082
    51
wenzelm@21404
    52
definition
wenzelm@21404
    53
  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    54
    --{*Standard definition for bounded sequence*}
huffman@20552
    55
  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
paulson@10751
    56
wenzelm@21404
    57
definition
wenzelm@21404
    58
  NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    59
    --{*Nonstandard definition for bounded sequence*}
wenzelm@19765
    60
  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
paulson@15082
    61
wenzelm@21404
    62
definition
wenzelm@21404
    63
  monoseq :: "(nat=>real)=>bool" where
paulson@15082
    64
    --{*Definition for monotonicity*}
wenzelm@19765
    65
  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
paulson@10751
    66
wenzelm@21404
    67
definition
wenzelm@21404
    68
  subseq :: "(nat => nat) => bool" where
paulson@15082
    69
    --{*Definition of subsequence*}
wenzelm@19765
    70
  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
paulson@10751
    71
wenzelm@21404
    72
definition
wenzelm@21404
    73
  Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    74
    --{*Standard definition of the Cauchy condition*}
huffman@20563
    75
  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
paulson@10751
    76
wenzelm@21404
    77
definition
wenzelm@21404
    78
  NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
paulson@15082
    79
    --{*Nonstandard definition*}
wenzelm@19765
    80
  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
paulson@15082
    81
paulson@15082
    82
huffman@22608
    83
subsection {* Bounded Sequences *}
huffman@22608
    84
huffman@22608
    85
lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
huffman@22608
    86
unfolding Bseq_def
huffman@22608
    87
proof (intro exI conjI allI)
huffman@22608
    88
  show "0 < max K 1" by simp
huffman@22608
    89
next
huffman@22608
    90
  fix n::nat
huffman@22608
    91
  have "norm (X n) \<le> K" by (rule K)
huffman@22608
    92
  thus "norm (X n) \<le> max K 1" by simp
huffman@22608
    93
qed
huffman@22608
    94
huffman@22608
    95
lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
huffman@22608
    96
unfolding Bseq_def by simp
huffman@22608
    97
huffman@22608
    98
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@22608
    99
unfolding Bseq_def by auto
huffman@22608
   100
huffman@22608
   101
lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
huffman@22608
   102
proof (rule BseqI)
huffman@22608
   103
  let ?A = "norm ` X ` {..N}"
huffman@22608
   104
  have 1: "finite ?A" by simp
huffman@22608
   105
  have 2: "?A \<noteq> {}" by auto
huffman@22608
   106
  fix n::nat
huffman@22608
   107
  show "norm (X n) \<le> max K (Max ?A)"
huffman@22608
   108
  proof (cases rule: linorder_le_cases)
huffman@22608
   109
    assume "n \<ge> N"
huffman@22608
   110
    hence "norm (X n) \<le> K" using K by simp
huffman@22608
   111
    thus "norm (X n) \<le> max K (Max ?A)" by simp
huffman@22608
   112
  next
huffman@22608
   113
    assume "n \<le> N"
huffman@22608
   114
    hence "norm (X n) \<in> ?A" by simp
huffman@22608
   115
    with 1 2 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
huffman@22608
   116
    thus "norm (X n) \<le> max K (Max ?A)" by simp
huffman@22608
   117
  qed
huffman@22608
   118
qed
huffman@22608
   119
huffman@22608
   120
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
huffman@22608
   121
unfolding Bseq_def by auto
huffman@22608
   122
huffman@22608
   123
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
huffman@22608
   124
apply (erule BseqE)
huffman@22608
   125
apply (rule_tac N="k" and K="K" in BseqI2)
huffman@22608
   126
apply clarify
huffman@22608
   127
apply (drule_tac x="n - k" in spec, simp)
huffman@22608
   128
done
huffman@22608
   129
huffman@22608
   130
huffman@22608
   131
subsection {* Sequences That Converge to Zero *}
huffman@22608
   132
huffman@22608
   133
lemma ZseqI:
huffman@22608
   134
  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X"
huffman@22608
   135
unfolding Zseq_def by simp
huffman@22608
   136
huffman@22608
   137
lemma ZseqD:
huffman@22608
   138
  "\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r"
huffman@22608
   139
unfolding Zseq_def by simp
huffman@22608
   140
huffman@22608
   141
lemma Zseq_zero: "Zseq (\<lambda>n. 0)"
huffman@22608
   142
unfolding Zseq_def by simp
huffman@22608
   143
huffman@22608
   144
lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)"
huffman@22608
   145
unfolding Zseq_def by force
huffman@22608
   146
huffman@22608
   147
lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)"
huffman@22608
   148
unfolding Zseq_def by simp
huffman@22608
   149
huffman@22608
   150
lemma Zseq_imp_Zseq:
huffman@22608
   151
  assumes X: "Zseq X"
huffman@22608
   152
  assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
huffman@22608
   153
  shows "Zseq (\<lambda>n. Y n)"
huffman@22608
   154
proof (cases)
huffman@22608
   155
  assume K: "0 < K"
huffman@22608
   156
  show ?thesis
huffman@22608
   157
  proof (rule ZseqI)
huffman@22608
   158
    fix r::real assume "0 < r"
huffman@22608
   159
    hence "0 < r / K"
huffman@22608
   160
      using K by (rule divide_pos_pos)
huffman@22608
   161
    then obtain N where "\<forall>n\<ge>N. norm (X n) < r / K"
huffman@22608
   162
      using ZseqD [OF X] by fast
huffman@22608
   163
    hence "\<forall>n\<ge>N. norm (X n) * K < r"
huffman@22608
   164
      by (simp add: pos_less_divide_eq K)
huffman@22608
   165
    hence "\<forall>n\<ge>N. norm (Y n) < r"
huffman@22608
   166
      by (simp add: order_le_less_trans [OF Y])
huffman@22608
   167
    thus "\<exists>N. \<forall>n\<ge>N. norm (Y n) < r" ..
huffman@22608
   168
  qed
huffman@22608
   169
next
huffman@22608
   170
  assume "\<not> 0 < K"
huffman@22608
   171
  hence K: "K \<le> 0" by (simp only: linorder_not_less)
huffman@22608
   172
  {
huffman@22608
   173
    fix n::nat
huffman@22608
   174
    have "norm (Y n) \<le> norm (X n) * K" by (rule Y)
huffman@22608
   175
    also have "\<dots> \<le> norm (X n) * 0"
huffman@22608
   176
      using K norm_ge_zero by (rule mult_left_mono)
huffman@22608
   177
    finally have "norm (Y n) = 0" by simp
huffman@22608
   178
  }
huffman@22608
   179
  thus ?thesis by (simp add: Zseq_zero)
huffman@22608
   180
qed
huffman@22608
   181
huffman@22608
   182
lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
huffman@22608
   183
by (erule_tac K="1" in Zseq_imp_Zseq, simp)
huffman@22608
   184
huffman@22608
   185
lemma Zseq_add:
huffman@22608
   186
  assumes X: "Zseq X"
huffman@22608
   187
  assumes Y: "Zseq Y"
huffman@22608
   188
  shows "Zseq (\<lambda>n. X n + Y n)"
huffman@22608
   189
proof (rule ZseqI)
huffman@22608
   190
  fix r::real assume "0 < r"
huffman@22608
   191
  hence r: "0 < r / 2" by simp
huffman@22608
   192
  obtain M where M: "\<forall>n\<ge>M. norm (X n) < r/2"
huffman@22608
   193
    using ZseqD [OF X r] by fast
huffman@22608
   194
  obtain N where N: "\<forall>n\<ge>N. norm (Y n) < r/2"
huffman@22608
   195
    using ZseqD [OF Y r] by fast
huffman@22608
   196
  show "\<exists>N. \<forall>n\<ge>N. norm (X n + Y n) < r"
huffman@22608
   197
  proof (intro exI allI impI)
huffman@22608
   198
    fix n assume n: "max M N \<le> n"
huffman@22608
   199
    have "norm (X n + Y n) \<le> norm (X n) + norm (Y n)"
huffman@22608
   200
      by (rule norm_triangle_ineq)
huffman@22608
   201
    also have "\<dots> < r/2 + r/2"
huffman@22608
   202
    proof (rule add_strict_mono)
huffman@22608
   203
      from M n show "norm (X n) < r/2" by simp
huffman@22608
   204
      from N n show "norm (Y n) < r/2" by simp
huffman@22608
   205
    qed
huffman@22608
   206
    finally show "norm (X n + Y n) < r" by simp
huffman@22608
   207
  qed
huffman@22608
   208
qed
huffman@22608
   209
huffman@22608
   210
lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n. - X n)"
huffman@22608
   211
unfolding Zseq_def by simp
huffman@22608
   212
huffman@22608
   213
lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n - Y n)"
huffman@22608
   214
by (simp only: diff_minus Zseq_add Zseq_minus)
huffman@22608
   215
huffman@22608
   216
lemma (in bounded_linear) Zseq:
huffman@22608
   217
  assumes X: "Zseq X"
huffman@22608
   218
  shows "Zseq (\<lambda>n. f (X n))"
huffman@22608
   219
proof -
huffman@22608
   220
  obtain K where "\<And>x. norm (f x) \<le> norm x * K"
huffman@22608
   221
    using bounded by fast
huffman@22608
   222
  with X show ?thesis
huffman@22608
   223
    by (rule Zseq_imp_Zseq)
huffman@22608
   224
qed
huffman@22608
   225
huffman@22608
   226
lemma (in bounded_bilinear) Zseq_prod:
huffman@22608
   227
  assumes X: "Zseq X"
huffman@22608
   228
  assumes Y: "Zseq Y"
huffman@22608
   229
  shows "Zseq (\<lambda>n. X n ** Y n)"
huffman@22608
   230
proof (rule ZseqI)
huffman@22608
   231
  fix r::real assume r: "0 < r"
huffman@22608
   232
  obtain K where K: "0 < K"
huffman@22608
   233
    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
huffman@22608
   234
    using pos_bounded by fast
huffman@22608
   235
  from K have K': "0 < inverse K"
huffman@22608
   236
    by (rule positive_imp_inverse_positive)
huffman@22608
   237
  obtain M where M: "\<forall>n\<ge>M. norm (X n) < r"
huffman@22608
   238
    using ZseqD [OF X r] by fast
huffman@22608
   239
  obtain N where N: "\<forall>n\<ge>N. norm (Y n) < inverse K"
huffman@22608
   240
    using ZseqD [OF Y K'] by fast
huffman@22608
   241
  show "\<exists>N. \<forall>n\<ge>N. norm (X n ** Y n) < r"
huffman@22608
   242
  proof (intro exI allI impI)
huffman@22608
   243
    fix n assume n: "max M N \<le> n"
huffman@22608
   244
    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
huffman@22608
   245
      by (rule norm_le)
huffman@22608
   246
    also have "norm (X n) * norm (Y n) * K < r * inverse K * K"
huffman@22608
   247
    proof (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero K)
huffman@22608
   248
      from M n show Xn: "norm (X n) < r" by simp
huffman@22608
   249
      from N n show Yn: "norm (Y n) < inverse K" by simp
huffman@22608
   250
    qed
huffman@22608
   251
    also from K have "r * inverse K * K = r" by simp
huffman@22608
   252
    finally show "norm (X n ** Y n) < r" .
huffman@22608
   253
  qed
huffman@22608
   254
qed
huffman@22608
   255
huffman@22608
   256
lemma (in bounded_bilinear) Zseq_prod_Bseq:
huffman@22608
   257
  assumes X: "Zseq X"
huffman@22608
   258
  assumes Y: "Bseq Y"
huffman@22608
   259
  shows "Zseq (\<lambda>n. X n ** Y n)"
huffman@22608
   260
proof -
huffman@22608
   261
  obtain K where K: "0 \<le> K"
huffman@22608
   262
    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
huffman@22608
   263
    using nonneg_bounded by fast
huffman@22608
   264
  obtain B where B: "0 < B"
huffman@22608
   265
    and norm_Y: "\<And>n. norm (Y n) \<le> B"
huffman@22608
   266
    using Y [unfolded Bseq_def] by fast
huffman@22608
   267
  from X show ?thesis
huffman@22608
   268
  proof (rule Zseq_imp_Zseq)
huffman@22608
   269
    fix n::nat
huffman@22608
   270
    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
huffman@22608
   271
      by (rule norm_le)
huffman@22608
   272
    also have "\<dots> \<le> norm (X n) * B * K"
huffman@22608
   273
      by (intro mult_mono' order_refl norm_Y norm_ge_zero
huffman@22608
   274
                mult_nonneg_nonneg K)
huffman@22608
   275
    also have "\<dots> = norm (X n) * (B * K)"
huffman@22608
   276
      by (rule mult_assoc)
huffman@22608
   277
    finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" .
huffman@22608
   278
  qed
huffman@22608
   279
qed
huffman@22608
   280
huffman@22608
   281
lemma (in bounded_bilinear) Bseq_prod_Zseq:
huffman@22608
   282
  assumes X: "Bseq X"
huffman@22608
   283
  assumes Y: "Zseq Y"
huffman@22608
   284
  shows "Zseq (\<lambda>n. X n ** Y n)"
huffman@22608
   285
proof -
huffman@22608
   286
  obtain K where K: "0 \<le> K"
huffman@22608
   287
    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
huffman@22608
   288
    using nonneg_bounded by fast
huffman@22608
   289
  obtain B where B: "0 < B"
huffman@22608
   290
    and norm_X: "\<And>n. norm (X n) \<le> B"
huffman@22608
   291
    using X [unfolded Bseq_def] by fast
huffman@22608
   292
  from Y show ?thesis
huffman@22608
   293
  proof (rule Zseq_imp_Zseq)
huffman@22608
   294
    fix n::nat
huffman@22608
   295
    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
huffman@22608
   296
      by (rule norm_le)
huffman@22608
   297
    also have "\<dots> \<le> B * norm (Y n) * K"
huffman@22608
   298
      by (intro mult_mono' order_refl norm_X norm_ge_zero
huffman@22608
   299
                mult_nonneg_nonneg K)
huffman@22608
   300
    also have "\<dots> = norm (Y n) * (B * K)"
huffman@22608
   301
      by (simp only: mult_ac)
huffman@22608
   302
    finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" .
huffman@22608
   303
  qed
huffman@22608
   304
qed
huffman@22608
   305
huffman@22608
   306
lemma (in bounded_bilinear) Zseq_prod_left:
huffman@22608
   307
  "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
huffman@22608
   308
by (rule bounded_linear_left [THEN bounded_linear.Zseq])
huffman@22608
   309
huffman@22608
   310
lemma (in bounded_bilinear) Zseq_prod_right:
huffman@22608
   311
  "Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)"
huffman@22608
   312
by (rule bounded_linear_right [THEN bounded_linear.Zseq])
huffman@22608
   313
huffman@22608
   314
lemmas Zseq_mult = bounded_bilinear_mult.Zseq_prod
huffman@22608
   315
lemmas Zseq_mult_right = bounded_bilinear_mult.Zseq_prod_right
huffman@22608
   316
lemmas Zseq_mult_left = bounded_bilinear_mult.Zseq_prod_left
huffman@22608
   317
huffman@22608
   318
huffman@20696
   319
subsection {* Limits of Sequences *}
huffman@20696
   320
huffman@20696
   321
subsubsection {* Purely standard proofs *}
paulson@15082
   322
paulson@15082
   323
lemma LIMSEQ_iff:
huffman@20563
   324
      "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
huffman@22608
   325
by (rule LIMSEQ_def)
huffman@22608
   326
huffman@22608
   327
lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) ----> L) = Zseq (\<lambda>n. X n - L)"
huffman@22608
   328
by (simp only: LIMSEQ_def Zseq_def)
paulson@15082
   329
huffman@20751
   330
lemma LIMSEQ_I:
huffman@20751
   331
  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
huffman@20751
   332
by (simp add: LIMSEQ_def)
huffman@20751
   333
huffman@20751
   334
lemma LIMSEQ_D:
huffman@20751
   335
  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
huffman@20751
   336
by (simp add: LIMSEQ_def)
huffman@20751
   337
huffman@22608
   338
lemma LIMSEQ_const: "(\<lambda>n. k) ----> k"
huffman@20696
   339
by (simp add: LIMSEQ_def)
huffman@20696
   340
huffman@22608
   341
lemma LIMSEQ_const_iff: "(\<lambda>n. k) ----> l = (k = l)"
huffman@22608
   342
by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff)
huffman@22608
   343
huffman@20696
   344
lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
huffman@20696
   345
apply (simp add: LIMSEQ_def, safe)
huffman@20696
   346
apply (drule_tac x="r" in spec, safe)
huffman@20696
   347
apply (rule_tac x="no" in exI, safe)
huffman@20696
   348
apply (drule_tac x="n" in spec, safe)
huffman@20696
   349
apply (erule order_le_less_trans [OF norm_triangle_ineq3])
huffman@20696
   350
done
huffman@20696
   351
huffman@22615
   352
lemma LIMSEQ_ignore_initial_segment:
huffman@22615
   353
  "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
huffman@22615
   354
apply (rule LIMSEQ_I)
huffman@22615
   355
apply (drule (1) LIMSEQ_D)
huffman@22615
   356
apply (erule exE, rename_tac N)
huffman@22615
   357
apply (rule_tac x=N in exI)
huffman@22615
   358
apply simp
huffman@22615
   359
done
huffman@20696
   360
huffman@22615
   361
lemma LIMSEQ_offset:
huffman@22615
   362
  "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
huffman@22615
   363
apply (rule LIMSEQ_I)
huffman@22615
   364
apply (drule (1) LIMSEQ_D)
huffman@22615
   365
apply (erule exE, rename_tac N)
huffman@22615
   366
apply (rule_tac x="N + k" in exI)
huffman@22615
   367
apply clarify
huffman@22615
   368
apply (drule_tac x="n - k" in spec)
huffman@22615
   369
apply (simp add: le_diff_conv2)
huffman@20696
   370
done
huffman@20696
   371
huffman@22615
   372
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
huffman@22615
   373
by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
huffman@22615
   374
huffman@22615
   375
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
huffman@22615
   376
by (rule_tac k="1" in LIMSEQ_offset, simp)
huffman@22615
   377
huffman@22615
   378
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
huffman@22615
   379
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
huffman@22615
   380
huffman@22608
   381
lemma add_diff_add:
huffman@22608
   382
  fixes a b c d :: "'a::ab_group_add"
huffman@22608
   383
  shows "(a + c) - (b + d) = (a - b) + (c - d)"
huffman@22608
   384
by simp
huffman@22608
   385
huffman@22608
   386
lemma minus_diff_minus:
huffman@22608
   387
  fixes a b :: "'a::ab_group_add"
huffman@22608
   388
  shows "(- a) - (- b) = - (a - b)"
huffman@22608
   389
by simp
huffman@22608
   390
huffman@22608
   391
lemma LIMSEQ_add: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) ----> a + b"
huffman@22608
   392
by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add)
huffman@22608
   393
huffman@22608
   394
lemma LIMSEQ_minus: "X ----> a \<Longrightarrow> (\<lambda>n. - X n) ----> - a"
huffman@22608
   395
by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus)
huffman@22608
   396
huffman@22608
   397
lemma LIMSEQ_minus_cancel: "(\<lambda>n. - X n) ----> - a \<Longrightarrow> X ----> a"
huffman@22608
   398
by (drule LIMSEQ_minus, simp)
huffman@22608
   399
huffman@22608
   400
lemma LIMSEQ_diff: "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n - Y n) ----> a - b"
huffman@22608
   401
by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
huffman@22608
   402
huffman@22608
   403
lemma LIMSEQ_unique: "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
huffman@22608
   404
by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff)
huffman@22608
   405
huffman@22608
   406
lemma (in bounded_linear) LIMSEQ:
huffman@22608
   407
  "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
huffman@22608
   408
by (simp only: LIMSEQ_Zseq_iff diff [symmetric] Zseq)
huffman@22608
   409
huffman@22608
   410
lemma (in bounded_bilinear) LIMSEQ:
huffman@22608
   411
  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) ----> a ** b"
huffman@22608
   412
by (simp only: LIMSEQ_Zseq_iff prod_diff_prod
huffman@22608
   413
               Zseq_add Zseq_prod Zseq_prod_left Zseq_prod_right)
huffman@22608
   414
huffman@22608
   415
lemma LIMSEQ_mult:
huffman@22608
   416
  fixes a b :: "'a::real_normed_algebra"
huffman@22608
   417
  shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
huffman@22608
   418
by (rule bounded_bilinear_mult.LIMSEQ)
huffman@22608
   419
huffman@22608
   420
lemma inverse_diff_inverse:
huffman@22608
   421
  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
huffman@22608
   422
   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
huffman@22608
   423
by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
huffman@22608
   424
huffman@22608
   425
lemma Bseq_inverse_lemma:
huffman@22608
   426
  fixes x :: "'a::real_normed_div_algebra"
huffman@22608
   427
  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
huffman@22608
   428
apply (subst nonzero_norm_inverse, clarsimp)
huffman@22608
   429
apply (erule (1) le_imp_inverse_le)
huffman@22608
   430
done
huffman@22608
   431
huffman@22608
   432
lemma Bseq_inverse:
huffman@22608
   433
  fixes a :: "'a::real_normed_div_algebra"
huffman@22608
   434
  assumes X: "X ----> a"
huffman@22608
   435
  assumes a: "a \<noteq> 0"
huffman@22608
   436
  shows "Bseq (\<lambda>n. inverse (X n))"
huffman@22608
   437
proof -
huffman@22608
   438
  from a have "0 < norm a" by simp
huffman@22608
   439
  hence "\<exists>r>0. r < norm a" by (rule dense)
huffman@22608
   440
  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
huffman@22608
   441
  obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
huffman@22608
   442
    using LIMSEQ_D [OF X r1] by fast
huffman@22608
   443
  show ?thesis
huffman@22608
   444
  proof (rule BseqI2 [rule_format])
huffman@22608
   445
    fix n assume n: "N \<le> n"
huffman@22608
   446
    hence 1: "norm (X n - a) < r" by (rule N)
huffman@22608
   447
    hence 2: "X n \<noteq> 0" using r2 by auto
huffman@22608
   448
    hence "norm (inverse (X n)) = inverse (norm (X n))"
huffman@22608
   449
      by (rule nonzero_norm_inverse)
huffman@22608
   450
    also have "\<dots> \<le> inverse (norm a - r)"
huffman@22608
   451
    proof (rule le_imp_inverse_le)
huffman@22608
   452
      show "0 < norm a - r" using r2 by simp
huffman@22608
   453
    next
huffman@22608
   454
      have "norm a - norm (X n) \<le> norm (a - X n)"
huffman@22608
   455
        by (rule norm_triangle_ineq2)
huffman@22608
   456
      also have "\<dots> = norm (X n - a)"
huffman@22608
   457
        by (rule norm_minus_commute)
huffman@22608
   458
      also have "\<dots> < r" using 1 .
huffman@22608
   459
      finally show "norm a - r \<le> norm (X n)" by simp
huffman@22608
   460
    qed
huffman@22608
   461
    finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" .
huffman@22608
   462
  qed
huffman@22608
   463
qed
huffman@22608
   464
huffman@22608
   465
lemma LIMSEQ_inverse_lemma:
huffman@22608
   466
  fixes a :: "'a::real_normed_div_algebra"
huffman@22608
   467
  shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk>
huffman@22608
   468
         \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
huffman@22608
   469
apply (subst LIMSEQ_Zseq_iff)
huffman@22608
   470
apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
huffman@22608
   471
apply (rule Zseq_minus)
huffman@22608
   472
apply (rule Zseq_mult_left)
huffman@22608
   473
apply (rule bounded_bilinear_mult.Bseq_prod_Zseq)
huffman@22608
   474
apply (erule (1) Bseq_inverse)
huffman@22608
   475
apply (simp add: LIMSEQ_Zseq_iff)
huffman@22608
   476
done
huffman@22608
   477
huffman@22608
   478
lemma LIMSEQ_inverse:
huffman@22608
   479
  fixes a :: "'a::real_normed_div_algebra"
huffman@22608
   480
  assumes X: "X ----> a"
huffman@22608
   481
  assumes a: "a \<noteq> 0"
huffman@22608
   482
  shows "(\<lambda>n. inverse (X n)) ----> inverse a"
huffman@22608
   483
proof -
huffman@22608
   484
  from a have "0 < norm a" by simp
huffman@22608
   485
  then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a"
huffman@22608
   486
    using LIMSEQ_D [OF X] by fast
huffman@22608
   487
  hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto
huffman@22608
   488
  hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp
huffman@22608
   489
huffman@22608
   490
  from X have "(\<lambda>n. X (n + k)) ----> a"
huffman@22608
   491
    by (rule LIMSEQ_ignore_initial_segment)
huffman@22608
   492
  hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a"
huffman@22608
   493
    using a k by (rule LIMSEQ_inverse_lemma)
huffman@22608
   494
  thus "(\<lambda>n. inverse (X n)) ----> inverse a"
huffman@22608
   495
    by (rule LIMSEQ_offset)
huffman@22608
   496
qed
huffman@22608
   497
huffman@22608
   498
lemma LIMSEQ_divide:
huffman@22608
   499
  fixes a b :: "'a::real_normed_field"
huffman@22608
   500
  shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b"
huffman@22608
   501
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
huffman@22608
   502
huffman@22608
   503
lemma LIMSEQ_pow:
huffman@22608
   504
  fixes a :: "'a::{real_normed_algebra,recpower}"
huffman@22608
   505
  shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
huffman@22608
   506
by (induct m) (simp_all add: power_Suc LIMSEQ_const LIMSEQ_mult)
huffman@22608
   507
huffman@22608
   508
lemma LIMSEQ_setsum:
huffman@22608
   509
  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
huffman@22608
   510
  shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
huffman@22608
   511
proof (cases "finite S")
huffman@22608
   512
  case True
huffman@22608
   513
  thus ?thesis using n
huffman@22608
   514
  proof (induct)
huffman@22608
   515
    case empty
huffman@22608
   516
    show ?case
huffman@22608
   517
      by (simp add: LIMSEQ_const)
huffman@22608
   518
  next
huffman@22608
   519
    case insert
huffman@22608
   520
    thus ?case
huffman@22608
   521
      by (simp add: LIMSEQ_add)
huffman@22608
   522
  qed
huffman@22608
   523
next
huffman@22608
   524
  case False
huffman@22608
   525
  thus ?thesis
huffman@22608
   526
    by (simp add: LIMSEQ_const)
huffman@22608
   527
qed
huffman@22608
   528
huffman@22608
   529
lemma LIMSEQ_setprod:
huffman@22608
   530
  fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"
huffman@22608
   531
  assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
huffman@22608
   532
  shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
huffman@22608
   533
proof (cases "finite S")
huffman@22608
   534
  case True
huffman@22608
   535
  thus ?thesis using n
huffman@22608
   536
  proof (induct)
huffman@22608
   537
    case empty
huffman@22608
   538
    show ?case
huffman@22608
   539
      by (simp add: LIMSEQ_const)
huffman@22608
   540
  next
huffman@22608
   541
    case insert
huffman@22608
   542
    thus ?case
huffman@22608
   543
      by (simp add: LIMSEQ_mult)
huffman@22608
   544
  qed
huffman@22608
   545
next
huffman@22608
   546
  case False
huffman@22608
   547
  thus ?thesis
huffman@22608
   548
    by (simp add: setprod_def LIMSEQ_const)
huffman@22608
   549
qed
huffman@22608
   550
huffman@22614
   551
lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
huffman@22614
   552
by (simp add: LIMSEQ_add LIMSEQ_const)
huffman@22614
   553
huffman@22614
   554
(* FIXME: delete *)
huffman@22614
   555
lemma LIMSEQ_add_minus:
huffman@22614
   556
     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
huffman@22614
   557
by (simp only: LIMSEQ_add LIMSEQ_minus)
huffman@22614
   558
huffman@22614
   559
lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
huffman@22614
   560
by (simp add: LIMSEQ_diff LIMSEQ_const)
huffman@22614
   561
huffman@22614
   562
lemma LIMSEQ_diff_approach_zero: 
huffman@22614
   563
  "g ----> L ==> (%x. f x - g x) ----> 0  ==>
huffman@22614
   564
     f ----> L"
huffman@22614
   565
  apply (drule LIMSEQ_add)
huffman@22614
   566
  apply assumption
huffman@22614
   567
  apply simp
huffman@22614
   568
done
huffman@22614
   569
huffman@22614
   570
lemma LIMSEQ_diff_approach_zero2: 
huffman@22614
   571
  "f ----> L ==> (%x. f x - g x) ----> 0  ==>
huffman@22614
   572
     g ----> L";
huffman@22614
   573
  apply (drule LIMSEQ_diff)
huffman@22614
   574
  apply assumption
huffman@22614
   575
  apply simp
huffman@22614
   576
done
huffman@22614
   577
huffman@22614
   578
text{*A sequence tends to zero iff its abs does*}
huffman@22614
   579
lemma LIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----> 0) = (X ----> 0)"
huffman@22614
   580
by (simp add: LIMSEQ_def)
huffman@22614
   581
huffman@22614
   582
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> (0::real))"
huffman@22614
   583
by (simp add: LIMSEQ_def)
huffman@22614
   584
huffman@22614
   585
lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
huffman@22614
   586
by (drule LIMSEQ_norm, simp)
huffman@22614
   587
huffman@22614
   588
text{*An unbounded sequence's inverse tends to 0*}
huffman@22614
   589
huffman@22614
   590
text{* standard proof seems easier *}
huffman@22614
   591
lemma LIMSEQ_inverse_zero:
huffman@22614
   592
      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
huffman@22614
   593
apply (simp add: LIMSEQ_def, safe)
huffman@22614
   594
apply (drule_tac x = "inverse r" in spec, safe)
huffman@22614
   595
apply (rule_tac x = N in exI, safe)
huffman@22614
   596
apply (drule spec, auto)
huffman@22614
   597
apply (frule positive_imp_inverse_positive)
huffman@22614
   598
apply (frule order_less_trans, assumption)
huffman@22614
   599
apply (frule_tac a = "f n" in positive_imp_inverse_positive)
huffman@22614
   600
apply (simp add: abs_if) 
huffman@22614
   601
apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
huffman@22614
   602
apply (auto intro: inverse_less_iff_less [THEN iffD2]
huffman@22614
   603
            simp del: inverse_inverse_eq)
huffman@22614
   604
done
huffman@22614
   605
huffman@22614
   606
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
huffman@22614
   607
huffman@22614
   608
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
huffman@22614
   609
apply (rule LIMSEQ_inverse_zero, safe)
huffman@22614
   610
apply (cut_tac x = y in reals_Archimedean2)
huffman@22614
   611
apply (safe, rule_tac x = n in exI)
huffman@22614
   612
apply (auto simp add: real_of_nat_Suc)
huffman@22614
   613
done
huffman@22614
   614
huffman@22614
   615
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
huffman@22614
   616
infinity is now easily proved*}
huffman@22614
   617
huffman@22614
   618
lemma LIMSEQ_inverse_real_of_nat_add:
huffman@22614
   619
     "(%n. r + inverse(real(Suc n))) ----> r"
huffman@22614
   620
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
huffman@22614
   621
huffman@22614
   622
lemma LIMSEQ_inverse_real_of_nat_add_minus:
huffman@22614
   623
     "(%n. r + -inverse(real(Suc n))) ----> r"
huffman@22614
   624
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
huffman@22614
   625
huffman@22614
   626
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
huffman@22614
   627
     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
huffman@22614
   628
by (cut_tac b=1 in
huffman@22614
   629
        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
huffman@22614
   630
huffman@22615
   631
lemma LIMSEQ_le_const:
huffman@22615
   632
  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
huffman@22615
   633
apply (rule ccontr, simp only: linorder_not_le)
huffman@22615
   634
apply (drule_tac r="a - x" in LIMSEQ_D, simp)
huffman@22615
   635
apply clarsimp
huffman@22615
   636
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1)
huffman@22615
   637
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2)
huffman@22615
   638
apply simp
huffman@22615
   639
done
huffman@22615
   640
huffman@22615
   641
lemma LIMSEQ_le_const2:
huffman@22615
   642
  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
huffman@22615
   643
apply (subgoal_tac "- a \<le> - x", simp)
huffman@22615
   644
apply (rule LIMSEQ_le_const)
huffman@22615
   645
apply (erule LIMSEQ_minus)
huffman@22615
   646
apply simp
huffman@22615
   647
done
huffman@22615
   648
huffman@22615
   649
lemma LIMSEQ_le:
huffman@22615
   650
  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
huffman@22615
   651
apply (subgoal_tac "0 \<le> y - x", simp)
huffman@22615
   652
apply (rule LIMSEQ_le_const)
huffman@22615
   653
apply (erule (1) LIMSEQ_diff)
huffman@22615
   654
apply (simp add: le_diff_eq)
huffman@22615
   655
done
huffman@22615
   656
huffman@20696
   657
subsubsection {* Purely nonstandard proofs *}
huffman@20696
   658
paulson@15082
   659
lemma NSLIMSEQ_iff:
huffman@20552
   660
    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
paulson@15082
   661
by (simp add: NSLIMSEQ_def)
paulson@15082
   662
huffman@20751
   663
lemma NSLIMSEQ_I:
huffman@20751
   664
  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X ----NS> L"
huffman@20751
   665
by (simp add: NSLIMSEQ_def)
huffman@20751
   666
huffman@20751
   667
lemma NSLIMSEQ_D:
huffman@20751
   668
  "\<lbrakk>X ----NS> L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
huffman@20751
   669
by (simp add: NSLIMSEQ_def)
huffman@20751
   670
huffman@20696
   671
lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
huffman@20696
   672
by (simp add: NSLIMSEQ_def)
huffman@20696
   673
huffman@20696
   674
lemma NSLIMSEQ_add:
huffman@20696
   675
      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
huffman@20696
   676
by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
huffman@20696
   677
huffman@20696
   678
lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
huffman@20696
   679
by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
huffman@20696
   680
huffman@20696
   681
lemma NSLIMSEQ_mult:
huffman@20696
   682
  fixes a b :: "'a::real_normed_algebra"
huffman@20696
   683
  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
huffman@20696
   684
by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
huffman@20696
   685
huffman@20696
   686
lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
huffman@20696
   687
by (auto simp add: NSLIMSEQ_def)
huffman@20696
   688
huffman@20696
   689
lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
huffman@20696
   690
by (drule NSLIMSEQ_minus, simp)
huffman@20696
   691
huffman@20696
   692
(* FIXME: delete *)
huffman@20696
   693
lemma NSLIMSEQ_add_minus:
huffman@20696
   694
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
huffman@20696
   695
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
huffman@20696
   696
huffman@20696
   697
lemma NSLIMSEQ_diff:
huffman@20696
   698
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
huffman@20696
   699
by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
huffman@20696
   700
huffman@20696
   701
lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
huffman@20696
   702
by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
huffman@20696
   703
huffman@20696
   704
lemma NSLIMSEQ_inverse:
huffman@20696
   705
  fixes a :: "'a::real_normed_div_algebra"
huffman@20696
   706
  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
huffman@20696
   707
by (simp add: NSLIMSEQ_def star_of_approx_inverse)
huffman@20696
   708
huffman@20696
   709
lemma NSLIMSEQ_mult_inverse:
huffman@20696
   710
  fixes a b :: "'a::real_normed_field"
huffman@20696
   711
  shows
huffman@20696
   712
     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
huffman@20696
   713
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
huffman@20696
   714
huffman@20696
   715
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
huffman@20696
   716
by transfer simp
huffman@20696
   717
huffman@20696
   718
lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
huffman@20696
   719
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
huffman@20696
   720
huffman@20696
   721
text{*Uniqueness of limit*}
huffman@20696
   722
lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
huffman@20696
   723
apply (simp add: NSLIMSEQ_def)
huffman@20696
   724
apply (drule HNatInfinite_whn [THEN [2] bspec])+
huffman@20696
   725
apply (auto dest: approx_trans3)
huffman@20696
   726
done
huffman@20696
   727
huffman@20696
   728
lemma NSLIMSEQ_pow [rule_format]:
huffman@20696
   729
  fixes a :: "'a::{real_normed_algebra,recpower}"
huffman@20696
   730
  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
huffman@20696
   731
apply (induct "m")
huffman@20696
   732
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
huffman@20696
   733
done
huffman@20696
   734
huffman@22614
   735
text{*We can now try and derive a few properties of sequences,
huffman@22614
   736
     starting with the limit comparison property for sequences.*}
huffman@22614
   737
huffman@22614
   738
lemma NSLIMSEQ_le:
huffman@22614
   739
       "[| f ----NS> l; g ----NS> m;
huffman@22614
   740
           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
huffman@22614
   741
        |] ==> l \<le> (m::real)"
huffman@22614
   742
apply (simp add: NSLIMSEQ_def, safe)
huffman@22614
   743
apply (drule starfun_le_mono)
huffman@22614
   744
apply (drule HNatInfinite_whn [THEN [2] bspec])+
huffman@22614
   745
apply (drule_tac x = whn in spec)
huffman@22614
   746
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
huffman@22614
   747
apply clarify
huffman@22614
   748
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
huffman@22614
   749
done
huffman@22614
   750
huffman@22614
   751
lemma NSLIMSEQ_le_const: "[| X ----NS> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
huffman@22614
   752
by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
huffman@22614
   753
huffman@22614
   754
lemma NSLIMSEQ_le_const2: "[| X ----NS> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
huffman@22614
   755
by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
huffman@22614
   756
huffman@22614
   757
text{*Shift a convergent series by 1:
huffman@22614
   758
  By the equivalence between Cauchiness and convergence and because
huffman@22614
   759
  the successor of an infinite hypernatural is also infinite.*}
huffman@22614
   760
huffman@22614
   761
lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
huffman@22614
   762
apply (unfold NSLIMSEQ_def, safe)
huffman@22614
   763
apply (drule_tac x="N + 1" in bspec)
huffman@22614
   764
apply (erule HNatInfinite_add)
huffman@22614
   765
apply (simp add: starfun_shift_one)
huffman@22614
   766
done
huffman@22614
   767
huffman@22614
   768
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
huffman@22614
   769
apply (unfold NSLIMSEQ_def, safe)
huffman@22614
   770
apply (drule_tac x="N - 1" in bspec) 
huffman@22614
   771
apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
huffman@22614
   772
apply (simp add: starfun_shift_one one_le_HNatInfinite)
huffman@22614
   773
done
huffman@22614
   774
huffman@22614
   775
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
huffman@22614
   776
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
huffman@22614
   777
huffman@20696
   778
subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
paulson@15082
   779
paulson@15082
   780
lemma LIMSEQ_NSLIMSEQ:
huffman@20751
   781
  assumes X: "X ----> L" shows "X ----NS> L"
huffman@20751
   782
proof (rule NSLIMSEQ_I)
huffman@20751
   783
  fix N assume N: "N \<in> HNatInfinite"
huffman@20751
   784
  have "starfun X N - star_of L \<in> Infinitesimal"
huffman@20751
   785
  proof (rule InfinitesimalI2)
huffman@20751
   786
    fix r::real assume r: "0 < r"
huffman@20751
   787
    from LIMSEQ_D [OF X r]
huffman@20751
   788
    obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
huffman@20751
   789
    hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   790
      by transfer
huffman@20751
   791
    thus "hnorm (starfun X N - star_of L) < star_of r"
huffman@20751
   792
      using N by (simp add: star_of_le_HNatInfinite)
huffman@20751
   793
  qed
huffman@20751
   794
  thus "starfun X N \<approx> star_of L"
huffman@20751
   795
    by (unfold approx_def)
huffman@20751
   796
qed
paulson@15082
   797
huffman@20751
   798
lemma NSLIMSEQ_LIMSEQ:
huffman@20751
   799
  assumes X: "X ----NS> L" shows "X ----> L"
huffman@20751
   800
proof (rule LIMSEQ_I)
huffman@20751
   801
  fix r::real assume r: "0 < r"
huffman@20751
   802
  have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   803
  proof (intro exI allI impI)
huffman@20751
   804
    fix n assume "whn \<le> n"
huffman@20751
   805
    with HNatInfinite_whn have "n \<in> HNatInfinite"
huffman@20751
   806
      by (rule HNatInfinite_upward_closed)
huffman@20751
   807
    with X have "starfun X n \<approx> star_of L"
huffman@20751
   808
      by (rule NSLIMSEQ_D)
huffman@20751
   809
    hence "starfun X n - star_of L \<in> Infinitesimal"
huffman@20751
   810
      by (unfold approx_def)
huffman@20751
   811
    thus "hnorm (starfun X n - star_of L) < star_of r"
huffman@20751
   812
      using r by (rule InfinitesimalD2)
huffman@20751
   813
  qed
huffman@20751
   814
  thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
huffman@20751
   815
    by transfer
huffman@20751
   816
qed
paulson@15082
   817
huffman@20751
   818
theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
huffman@20751
   819
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
paulson@15082
   820
huffman@20751
   821
(* Used once by Integration/Rats.thy in AFP *)
paulson@15082
   822
lemma NSLIMSEQ_finite_set:
paulson@15082
   823
     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
huffman@20751
   824
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
paulson@15082
   825
huffman@22615
   826
subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
huffman@22614
   827
huffman@22614
   828
text{*We prove the NS version from the standard one, since the NS proof
huffman@22614
   829
   seems more complicated than the standard one above!*}
huffman@22614
   830
lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) ----NS> 0) = (X ----NS> 0)"
huffman@22614
   831
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_norm_zero)
huffman@22614
   832
huffman@22614
   833
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> (0::real))"
huffman@22614
   834
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
huffman@22614
   835
huffman@22614
   836
text{*Generalization to other limits*}
huffman@22614
   837
lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
huffman@22614
   838
apply (simp add: NSLIMSEQ_def)
huffman@22614
   839
apply (auto intro: approx_hrabs 
huffman@22614
   840
            simp add: starfun_abs)
avigad@16819
   841
done
avigad@16819
   842
huffman@22614
   843
lemma NSLIMSEQ_inverse_zero:
huffman@22614
   844
     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
huffman@22614
   845
      ==> (%n. inverse(f n)) ----NS> 0"
huffman@22614
   846
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
huffman@22614
   847
huffman@22614
   848
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
huffman@22614
   849
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
huffman@22614
   850
huffman@22614
   851
lemma NSLIMSEQ_inverse_real_of_nat_add:
huffman@22614
   852
     "(%n. r + inverse(real(Suc n))) ----NS> r"
huffman@22614
   853
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
huffman@22614
   854
huffman@22614
   855
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
huffman@22614
   856
     "(%n. r + -inverse(real(Suc n))) ----NS> r"
huffman@22614
   857
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
huffman@22614
   858
huffman@22614
   859
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
huffman@22614
   860
     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
huffman@22614
   861
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
huffman@22614
   862
paulson@15082
   863
huffman@20696
   864
subsection {* Convergence *}
paulson@15082
   865
paulson@15082
   866
lemma limI: "X ----> L ==> lim X = L"
paulson@15082
   867
apply (simp add: lim_def)
paulson@15082
   868
apply (blast intro: LIMSEQ_unique)
paulson@15082
   869
done
paulson@15082
   870
paulson@15082
   871
lemma nslimI: "X ----NS> L ==> nslim X = L"
paulson@15082
   872
apply (simp add: nslim_def)
paulson@15082
   873
apply (blast intro: NSLIMSEQ_unique)
paulson@15082
   874
done
paulson@15082
   875
paulson@15082
   876
lemma lim_nslim_iff: "lim X = nslim X"
paulson@15082
   877
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   878
paulson@15082
   879
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
paulson@15082
   880
by (simp add: convergent_def)
paulson@15082
   881
paulson@15082
   882
lemma convergentI: "(X ----> L) ==> convergent X"
paulson@15082
   883
by (auto simp add: convergent_def)
paulson@15082
   884
paulson@15082
   885
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
paulson@15082
   886
by (simp add: NSconvergent_def)
paulson@15082
   887
paulson@15082
   888
lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
paulson@15082
   889
by (auto simp add: NSconvergent_def)
paulson@15082
   890
paulson@15082
   891
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
paulson@15082
   892
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
paulson@15082
   893
paulson@15082
   894
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
huffman@20682
   895
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
paulson@15082
   896
paulson@15082
   897
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
huffman@20682
   898
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
paulson@15082
   899
huffman@20696
   900
lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
huffman@20696
   901
apply (simp add: convergent_def)
huffman@20696
   902
apply (auto dest: LIMSEQ_minus)
huffman@20696
   903
apply (drule LIMSEQ_minus, auto)
huffman@20696
   904
done
huffman@20696
   905
huffman@20696
   906
huffman@20696
   907
subsection {* Bounded Monotonic Sequences *}
huffman@20696
   908
paulson@15082
   909
text{*Subsequence (alternative definition, (e.g. Hoskins)*}
paulson@15082
   910
paulson@15082
   911
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
paulson@15082
   912
apply (simp add: subseq_def)
paulson@15082
   913
apply (auto dest!: less_imp_Suc_add)
paulson@15082
   914
apply (induct_tac k)
paulson@15082
   915
apply (auto intro: less_trans)
paulson@15082
   916
done
paulson@15082
   917
paulson@15082
   918
lemma monoseq_Suc:
paulson@15082
   919
   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
paulson@15082
   920
                 | (\<forall>n. X (Suc n) \<le> X n))"
paulson@15082
   921
apply (simp add: monoseq_def)
paulson@15082
   922
apply (auto dest!: le_imp_less_or_eq)
paulson@15082
   923
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
paulson@15082
   924
apply (induct_tac "ka")
paulson@15082
   925
apply (auto intro: order_trans)
wenzelm@18585
   926
apply (erule contrapos_np)
paulson@15082
   927
apply (induct_tac "k")
paulson@15082
   928
apply (auto intro: order_trans)
paulson@15082
   929
done
paulson@15082
   930
nipkow@15360
   931
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
paulson@15082
   932
by (simp add: monoseq_def)
paulson@15082
   933
nipkow@15360
   934
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
paulson@15082
   935
by (simp add: monoseq_def)
paulson@15082
   936
paulson@15082
   937
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
paulson@15082
   938
by (simp add: monoseq_Suc)
paulson@15082
   939
paulson@15082
   940
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
paulson@15082
   941
by (simp add: monoseq_Suc)
paulson@15082
   942
huffman@20696
   943
text{*Bounded Sequence*}
paulson@15082
   944
huffman@20552
   945
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
paulson@15082
   946
by (simp add: Bseq_def)
paulson@15082
   947
huffman@20552
   948
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
paulson@15082
   949
by (auto simp add: Bseq_def)
paulson@15082
   950
paulson@15082
   951
lemma lemma_NBseq_def:
huffman@20552
   952
     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
huffman@20552
   953
      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
paulson@15082
   954
apply auto
paulson@15082
   955
 prefer 2 apply force
paulson@15082
   956
apply (cut_tac x = K in reals_Archimedean2, clarify)
paulson@15082
   957
apply (rule_tac x = n in exI, clarify)
paulson@15082
   958
apply (drule_tac x = na in spec)
paulson@15082
   959
apply (auto simp add: real_of_nat_Suc)
paulson@15082
   960
done
paulson@15082
   961
paulson@15082
   962
text{* alternative definition for Bseq *}
huffman@20552
   963
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
paulson@15082
   964
apply (simp add: Bseq_def)
paulson@15082
   965
apply (simp (no_asm) add: lemma_NBseq_def)
paulson@15082
   966
done
paulson@15082
   967
paulson@15082
   968
lemma lemma_NBseq_def2:
huffman@20552
   969
     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
paulson@15082
   970
apply (subst lemma_NBseq_def, auto)
paulson@15082
   971
apply (rule_tac x = "Suc N" in exI)
paulson@15082
   972
apply (rule_tac [2] x = N in exI)
paulson@15082
   973
apply (auto simp add: real_of_nat_Suc)
paulson@15082
   974
 prefer 2 apply (blast intro: order_less_imp_le)
paulson@15082
   975
apply (drule_tac x = n in spec, simp)
paulson@15082
   976
done
paulson@15082
   977
paulson@15082
   978
(* yet another definition for Bseq *)
huffman@20552
   979
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
paulson@15082
   980
by (simp add: Bseq_def lemma_NBseq_def2)
paulson@15082
   981
huffman@17318
   982
lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
paulson@15082
   983
by (simp add: NSBseq_def)
paulson@15082
   984
huffman@21842
   985
lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
huffman@21842
   986
unfolding Standard_def by auto
huffman@21842
   987
huffman@21842
   988
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
huffman@21842
   989
apply (cases "N \<in> HNatInfinite")
huffman@21842
   990
apply (erule (1) NSBseqD)
huffman@21842
   991
apply (rule subsetD [OF Standard_subset_HFinite])
huffman@21842
   992
apply (simp add: HNatInfinite_def Nats_eq_Standard)
huffman@21842
   993
done
huffman@21842
   994
huffman@17318
   995
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
paulson@15082
   996
by (simp add: NSBseq_def)
paulson@15082
   997
paulson@15082
   998
text{*The standard definition implies the nonstandard definition*}
paulson@15082
   999
huffman@20552
  1000
lemma lemma_Bseq: "\<forall>n. norm (X n) \<le> K ==> \<forall>n. norm(X((f::nat=>nat) n)) \<le> K"
paulson@15082
  1001
by auto
paulson@15082
  1002
paulson@15082
  1003
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
huffman@21139
  1004
proof (unfold NSBseq_def, safe)
huffman@21139
  1005
  assume X: "Bseq X"
huffman@21139
  1006
  fix N assume N: "N \<in> HNatInfinite"
huffman@21139
  1007
  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
huffman@21139
  1008
  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
huffman@21139
  1009
  hence "hnorm (starfun X N) \<le> star_of K" by simp
huffman@21139
  1010
  also have "star_of K < star_of (K + 1)" by simp
huffman@21139
  1011
  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
huffman@21139
  1012
  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
huffman@21139
  1013
qed
paulson@15082
  1014
paulson@15082
  1015
text{*The nonstandard definition implies the standard definition*}
paulson@15082
  1016
huffman@21842
  1017
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
huffman@21842
  1018
apply (insert HInfinite_omega)
huffman@21842
  1019
apply (simp add: HInfinite_def)
huffman@21842
  1020
apply (simp add: order_less_imp_le)
paulson@15082
  1021
done
paulson@15082
  1022
huffman@21842
  1023
lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
huffman@21842
  1024
proof (rule ccontr)
huffman@21842
  1025
  let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
huffman@21842
  1026
  assume "NSBseq X"
huffman@21842
  1027
  hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
huffman@21842
  1028
    by (rule NSBseqD2)
huffman@21842
  1029
  assume "\<not> Bseq X"
huffman@21842
  1030
  hence "\<forall>K>0. \<exists>n. K < norm (X n)"
huffman@21842
  1031
    by (simp add: Bseq_def linorder_not_le)
huffman@21842
  1032
  hence "\<forall>K>0. K < norm (X (?n K))"
huffman@21842
  1033
    by (auto intro: LeastI_ex)
huffman@21842
  1034
  hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
huffman@21842
  1035
    by transfer
huffman@21842
  1036
  hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
huffman@21842
  1037
    by simp
huffman@21842
  1038
  hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
huffman@21842
  1039
    by (simp add: order_less_trans [OF SReal_less_omega])
huffman@21842
  1040
  hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
huffman@21842
  1041
    by (simp add: HInfinite_def)
huffman@21842
  1042
  with finite show "False"
huffman@21842
  1043
    by (simp add: HFinite_HInfinite_iff)
huffman@21842
  1044
qed
paulson@15082
  1045
paulson@15082
  1046
text{* Equivalence of nonstandard and standard definitions
paulson@15082
  1047
  for a bounded sequence*}
paulson@15082
  1048
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
paulson@15082
  1049
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
paulson@15082
  1050
paulson@15082
  1051
text{*A convergent sequence is bounded: 
paulson@15082
  1052
 Boundedness as a necessary condition for convergence. 
paulson@15082
  1053
 The nonstandard version has no existential, as usual *}
paulson@15082
  1054
paulson@15082
  1055
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
paulson@15082
  1056
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
huffman@20552
  1057
apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
paulson@15082
  1058
done
paulson@15082
  1059
paulson@15082
  1060
text{*Standard Version: easily now proved using equivalence of NS and
paulson@15082
  1061
 standard definitions *}
paulson@15082
  1062
lemma convergent_Bseq: "convergent X ==> Bseq X"
paulson@15082
  1063
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
paulson@15082
  1064
huffman@20696
  1065
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
paulson@15082
  1066
paulson@15082
  1067
lemma Bseq_isUb:
paulson@15082
  1068
  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
paulson@15082
  1069
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
paulson@15082
  1070
paulson@15082
  1071
paulson@15082
  1072
text{* Use completeness of reals (supremum property)
paulson@15082
  1073
   to show that any bounded sequence has a least upper bound*}
paulson@15082
  1074
paulson@15082
  1075
lemma Bseq_isLub:
paulson@15082
  1076
  "!!(X::nat=>real). Bseq X ==>
paulson@15082
  1077
   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
paulson@15082
  1078
by (blast intro: reals_complete Bseq_isUb)
paulson@15082
  1079
huffman@20552
  1080
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
paulson@15082
  1081
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
paulson@15082
  1082
huffman@20552
  1083
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
paulson@15082
  1084
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
paulson@15082
  1085
paulson@15082
  1086
huffman@20696
  1087
subsubsection{*A Bounded and Monotonic Sequence Converges*}
paulson@15082
  1088
paulson@15082
  1089
lemma lemma_converg1:
nipkow@15360
  1090
     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
paulson@15082
  1091
                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
nipkow@15360
  1092
               |] ==> \<forall>n \<ge> ma. X n = X ma"
paulson@15082
  1093
apply safe
paulson@15082
  1094
apply (drule_tac y = "X n" in isLubD2)
paulson@15082
  1095
apply (blast dest: order_antisym)+
paulson@15082
  1096
done
paulson@15082
  1097
paulson@15082
  1098
text{* The best of both worlds: Easier to prove this result as a standard
paulson@15082
  1099
   theorem and then use equivalence to "transfer" it into the
paulson@15082
  1100
   equivalent nonstandard form if needed!*}
paulson@15082
  1101
paulson@15082
  1102
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
paulson@15082
  1103
apply (simp add: LIMSEQ_def)
paulson@15082
  1104
apply (rule_tac x = "X m" in exI, safe)
paulson@15082
  1105
apply (rule_tac x = m in exI, safe)
paulson@15082
  1106
apply (drule spec, erule impE, auto)
paulson@15082
  1107
done
paulson@15082
  1108
paulson@15082
  1109
text{*Now, the same theorem in terms of NS limit *}
nipkow@15360
  1110
lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
paulson@15082
  1111
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
paulson@15082
  1112
paulson@15082
  1113
lemma lemma_converg2:
paulson@15082
  1114
   "!!(X::nat=>real).
paulson@15082
  1115
    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
paulson@15082
  1116
apply safe
paulson@15082
  1117
apply (drule_tac y = "X m" in isLubD2)
paulson@15082
  1118
apply (auto dest!: order_le_imp_less_or_eq)
paulson@15082
  1119
done
paulson@15082
  1120
paulson@15082
  1121
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
paulson@15082
  1122
by (rule setleI [THEN isUbI], auto)
paulson@15082
  1123
paulson@15082
  1124
text{* FIXME: @{term "U - T < U"} is redundant *}
paulson@15082
  1125
lemma lemma_converg4: "!!(X::nat=> real).
paulson@15082
  1126
               [| \<forall>m. X m ~= U;
paulson@15082
  1127
                  isLub UNIV {x. \<exists>n. X n = x} U;
paulson@15082
  1128
                  0 < T;
paulson@15082
  1129
                  U + - T < U
paulson@15082
  1130
               |] ==> \<exists>m. U + -T < X m & X m < U"
paulson@15082
  1131
apply (drule lemma_converg2, assumption)
paulson@15082
  1132
apply (rule ccontr, simp)
paulson@15082
  1133
apply (simp add: linorder_not_less)
paulson@15082
  1134
apply (drule lemma_converg3)
paulson@15082
  1135
apply (drule isLub_le_isUb, assumption)
paulson@15082
  1136
apply (auto dest: order_less_le_trans)
paulson@15082
  1137
done
paulson@15082
  1138
paulson@15082
  1139
text{*A standard proof of the theorem for monotone increasing sequence*}
paulson@15082
  1140
paulson@15082
  1141
lemma Bseq_mono_convergent:
huffman@20552
  1142
     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
paulson@15082
  1143
apply (simp add: convergent_def)
paulson@15082
  1144
apply (frule Bseq_isLub, safe)
paulson@15082
  1145
apply (case_tac "\<exists>m. X m = U", auto)
paulson@15082
  1146
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
paulson@15082
  1147
(* second case *)
paulson@15082
  1148
apply (rule_tac x = U in exI)
paulson@15082
  1149
apply (subst LIMSEQ_iff, safe)
paulson@15082
  1150
apply (frule lemma_converg2, assumption)
paulson@15082
  1151
apply (drule lemma_converg4, auto)
paulson@15082
  1152
apply (rule_tac x = m in exI, safe)
paulson@15082
  1153
apply (subgoal_tac "X m \<le> X n")
paulson@15082
  1154
 prefer 2 apply blast
paulson@15082
  1155
apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
paulson@15082
  1156
done
paulson@15082
  1157
paulson@15082
  1158
text{*Nonstandard version of the theorem*}
paulson@15082
  1159
paulson@15082
  1160
lemma NSBseq_mono_NSconvergent:
huffman@20552
  1161
     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
paulson@15082
  1162
by (auto intro: Bseq_mono_convergent 
paulson@15082
  1163
         simp add: convergent_NSconvergent_iff [symmetric] 
paulson@15082
  1164
                   Bseq_NSBseq_iff [symmetric])
paulson@15082
  1165
paulson@15082
  1166
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
paulson@15082
  1167
by (simp add: Bseq_def)
paulson@15082
  1168
paulson@15082
  1169
text{*Main monotonicity theorem*}
paulson@15082
  1170
lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
paulson@15082
  1171
apply (simp add: monoseq_def, safe)
paulson@15082
  1172
apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
paulson@15082
  1173
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
paulson@15082
  1174
apply (auto intro!: Bseq_mono_convergent)
paulson@15082
  1175
done
paulson@15082
  1176
huffman@20696
  1177
subsubsection{*A Few More Equivalence Theorems for Boundedness*}
paulson@15082
  1178
paulson@15082
  1179
text{*alternative formulation for boundedness*}
huffman@20552
  1180
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
paulson@15082
  1181
apply (unfold Bseq_def, safe)
huffman@20552
  1182
apply (rule_tac [2] x = "k + norm x" in exI)
nipkow@15360
  1183
apply (rule_tac x = K in exI, simp)
paulson@15221
  1184
apply (rule exI [where x = 0], auto)
huffman@20552
  1185
apply (erule order_less_le_trans, simp)
huffman@20552
  1186
apply (drule_tac x=n in spec, fold diff_def)
huffman@20552
  1187
apply (drule order_trans [OF norm_triangle_ineq2])
huffman@20552
  1188
apply simp
paulson@15082
  1189
done
paulson@15082
  1190
paulson@15082
  1191
text{*alternative formulation for boundedness*}
huffman@20552
  1192
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
paulson@15082
  1193
apply safe
paulson@15082
  1194
apply (simp add: Bseq_def, safe)
huffman@20552
  1195
apply (rule_tac x = "K + norm (X N)" in exI)
paulson@15082
  1196
apply auto
huffman@20552
  1197
apply (erule order_less_le_trans, simp)
paulson@15082
  1198
apply (rule_tac x = N in exI, safe)
huffman@20552
  1199
apply (drule_tac x = n in spec)
huffman@20552
  1200
apply (rule order_trans [OF norm_triangle_ineq], simp)
paulson@15082
  1201
apply (auto simp add: Bseq_iff2)
paulson@15082
  1202
done
paulson@15082
  1203
huffman@20552
  1204
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
paulson@15082
  1205
apply (simp add: Bseq_def)
paulson@15221
  1206
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
webertj@20217
  1207
apply (drule_tac x = n in spec, arith)
paulson@15082
  1208
done
paulson@15082
  1209
paulson@15082
  1210
huffman@20696
  1211
subsection {* Cauchy Sequences *}
paulson@15082
  1212
huffman@20751
  1213
lemma CauchyI:
huffman@20751
  1214
  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
huffman@20751
  1215
by (simp add: Cauchy_def)
huffman@20751
  1216
huffman@20751
  1217
lemma CauchyD:
huffman@20751
  1218
  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
huffman@20751
  1219
by (simp add: Cauchy_def)
huffman@20751
  1220
huffman@20751
  1221
lemma NSCauchyI:
huffman@20751
  1222
  "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
huffman@20751
  1223
   \<Longrightarrow> NSCauchy X"
huffman@20751
  1224
by (simp add: NSCauchy_def)
huffman@20751
  1225
huffman@20751
  1226
lemma NSCauchyD:
huffman@20751
  1227
  "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
huffman@20751
  1228
   \<Longrightarrow> starfun X M \<approx> starfun X N"
huffman@20751
  1229
by (simp add: NSCauchy_def)
huffman@20751
  1230
huffman@20696
  1231
subsubsection{*Equivalence Between NS and Standard*}
huffman@20696
  1232
huffman@20751
  1233
lemma Cauchy_NSCauchy:
huffman@20751
  1234
  assumes X: "Cauchy X" shows "NSCauchy X"
huffman@20751
  1235
proof (rule NSCauchyI)
huffman@20751
  1236
  fix M assume M: "M \<in> HNatInfinite"
huffman@20751
  1237
  fix N assume N: "N \<in> HNatInfinite"
huffman@20751
  1238
  have "starfun X M - starfun X N \<in> Infinitesimal"
huffman@20751
  1239
  proof (rule InfinitesimalI2)
huffman@20751
  1240
    fix r :: real assume r: "0 < r"
huffman@20751
  1241
    from CauchyD [OF X r]
huffman@20751
  1242
    obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
huffman@20751
  1243
    hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
huffman@20751
  1244
           hnorm (starfun X m - starfun X n) < star_of r"
huffman@20751
  1245
      by transfer
huffman@20751
  1246
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@20751
  1247
      using M N by (simp add: star_of_le_HNatInfinite)
huffman@20751
  1248
  qed
huffman@20751
  1249
  thus "starfun X M \<approx> starfun X N"
huffman@20751
  1250
    by (unfold approx_def)
huffman@20751
  1251
qed
paulson@15082
  1252
huffman@20751
  1253
lemma NSCauchy_Cauchy:
huffman@20751
  1254
  assumes X: "NSCauchy X" shows "Cauchy X"
huffman@20751
  1255
proof (rule CauchyI)
huffman@20751
  1256
  fix r::real assume r: "0 < r"
huffman@20751
  1257
  have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
huffman@20751
  1258
  proof (intro exI allI impI)
huffman@20751
  1259
    fix M assume "whn \<le> M"
huffman@20751
  1260
    with HNatInfinite_whn have M: "M \<in> HNatInfinite"
huffman@20751
  1261
      by (rule HNatInfinite_upward_closed)
huffman@20751
  1262
    fix N assume "whn \<le> N"
huffman@20751
  1263
    with HNatInfinite_whn have N: "N \<in> HNatInfinite"
huffman@20751
  1264
      by (rule HNatInfinite_upward_closed)
huffman@20751
  1265
    from X M N have "starfun X M \<approx> starfun X N"
huffman@20751
  1266
      by (rule NSCauchyD)
huffman@20751
  1267
    hence "starfun X M - starfun X N \<in> Infinitesimal"
huffman@20751
  1268
      by (unfold approx_def)
huffman@20751
  1269
    thus "hnorm (starfun X M - starfun X N) < star_of r"
huffman@20751
  1270
      using r by (rule InfinitesimalD2)
huffman@20751
  1271
  qed
huffman@20751
  1272
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
huffman@20751
  1273
    by transfer
huffman@20751
  1274
qed
paulson@15082
  1275
paulson@15082
  1276
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
paulson@15082
  1277
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
paulson@15082
  1278
huffman@20696
  1279
subsubsection {* Cauchy Sequences are Bounded *}
huffman@20696
  1280
paulson@15082
  1281
text{*A Cauchy sequence is bounded -- this is the standard
paulson@15082
  1282
  proof mechanization rather than the nonstandard proof*}
paulson@15082
  1283
huffman@20563
  1284
lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
huffman@20552
  1285
          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
huffman@20552
  1286
apply (clarify, drule spec, drule (1) mp)
huffman@20563
  1287
apply (simp only: norm_minus_commute)
huffman@20552
  1288
apply (drule order_le_less_trans [OF norm_triangle_ineq2])
huffman@20552
  1289
apply simp
huffman@20552
  1290
done
paulson@15082
  1291
paulson@15082
  1292
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
huffman@20552
  1293
apply (simp add: Cauchy_def)
huffman@20552
  1294
apply (drule spec, drule mp, rule zero_less_one, safe)
huffman@20552
  1295
apply (drule_tac x="M" in spec, simp)
paulson@15082
  1296
apply (drule lemmaCauchy)
huffman@22608
  1297
apply (rule_tac k="M" in Bseq_offset)
huffman@20552
  1298
apply (simp add: Bseq_def)
huffman@20552
  1299
apply (rule_tac x="1 + norm (X M)" in exI)
huffman@20552
  1300
apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
huffman@20552
  1301
apply (simp add: order_less_imp_le)
paulson@15082
  1302
done
paulson@15082
  1303
paulson@15082
  1304
text{*A Cauchy sequence is bounded -- nonstandard version*}
paulson@15082
  1305
paulson@15082
  1306
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
paulson@15082
  1307
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
paulson@15082
  1308
huffman@20696
  1309
subsubsection {* Cauchy Sequences are Convergent *}
paulson@15082
  1310
huffman@20830
  1311
axclass banach \<subseteq> real_normed_vector
huffman@20830
  1312
  Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
huffman@20830
  1313
paulson@15082
  1314
text{*Equivalence of Cauchy criterion and convergence:
paulson@15082
  1315
  We will prove this using our NS formulation which provides a
paulson@15082
  1316
  much easier proof than using the standard definition. We do not
paulson@15082
  1317
  need to use properties of subsequences such as boundedness,
paulson@15082
  1318
  monotonicity etc... Compare with Harrison's corresponding proof
paulson@15082
  1319
  in HOL which is much longer and more complicated. Of course, we do
paulson@15082
  1320
  not have problems which he encountered with guessing the right
paulson@15082
  1321
  instantiations for his 'espsilon-delta' proof(s) in this case
paulson@15082
  1322
  since the NS formulations do not involve existential quantifiers.*}
paulson@15082
  1323
huffman@20691
  1324
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
huffman@20691
  1325
apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
huffman@20691
  1326
apply (auto intro: approx_trans2)
huffman@20691
  1327
done
huffman@20691
  1328
huffman@20691
  1329
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
huffman@20691
  1330
apply (rule NSconvergent_NSCauchy [THEN NSCauchy_Cauchy])
huffman@20691
  1331
apply (simp add: convergent_NSconvergent_iff)
huffman@20691
  1332
done
huffman@20691
  1333
huffman@20830
  1334
lemma real_NSCauchy_NSconvergent:
huffman@20830
  1335
  fixes X :: "nat \<Rightarrow> real"
huffman@20830
  1336
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@20830
  1337
apply (simp add: NSconvergent_def NSLIMSEQ_def)
paulson@15082
  1338
apply (frule NSCauchy_NSBseq)
huffman@20830
  1339
apply (simp add: NSBseq_def NSCauchy_def)
paulson@15082
  1340
apply (drule HNatInfinite_whn [THEN [2] bspec])
paulson@15082
  1341
apply (drule HNatInfinite_whn [THEN [2] bspec])
paulson@15082
  1342
apply (auto dest!: st_part_Ex simp add: SReal_iff)
paulson@15082
  1343
apply (blast intro: approx_trans3)
paulson@15082
  1344
done
paulson@15082
  1345
paulson@15082
  1346
text{*Standard proof for free*}
huffman@20830
  1347
lemma real_Cauchy_convergent:
huffman@20830
  1348
  fixes X :: "nat \<Rightarrow> real"
huffman@20830
  1349
  shows "Cauchy X \<Longrightarrow> convergent X"
huffman@20830
  1350
apply (drule Cauchy_NSCauchy [THEN real_NSCauchy_NSconvergent])
huffman@20830
  1351
apply (erule convergent_NSconvergent_iff [THEN iffD2])
huffman@20830
  1352
done
huffman@20830
  1353
huffman@20830
  1354
instance real :: banach
huffman@20830
  1355
by intro_classes (rule real_Cauchy_convergent)
huffman@20830
  1356
huffman@20830
  1357
lemma NSCauchy_NSconvergent:
huffman@20830
  1358
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
  1359
  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
huffman@20830
  1360
apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
huffman@20830
  1361
apply (erule convergent_NSconvergent_iff [THEN iffD1])
huffman@20830
  1362
done
huffman@20830
  1363
huffman@20830
  1364
lemma NSCauchy_NSconvergent_iff:
huffman@20830
  1365
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
  1366
  shows "NSCauchy X = NSconvergent X"
huffman@20830
  1367
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
huffman@20830
  1368
huffman@20830
  1369
lemma Cauchy_convergent_iff:
huffman@20830
  1370
  fixes X :: "nat \<Rightarrow> 'a::banach"
huffman@20830
  1371
  shows "Cauchy X = convergent X"
huffman@20830
  1372
by (fast intro: Cauchy_convergent convergent_Cauchy)
paulson@15082
  1373
paulson@15082
  1374
huffman@20696
  1375
subsection {* Power Sequences *}
paulson@15082
  1376
paulson@15082
  1377
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
paulson@15082
  1378
"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
paulson@15082
  1379
  also fact that bounded and monotonic sequence converges.*}
paulson@15082
  1380
huffman@20552
  1381
lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
paulson@15082
  1382
apply (simp add: Bseq_def)
paulson@15082
  1383
apply (rule_tac x = 1 in exI)
paulson@15082
  1384
apply (simp add: power_abs)
paulson@15082
  1385
apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
paulson@15082
  1386
done
paulson@15082
  1387
paulson@15082
  1388
lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
paulson@15082
  1389
apply (clarify intro!: mono_SucI2)
paulson@15082
  1390
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
paulson@15082
  1391
done
paulson@15082
  1392
huffman@20552
  1393
lemma convergent_realpow:
huffman@20552
  1394
  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
paulson@15082
  1395
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
paulson@15082
  1396
paulson@15082
  1397
text{* We now use NS criterion to bring proof of theorem through *}
paulson@15082
  1398
huffman@20552
  1399
lemma NSLIMSEQ_realpow_zero:
huffman@20552
  1400
  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----NS> 0"
paulson@15082
  1401
apply (simp add: NSLIMSEQ_def)
paulson@15082
  1402
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
paulson@15082
  1403
apply (frule NSconvergentD)
huffman@17318
  1404
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
paulson@15082
  1405
apply (frule HNatInfinite_add_one)
paulson@15082
  1406
apply (drule bspec, assumption)
paulson@15082
  1407
apply (drule bspec, assumption)
paulson@15082
  1408
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
paulson@15082
  1409
apply (simp add: hyperpow_add)
huffman@21810
  1410
apply (drule approx_mult_subst_star_of, assumption)
paulson@15082
  1411
apply (drule approx_trans3, assumption)
huffman@17318
  1412
apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
paulson@15082
  1413
done
paulson@15082
  1414
huffman@22628
  1415
lemma LIMSEQ_inverse_realpow_zero_lemma:
huffman@22628
  1416
  fixes x :: real
huffman@22628
  1417
  assumes x: "0 \<le> x"
huffman@22628
  1418
  shows "real n * x + 1 \<le> (x + 1) ^ n"
huffman@22628
  1419
apply (induct n)
huffman@22628
  1420
apply simp
huffman@22628
  1421
apply simp
huffman@22628
  1422
apply (rule order_trans)
huffman@22628
  1423
prefer 2
huffman@22628
  1424
apply (erule mult_left_mono)
huffman@22628
  1425
apply (rule add_increasing [OF x], simp)
huffman@22628
  1426
apply (simp add: real_of_nat_Suc)
huffman@22628
  1427
apply (simp add: ring_distrib)
huffman@22628
  1428
apply (simp add: mult_nonneg_nonneg x)
huffman@22628
  1429
done
huffman@22628
  1430
huffman@22628
  1431
lemma LIMSEQ_inverse_realpow_zero:
huffman@22628
  1432
  "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
huffman@22628
  1433
proof (rule LIMSEQ_inverse_zero [rule_format])
huffman@22628
  1434
  fix y :: real
huffman@22628
  1435
  assume x: "1 < x"
huffman@22628
  1436
  hence "0 < x - 1" by simp
huffman@22628
  1437
  hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)"
huffman@22628
  1438
    by (rule reals_Archimedean3)
huffman@22628
  1439
  hence "\<exists>N::nat. y < real N * (x - 1)" ..
huffman@22628
  1440
  then obtain N::nat where "y < real N * (x - 1)" ..
huffman@22628
  1441
  also have "\<dots> \<le> real N * (x - 1) + 1" by simp
huffman@22628
  1442
  also have "\<dots> \<le> (x - 1 + 1) ^ N"
huffman@22628
  1443
    by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp)
huffman@22628
  1444
  also have "\<dots> = x ^ N" by simp
huffman@22628
  1445
  finally have "y < x ^ N" .
huffman@22628
  1446
  hence "\<forall>n\<ge>N. y < x ^ n"
huffman@22628
  1447
    apply clarify
huffman@22628
  1448
    apply (erule order_less_le_trans)
huffman@22628
  1449
    apply (erule power_increasing)
huffman@22628
  1450
    apply (rule order_less_imp_le [OF x])
huffman@22628
  1451
    done
huffman@22628
  1452
  thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" ..
huffman@22628
  1453
qed
huffman@22628
  1454
huffman@20552
  1455
lemma LIMSEQ_realpow_zero:
huffman@22628
  1456
  "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
huffman@22628
  1457
proof (cases)
huffman@22628
  1458
  assume "x = 0"
huffman@22628
  1459
  hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const)
huffman@22628
  1460
  thus ?thesis by (rule LIMSEQ_imp_Suc)
huffman@22628
  1461
next
huffman@22628
  1462
  assume "0 \<le> x" and "x \<noteq> 0"
huffman@22628
  1463
  hence x0: "0 < x" by simp
huffman@22628
  1464
  assume x1: "x < 1"
huffman@22628
  1465
  from x0 x1 have "1 < inverse x"
huffman@22628
  1466
    by (rule real_inverse_gt_one)
huffman@22628
  1467
  hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
huffman@22628
  1468
    by (rule LIMSEQ_inverse_realpow_zero)
huffman@22628
  1469
  thus ?thesis by (simp add: power_inverse)
huffman@22628
  1470
qed
paulson@15082
  1471
huffman@20685
  1472
lemma LIMSEQ_power_zero:
huffman@20685
  1473
  fixes x :: "'a::{real_normed_div_algebra,recpower}"
huffman@20685
  1474
  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
huffman@20685
  1475
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
huffman@20685
  1476
apply (simp add: norm_power [symmetric] LIMSEQ_norm_zero)
huffman@20685
  1477
done
huffman@20685
  1478
huffman@20552
  1479
lemma LIMSEQ_divide_realpow_zero:
huffman@20552
  1480
  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
paulson@15082
  1481
apply (cut_tac a = a and x1 = "inverse x" in
paulson@15082
  1482
        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
paulson@15082
  1483
apply (auto simp add: divide_inverse power_inverse)
paulson@15082
  1484
apply (simp add: inverse_eq_divide pos_divide_less_eq)
paulson@15082
  1485
done
paulson@15082
  1486
paulson@15102
  1487
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
paulson@15082
  1488
huffman@20552
  1489
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
huffman@20685
  1490
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
paulson@15082
  1491
huffman@20552
  1492
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
paulson@15082
  1493
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
paulson@15082
  1494
huffman@20552
  1495
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
paulson@15082
  1496
apply (rule LIMSEQ_rabs_zero [THEN iffD1])
paulson@15082
  1497
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
paulson@15082
  1498
done
paulson@15082
  1499
huffman@20552
  1500
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
paulson@15082
  1501
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
paulson@15082
  1502
paulson@15082
  1503
(***---------------------------------------------------------------
paulson@15082
  1504
    Theorems proved by Harrison in HOL that we do not need
paulson@15082
  1505
    in order to prove equivalence between Cauchy criterion
paulson@15082
  1506
    and convergence:
paulson@15082
  1507
 -- Show that every sequence contains a monotonic subsequence
paulson@15082
  1508
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
paulson@15082
  1509
 -- Show that a subsequence of a bounded sequence is bounded
paulson@15082
  1510
Goal "Bseq X ==> Bseq (%n. X (f n))";
paulson@15082
  1511
 -- Show we can take subsequential terms arbitrarily far
paulson@15082
  1512
    up a sequence
paulson@15082
  1513
Goal "subseq f ==> n \<le> f(n)";
paulson@15082
  1514
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
paulson@15082
  1515
 ---------------------------------------------------------------***)
paulson@15082
  1516
paulson@10751
  1517
end