764 qed |
764 qed |
765 also have "nat \<dots> = card (\<Union>A)" by simp |
765 also have "nat \<dots> = card (\<Union>A)" by simp |
766 finally show ?thesis .. |
766 finally show ?thesis .. |
767 qed |
767 qed |
768 |
768 |
|
769 text{* The number of nat lists of length @{text m} summing to @{text N} is |
|
770 @{term "(N + m - 1) choose N"}: *} |
|
771 |
|
772 lemma card_length_listsum_rec: |
|
773 assumes "m\<ge>1" |
|
774 shows "card {l::nat list. length l = m \<and> listsum l = N} = |
|
775 (card {l. length l = (m - 1) \<and> listsum l = N} + |
|
776 card {l. length l = m \<and> listsum l + 1 = N})" |
|
777 (is "card ?C = (card ?A + card ?B)") |
|
778 proof - |
|
779 let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}" |
|
780 let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}" |
|
781 let ?f ="\<lambda> l. 0#l" |
|
782 let ?g ="\<lambda> l. (hd l + 1) # tl l" |
|
783 have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp |
|
784 have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs" |
|
785 by(auto simp add: neq_Nil_conv) |
|
786 have f: "bij_betw ?f ?A ?A'" |
|
787 apply(rule bij_betw_byWitness[where f' = tl]) |
|
788 using assms |
|
789 by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv) |
|
790 have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs" |
|
791 by (metis 1 listsum_simps(2) 2) |
|
792 have g: "bij_betw ?g ?B ?B'" |
|
793 apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"]) |
|
794 using assms |
|
795 by (auto simp: 2 length_0_conv[symmetric] intro!: 3 |
|
796 simp del: length_greater_0_conv length_0_conv) |
|
797 { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" |
|
798 using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto } |
|
799 note fin = this |
|
800 have fin_A: "finite ?A" using fin[of _ "N+1"] |
|
801 by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"], |
|
802 auto simp: member_le_listsum_nat less_Suc_eq_le) |
|
803 have fin_B: "finite ?B" |
|
804 by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"], |
|
805 auto simp: member_le_listsum_nat less_Suc_eq_le fin) |
|
806 have uni: "?C = ?A' \<union> ?B'" by auto |
|
807 have disj: "?A' \<inter> ?B' = {}" by auto |
|
808 have "card ?C = card(?A' \<union> ?B')" using uni by simp |
|
809 also have "\<dots> = card ?A + card ?B" |
|
810 using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g] |
|
811 bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B |
|
812 by presburger |
|
813 finally show ?thesis . |
|
814 qed |
|
815 |
|
816 lemma card_length_listsum: |
|
817 "m\<ge>1 \<Longrightarrow> card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N" |
|
818 proof (induct "N + m - 1" arbitrary: N m) |
|
819 -- "In the base case, the only solution is [0]." |
|
820 case 0 |
|
821 have 1: "0 = N + m - 1 " by fact |
|
822 hence 2: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}" |
|
823 by(auto simp: length_Suc_conv) |
|
824 show "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N" |
|
825 proof - |
|
826 from 1 "0.prems" have "m=1 \<and> N=0" by auto |
|
827 with "0.prems" show ?thesis by (auto simp add: 2) |
|
828 qed |
|
829 next |
|
830 case (Suc k) |
|
831 |
|
832 have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l = N} = |
|
833 (N + (m - 1) - 1) choose N" |
|
834 proof cases |
|
835 assume "m = 1" |
|
836 with Suc.hyps have "N\<ge>1" by auto |
|
837 with `m = 1` show ?thesis by (subst binomial_eq_0, auto) |
|
838 next |
|
839 assume "m \<noteq> 1" thus ?thesis using Suc by fastforce |
|
840 qed |
|
841 |
|
842 from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} = |
|
843 (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)" |
|
844 proof - |
|
845 have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith |
|
846 from Suc have "N>0 \<Longrightarrow> |
|
847 card {l::nat list. size l = m \<and> listsum l + 1 = N} = |
|
848 ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux) |
|
849 thus ?thesis by auto |
|
850 qed |
|
851 |
|
852 from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} + |
|
853 card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N" |
|
854 by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def) |
|
855 thus ?case using card_length_listsum_rec[OF Suc.prems] by auto |
|
856 qed |
|
857 |
769 end |
858 end |