summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 05 Sep 2014 14:58:13 +0200 | |

changeset 58193 | ae8a5e111ee1 |

parent 58192 | d0dffec0da2b |

child 58194 | 3d90a96fd6a9 |

added lemma

--- 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