864 by (simp add: a) |
864 by (simp add: a) |
865 finally show ?thesis . |
865 finally show ?thesis . |
866 qed |
866 qed |
867 |
867 |
868 |
868 |
869 subsection \<open>@{term sum} and @{term setprod}\<close> |
869 subsection \<open>@{term sum} and @{term prod}\<close> |
870 |
870 |
871 lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))" |
871 lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))" |
872 by (induct A rule: infinite_finite_induct) auto |
872 by (induct A rule: infinite_finite_induct) auto |
873 |
873 |
874 lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))" |
874 lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))" |
875 by (induct A rule: infinite_finite_induct) auto |
875 by (induct A rule: infinite_finite_induct) auto |
876 |
876 |
877 lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))" |
877 lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))" |
878 by (induct A rule: infinite_finite_induct) auto |
878 by (induct A rule: infinite_finite_induct) auto |
879 |
879 |
880 lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))" |
880 lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))" |
881 by (induct A rule: infinite_finite_induct) auto |
881 by (induct A rule: infinite_finite_induct) auto |
882 |
882 |
883 lemmas int_sum = of_nat_sum [where 'a=int] |
883 lemmas int_sum = of_nat_sum [where 'a=int] |
884 lemmas int_setprod = of_nat_setprod [where 'a=int] |
884 lemmas int_prod = of_nat_prod [where 'a=int] |
885 |
885 |
886 |
886 |
887 text \<open>Legacy theorems\<close> |
887 text \<open>Legacy theorems\<close> |
888 |
888 |
889 lemmas zle_int = of_nat_le_iff [where 'a=int] |
889 lemmas zle_int = of_nat_le_iff [where 'a=int] |