src/HOL/List.thy
 changeset 52141 eff000cab70f parent 52131 366fa32ee2a3 child 52148 893b15200ec1
equal 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)+`