2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Description : Finite summation and infinite series |
4 Description : Finite summation and infinite series |
5 for hyperreals |
5 for hyperreals |
6 *) |
6 *) |
|
7 |
|
8 val hypreal_of_nat_eq = thm"hypreal_of_nat_eq"; |
7 |
9 |
8 Goalw [sumhr_def] |
10 Goalw [sumhr_def] |
9 "sumhr(M,N,f) = \ |
11 "sumhr(M,N,f) = \ |
10 \ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \ |
12 \ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \ |
11 \ hyprel ``{%n::nat. sumr (X n) (Y n) f})"; |
13 \ hyprel ``{%n::nat. sumr (X n) (Y n) f})"; |
123 by (auto_tac (claset(), |
125 by (auto_tac (claset(), |
124 simpset() addsimps [sumhr, hypreal_le,hypreal_hrabs,sumr_rabs])); |
126 simpset() addsimps [sumhr, hypreal_le,hypreal_hrabs,sumr_rabs])); |
125 qed "sumhr_hrabs"; |
127 qed "sumhr_hrabs"; |
126 |
128 |
127 (* other general version also needed *) |
129 (* other general version also needed *) |
128 Goalw [hypnat_of_nat_def] |
130 Goal "(ALL r. m <= r & r < n --> f r = g r) --> \ |
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, f) = \ |
131 \ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"; |
132 \ sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"; |
132 by (Step_tac 1 THEN dtac sumr_fun_eq 1); |
133 by (Step_tac 1 THEN dtac sumr_fun_eq 1); |
133 by (auto_tac (claset(), simpset() addsimps [sumhr])); |
134 by (auto_tac (claset(), simpset() addsimps [sumhr, hypnat_of_nat_eq])); |
134 qed "sumhr_fun_hypnat_eq"; |
135 qed "sumhr_fun_hypnat_eq"; |
135 |
136 |
136 Goalw [hypnat_zero_def,hypreal_of_real_def] |
137 Goalw [hypnat_zero_def,hypreal_of_real_def] |
137 "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r"; |
138 "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 (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
161 by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
162 by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
162 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
163 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
163 by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus])); |
164 by (auto_tac (claset(), simpset() addsimps [sumhr, hypreal_minus,sumr_minus])); |
164 qed "sumhr_minus"; |
165 qed "sumhr_minus"; |
165 |
166 |
166 Goalw [hypnat_of_nat_def] |
167 Goal "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"; |
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); |
168 by (res_inst_tac [("z","m")] eq_Abs_hypnat 1); |
169 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
169 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
170 by (auto_tac (claset(), |
170 by (auto_tac (claset(), |
171 simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds, hypnat_of_nat_eq])); |
171 simpset() addsimps [sumhr, hypnat_add,sumr_shift_bounds])); |
|
172 qed "sumhr_shift_bounds"; |
172 qed "sumhr_shift_bounds"; |
173 |
173 |
174 (*------------------------------------------------------------------ |
174 (*------------------------------------------------------------------ |
175 Theorems about NS sums - infinite sums are obtained |
175 Theorems about NS sums - infinite sums are obtained |
176 by summing to some infinite hypernatural (such as whn) |
176 by summing to some infinite hypernatural (such as whn) |
194 by (simp_tac (simpset() delsimps [realpow_Suc] |
194 by (simp_tac (simpset() delsimps [realpow_Suc] |
195 addsimps [sumhr,hypnat_add,double_lemma, hypreal_zero_def]) 1); |
195 addsimps [sumhr,hypnat_add,double_lemma, hypreal_zero_def]) 1); |
196 qed "sumhr_minus_one_realpow_zero"; |
196 qed "sumhr_minus_one_realpow_zero"; |
197 Addsimps [sumhr_minus_one_realpow_zero]; |
197 Addsimps [sumhr_minus_one_realpow_zero]; |
198 |
198 |
199 Goalw [hypnat_of_nat_def,hypreal_of_real_def] |
199 Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \ |
200 "(ALL n. m <= Suc n --> f n = r) & m <= na \ |
|
201 \ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \ |
200 \ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \ |
202 \ (hypreal_of_nat (na - m) * hypreal_of_real r)"; |
201 \ (hypreal_of_nat (na - m) * hypreal_of_real r)"; |
203 by (auto_tac (claset() addSDs [sumr_interval_const], |
202 by (auto_tac (claset() addSDs [sumr_interval_const], |
204 simpset() addsimps [sumhr,hypreal_of_nat_def, |
203 simpset() addsimps [hypreal_of_real_def, sumhr,hypreal_of_nat_eq, hypnat_of_nat_eq, |
205 hypreal_of_real_def, hypreal_mult])); |
204 hypreal_of_real_def, hypreal_mult])); |
206 qed "sumhr_interval_const"; |
205 qed "sumhr_interval_const"; |
207 |
206 |
208 Goalw [hypnat_zero_def] |
207 Goalw [hypnat_zero_def] |
209 "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"; |
208 "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"; |