26 |
26 |
27 definition |
27 definition |
28 NSsuminf :: "(nat=>real) => real" where |
28 NSsuminf :: "(nat=>real) => real" where |
29 "NSsuminf f = (THE s. f NSsums s)" |
29 "NSsuminf f = (THE s. f NSsums s)" |
30 |
30 |
31 |
31 lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N" |
32 lemma sumhr: |
32 by (simp add: sumhr_def) |
33 "sumhr(star_n M, star_n N, f) = |
|
34 star_n (%n. setsum f {M n..<N n})" |
|
35 by (simp add: sumhr_def starfun2_star_n) |
|
36 |
33 |
37 text{*Base case in definition of @{term sumr}*} |
34 text{*Base case in definition of @{term sumr}*} |
38 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0" |
35 lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0" |
39 apply (cases m) |
36 unfolding sumhr_app by transfer simp |
40 apply (simp add: star_n_zero_num sumhr symmetric) |
|
41 done |
|
42 |
37 |
43 text{*Recursive case in definition of @{term sumr}*} |
38 text{*Recursive case in definition of @{term sumr}*} |
44 lemma sumhr_if: |
39 lemma sumhr_if: |
45 "sumhr(m,n+1,f) = |
40 "!!m n. sumhr(m,n+1,f) = |
46 (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)" |
41 (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)" |
47 apply (cases m, cases n) |
42 unfolding sumhr_app by transfer simp |
48 apply (auto simp add: star_n_one_num sumhr star_n_add star_n_le starfun |
43 |
49 star_n_zero_num star_n_eq_iff, ultra+) |
44 lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0" |
50 done |
45 unfolding sumhr_app by transfer simp |
51 |
46 |
52 lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0" |
47 lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0" |
53 apply (cases n) |
48 unfolding sumhr_app by transfer simp |
54 apply (simp add: star_n_one_num sumhr star_n_add star_n_zero_num) |
49 |
55 done |
50 lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m" |
56 |
51 unfolding sumhr_app by transfer simp |
57 lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0" |
52 |
58 apply (cases n) |
53 lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0" |
59 apply (simp add: sumhr star_n_zero_num) |
54 unfolding sumhr_app by transfer simp |
60 done |
55 |
61 |
56 lemma sumhr_add: |
62 lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *f* f) m" |
57 "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
63 apply (cases m) |
58 unfolding sumhr_app by transfer (rule setsum_addf [symmetric]) |
64 apply (simp add: sumhr star_n_one_num star_n_add starfun) |
59 |
65 done |
60 lemma sumhr_mult: |
66 |
61 "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
67 lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0" |
62 unfolding sumhr_app by transfer (rule setsum_right_distrib) |
68 apply (cases m, cases k) |
63 |
69 apply (simp add: sumhr star_n_add star_n_zero_num) |
64 lemma sumhr_split_add: |
70 done |
65 "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
71 |
66 unfolding sumhr_app by transfer (simp add: setsum_add_nat_ivl) |
72 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
|
73 apply (cases m, cases n) |
|
74 apply (simp add: sumhr star_n_add setsum_addf) |
|
75 done |
|
76 |
|
77 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
|
78 apply (cases m, cases n) |
|
79 apply (simp add: sumhr star_of_def star_n_mult setsum_right_distrib) |
|
80 done |
|
81 |
|
82 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
|
83 apply (cases n, cases p) |
|
84 apply (auto elim!: FreeUltrafilterNat_subset simp |
|
85 add: star_n_zero_num sumhr star_n_add star_n_less setsum_add_nat_ivl star_n_eq_iff) |
|
86 done |
|
87 |
67 |
88 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
68 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
89 by (drule_tac f = f in sumhr_split_add [symmetric], simp) |
69 by (drule_tac f = f in sumhr_split_add [symmetric], simp) |
90 |
70 |
91 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
71 lemma sumhr_hrabs: "!!m n. abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
92 apply (cases n, cases m) |
72 unfolding sumhr_app by transfer (rule setsum_abs) |
93 apply (simp add: sumhr star_n_le star_n_abs setsum_abs) |
|
94 done |
|
95 |
73 |
96 text{* other general version also needed *} |
74 text{* other general version also needed *} |
97 lemma sumhr_fun_hypnat_eq: |
75 lemma sumhr_fun_hypnat_eq: |
98 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
76 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
99 sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
77 sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
100 sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
78 sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
101 by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong) |
79 unfolding sumhr_app by transfer simp |
102 |
|
103 |
80 |
104 lemma sumhr_const: |
81 lemma sumhr_const: |
105 "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
82 "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
106 apply (cases n) |
83 unfolding sumhr_app by transfer (simp add: real_of_nat_def) |
107 apply (simp add: sumhr star_n_zero_num hypreal_of_hypnat |
84 |
108 star_of_def star_n_mult real_of_nat_def) |
85 lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0" |
109 done |
86 unfolding sumhr_app by transfer simp |
110 |
87 |
111 lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0" |
88 lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
112 apply (cases m, cases n) |
89 unfolding sumhr_app by transfer (rule setsum_negf) |
113 apply (auto elim: FreeUltrafilterNat_subset |
|
114 simp add: sumhr star_n_less star_n_zero_num star_n_eq_iff) |
|
115 done |
|
116 |
|
117 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
|
118 apply (cases m, cases n) |
|
119 apply (simp add: sumhr star_n_minus setsum_negf) |
|
120 done |
|
121 |
90 |
122 lemma sumhr_shift_bounds: |
91 lemma sumhr_shift_bounds: |
123 "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" |
92 "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = |
124 apply (cases m, cases n) |
93 sumhr(m,n,%i. f(i + k))" |
125 apply (simp add: sumhr star_n_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq) |
94 unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl) |
126 done |
|
127 |
95 |
128 |
96 |
129 subsection{*Nonstandard Sums*} |
97 subsection{*Nonstandard Sums*} |
130 |
98 |
131 text{*Infinite sums are obtained by summing to some infinite hypernatural |
99 text{*Infinite sums are obtained by summing to some infinite hypernatural |
132 (such as @{term whn})*} |
100 (such as @{term whn})*} |
133 lemma sumhr_hypreal_of_hypnat_omega: |
101 lemma sumhr_hypreal_of_hypnat_omega: |
134 "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn" |
102 "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn" |
135 by (simp add: hypnat_omega_def star_n_zero_num sumhr hypreal_of_hypnat |
103 by (simp add: sumhr_const) |
136 real_of_nat_def) |
|
137 |
104 |
138 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1" |
105 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1" |
139 by (simp add: hypnat_omega_def star_n_zero_num omega_def star_n_one_num |
106 apply (simp add: sumhr_const) |
140 sumhr star_n_diff real_of_nat_def) |
107 (* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *) |
|
108 (* maybe define omega = hypreal_of_hypnat whn + 1 *) |
|
109 apply (unfold star_class_defs omega_def hypnat_omega_def |
|
110 hypreal_of_hypnat_def star_of_def) |
|
111 apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def) |
|
112 done |
141 |
113 |
142 lemma sumhr_minus_one_realpow_zero [simp]: |
114 lemma sumhr_minus_one_realpow_zero [simp]: |
143 "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0" |
115 "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0" |
144 by (simp del: realpow_Suc |
116 unfolding sumhr_app |
145 add: sumhr star_n_add nat_mult_2 [symmetric] star_n_zero_num |
117 by transfer (simp del: realpow_Suc add: nat_mult_2 [symmetric]) |
146 star_n_zero_num hypnat_omega_def) |
|
147 |
118 |
148 lemma sumhr_interval_const: |
119 lemma sumhr_interval_const: |
149 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
120 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
150 ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
121 ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
151 (hypreal_of_nat (na - m) * hypreal_of_real r)" |
122 (hypreal_of_nat (na - m) * hypreal_of_real r)" |
152 by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq |
123 unfolding sumhr_app by transfer simp |
153 real_of_nat_def star_of_def star_n_mult cong: setsum_ivl_cong) |
124 |
154 |
125 lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)" |
155 lemma starfunNat_sumr: "( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)" |
126 unfolding sumhr_app by transfer (rule refl) |
156 apply (cases N) |
|
157 apply (simp add: star_n_zero_num starfun sumhr) |
|
158 done |
|
159 |
127 |
160 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f) |
128 lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f) |
161 ==> abs (sumhr(M, N, f)) @= 0" |
129 ==> abs (sumhr(M, N, f)) @= 0" |
162 apply (cut_tac x = M and y = N in linorder_less_linear) |
130 apply (cut_tac x = M and y = N in linorder_less_linear) |
163 apply (auto simp add: approx_refl) |
131 apply (auto simp add: approx_refl) |