src/HOL/Number_Theory/Binomial.thy
 author haftmann Mon, 08 Mar 2010 09:38:58 +0100 changeset 35644 d20cf282342e parent 32479 521cc9bf2958 child 35731 1bdaa24fb56d permissions -rw-r--r--
transfer: avoid camel case
```
(*  Title:      Binomial.thy
Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow

Defines the "choose" function, and establishes basic properties.

The original theory "Binomial" was by Lawrence C. Paulson, based on
the work of Andy Gordon and Florian Kammueller. The approach here,
which derives the definition of binomial coefficients in terms of the
factorial function, is due to Jeremy Avigad. The binomial theorem was
formalized by Tobias Nipkow.

*)

theory Binomial
imports Cong Fact
begin

subsection {* Main definitions *}

class binomial =

fixes
binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)

(* definitions for the natural numbers *)

instantiation nat :: binomial

begin

fun
binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"binomial_nat n k =
(if k = 0 then 1 else
if n = 0 then 0 else
(binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"

instance proof qed

end

(* definitions for the integers *)

instantiation int :: binomial

begin

definition
binomial_int :: "int => int \<Rightarrow> int"
where
"binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
else 0)"
instance proof qed

end

subsection {* Set up Transfer *}

lemma transfer_nat_int_binomial:
"(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) =
nat (binomial n k)"
unfolding binomial_int_def
by auto

lemma transfer_nat_int_binomial_closure:
"n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"

transfer_nat_int_binomial transfer_nat_int_binomial_closure]

lemma transfer_int_nat_binomial:
"binomial (int n) (int k) = int (binomial n k)"
unfolding fact_int_def binomial_int_def by auto

lemma transfer_int_nat_binomial_closure:
"is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"

transfer_int_nat_binomial transfer_int_nat_binomial_closure]

subsection {* Binomial coefficients *}

lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1"
by simp

lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"

lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
by (induct n rule: induct'_nat, auto)

lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
unfolding binomial_int_def apply (case_tac "n < 0")
apply force
apply (simp del: binomial_nat.simps)
done

lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
by simp

lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
unfolding binomial_int_def apply (subst choose_reduce_nat)
apply (auto simp del: binomial_nat.simps
done

lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) =
(n choose (k + 1)) + (n choose k)"

lemma choose_Suc_nat: "(Suc n) choose (Suc k) =
(n choose (Suc k)) + (n choose k)"

lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) =
(n choose (k + 1)) + (n choose k)"

declare binomial_nat.simps [simp del]

lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)

lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"

lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)

lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"

lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1"
apply (induct n rule: induct'_nat, force)
apply (case_tac "n = 0")
apply auto
apply (subst choose_reduce_nat)
(* natdiff_cancel_numerals introduces Suc *)
done

lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n"
using plus_one_choose_self_nat by (simp add: One_nat_def)

lemma plus_one_choose_self_int [rule_format, simp]:
"(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"

(* bounded quantification doesn't work with the unicode characters? *)
lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat).
((n::nat) choose k) > 0"
apply (induct n rule: induct'_nat)
apply force
apply clarify
apply (case_tac "k = 0")
apply force
apply (subst choose_reduce_nat)
apply auto
done

lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
((n::int) choose k) > 0"
by (auto simp add: binomial_int_def choose_pos_nat)

lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
(ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
apply (induct n rule: induct'_nat)
apply auto
apply (case_tac "k = 0")
apply auto
apply (case_tac "k = n + 1")
apply auto
apply (drule_tac x = n in spec) back back
apply (drule_tac x = "k - 1" in spec) back back back
apply auto
done

lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow>
fact k * fact (n - k) * (n choose k) = fact n"
apply (rule binomial_induct [of _ k n])
apply auto
proof -
fix k :: nat and n
assume less: "k < n"
assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
by (subst fact_plus_one_nat, auto)
assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
fact n"
with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
(n choose (k + 1)) = (n - k) * fact n"
by (subst (2) fact_plus_one_nat, auto)
with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) =
(n - k) * fact n" by simp
have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
fact (k + 1) * fact (n - k) * (n choose (k + 1)) +
fact (k + 1) * fact (n - k) * (n choose k)"
by (subst choose_reduce_nat, auto simp add: ring_simps)
also note one
also note two
also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
apply (subst fact_plus_one_nat)
apply (subst left_distrib [symmetric])
apply simp
done
finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
fact (n + 1)" .
qed

lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
n choose k = fact n div (fact k * fact (n - k))"
apply (frule choose_altdef_aux_nat)
apply (erule subst)
done

lemma choose_altdef_int:
assumes "(0::int) <= k" and "k <= n"
shows "n choose k = fact n div (fact k * fact (n - k))"

apply (subst tsub_eq [symmetric], rule prems)
apply (rule choose_altdef_nat [transferred])
using prems apply auto
done

lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
unfolding dvd_def apply (frule choose_altdef_aux_nat)
(* why don't blast and auto get this??? *)
apply (rule exI)
apply (erule sym)
done

lemma choose_dvd_int:
assumes "(0::int) <= k" and "k <= n"
shows "fact k * fact (n - k) dvd fact n"

apply (subst tsub_eq [symmetric], rule prems)
apply (rule choose_dvd_nat [transferred])
using prems apply auto
done

(* generalizes Tobias Nipkow's proof to any commutative semiring *)
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
(SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
proof (induct n rule: induct'_nat)
show "?P 0" by simp
next
fix n
assume ih: "?P n"
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 decomp3: "{1..n+1} = {n+1} Un {1..n}"
by auto
have "(a+b)^(n+1) =
(a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
using ih by (simp add: power_plus_one)
also have "... =  a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
by (rule distrib)
also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
(SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
also have "... = a^(n+1) + b^(n+1) +
(SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
(SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
also have
"... = a^(n+1) + b^(n+1) +
(SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
choose_reduce_nat)
also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
using decomp by (simp add: ring_simps)
finally show "?P (n + 1)" by simp
qed

lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
by auto

lemma card_subsets_nat [rule_format]:
fixes S :: "'a set"
assumes "finite S"
shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k"
(is "?P S")
using `finite S`
proof (induct set: finite)
show "?P {}" by (auto simp add: set_explicit)
next fix x :: "'a" and F
assume iassms: "finite F" "x ~: F"
assume ih: "?P F"
show "?P (insert x F)" (is "ALL k. ?Q k")
proof
fix k
show "card {T. T \<subseteq> (insert x F) \<and> card T = k} =
card (insert x F) choose k" (is "?Q k")
proof (induct k rule: induct'_nat)
from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
apply auto
apply (subst (asm) card_0_eq)
apply (auto elim: finite_subset)
done
thus "?Q 0"
by auto
next fix k
show "?Q (k + 1)"
proof -
from iassms have fin: "finite (insert x F)" by auto
hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
{T. T \<le> F & card T = k + 1} Un
{T. T \<le> insert x F & x : T & card T = k + 1}"
by (auto intro!: subsetI)
with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
card ({T. T \<subseteq> F \<and> card T = k + 1}) +
card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
apply (subst card_Un_disjoint [symmetric])
apply auto
(* note: nice! Didn't have to say anything here *)
done
also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) =
card F choose (k+1)" by auto
also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
card ({T. T <= F & card T = k})"
proof -
let ?f = "%T. T Un {x}"
from iassms have "inj_on ?f {T. T <= F & card T = k}"
unfolding inj_on_def by (auto intro!: subsetI)
hence "card ({T. T <= F & card T = k}) =
card(?f ` {T. T <= F & card T = k})"
by (rule card_image [symmetric])
also from iassms fin have "?f ` {T. T <= F & card T = k} =
{T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
unfolding image_def
(* I can't figure out why this next line takes so long *)
apply auto
apply (frule (1) finite_subset, force)
apply (rule_tac x = "xa - {x}" in exI)
apply (subst card_Diff_singleton)
apply (auto elim: finite_subset)
done
finally show ?thesis by (rule sym)
qed
also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
by auto
finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
card F choose (k + 1) + (card F choose k)".
with iassms choose_plus_one_nat show ?thesis
by auto
qed
qed
qed
qed

end
```