# HG changeset patch # User paulson # Date 1385224897 0 # Node ID e51a0c4965f7a3d74571e73ce5c9491e5930e22c # Parent cfe53047dc16e465ac0d819cb649283866f08e2d# Parent 08b642269a0d66e0e45baa14e603b1c7feeb4db4 merged diff -r cfe53047dc16 -r e51a0c4965f7 src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Sat Nov 23 17:15:44 2013 +0100 +++ b/src/HOL/Library/Binomial.thy Sat Nov 23 16:41:37 2013 +0000 @@ -26,6 +26,11 @@ lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" by simp +lemma choose_reduce_nat: + "0 < (n::nat) \ 0 < k \ + (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))" + by (metis Suc_diff_1 binomial.simps(2) nat_add_commute neq0_conv) + lemma binomial_eq_0: "n < k \ n choose k = 0" by (induct n arbitrary: k) auto @@ -44,10 +49,7 @@ by (induct n k rule: diff_induct) simp_all lemma binomial_eq_0_iff: "n choose k = 0 \ n < k" - apply (safe intro!: binomial_eq_0) - apply (erule contrapos_pp) - apply (simp add: zero_less_binomial) - done + by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial) lemma zero_less_binomial_iff: "n choose k > 0 \ k \ n" by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv) @@ -90,19 +92,7 @@ apply safe apply (auto intro: finite_subset [THEN card_insert_disjoint]) apply (drule_tac x = "xa - {x}" in spec) - apply (subgoal_tac "x \ xa") - apply auto - apply (erule rev_mp, subst card_Diff_singleton) - apply (auto intro: finite_subset) - done -(* -lemma "finite(UN y. {x. P x y})" -apply simp -lemma Collect_ex_eq - -lemma "{x. \y. P x y} = (UN y. {x. P x y})" -apply blast -*) + by (metis card_Diff_singleton_if card_infinite diff_Suc_1 in_mono insert_Diff_single insert_absorb lessI less_nat_zero_code subset_insert_iff) lemma finite_bex_subset [simp]: assumes "finite B" @@ -120,71 +110,75 @@ "finite A \ x \ A \ card {B. \C. C \ A \ card C = k \ B = insert x C} = card {B. B \ A & card(B) = k}" - apply (rule_tac f = "\s. s - {x}" and g = "insert x" in card_bij_eq) - apply (auto elim!: equalityE simp add: inj_on_def) - apply (subst Diff_insert0) - apply auto + apply (rule card_bij_eq [where f = "\s. s - {x}" and g = "insert x"]) + apply (auto elim!: equalityE simp add: inj_on_def) + apply (metis card_Diff_singleton_if finite_subset in_mono) done text {* Main theorem: combinatorial statement about number of subsets of a set. *} -lemma n_sub_lemma: - "finite A \ card {B. B \ A \ card B = k} = (card A choose k)" - apply (induct k arbitrary: A) - apply (simp add: card_s_0_eq_empty) - apply atomize - apply (rotate_tac -1) - apply (erule finite_induct) - apply (simp_all (no_asm_simp) cong add: conj_cong - add: card_s_0_eq_empty choose_deconstruct) - apply (subst card_Un_disjoint) - prefer 4 apply (force simp add: constr_bij) - prefer 3 apply force - prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] - finite_subset [of _ "Pow (insert x F)", standard]) - apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) - done - theorem n_subsets: "finite A \ card {B. B \ A \ card B = k} = (card A choose k)" - by (simp add: n_sub_lemma) +proof (induct k arbitrary: A) + case 0 then show ?case by (simp add: card_s_0_eq_empty) +next + case (Suc k) + show ?case using `finite A` + proof (induct A) + case empty show ?case by (simp add: card_s_0_eq_empty) + next + case (insert x A) + then show ?case using Suc.hyps + apply (simp add: card_s_0_eq_empty choose_deconstruct) + apply (subst card_Un_disjoint) + prefer 4 apply (force simp add: constr_bij) + prefer 3 apply force + prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2] + finite_subset [of _ "Pow (insert x F)", standard]) + apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset]) + done + qed +qed text{* The binomial theorem (courtesy of Tobias Nipkow): *} -theorem binomial: "(a + b::nat)^n = (\k=0..n. (n choose k) * a^k * b^(n - k))" +(* Avigad's version, generalized to any commutative semiring *) +theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = + (\k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n") proof (induct n) - case 0 - then show ?case by simp + case 0 then show "?P 0" by simp next case (Suc n) - have decomp: "{0..n+1} = {0} \ {n+1} \ {1..n}" - by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) - have decomp2: "{0..n} = {0} \ {1..n}" - by (auto simp add:atLeastAtMost_def atLeast_def atMost_def) - have "(a + b)^(n + 1) = (a + b) * (\k=0..n. (n choose k) * a^k * b^(n - k))" - using Suc by simp - also have "\ = a*(\k=0..n. (n choose k) * a^k * b^(n-k)) + - b*(\k=0..n. (n choose k) * a^k * b^(n-k))" - by (rule nat_distrib) - also have "\ = (\k=0..n. (n choose k) * a^(k+1) * b^(n-k)) + - (\k=0..n. (n choose k) * a^k * b^(n-k+1))" - by (simp add: setsum_right_distrib mult_ac) - also have "\ = (\k=0..n. (n choose k) * a^k * b^(n+1-k)) + - (\k=1..n+1. (n choose (k - 1)) * a^k * b^(n+1-k))" - by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le - del:setsum_cl_ivl_Suc) + have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}" + by auto + have decomp2: "{0..n} = {0} Un {1..n}" + by auto + have "(a+b)^(n+1) = + (a+b) * (\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" + using Suc.hyps by simp + also have "\ = a*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k)) + + b*(\k=0..n. of_nat (n choose k) * a^k * b^(n-k))" + by (rule distrib) + also have "\ = (\k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) + + (\k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))" + by (auto simp add: setsum_right_distrib mult_ac) + also have "\ = (\k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) + + (\k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))" + by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps + del:setsum_cl_ivl_Suc) also have "\ = a^(n+1) + b^(n+1) + - (\k=1..n. (n choose (k - 1)) * a^k * b^(n+1-k)) + - (\k=1..n. (n choose k) * a^k * b^(n+1-k))" + (\k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) + + (\k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))" by (simp add: decomp2) also have - "\ = a^(n+1) + b^(n+1) + (\k=1..n. (n+1 choose k) * a^k * b^(n+1-k))" - by (simp add: nat_distrib setsum_addf binomial.simps) - also have "\ = (\k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" - using decomp by simp - finally show ?case by simp + "\ = a^(n+1) + b^(n+1) + + (\k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))" + by (auto simp add: field_simps setsum_addf [symmetric] choose_reduce_nat) + also have "\ = (\k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))" + using decomp by (simp add: field_simps) + finally show "?P (Suc n)" by simp qed subsection{* Pochhammer's symbol : generalized raising factorial*}