src/HOL/Hyperreal/HSeries.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15047 fa62de5862b9
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
paulson@10751
     1
(*  Title       : HSeries.thy
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@14413
     4
paulson@14413
     5
Converted to Isar and polished by lcp    
paulson@10751
     6
*) 
paulson@10751
     7
paulson@14413
     8
header{*Finite Summation and Infinite Series for Hyperreals*}
paulson@10751
     9
nipkow@15131
    10
theory HSeries
nipkow@15131
    11
import Series
nipkow@15131
    12
begin
paulson@10751
    13
paulson@14413
    14
constdefs 
paulson@14413
    15
  sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
paulson@14413
    16
   "sumhr p == 
paulson@14413
    17
      (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
paulson@14413
    18
                             hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
paulson@10751
    19
paulson@14413
    20
  NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
paulson@10751
    21
   "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
paulson@10751
    22
paulson@14413
    23
  NSsummable :: "(nat=>real) => bool"
paulson@14413
    24
   "NSsummable f == (\<exists>s. f NSsums s)"
paulson@10751
    25
paulson@14413
    26
  NSsuminf   :: "(nat=>real) => real"
paulson@10751
    27
   "NSsuminf f == (@s. f NSsums s)"
paulson@10751
    28
paulson@14413
    29
paulson@14413
    30
lemma sumhr: 
paulson@14413
    31
     "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
paulson@14413
    32
            Abs_hypnat(hypnatrel``{%n. N n}), f) =  
paulson@14413
    33
      Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"
paulson@14413
    34
apply (simp add: sumhr_def)
paulson@14413
    35
apply (rule arg_cong [where f = Abs_hypreal]) 
paulson@14413
    36
apply (auto, ultra)
paulson@14413
    37
done
paulson@14413
    38
paulson@14413
    39
text{*Base case in definition of @{term sumr}*}
paulson@14413
    40
lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
paulson@14468
    41
apply (cases m)
paulson@14413
    42
apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
paulson@14413
    43
done
paulson@14413
    44
paulson@14413
    45
text{*Recursive case in definition of @{term sumr}*}
paulson@14413
    46
lemma sumhr_if: 
paulson@14413
    47
     "sumhr(m,n+1,f) = 
paulson@14413
    48
      (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
paulson@14468
    49
apply (cases m, cases n)
paulson@14413
    50
apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
paulson@14413
    51
           hypreal_add hypreal_zero_def,   ultra+)
paulson@14413
    52
done
paulson@14413
    53
paulson@14413
    54
lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
paulson@14468
    55
apply (cases n)
paulson@14413
    56
apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
paulson@14413
    57
done
paulson@14413
    58
paulson@14413
    59
lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
paulson@14468
    60
apply (cases n)
paulson@14413
    61
apply (simp add: sumhr hypreal_zero_def)
paulson@14413
    62
done
paulson@14413
    63
paulson@14413
    64
lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
paulson@14468
    65
apply (cases m)
paulson@14413
    66
apply (simp add: sumhr hypnat_one_def  hypnat_add starfunNat)
paulson@14413
    67
done
paulson@14413
    68
paulson@14413
    69
lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
paulson@14468
    70
apply (cases m, cases k)
paulson@14413
    71
apply (simp add: sumhr hypnat_add hypreal_zero_def)
paulson@14413
    72
done
paulson@14413
    73
paulson@14413
    74
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
paulson@14468
    75
apply (cases m, cases n)
paulson@14413
    76
apply (simp add: sumhr hypreal_add sumr_add)
paulson@14413
    77
done
paulson@14413
    78
paulson@14413
    79
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
paulson@14468
    80
apply (cases m, cases n)
paulson@14413
    81
apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
paulson@14413
    82
done
paulson@14413
    83
paulson@14413
    84
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
paulson@14468
    85
apply (cases n, cases p)
paulson@14413
    86
apply (auto elim!: FreeUltrafilterNat_subset simp 
paulson@14413
    87
            add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
paulson@14413
    88
done
paulson@14413
    89
paulson@14413
    90
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
paulson@14413
    91
by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
paulson@14413
    92
paulson@14413
    93
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
paulson@14468
    94
apply (cases n, cases m)
paulson@14413
    95
apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
paulson@14413
    96
done
paulson@14413
    97
paulson@14413
    98
text{* other general version also needed *}
paulson@14413
    99
lemma sumhr_fun_hypnat_eq:
paulson@14413
   100
   "(\<forall>r. m \<le> r & r < n --> f r = g r) -->  
paulson@14413
   101
      sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =  
paulson@14413
   102
      sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
paulson@14413
   103
apply (safe, drule sumr_fun_eq)
paulson@14413
   104
apply (simp add: sumhr hypnat_of_nat_eq)
paulson@14413
   105
done
paulson@14413
   106
paulson@15047
   107
lemma sumhr_const:
paulson@15047
   108
     "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
paulson@14468
   109
apply (cases n)
paulson@14413
   110
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
paulson@15047
   111
                 hypreal_mult real_of_nat_def)
paulson@14413
   112
done
paulson@14413
   113
paulson@14413
   114
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
paulson@14468
   115
apply (cases m, cases n)
paulson@14413
   116
apply (auto elim: FreeUltrafilterNat_subset 
paulson@14413
   117
            simp add: sumhr hypnat_less hypreal_zero_def)
paulson@14413
   118
done
paulson@14413
   119
paulson@14413
   120
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
paulson@14468
   121
apply (cases m, cases n)
paulson@14413
   122
apply (simp add: sumhr hypreal_minus sumr_minus)
paulson@14413
   123
done
paulson@14413
   124
paulson@14413
   125
lemma sumhr_shift_bounds:
paulson@14413
   126
     "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
paulson@14468
   127
apply (cases m, cases n)
paulson@14413
   128
apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
paulson@14413
   129
done
paulson@14413
   130
paulson@14413
   131
paulson@14413
   132
subsection{*Nonstandard Sums*}
paulson@14413
   133
paulson@14413
   134
text{*Infinite sums are obtained by summing to some infinite hypernatural
paulson@14413
   135
 (such as @{term whn})*}
paulson@14413
   136
lemma sumhr_hypreal_of_hypnat_omega: 
paulson@14413
   137
      "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
paulson@15047
   138
by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat
paulson@15047
   139
              real_of_nat_def)
paulson@14413
   140
paulson@14413
   141
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
paulson@14413
   142
by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
paulson@15047
   143
              sumhr hypreal_diff real_of_nat_def)
paulson@14413
   144
paulson@14413
   145
lemma sumhr_minus_one_realpow_zero [simp]: 
paulson@14413
   146
     "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
paulson@14413
   147
by (simp del: realpow_Suc 
paulson@14435
   148
         add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def 
paulson@14413
   149
              hypnat_zero_def hypnat_omega_def)
paulson@14413
   150
paulson@14413
   151
lemma sumhr_interval_const:
paulson@14413
   152
     "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
paulson@14413
   153
      ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
paulson@14413
   154
          (hypreal_of_nat (na - m) * hypreal_of_real r)"
paulson@14413
   155
by (auto dest!: sumr_interval_const 
paulson@14413
   156
         simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq 
paulson@14413
   157
                   hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
paulson@14413
   158
paulson@14413
   159
lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
paulson@14468
   160
apply (cases N)
paulson@14413
   161
apply (simp add: hypnat_zero_def starfunNat sumhr)
paulson@14413
   162
done
paulson@14413
   163
paulson@14413
   164
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)  
paulson@14413
   165
      ==> abs (sumhr(M, N, f)) @= 0"
paulson@14413
   166
apply (cut_tac x = M and y = N in linorder_less_linear)
paulson@14413
   167
apply (auto simp add: approx_refl)
paulson@14413
   168
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
paulson@14413
   169
apply (auto dest: approx_hrabs 
paulson@14413
   170
            simp add: sumhr_split_diff diff_minus [symmetric])
paulson@14413
   171
done
paulson@14413
   172
paulson@14413
   173
(*----------------------------------------------------------------
paulson@14413
   174
      infinite sums: Standard and NS theorems
paulson@14413
   175
 ----------------------------------------------------------------*)
paulson@14413
   176
lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
paulson@14413
   177
by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
paulson@14413
   178
paulson@14413
   179
lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
paulson@14413
   180
by (simp add: summable_def NSsummable_def sums_NSsums_iff)
paulson@14413
   181
paulson@14413
   182
lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
paulson@14413
   183
by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
paulson@14413
   184
paulson@14413
   185
lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
paulson@14413
   186
by (simp add: NSsums_def NSsummable_def, blast)
paulson@14413
   187
paulson@14413
   188
lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
paulson@14413
   189
apply (simp add: NSsummable_def NSsuminf_def)
paulson@14413
   190
apply (blast intro: someI2)
paulson@14413
   191
done
paulson@14413
   192
paulson@14413
   193
lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
paulson@14413
   194
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
paulson@14413
   195
paulson@14413
   196
lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
paulson@14413
   197
by (simp add: sums_NSsums_iff [symmetric] series_zero)
paulson@14413
   198
paulson@14413
   199
lemma NSsummable_NSCauchy:
paulson@14413
   200
     "NSsummable f =  
paulson@14413
   201
      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
paulson@14413
   202
apply (auto simp add: summable_NSsummable_iff [symmetric] 
paulson@14413
   203
       summable_convergent_sumr_iff convergent_NSconvergent_iff 
paulson@14413
   204
       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
paulson@14413
   205
apply (cut_tac x = M and y = N in linorder_less_linear)
paulson@14413
   206
apply (auto simp add: approx_refl)
paulson@14413
   207
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
paulson@14413
   208
apply (rule_tac [2] approx_minus_iff [THEN iffD2])
paulson@14413
   209
apply (auto dest: approx_hrabs_zero_cancel 
paulson@14413
   210
            simp add: sumhr_split_diff diff_minus [symmetric])
paulson@14413
   211
done
paulson@14413
   212
paulson@14413
   213
paulson@14413
   214
text{*Terms of a convergent series tend to zero*}
paulson@14413
   215
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
paulson@14413
   216
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
paulson@14413
   217
apply (drule bspec, auto)
paulson@14413
   218
apply (drule_tac x = "N + 1 " in bspec)
paulson@14413
   219
apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
paulson@14413
   220
done
paulson@14413
   221
paulson@14413
   222
text{* Easy to prove stsandard case now *}
paulson@14413
   223
lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0"
paulson@14413
   224
by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero)
paulson@14413
   225
paulson@14413
   226
text{*Nonstandard comparison test*}
paulson@14413
   227
lemma NSsummable_comparison_test:
paulson@14413
   228
     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
paulson@14413
   229
by (auto intro: summable_comparison_test 
paulson@14413
   230
         simp add: summable_NSsummable_iff [symmetric])
paulson@14413
   231
paulson@14413
   232
lemma NSsummable_rabs_comparison_test:
paulson@14413
   233
     "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
paulson@14413
   234
      ==> NSsummable (%k. abs (f k))"
paulson@14413
   235
apply (rule NSsummable_comparison_test)
paulson@14413
   236
apply (auto simp add: abs_idempotent)
paulson@14413
   237
done
paulson@14413
   238
paulson@14413
   239
ML
paulson@14413
   240
{*
paulson@14413
   241
val sumhr = thm "sumhr";
paulson@14413
   242
val sumhr_zero = thm "sumhr_zero";
paulson@14413
   243
val sumhr_if = thm "sumhr_if";
paulson@14413
   244
val sumhr_Suc_zero = thm "sumhr_Suc_zero";
paulson@14413
   245
val sumhr_eq_bounds = thm "sumhr_eq_bounds";
paulson@14413
   246
val sumhr_Suc = thm "sumhr_Suc";
paulson@14413
   247
val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
paulson@14413
   248
val sumhr_add = thm "sumhr_add";
paulson@14413
   249
val sumhr_mult = thm "sumhr_mult";
paulson@14413
   250
val sumhr_split_add = thm "sumhr_split_add";
paulson@14413
   251
val sumhr_split_diff = thm "sumhr_split_diff";
paulson@14413
   252
val sumhr_hrabs = thm "sumhr_hrabs";
paulson@14413
   253
val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
paulson@14413
   254
val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
paulson@14413
   255
val sumhr_minus = thm "sumhr_minus";
paulson@14413
   256
val sumhr_shift_bounds = thm "sumhr_shift_bounds";
paulson@14413
   257
val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
paulson@14413
   258
val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
paulson@14413
   259
val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
paulson@14413
   260
val sumhr_interval_const = thm "sumhr_interval_const";
paulson@14413
   261
val starfunNat_sumr = thm "starfunNat_sumr";
paulson@14413
   262
val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
paulson@14413
   263
val sums_NSsums_iff = thm "sums_NSsums_iff";
paulson@14413
   264
val summable_NSsummable_iff = thm "summable_NSsummable_iff";
paulson@14413
   265
val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
paulson@14413
   266
val NSsums_NSsummable = thm "NSsums_NSsummable";
paulson@14413
   267
val NSsummable_NSsums = thm "NSsummable_NSsums";
paulson@14413
   268
val NSsums_unique = thm "NSsums_unique";
paulson@14413
   269
val NSseries_zero = thm "NSseries_zero";
paulson@14413
   270
val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
paulson@14413
   271
val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
paulson@14413
   272
val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
paulson@14413
   273
val NSsummable_comparison_test = thm "NSsummable_comparison_test";
paulson@14413
   274
val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
paulson@14413
   275
*}
paulson@14413
   276
paulson@10751
   277
end