equal
deleted
inserted
replaced
155 sumhr hypreal_diff real_of_nat_Suc) |
155 sumhr hypreal_diff real_of_nat_Suc) |
156 |
156 |
157 lemma sumhr_minus_one_realpow_zero [simp]: |
157 lemma sumhr_minus_one_realpow_zero [simp]: |
158 "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0" |
158 "sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0" |
159 by (simp del: realpow_Suc |
159 by (simp del: realpow_Suc |
160 add: sumhr hypnat_add double_lemma hypreal_zero_def |
160 add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def |
161 hypnat_zero_def hypnat_omega_def) |
161 hypnat_zero_def hypnat_omega_def) |
162 |
162 |
163 lemma sumhr_interval_const: |
163 lemma sumhr_interval_const: |
164 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
164 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
165 ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |
165 ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = |