# HG changeset patch
# User nipkow
# Date 1409921893 -7200
# Node ID ae8a5e111ee1c507ea50c68686a0247f4579a4a1
# Parent  d0dffec0da2ba7a3b1cc3ab45d44ed021b2fde7e
added lemma

diff -r d0dffec0da2b -r ae8a5e111ee1 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Fri Sep 05 14:58:13 2014 +0200
@@ -766,4 +766,93 @@
   finally show ?thesis ..
 qed
 
+text{* The number of nat lists of length @{text m} summing to @{text N} is
+@{term "(N + m - 1) choose N"}: *} 
+
+lemma card_length_listsum_rec:
+  assumes "m\<ge>1"
+  shows "card {l::nat list. length l = m \<and> listsum l = N} =
+    (card {l. length l = (m - 1) \<and> listsum l = N} +
+    card {l. length l = m \<and> listsum l + 1 =  N})"
+    (is "card ?C = (card ?A + card ?B)")
+proof - 
+  let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
+  let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
+  let ?f ="\<lambda> l. 0#l"
+  let ?g ="\<lambda> l. (hd l + 1) # tl l"
+  have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp
+  have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs"
+    by(auto simp add: neq_Nil_conv)
+  have f: "bij_betw ?f ?A ?A'"
+    apply(rule bij_betw_byWitness[where f' = tl])
+    using assms 
+    by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
+  have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs"
+    by (metis 1 listsum_simps(2) 2)
+  have g: "bij_betw ?g ?B ?B'"
+    apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"])
+    using assms
+    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
+      simp del: length_greater_0_conv length_0_conv)
+  { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}"
+    using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto }
+    note fin = this
+  have fin_A: "finite ?A" using fin[of _ "N+1"]
+    by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"], 
+      auto simp: member_le_listsum_nat less_Suc_eq_le)
+  have fin_B: "finite ?B"
+    by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"], 
+      auto simp: member_le_listsum_nat less_Suc_eq_le fin)
+  have uni: "?C = ?A' \<union> ?B'" by auto
+  have disj: "?A' \<inter> ?B' = {}" by auto
+  have "card ?C = card(?A' \<union> ?B')" using uni by simp
+  also have "\<dots> = card ?A + card ?B"
+    using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
+      bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
+    by presburger
+  finally show ?thesis .
+qed
+
+lemma card_length_listsum:
+  "m\<ge>1 \<Longrightarrow> card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
+proof (induct "N + m - 1" arbitrary: N m)
+-- "In the base case, the only solution is [0]."
+  case 0
+  have 1: "0 = N + m - 1 " by fact
+  hence 2: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
+    by(auto simp: length_Suc_conv)
+  show "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
+  proof -
+    from 1 "0.prems" have "m=1 \<and> N=0" by auto
+    with "0.prems" show ?thesis by (auto simp add: 2)
+  qed
+next
+  case (Suc k)
+  
+  have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} = 
+    (N + (m - 1) - 1) choose N"
+  proof cases
+    assume "m = 1"
+    with Suc.hyps have "N\<ge>1" by auto
+    with `m = 1` show ?thesis  by (subst binomial_eq_0, auto)
+  next
+    assume "m \<noteq> 1" thus ?thesis using Suc by fastforce
+  qed
+
+  from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
+    (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
+  proof -
+    have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith
+    from Suc have "N>0 \<Longrightarrow>
+      card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
+      ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)
+    thus ?thesis by auto
+  qed
+
+  from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} + 
+      card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
+    by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
+  thus ?case using card_length_listsum_rec[OF Suc.prems] by auto
+qed
+
 end