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