src/HOL/Old_Number_Theory/Finite2.thy
changeset 57129 7edb7550663e
parent 51489 f738e6dbd844
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Fri May 30 12:54:42 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri May 30 14:55:10 2014 +0200
     1.3 @@ -185,38 +185,4 @@
     1.4    by (auto simp add: card_bdd_int_set_l_le)
     1.5  
     1.6  
     1.7 -subsection {* Cardinality of finite cartesian products *}
     1.8 -
     1.9 -(* FIXME could be useful in general but not needed here
    1.10 -lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
    1.11 -  by blast
    1.12 - *)
    1.13 -
    1.14 -text {* Lemmas for counting arguments. *}
    1.15 -
    1.16 -lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
    1.17 -    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
    1.18 -  apply (frule_tac h = g and f = f in setsum_reindex)
    1.19 -  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
    1.20 -   apply (simp add: inj_on_def)
    1.21 -  apply (subgoal_tac "card A = card B")
    1.22 -   apply (drule_tac A = "f ` A" and B = B in card_seteq)
    1.23 -     apply (auto simp add: card_image)
    1.24 -  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
    1.25 -  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
    1.26 -    apply auto
    1.27 -  done
    1.28 -
    1.29 -lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
    1.30 -    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
    1.31 -  apply (frule_tac h = g and f = f in setprod_reindex)
    1.32 -  apply (subgoal_tac "setprod g B = setprod g (f ` A)")
    1.33 -   apply (simp add: inj_on_def)
    1.34 -  apply (subgoal_tac "card A = card B")
    1.35 -   apply (drule_tac A = "f ` A" and B = B in card_seteq)
    1.36 -     apply (auto simp add: card_image)
    1.37 -  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
    1.38 -  apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
    1.39 -  done
    1.40 -
    1.41  end