diff -r 4874411752fe -r 7edb7550663e src/HOL/Old_Number_Theory/Finite2.thy --- a/src/HOL/Old_Number_Theory/Finite2.thy Fri May 30 12:54:42 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Finite2.thy Fri May 30 14:55:10 2014 +0200 @@ -185,38 +185,4 @@ by (auto simp add: card_bdd_int_set_l_le) -subsection {* Cardinality of finite cartesian products *} - -(* FIXME could be useful in general but not needed here -lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \ (A <*> B)" - by blast - *) - -text {* Lemmas for counting arguments. *} - -lemma setsum_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; - g ` B \ A; inj_on g B |] ==> setsum g B = setsum (g \ f) A" - apply (frule_tac h = g and f = f in setsum_reindex) - apply (subgoal_tac "setsum g B = setsum g (f ` A)") - apply (simp add: inj_on_def) - apply (subgoal_tac "card A = card B") - apply (drule_tac A = "f ` A" and B = B in card_seteq) - apply (auto simp add: card_image) - apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) - apply (frule_tac A = B and B = A and f = g in card_inj_on_le) - apply auto - done - -lemma setprod_bij_eq: "[| finite A; finite B; f ` A \ B; inj_on f A; - g ` B \ A; inj_on g B |] ==> setprod g B = setprod (g \ f) A" - apply (frule_tac h = g and f = f in setprod_reindex) - apply (subgoal_tac "setprod g B = setprod g (f ` A)") - apply (simp add: inj_on_def) - apply (subgoal_tac "card A = card B") - apply (drule_tac A = "f ` A" and B = B in card_seteq) - apply (auto simp add: card_image) - apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto) - apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto) - done - end