equal
deleted
inserted
replaced
122 lemma (in monoid_add) length_concat: |
122 lemma (in monoid_add) length_concat: |
123 "length (concat xss) = sum_list (map length xss)" |
123 "length (concat xss) = sum_list (map length xss)" |
124 by (induct xss) simp_all |
124 by (induct xss) simp_all |
125 |
125 |
126 lemma (in monoid_add) length_product_lists: |
126 lemma (in monoid_add) length_product_lists: |
127 "length (product_lists xss) = foldr ( * ) (map length xss) 1" |
127 "length (product_lists xss) = foldr (*) (map length xss) 1" |
128 proof (induct xss) |
128 proof (induct xss) |
129 case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) |
129 case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def) |
130 qed simp |
130 qed simp |
131 |
131 |
132 lemma (in monoid_add) sum_list_map_filter: |
132 lemma (in monoid_add) sum_list_map_filter: |