--- a/src/HOL/Hyperreal/HSeries.ML Wed Feb 25 15:17:24 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,308 +0,0 @@
-(* Title : HSeries.ML
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : Finite summation and infinite series
- for hyperreals
-*)
-
-val hypreal_of_nat_eq = thm"hypreal_of_nat_eq";
-
-Goalw [sumhr_def]
- "sumhr(M,N,f) = \
-\ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \
-\ hyprel ``{%n::nat. sumr (X n) (Y n) f})";
-by (Auto_tac);
-qed "sumhr_iff";
-
-Goalw [sumhr_def]
- "sumhr(Abs_hypnat(hypnatrel``{%n. M n}), \
-\ Abs_hypnat(hypnatrel``{%n. N n}), f) = \
-\ Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (Auto_tac THEN Ultra_tac 1);
-qed "sumhr";
-
-(*-------------------------------------------------------
- lcp's suggestion: exploit pattern matching
- facilities and use as definition instead (to do)
- -------------------------------------------------------*)
-Goalw [sumhr_def]
- "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
-\ UN Y: Rep_hypnat(N). \
-\ hyprel ``{%n::nat. sumr (X n) (Y n) f})) p";
-by (res_inst_tac [("p","p")] PairE 1);
-by (res_inst_tac [("p","y")] PairE 1);
-by (Auto_tac);
-qed "sumhr_iff2";
-
-(* Theorem corresponding to base case in def of sumr *)
-Goalw [hypnat_zero_def]
- "sumhr (m,0,f) = 0";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, symmetric hypreal_zero_def]));
-qed "sumhr_zero";
-Addsimps [sumhr_zero];
-
-(* Theorem corresponding to recursive case in def of sumr *)
-Goalw [hypnat_one_def]
- "sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then 0 \
-\ else sumhr(m,n,f) + ( *fNat* f) n)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add,hypnat_le,starfunNat,hypreal_add,
- hypreal_zero_def]));
-by (ALLGOALS(Ultra_tac));
-qed "sumhr_if";
-
-Goalw [hypnat_one_def] "sumhr (n + (1::hypnat), n, f) = 0";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def]));
-qed "sumhr_Suc_zero";
-Addsimps [sumhr_Suc_zero];
-
-Goal "sumhr (n,n,f) = 0";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_zero_def]));
-qed "sumhr_eq_bounds";
-Addsimps [sumhr_eq_bounds];
-
-Goalw [hypnat_one_def]
- "sumhr (m,m + (1::hypnat),f) = ( *fNat* f) m";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add,starfunNat]));
-qed "sumhr_Suc";
-Addsimps [sumhr_Suc];
-
-Goal "sumhr(m+k,k,f) = 0";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add, hypreal_zero_def]));
-qed "sumhr_add_lbound_zero";
-Addsimps [sumhr_add_lbound_zero];
-
-Goal "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_add,sumr_add]));
-qed "sumhr_add";
-
-Goalw [hypreal_of_real_def]
- "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_mult,sumr_mult]));
-qed "sumhr_mult";
-
-Goalw [hypnat_zero_def]
- "n < p ==> sumhr (0,n,f) + sumhr (n,p,f) = sumhr (0,p,f)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","p")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset],
- simpset() addsimps [sumhr,hypreal_add,hypnat_less, sumr_split_add]));
-qed "sumhr_split_add";
-
-(*FIXME delete*)
-Goal "n < p ==> sumhr (0, p, f) + - sumhr (0, n, f) = sumhr (n,p,f)";
-by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
-by (Asm_simp_tac 1);
-qed "sumhr_split_add_minus";
-
-Goal "n < p ==> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n,p,f)";
-by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
-by (Asm_simp_tac 1);
-qed "sumhr_split_diff";
-
-Goal "abs(sumhr(m,n,f)) <= sumhr(m,n,%i. abs(f i))";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_le,hypreal_hrabs,sumr_rabs]));
-qed "sumhr_hrabs";
-
-(* other general version also needed *)
-Goal "(ALL r. m <= r & r < n --> f r = g r) --> \
-\ sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = \
-\ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)";
-by (Step_tac 1 THEN dtac sumr_fun_eq 1);
-by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_of_nat_eq]));
-qed "sumhr_fun_hypnat_eq";
-
-Goalw [hypnat_zero_def,hypreal_of_real_def]
- "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_simp_tac
- (simpset() addsimps [sumhr, hypreal_of_hypnat,hypreal_mult]) 1);
-qed "sumhr_const";
-
-Goalw [hypnat_zero_def,hypreal_of_real_def]
- "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = \
-\ sumhr(0,n,%i. f i + -r)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [sumhr,
- hypreal_of_hypnat,hypreal_mult,hypreal_add,
- hypreal_minus,sumr_add RS sym]) 1);
-qed "sumhr_add_mult_const";
-
-Goal "n < m ==> sumhr (m,n,f) = 0";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],
- simpset() addsimps [sumhr,hypnat_less, hypreal_zero_def]));
-qed "sumhr_less_bounds_zero";
-Addsimps [sumhr_less_bounds_zero];
-
-Goal "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus]));
-qed "sumhr_minus";
-
-Goal "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds, hypnat_of_nat_eq]));
-qed "sumhr_shift_bounds";
-
-(*------------------------------------------------------------------
- Theorems about NS sums - infinite sums are obtained
- by summing to some infinite hypernatural (such as whn)
- -----------------------------------------------------------------*)
-Goalw [hypnat_omega_def,hypnat_zero_def]
- "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn";
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_of_hypnat]));
-qed "sumhr_hypreal_of_hypnat_omega";
-
-Goalw [hypnat_omega_def,hypnat_zero_def,omega_def]
- "sumhr(0, whn, %i. 1) = omega - 1";
-by (simp_tac (HOL_ss addsimps [numeral_1_eq_1, hypreal_one_def]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc]));
-qed "sumhr_hypreal_omega_minus_one";
-
-Goalw [hypnat_zero_def, hypnat_omega_def]
- "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0";
-by (simp_tac (simpset() delsimps [realpow_Suc]
- addsimps [sumhr,hypnat_add,double_lemma, hypreal_zero_def]) 1);
-qed "sumhr_minus_one_realpow_zero";
-Addsimps [sumhr_minus_one_realpow_zero];
-
-Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
-\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
-\ (hypreal_of_nat (na - m) * hypreal_of_real r)";
-by (auto_tac (claset() addSDs [sumr_interval_const],
- simpset() addsimps [hypreal_of_real_def, sumhr,hypreal_of_nat_eq, hypnat_of_nat_eq,
- hypreal_of_real_def, hypreal_mult]));
-qed "sumhr_interval_const";
-
-Goalw [hypnat_zero_def]
- "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1);
-qed "starfunNat_sumr";
-
-Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
-\ ==> abs (sumhr (M, N, f)) @= 0";
-by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
-by (auto_tac (claset(), simpset() addsimps [approx_refl]));
-by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
-by (auto_tac (claset() addDs [approx_hrabs],
- simpset() addsimps [sumhr_split_add_minus]));
-qed "sumhr_hrabs_approx";
-Addsimps [sumhr_hrabs_approx];
-
-(*----------------------------------------------------------------
- infinite sums: Standard and NS theorems
- ----------------------------------------------------------------*)
-Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "sums_NSsums_iff";
-
-Goalw [summable_def,NSsummable_def]
- "(summable f) = (NSsummable f)";
-by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
-qed "summable_NSsummable_iff";
-
-Goalw [suminf_def,NSsuminf_def]
- "(suminf f) = (NSsuminf f)";
-by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
-qed "suminf_NSsuminf_iff";
-
-Goalw [NSsums_def,NSsummable_def]
- "f NSsums l ==> NSsummable f";
-by (Blast_tac 1);
-qed "NSsums_NSsummable";
-
-Goalw [NSsummable_def,NSsuminf_def]
- "NSsummable f ==> f NSsums (NSsuminf f)";
-by (blast_tac (claset() addIs [someI2]) 1);
-qed "NSsummable_NSsums";
-
-Goal "f NSsums s ==> (s = NSsuminf f)";
-by (asm_full_simp_tac
- (simpset() addsimps [suminf_NSsuminf_iff RS sym,sums_NSsums_iff,
- sums_unique]) 1);
-qed "NSsums_unique";
-
-Goal "ALL m. n <= Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)";
-by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1);
-qed "NSseries_zero";
-
-Goal "NSsummable f = \
-\ (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= 0)";
-by (auto_tac (claset(),
- simpset() addsimps [summable_NSsummable_iff RS sym,
- summable_convergent_sumr_iff, convergent_NSconvergent_iff,
- NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
- starfunNat_sumr]));
-by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
-by (auto_tac (claset(), simpset() addsimps [approx_refl]));
-by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
-by (rtac (approx_minus_iff RS iffD2) 2);
-by (auto_tac (claset() addDs [approx_hrabs_zero_cancel],
- simpset() addsimps [sumhr_split_add_minus]));
-qed "NSsummable_NSCauchy";
-
-(*-------------------------------------------------------------------
- Terms of a convergent series tend to zero
- -------------------------------------------------------------------*)
-Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> 0";
-by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
-by (dtac bspec 1 THEN Auto_tac);
-by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1);
-by (auto_tac (claset() addIs [HNatInfinite_add_one, approx_hrabs_zero_cancel],
- simpset()));
-qed "NSsummable_NSLIMSEQ_zero";
-
-(* Easy to prove stsandard case now *)
-Goal "summable f ==> f ----> 0";
-by (auto_tac (claset(),
- simpset() addsimps [summable_NSsummable_iff,
- LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero]));
-qed "summable_LIMSEQ_zero";
-
-(*-------------------------------------------------------------------
- NS Comparison test
- -------------------------------------------------------------------*)
-
-Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
-\ NSsummable g \
-\ |] ==> NSsummable f";
-by (auto_tac (claset() addIs [summable_comparison_test],
- simpset() addsimps [summable_NSsummable_iff RS sym]));
-qed "NSsummable_comparison_test";
-
-Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
-\ NSsummable g \
-\ |] ==> NSsummable (%k. abs (f k))";
-by (rtac NSsummable_comparison_test 1);
-by (auto_tac (claset(), simpset() addsimps [abs_idempotent]));
-qed "NSsummable_rabs_comparison_test";
--- a/src/HOL/Hyperreal/HSeries.thy Wed Feb 25 15:17:24 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Wed Feb 25 16:22:36 2004 +0100
@@ -1,30 +1,291 @@
(* Title : HSeries.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : Finite summation and infinite series
- for hyperreals
+
+Converted to Isar and polished by lcp
*)
-HSeries = Series +
+header{*Finite Summation and Infinite Series for Hyperreals*}
-consts
- sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
+theory HSeries = Series:
-defs
- sumhr_def
- "sumhr p
- == Abs_hypreal(UN X:Rep_hypnat(fst p).
- UN Y: Rep_hypnat(fst(snd p)).
- hyprel``{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
+constdefs
+ sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
+ "sumhr p ==
+ (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).
+ hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
-constdefs
- NSsums :: [nat=>real,real] => bool (infixr 80)
+ NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80)
"f NSsums s == (%n. sumr 0 n f) ----NS> s"
- NSsummable :: (nat=>real) => bool
- "NSsummable f == (EX s. f NSsums s)"
+ NSsummable :: "(nat=>real) => bool"
+ "NSsummable f == (\<exists>s. f NSsums s)"
- NSsuminf :: (nat=>real) => real
+ NSsuminf :: "(nat=>real) => real"
"NSsuminf f == (@s. f NSsums s)"
+
+lemma sumhr:
+ "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),
+ Abs_hypnat(hypnatrel``{%n. N n}), f) =
+ Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"
+apply (simp add: sumhr_def)
+apply (rule arg_cong [where f = Abs_hypreal])
+apply (auto, ultra)
+done
+
+text{*Base case in definition of @{term sumr}*}
+lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
+apply (rule eq_Abs_hypnat [of m])
+apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
+done
+
+text{*Recursive case in definition of @{term sumr}*}
+lemma sumhr_if:
+ "sumhr(m,n+1,f) =
+ (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
+ hypreal_add hypreal_zero_def, ultra+)
+done
+
+lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
+done
+
+lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypreal_zero_def)
+done
+
+lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
+apply (rule eq_Abs_hypnat [of m])
+apply (simp add: sumhr hypnat_one_def hypnat_add starfunNat)
+done
+
+lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of k])
+apply (simp add: sumhr hypnat_add hypreal_zero_def)
+done
+
+lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypreal_add sumr_add)
+done
+
+lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult)
+done
+
+lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypnat [of p])
+apply (auto elim!: FreeUltrafilterNat_subset simp
+ add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
+done
+
+lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
+by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
+
+lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
+apply (rule eq_Abs_hypnat [of n])
+apply (rule eq_Abs_hypnat [of m])
+apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs)
+done
+
+text{* other general version also needed *}
+lemma sumhr_fun_hypnat_eq:
+ "(\<forall>r. m \<le> r & r < n --> f r = g r) -->
+ sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
+ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
+apply (safe, drule sumr_fun_eq)
+apply (simp add: sumhr hypnat_of_nat_eq)
+done
+
+lemma sumhr_const: "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat hypreal_mult)
+done
+
+lemma sumhr_add_mult_const:
+ "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) =
+ sumhr(0,n,%i. f i + -r)"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat
+ hypreal_mult hypreal_add hypreal_minus sumr_add [symmetric])
+done
+
+lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (auto elim: FreeUltrafilterNat_subset
+ simp add: sumhr hypnat_less hypreal_zero_def)
+done
+
+lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypreal_minus sumr_minus)
+done
+
+lemma sumhr_shift_bounds:
+ "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
+done
+
+
+subsection{*Nonstandard Sums*}
+
+text{*Infinite sums are obtained by summing to some infinite hypernatural
+ (such as @{term whn})*}
+lemma sumhr_hypreal_of_hypnat_omega:
+ "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
+by (simp add: hypnat_omega_def hypnat_zero_def sumhr hypreal_of_hypnat)
+
+lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
+by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
+ sumhr hypreal_diff real_of_nat_Suc)
+
+lemma sumhr_minus_one_realpow_zero [simp]:
+ "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
+by (simp del: realpow_Suc
+ add: sumhr hypnat_add double_lemma hypreal_zero_def
+ hypnat_zero_def hypnat_omega_def)
+
+lemma sumhr_interval_const:
+ "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
+ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =
+ (hypreal_of_nat (na - m) * hypreal_of_real r)"
+by (auto dest!: sumr_interval_const
+ simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq
+ hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
+
+lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
+apply (rule eq_Abs_hypnat [of N])
+apply (simp add: hypnat_zero_def starfunNat sumhr)
+done
+
+lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
+ ==> abs (sumhr(M, N, f)) @= 0"
+apply (cut_tac x = M and y = N in linorder_less_linear)
+apply (auto simp add: approx_refl)
+apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
+apply (auto dest: approx_hrabs
+ simp add: sumhr_split_diff diff_minus [symmetric])
+done
+
+(*----------------------------------------------------------------
+ infinite sums: Standard and NS theorems
+ ----------------------------------------------------------------*)
+lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
+by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
+
+lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
+by (simp add: summable_def NSsummable_def sums_NSsums_iff)
+
+lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
+by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
+
+lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
+by (simp add: NSsums_def NSsummable_def, blast)
+
+lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
+apply (simp add: NSsummable_def NSsuminf_def)
+apply (blast intro: someI2)
+done
+
+lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
+by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
+
+lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
+by (simp add: sums_NSsums_iff [symmetric] series_zero)
+
+lemma NSsummable_NSCauchy:
+ "NSsummable f =
+ (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. abs (sumhr(M,N,f)) @= 0)"
+apply (auto simp add: summable_NSsummable_iff [symmetric]
+ summable_convergent_sumr_iff convergent_NSconvergent_iff
+ NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
+apply (cut_tac x = M and y = N in linorder_less_linear)
+apply (auto simp add: approx_refl)
+apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
+apply (rule_tac [2] approx_minus_iff [THEN iffD2])
+apply (auto dest: approx_hrabs_zero_cancel
+ simp add: sumhr_split_diff diff_minus [symmetric])
+done
+
+
+text{*Terms of a convergent series tend to zero*}
+lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f ----NS> 0"
+apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
+apply (drule bspec, auto)
+apply (drule_tac x = "N + 1 " in bspec)
+apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
+done
+
+text{* Easy to prove stsandard case now *}
+lemma summable_LIMSEQ_zero: "summable f ==> f ----> 0"
+by (simp add: summable_NSsummable_iff LIMSEQ_NSLIMSEQ_iff NSsummable_NSLIMSEQ_zero)
+
+text{*Nonstandard comparison test*}
+lemma NSsummable_comparison_test:
+ "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |] ==> NSsummable f"
+by (auto intro: summable_comparison_test
+ simp add: summable_NSsummable_iff [symmetric])
+
+lemma NSsummable_rabs_comparison_test:
+ "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; NSsummable g |]
+ ==> NSsummable (%k. abs (f k))"
+apply (rule NSsummable_comparison_test)
+apply (auto simp add: abs_idempotent)
+done
+
+ML
+{*
+val sumhr = thm "sumhr";
+val sumhr_zero = thm "sumhr_zero";
+val sumhr_if = thm "sumhr_if";
+val sumhr_Suc_zero = thm "sumhr_Suc_zero";
+val sumhr_eq_bounds = thm "sumhr_eq_bounds";
+val sumhr_Suc = thm "sumhr_Suc";
+val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
+val sumhr_add = thm "sumhr_add";
+val sumhr_mult = thm "sumhr_mult";
+val sumhr_split_add = thm "sumhr_split_add";
+val sumhr_split_diff = thm "sumhr_split_diff";
+val sumhr_hrabs = thm "sumhr_hrabs";
+val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
+val sumhr_const = thm "sumhr_const";
+val sumhr_add_mult_const = thm "sumhr_add_mult_const";
+val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
+val sumhr_minus = thm "sumhr_minus";
+val sumhr_shift_bounds = thm "sumhr_shift_bounds";
+val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
+val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
+val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
+val sumhr_interval_const = thm "sumhr_interval_const";
+val starfunNat_sumr = thm "starfunNat_sumr";
+val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
+val sums_NSsums_iff = thm "sums_NSsums_iff";
+val summable_NSsummable_iff = thm "summable_NSsummable_iff";
+val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
+val NSsums_NSsummable = thm "NSsums_NSsummable";
+val NSsummable_NSsums = thm "NSsummable_NSsums";
+val NSsums_unique = thm "NSsums_unique";
+val NSseries_zero = thm "NSseries_zero";
+val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
+val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
+val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
+val NSsummable_comparison_test = thm "NSsummable_comparison_test";
+val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
+*}
+
end