equal
deleted
inserted
replaced
264 |
264 |
265 subsection {* Reindexing sums and products *} |
265 subsection {* Reindexing sums and products *} |
266 |
266 |
267 lemma sum_prop [rule_format]: "finite B ==> |
267 lemma sum_prop [rule_format]: "finite B ==> |
268 inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"; |
268 inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"; |
269 apply (rule finite_induct, assumption, force) |
269 by (rule finite_induct, auto) |
270 apply (rule impI, auto) |
|
271 apply (simp add: inj_on_def) |
|
272 apply (subgoal_tac "f x \<notin> f ` F") |
|
273 apply (subgoal_tac "finite (f ` F)"); |
|
274 apply (auto simp add: setsum_insert) |
|
275 by (simp add: inj_on_def) |
|
276 |
270 |
277 lemma sum_prop_id: "finite B ==> inj_on f B ==> |
271 lemma sum_prop_id: "finite B ==> inj_on f B ==> |
278 setsum f B = setsum id (f ` B)"; |
272 setsum f B = setsum id (f ` B)"; |
279 by (auto simp add: sum_prop id_o) |
273 by (auto simp add: sum_prop id_o) |
280 |
274 |