src/HOL/List.thy
changeset 52141 eff000cab70f
parent 52131 366fa32ee2a3
child 52148 893b15200ec1
equal deleted inserted replaced
52140:88a69da5d3fa 52141:eff000cab70f
  4310   moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
  4310   moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
  4311     by auto
  4311     by auto
  4312   moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
  4312   moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
  4313     by (simp add: card_Diff_subset distinct_card)
  4313     by (simp add: card_Diff_subset distinct_card)
  4314   moreover have "{xs. ?k_list (Suc k) xs} =
  4314   moreover have "{xs. ?k_list (Suc k) xs} =
  4315       (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
  4315       (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
  4316     by (auto simp: length_Suc_conv)
  4316     by (auto simp: length_Suc_conv)
  4317   moreover
  4317   moreover
  4318   have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
  4318   have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
  4319   then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
  4319   then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
  4320     by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+
  4320     by (subst setprod_insert[symmetric]) (simp add: atLeastAtMost_insertL)+