src/HOL/Hyperreal/HSeries.ML
author nipkow
Fri Feb 07 16:40:23 2003 +0100 (2003-02-07)
changeset 13810 c3fbfd472365
parent 12018 ec054019c910
child 14371 c78c7da09519
permissions -rw-r--r--
(*f -> ( *f because of new comments
paulson@10751
     1
(*  Title       : HSeries.ML
paulson@10751
     2
    Author      : Jacques D. Fleuriot
paulson@10751
     3
    Copyright   : 1998  University of Cambridge
paulson@10751
     4
    Description : Finite summation and infinite series
paulson@10751
     5
                  for hyperreals
paulson@10751
     6
*) 
paulson@10751
     7
paulson@10751
     8
Goalw [sumhr_def]
paulson@10751
     9
     "sumhr(M,N,f) =  \
paulson@10751
    10
\       Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
nipkow@10834
    11
\         hyprel ``{%n::nat. sumr (X n) (Y n) f})";
paulson@10751
    12
by (Auto_tac);
paulson@10751
    13
qed "sumhr_iff";
paulson@10751
    14
paulson@10751
    15
Goalw [sumhr_def]
nipkow@10834
    16
     "sumhr(Abs_hypnat(hypnatrel``{%n. M n}), \
nipkow@10834
    17
\           Abs_hypnat(hypnatrel``{%n. N n}), f) = \
nipkow@10834
    18
\     Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})";
paulson@10751
    19
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
paulson@10751
    20
by (Auto_tac THEN Ultra_tac 1);
paulson@10751
    21
qed "sumhr";
paulson@10751
    22
paulson@10751
    23
(*------------------------------------------------------- 
paulson@10751
    24
  lcp's suggestion: exploit pattern matching 
paulson@10751
    25
  facilities and use as definition instead (to do)
paulson@10751
    26
 -------------------------------------------------------*)
paulson@10751
    27
Goalw [sumhr_def]
paulson@10751
    28
      "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
paulson@10751
    29
\                     UN Y: Rep_hypnat(N). \
nipkow@10834
    30
\           hyprel ``{%n::nat. sumr (X n) (Y n) f})) p";
paulson@10751
    31
by (res_inst_tac [("p","p")] PairE 1);
paulson@10751
    32
by (res_inst_tac [("p","y")] PairE 1);
paulson@10751
    33
by (Auto_tac);
paulson@10751
    34
qed "sumhr_iff2";
paulson@10751
    35
paulson@10751
    36
(* Theorem corresponding to base case in def of sumr *)
paulson@10751
    37
Goalw [hypnat_zero_def]
paulson@12018
    38
     "sumhr (m,0,f) = 0";
paulson@10751
    39
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    40
by (auto_tac (claset(), 
paulson@10751
    41
              simpset() addsimps [sumhr, symmetric hypreal_zero_def]));
paulson@10751
    42
qed "sumhr_zero";
paulson@10751
    43
Addsimps [sumhr_zero];
paulson@10751
    44
paulson@10751
    45
(* Theorem corresponding to recursive case in def of sumr *)
paulson@10751
    46
Goalw [hypnat_one_def]
paulson@12018
    47
     "sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then 0 \
nipkow@13810
    48
\                         else sumhr(m,n,f) + ( *fNat* f) n)";
paulson@10751
    49
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    50
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
    51
by (auto_tac (claset(),
paulson@12018
    52
     simpset() addsimps [sumhr, hypnat_add,hypnat_le,starfunNat,hypreal_add, 
paulson@12018
    53
                         hypreal_zero_def]));
paulson@10751
    54
by (ALLGOALS(Ultra_tac));
paulson@10751
    55
qed "sumhr_if";
paulson@10751
    56
paulson@12018
    57
Goalw [hypnat_one_def] "sumhr (n + (1::hypnat), n, f) = 0";
paulson@10751
    58
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
    59
by (auto_tac (claset(),
paulson@12018
    60
              simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def]));
paulson@10751
    61
qed "sumhr_Suc_zero";
paulson@10751
    62
Addsimps [sumhr_Suc_zero];
paulson@10751
    63
paulson@12018
    64
Goal "sumhr (n,n,f) = 0";
paulson@10751
    65
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@12018
    66
by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_zero_def]));
paulson@10751
    67
qed "sumhr_eq_bounds";
paulson@10751
    68
Addsimps [sumhr_eq_bounds];
paulson@10751
    69
paulson@10751
    70
Goalw [hypnat_one_def] 
nipkow@13810
    71
     "sumhr (m,m + (1::hypnat),f) = ( *fNat* f) m";
paulson@10751
    72
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    73
by (auto_tac (claset(),
paulson@10751
    74
              simpset() addsimps [sumhr, hypnat_add,starfunNat]));
paulson@10751
    75
qed "sumhr_Suc";
paulson@10751
    76
Addsimps [sumhr_Suc];
paulson@10751
    77
paulson@12018
    78
Goal "sumhr(m+k,k,f) = 0";
paulson@10751
    79
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    80
by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
paulson@10751
    81
by (auto_tac (claset(),
paulson@12018
    82
              simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def]));
paulson@10751
    83
qed "sumhr_add_lbound_zero";
paulson@10751
    84
Addsimps [sumhr_add_lbound_zero];
paulson@10751
    85
paulson@10751
    86
Goal "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)";
paulson@10751
    87
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    88
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
    89
by (auto_tac (claset(),
paulson@10751
    90
              simpset() addsimps [sumhr, hypreal_add,sumr_add]));
paulson@10751
    91
qed "sumhr_add";
paulson@10751
    92
paulson@10751
    93
Goalw [hypreal_of_real_def]
paulson@10751
    94
      "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)";
paulson@10751
    95
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
    96
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
    97
by (auto_tac (claset(),
paulson@10751
    98
              simpset() addsimps [sumhr, hypreal_mult,sumr_mult]));
paulson@10751
    99
qed "sumhr_mult";
paulson@10751
   100
paulson@10751
   101
Goalw [hypnat_zero_def]
paulson@10751
   102
     "n < p ==> sumhr (0,n,f) + sumhr (n,p,f) = sumhr (0,p,f)";
paulson@10751
   103
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   104
by (res_inst_tac [("z","p")] eq_Abs_hypnat 1);
paulson@10751
   105
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset],
paulson@10751
   106
       simpset() addsimps [sumhr,hypreal_add,hypnat_less, sumr_split_add]));
paulson@10751
   107
qed "sumhr_split_add";
paulson@10751
   108
paulson@10751
   109
(*FIXME delete*)
paulson@10751
   110
Goal "n < p ==> sumhr (0, p, f) + - sumhr (0, n, f) = sumhr (n,p,f)";
paulson@10751
   111
by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
paulson@10751
   112
by (Asm_simp_tac 1);
paulson@10751
   113
qed "sumhr_split_add_minus";
paulson@10751
   114
paulson@10751
   115
Goal "n < p ==> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n,p,f)";
paulson@10751
   116
by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
paulson@10751
   117
by (Asm_simp_tac 1);
paulson@10751
   118
qed "sumhr_split_diff";
paulson@10751
   119
paulson@10751
   120
Goal "abs(sumhr(m,n,f)) <= sumhr(m,n,%i. abs(f i))";
paulson@10751
   121
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   122
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
   123
by (auto_tac (claset(),
paulson@10751
   124
              simpset() addsimps [sumhr, hypreal_le,hypreal_hrabs,sumr_rabs]));
paulson@10751
   125
qed "sumhr_hrabs";
paulson@10751
   126
paulson@10751
   127
(* other general version also needed *)
paulson@10751
   128
Goalw [hypnat_of_nat_def]
paulson@10751
   129
     "(ALL r. m <= r & r < n --> f r = g r) --> \
paulson@10751
   130
\     sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \
paulson@10751
   131
\     sumhr(hypnat_of_nat m, hypnat_of_nat n, g)";
paulson@10751
   132
by (Step_tac 1 THEN dtac sumr_fun_eq 1);
paulson@10751
   133
by (auto_tac (claset(), simpset() addsimps [sumhr]));
paulson@10751
   134
qed "sumhr_fun_hypnat_eq";
paulson@10751
   135
paulson@10751
   136
Goalw [hypnat_zero_def,hypreal_of_real_def]
paulson@10751
   137
      "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r";
paulson@10751
   138
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   139
by (asm_simp_tac
paulson@10751
   140
    (simpset() addsimps [sumhr, hypreal_of_hypnat,hypreal_mult]) 1);
paulson@10751
   141
qed "sumhr_const";
paulson@10751
   142
paulson@10751
   143
Goalw [hypnat_zero_def,hypreal_of_real_def]
paulson@10751
   144
     "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = \
paulson@10751
   145
\     sumhr(0,n,%i. f i + -r)";
paulson@10751
   146
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   147
by (asm_simp_tac (simpset() addsimps [sumhr,
paulson@10751
   148
		    hypreal_of_hypnat,hypreal_mult,hypreal_add,
paulson@10751
   149
		    hypreal_minus,sumr_add RS sym]) 1);
paulson@10751
   150
qed "sumhr_add_mult_const";
paulson@10751
   151
paulson@12018
   152
Goal "n < m ==> sumhr (m,n,f) = 0";
paulson@10751
   153
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
   154
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   155
by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],
paulson@12018
   156
              simpset() addsimps [sumhr,hypnat_less, hypreal_zero_def]));
paulson@10751
   157
qed "sumhr_less_bounds_zero";
paulson@10751
   158
Addsimps [sumhr_less_bounds_zero];
paulson@10751
   159
paulson@10751
   160
Goal "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)";
paulson@10751
   161
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
   162
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   163
by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus]));
paulson@10751
   164
qed "sumhr_minus";
paulson@10751
   165
paulson@10751
   166
Goalw [hypnat_of_nat_def]
paulson@10751
   167
     "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
paulson@10751
   168
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@10751
   169
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@10751
   170
by (auto_tac (claset(),
paulson@10751
   171
              simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds]));
paulson@10751
   172
qed "sumhr_shift_bounds";
paulson@10751
   173
paulson@10751
   174
(*------------------------------------------------------------------
paulson@10751
   175
      Theorems about NS sums - infinite sums are obtained
paulson@10751
   176
      by summing to some infinite hypernatural (such as whn)
paulson@10751
   177
 -----------------------------------------------------------------*)
paulson@10751
   178
Goalw [hypnat_omega_def,hypnat_zero_def] 
paulson@12018
   179
      "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn";
paulson@10751
   180
by (auto_tac (claset(),
paulson@10751
   181
              simpset() addsimps [sumhr, hypreal_of_hypnat]));
paulson@10751
   182
qed "sumhr_hypreal_of_hypnat_omega";
paulson@10751
   183
paulson@10751
   184
Goalw [hypnat_omega_def,hypnat_zero_def,omega_def]  
paulson@12018
   185
     "sumhr(0, whn, %i. 1) = omega - 1";
paulson@10751
   186
by (simp_tac (HOL_ss addsimps
paulson@12018
   187
             [hypreal_numeral_1_eq_1, hypreal_one_def]) 1); 
paulson@10751
   188
by (auto_tac (claset(),
paulson@10778
   189
              simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc]));
paulson@10751
   190
qed "sumhr_hypreal_omega_minus_one";
paulson@10751
   191
paulson@10751
   192
Goalw [hypnat_zero_def, hypnat_omega_def]
paulson@12018
   193
     "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0";
paulson@12018
   194
by (simp_tac (simpset() delsimps [realpow_Suc]
paulson@12018
   195
               addsimps [sumhr,hypnat_add,double_lemma, hypreal_zero_def]) 1);
paulson@10751
   196
qed "sumhr_minus_one_realpow_zero";
paulson@10751
   197
Addsimps [sumhr_minus_one_realpow_zero];
paulson@10751
   198
paulson@10751
   199
Goalw [hypnat_of_nat_def,hypreal_of_real_def]
paulson@10751
   200
     "(ALL n. m <= Suc n --> f n = r) & m <= na \
paulson@10751
   201
\          ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
paulson@10751
   202
\          (hypreal_of_nat (na - m) * hypreal_of_real r)";
paulson@10751
   203
by (auto_tac (claset() addSDs [sumr_interval_const],
paulson@10778
   204
              simpset() addsimps [sumhr,hypreal_of_nat_def,
paulson@10778
   205
                                  hypreal_of_real_def, hypreal_mult]));
paulson@10751
   206
qed "sumhr_interval_const";
paulson@10751
   207
paulson@10751
   208
Goalw [hypnat_zero_def]
nipkow@13810
   209
     "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
paulson@10751
   210
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
paulson@10751
   211
by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1);
paulson@10751
   212
qed "starfunNat_sumr";
paulson@10751
   213
paulson@10751
   214
Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
paulson@12018
   215
\     ==> abs (sumhr (M, N, f)) @= 0";
paulson@10751
   216
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
paulson@10919
   217
by (auto_tac (claset(), simpset() addsimps [approx_refl]));
paulson@10919
   218
by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
paulson@10919
   219
by (auto_tac (claset() addDs [approx_hrabs],
paulson@10751
   220
              simpset() addsimps [sumhr_split_add_minus]));
paulson@10919
   221
qed "sumhr_hrabs_approx";
paulson@10919
   222
Addsimps [sumhr_hrabs_approx];
paulson@10751
   223
paulson@10751
   224
(*----------------------------------------------------------------
paulson@10751
   225
      infinite sums: Standard and NS theorems
paulson@10751
   226
 ----------------------------------------------------------------*)
paulson@10751
   227
Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)";
paulson@10751
   228
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
paulson@10751
   229
qed "sums_NSsums_iff";
paulson@10751
   230
paulson@10751
   231
Goalw [summable_def,NSsummable_def] 
paulson@10751
   232
      "(summable f) = (NSsummable f)";
paulson@10751
   233
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
paulson@10751
   234
qed "summable_NSsummable_iff";
paulson@10751
   235
paulson@10751
   236
Goalw [suminf_def,NSsuminf_def] 
paulson@10751
   237
      "(suminf f) = (NSsuminf f)";
paulson@10751
   238
by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
paulson@10751
   239
qed "suminf_NSsuminf_iff";
paulson@10751
   240
paulson@10751
   241
Goalw [NSsums_def,NSsummable_def] 
paulson@10751
   242
      "f NSsums l ==> NSsummable f";
paulson@10751
   243
by (Blast_tac 1);
paulson@10751
   244
qed "NSsums_NSsummable";
paulson@10751
   245
paulson@10751
   246
Goalw [NSsummable_def,NSsuminf_def]
paulson@10751
   247
     "NSsummable f ==> f NSsums (NSsuminf f)";
paulson@10751
   248
by (blast_tac (claset() addIs [someI2]) 1);
paulson@10751
   249
qed "NSsummable_NSsums";
paulson@10751
   250
paulson@10751
   251
Goal "f NSsums s ==> (s = NSsuminf f)";
paulson@10751
   252
by (asm_full_simp_tac 
paulson@10751
   253
    (simpset() addsimps [suminf_NSsuminf_iff RS sym,sums_NSsums_iff,
paulson@10751
   254
                         sums_unique]) 1);
paulson@10751
   255
qed "NSsums_unique";
paulson@10751
   256
paulson@12018
   257
Goal "ALL m. n <= Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)";
paulson@10751
   258
by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1);
paulson@10751
   259
qed "NSseries_zero";
paulson@10751
   260
paulson@10751
   261
Goal "NSsummable f = \
paulson@12018
   262
\     (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= 0)";
paulson@10751
   263
by (auto_tac (claset(),
paulson@10751
   264
              simpset() addsimps [summable_NSsummable_iff RS sym,
paulson@10751
   265
                 summable_convergent_sumr_iff, convergent_NSconvergent_iff,
paulson@10751
   266
                 NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
paulson@10751
   267
                 starfunNat_sumr]));
paulson@10751
   268
by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
paulson@10919
   269
by (auto_tac (claset(), simpset() addsimps [approx_refl]));
paulson@10919
   270
by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
paulson@10919
   271
by (rtac (approx_minus_iff RS iffD2) 2);
paulson@10919
   272
by (auto_tac (claset() addDs [approx_hrabs_zero_cancel],
paulson@10751
   273
              simpset() addsimps [sumhr_split_add_minus]));
paulson@10751
   274
qed "NSsummable_NSCauchy";
paulson@10751
   275
paulson@10751
   276
(*-------------------------------------------------------------------
paulson@10751
   277
         Terms of a convergent series tend to zero
paulson@10751
   278
 -------------------------------------------------------------------*)
paulson@12018
   279
Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> 0";
paulson@10751
   280
by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
paulson@10751
   281
by (dtac bspec 1 THEN Auto_tac);
wenzelm@11713
   282
by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1);
paulson@12018
   283
by (auto_tac (claset() addIs [HNatInfinite_add_one, approx_hrabs_zero_cancel],
paulson@12018
   284
              simpset()));
paulson@10751
   285
qed "NSsummable_NSLIMSEQ_zero";
paulson@10751
   286
paulson@10751
   287
(* Easy to prove stsandard case now *)
paulson@12018
   288
Goal "summable f ==> f ----> 0";
paulson@10751
   289
by (auto_tac (claset(),
paulson@10751
   290
        simpset() addsimps [summable_NSsummable_iff,
paulson@10751
   291
                            LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero]));
paulson@10751
   292
qed "summable_LIMSEQ_zero";
paulson@10751
   293
paulson@10751
   294
(*-------------------------------------------------------------------
paulson@10751
   295
                  NS Comparison test
paulson@10751
   296
 -------------------------------------------------------------------*)
paulson@10751
   297
paulson@10751
   298
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
paulson@10751
   299
\        NSsummable g \
paulson@10751
   300
\     |] ==> NSsummable f";
paulson@10751
   301
by (auto_tac (claset() addIs [summable_comparison_test],
paulson@10751
   302
              simpset() addsimps [summable_NSsummable_iff RS sym]));
paulson@10751
   303
qed "NSsummable_comparison_test";
paulson@10751
   304
paulson@10751
   305
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
paulson@10751
   306
\        NSsummable g \
paulson@10751
   307
\     |] ==> NSsummable (%k. abs (f k))";
paulson@10751
   308
by (rtac NSsummable_comparison_test 1);
paulson@10751
   309
by (auto_tac (claset(), simpset() addsimps [abs_idempotent]));
paulson@10751
   310
qed "NSsummable_rabs_comparison_test";