--- a/src/HOL/Hyperreal/HSeries.thy Wed Dec 13 21:46:34 2006 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Wed Dec 13 23:15:39 2006 +0100
@@ -28,102 +28,70 @@
NSsuminf :: "(nat=>real) => real" where
"NSsuminf f = (THE s. f NSsums s)"
-
-lemma sumhr:
- "sumhr(star_n M, star_n N, f) =
- star_n (%n. setsum f {M n..<N n})"
-by (simp add: sumhr_def starfun2_star_n)
+lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N"
+by (simp add: sumhr_def)
text{*Base case in definition of @{term sumr}*}
-lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (cases m)
-apply (simp add: star_n_zero_num sumhr symmetric)
-done
+lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
+unfolding sumhr_app by transfer simp
text{*Recursive case in definition of @{term sumr}*}
lemma sumhr_if:
- "sumhr(m,n+1,f) =
+ "!!m n. sumhr(m,n+1,f) =
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
-apply (cases m, cases n)
-apply (auto simp add: star_n_one_num sumhr star_n_add star_n_le starfun
- star_n_zero_num star_n_eq_iff, ultra+)
-done
+unfolding sumhr_app by transfer simp
-lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (cases n)
-apply (simp add: star_n_one_num sumhr star_n_add star_n_zero_num)
-done
+lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
+unfolding sumhr_app by transfer simp
-lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (cases n)
-apply (simp add: sumhr star_n_zero_num)
-done
+lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
+unfolding sumhr_app by transfer simp
+
+lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
+unfolding sumhr_app by transfer simp
-lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *f* f) m"
-apply (cases m)
-apply (simp add: sumhr star_n_one_num star_n_add starfun)
-done
+lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
+unfolding sumhr_app by transfer simp
-lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (cases m, cases k)
-apply (simp add: sumhr star_n_add star_n_zero_num)
-done
+lemma sumhr_add:
+ "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
+unfolding sumhr_app by transfer (rule setsum_addf [symmetric])
-lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_add setsum_addf)
-done
+lemma sumhr_mult:
+ "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
+unfolding sumhr_app by transfer (rule setsum_right_distrib)
-lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib)
-done
-
-lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (cases n, cases p)
-apply (auto elim!: FreeUltrafilterNat_subset simp
- add: star_n_zero_num sumhr star_n_add star_n_less setsum_add_nat_ivl star_n_eq_iff)
-done
+lemma sumhr_split_add:
+ "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
+unfolding sumhr_app by transfer (simp add: setsum_add_nat_ivl)
lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
by (drule_tac f = f in sumhr_split_add [symmetric], simp)
-lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (cases n, cases m)
-apply (simp add: sumhr star_n_le star_n_abs setsum_abs)
-done
+lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
+unfolding sumhr_app by transfer (rule setsum_abs)
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)"
-by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong)
-
+unfolding sumhr_app by transfer simp
lemma sumhr_const:
- "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-apply (cases n)
-apply (simp add: sumhr star_n_zero_num hypreal_of_hypnat
- star_of_def star_n_mult real_of_nat_def)
-done
+ "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
+unfolding sumhr_app by transfer (simp add: real_of_nat_def)
-lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (cases m, cases n)
-apply (auto elim: FreeUltrafilterNat_subset
- simp add: sumhr star_n_less star_n_zero_num star_n_eq_iff)
-done
+lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
+unfolding sumhr_app by transfer simp
-lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_minus setsum_negf)
-done
+lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
+unfolding sumhr_app by transfer (rule setsum_negf)
lemma sumhr_shift_bounds:
- "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (cases m, cases n)
-apply (simp add: sumhr star_n_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
-done
+ "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
+ sumhr(m,n,%i. f(i + k))"
+unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl)
subsection{*Nonstandard Sums*}
@@ -132,30 +100,30 @@
(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 star_n_zero_num sumhr hypreal_of_hypnat
- real_of_nat_def)
+by (simp add: sumhr_const)
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
-by (simp add: hypnat_omega_def star_n_zero_num omega_def star_n_one_num
- sumhr star_n_diff real_of_nat_def)
+apply (simp add: sumhr_const)
+(* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
+(* maybe define omega = hypreal_of_hypnat whn + 1 *)
+apply (unfold star_class_defs omega_def hypnat_omega_def
+ hypreal_of_hypnat_def star_of_def)
+apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def)
+done
lemma sumhr_minus_one_realpow_zero [simp]:
- "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
-by (simp del: realpow_Suc
- add: sumhr star_n_add nat_mult_2 [symmetric] star_n_zero_num
- star_n_zero_num hypnat_omega_def)
+ "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
+unfolding sumhr_app
+by transfer (simp del: realpow_Suc add: nat_mult_2 [symmetric])
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(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq
- real_of_nat_def star_of_def star_n_mult cong: setsum_ivl_cong)
+unfolding sumhr_app by transfer simp
-lemma starfunNat_sumr: "( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
-apply (cases N)
-apply (simp add: star_n_zero_num starfun sumhr)
-done
+lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
+unfolding sumhr_app by transfer (rule refl)
lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
==> abs (sumhr(M, N, f)) @= 0"