# HG changeset patch # User Lars Hupel # Date 1516706926 -3600 # Node ID f1ba59ddd9a6d74251c636f527ad52cca4ee6e7b # Parent 3d33847dc911d5e5d16a5a589489eaabab1d8aed drop redundant cong rules diff -r 3d33847dc911 -r f1ba59ddd9a6 src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Mon Jan 22 22:45:45 2018 +0100 +++ b/src/HOL/Groups_List.thy Tue Jan 23 12:28:46 2018 +0100 @@ -8,34 +8,34 @@ locale monoid_list = monoid begin - + definition F :: "'a list \ 'a" where eq_foldr [code]: "F xs = foldr f xs \<^bold>1" - + lemma Nil [simp]: "F [] = \<^bold>1" by (simp add: eq_foldr) - + lemma Cons [simp]: "F (x # xs) = x \<^bold>* F xs" by (simp add: eq_foldr) - + lemma append [simp]: "F (xs @ ys) = F xs \<^bold>* F ys" by (induct xs) (simp_all add: assoc) - + end locale comm_monoid_list = comm_monoid + monoid_list begin - + lemma rev [simp]: "F (rev xs) = F xs" by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute) - + end - + locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set begin @@ -58,7 +58,7 @@ sublocale sum_list: monoid_list plus 0 defines sum_list = sum_list.F .. - + end context comm_monoid_add @@ -268,7 +268,7 @@ finally show ?thesis by(simp add:sum_list_map_eq_sum_count) qed -lemma sum_list_nonneg: +lemma sum_list_nonneg: "(\x. x \ set xs \ (x :: 'a :: ordered_comm_monoid_add) \ 0) \ sum_list xs \ 0" by (induction xs) simp_all @@ -276,17 +276,7 @@ "sum_list (map f (filter P xs)) = sum_list (map (\x. if P x then f x else 0) xs)" by (induction xs) simp_all -lemma sum_list_cong [fundef_cong]: - assumes "xs = ys" - assumes "\x. x \ set xs \ f x = g x" - shows "sum_list (map f xs) = sum_list (map g ys)" -proof - - from assms(2) have "sum_list (map f xs) = sum_list (map g xs)" - by (induction xs) simp_all - with assms(1) show ?thesis by simp -qed - -text \Summation of a strictly ascending sequence with length \n\ +text \Summation of a strictly ascending sequence with length \n\ can be upper-bounded by summation over \{0...\ lemma sorted_wrt_less_sum_mono_lowerbound: @@ -299,17 +289,17 @@ then show ?case by simp next case (snoc n ns) - have "sum f {0.. sum_list (map f ns)" using snoc by (auto simp: sorted_wrt_append) also have "length ns \ n" - using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto + using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto finally have "sum f {0.. sum_list (map f ns) + f n" using mono add_mono by blast thus ?case by simp -qed +qed subsection \Further facts about @{const List.n_lists}\ @@ -397,17 +387,7 @@ end -lemma prod_list_cong [fundef_cong]: - assumes "xs = ys" - assumes "\x. x \ set xs \ f x = g x" - shows "prod_list (map f xs) = prod_list (map g ys)" -proof - - from assms(2) have "prod_list (map f xs) = prod_list (map g xs)" - by (induction xs) simp_all - with assms(1) show ?thesis by simp -qed - -lemma prod_list_zero_iff: +lemma prod_list_zero_iff: "prod_list xs = 0 \ (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \ set xs" by (induction xs) simp_all diff -r 3d33847dc911 -r f1ba59ddd9a6 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Jan 22 22:45:45 2018 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Jan 23 12:28:46 2018 +0100 @@ -2059,7 +2059,7 @@ qed simp also have "\ = (\(x',p)\xs. ennreal p * (\\<^sup>+ x. indicator {x'} x \count_space UNIV))" using assms(1) - by (intro sum_list_cong, simp only: case_prod_unfold, subst nn_integral_cmult [symmetric]) + by (simp cong: map_cong only: case_prod_unfold, subst nn_integral_cmult [symmetric]) (auto intro!: assms(1) simp: max_def times_ereal.simps [symmetric] mult_ac ereal_indicator simp del: times_ereal.simps)+ also from assms have "\ = sum_list (map snd xs)" by (simp add: case_prod_unfold sum_list_ennreal)