equal
deleted
inserted
replaced
226 |
226 |
227 subsection \<open>Definition and basic properties\<close> |
227 subsection \<open>Definition and basic properties\<close> |
228 |
228 |
229 datatype ereal = ereal real | PInfty | MInfty |
229 datatype ereal = ereal real | PInfty | MInfty |
230 |
230 |
|
231 lemma ereal_cong: "x = y \<Longrightarrow> ereal x = ereal y" by simp |
|
232 |
231 instantiation ereal :: uminus |
233 instantiation ereal :: uminus |
232 begin |
234 begin |
233 |
235 |
234 fun uminus_ereal where |
236 fun uminus_ereal where |
235 "- (ereal r) = ereal (- r)" |
237 "- (ereal r) = ereal (- r)" |
768 then show ?thesis by induct auto |
770 then show ?thesis by induct auto |
769 next |
771 next |
770 case False |
772 case False |
771 then show ?thesis by simp |
773 then show ?thesis by simp |
772 qed |
774 qed |
|
775 |
|
776 lemma listsum_ereal [simp]: "listsum (map (\<lambda>x. ereal (f x)) xs) = ereal (listsum (map f xs))" |
|
777 by (induction xs) simp_all |
773 |
778 |
774 lemma setsum_Pinfty: |
779 lemma setsum_Pinfty: |
775 fixes f :: "'a \<Rightarrow> ereal" |
780 fixes f :: "'a \<Rightarrow> ereal" |
776 shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)" |
781 shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)" |
777 proof safe |
782 proof safe |