Commit 3165a09a by nipkow

### New entry Bell_Numbers_Spivey

 ... ... @@ -3662,3 +3662,23 @@ abstract = effectively decide ideal membership in finitely generated polynomial ideals. Furthermore, all functions can be executed on a concrete representation of multivariate polynomials as association lists. [Bell_Numbers_Spivey] title = Spivey's Generalized Recurrence for Bell Numbers author = Lukas Bulwahn date = 2016-05-04 topic = Mathematics/Combinatorics abstract = This entry defines the Bell numbers as the cardinality of set partitions for a carrier set of given size, and derives Spivey's generalized recurrence relation for Bell numbers following his elegant and intuitive combinatorial proof.

As the set construction for the combinatorial proof requires construction of three intermediate structures, the main difficulty of the formalization is handling the overall combinatorial argument in a structured way. The introduced proof structure allows us to compose the combinatorial argument from its subparts, and supports to keep track how the detailed proof steps are related to the overall argument. To obtain this structure, this entry uses set monad notation for the set construction's definition, introduces suitable predicates and rules, and follows a repeating structure in its Isar proof.

This diff is collapsed.
 chapter AFP session Bell_Numbers_Spivey (AFP) = "HOL" + options [timeout=600] theories [document = false] "../Discrete_Summation/Stirling" "../Card_Number_Partitions/Additions_to_Main" "~~/src/HOL/Eisbach/Eisbach" "~~/src/HOL/Library/FuncSet" "~~/src/HOL/Library/Monad_Syntax" theories "../Card_Partitions/Card_Partitions" Set_Partition Bell_Numbers document_files "root.bib" "root.tex"
 (* Author: Lukas Bulwahn *) section {* Set Partitions *} theory Set_Partition imports "~~/src/HOL/Library/FuncSet" "../Card_Partitions/Card_Partitions" begin subsection {* Useful Additions to Main Theories *} lemma set_eqI': assumes "\x. x \ A \ x \ B" assumes "\x. x \ B \ x \ A" shows "A = B" using assms by auto lemma comp_image: "(op  f \ op  g) = op  (f o g)" by rule auto subsection {* Introduction and Elimination Rules *} text {* The definition of partitions is in the Card\_Partitions theory. *} lemma partitionsI: assumes "\p. p \ P \ p \ {}" assumes "\P = A" assumes "\p p'. p \ P \ p' \ P \ p \ p' \ p \ p' = {}" shows "partitions P A" using assms unfolding partitions_def by blast lemma partitionsE: assumes "partitions P A" obtains "\p. p \ P \ p \ {}" "\P = A" "\p p'. p \ P \ p' \ P \ p \ p' \ p \ p' = {}" using assms unfolding partitions_def by blast subsection {* Basic Facts on Set Partitions *} lemma partitions_notemptyI: assumes "partitions P A" assumes "A \ {}" shows "P \ {}" using assms by (auto elim: partitionsE) lemma partitions_disjoint: assumes "partitions P A" assumes "partitions Q B" assumes "A \ B = {}" shows "P \ Q = {}" using assms by (fastforce elim: partitionsE) lemma partitions_eq_implies_eq_carrier: assumes "partitions Q A" assumes "partitions Q B" shows "A = B" using assms by (fastforce elim: partitionsE) subsection {* The Unique Part Containing an Element in a Set Partition *} lemma partitions_partitions_unique: assumes "partitions P A" assumes "x \ A" shows "\!X. x \ X \ X \ P" proof - from \partitions P A\ have "\P = A" by (auto elim: partitionsE) from this \x \ A\ obtain X where X: "x \ X \ X \ P" by blast { fix Y assume "x \ Y \ Y \ P" from this have "X = Y" using X \partitions P A\ by (meson partitionsE disjoint_iff_not_equal) } from this X show ?thesis by auto qed lemma partitions_the_part_mem: assumes "partitions P A" assumes "x \ A" shows "(THE X. x \ X \ X \ P) \ P" proof - from \x \ A\ have "\!X. x \ X \ X \ P" using \partitions P A\ by (simp add: partitions_partitions_unique) from this show "(THE X. x \ X \ X \ P) \ P" by (metis (no_types, lifting) theI) qed lemma partitions_the_part_eq: assumes "partitions P A" assumes "x \ X" "X \ P" shows "(THE X. x \ X \ X \ P) = X" proof - from \x \ X\ \X \ P\ have "x \ A" using \partitions P A\ by (auto elim: partitionsE) from this have "\!X. x \ X \ X \ P" using \partitions P A\ by (simp add: partitions_partitions_unique) from \x \ X\ \X \ P\ this show "(THE X. x \ X \ X \ P) = X" by (auto intro!: the1_equality) qed subsection {* Cardinality of Parts in a Set Partition *} lemma partitions_le_set_elements: assumes "finite A" assumes "partitions P A" shows "card P \ card A" using assms proof (induct A arbitrary: P) case empty from this show "card P \ card {}" by (simp add: partitions_empty) next case (insert a A) show ?case proof (cases "{a} \ P") case True have prop_partitions: "\p\P. p \ {}" "\P = insert a A" "\p\P. \p'\P. p \ p' \ p \ p' = {}" using \partitions P (insert a A)\ by (fastforce elim: partitionsE)+ from this(2, 3) \a \ A\ \{a} \ P\ have A_eq: "A = $$P - {{a}})" by auto (metis Int_iff UnionI empty_iff insert_iff) from prop_partitions A_eq have partitions: "partitions (P - {{a}}) A" by (intro partitionsI) auto from insert.hyps(3) this have "card (P - {{a}}) \ card A" by simp from this insert(1, 2, 4) \{a} \ P\ show ?thesis using finite_elements[OF \finite A\ partitions] by simp next case False from \partitions P (insert a A)\ obtain p where p_def: "p \ P" "a \ p" by (blast elim: partitionsE) from \partitions P (insert a A)\ p_def have a_notmem: "\p'\ P - {p}. a \ p'" by (blast elim: partitionsE) from \partitions P (insert a A)\ p_def have "p - {a} \ P" unfolding partitions_def by (metis Diff_insert_absorb Diff_subset inf.orderE mk_disjoint_insert) let ?P' = "insert (p - {a}) (P - {p})" have "partitions ?P' A" proof (rule partitionsI) from \partitions P (insert a A)\ have "\p\P. p \ {}" by (auto elim: partitionsE) from this p_def \{a} \ P\ show "\p'. p'\insert (p - {a}) (P - {p}) \ p' \ {}" by (simp; metis (no_types) Diff_eq_empty_iff subset_singletonD) next from \partitions P (insert a A)\ have "\P = insert a A" by (auto elim: partitionsE) from p_def this \a \ A\ a_notmem show "\insert (p - {a}) (P - {p}) = A" by auto next show "\pa pa'. pa\insert (p - {a}) (P - {p}) \ pa'\insert (p - {a}) (P - {p}) \ pa \ pa' \ pa \ pa' = {}" using \partitions P (insert a A)\ p_def a_notmem unfolding partitions_def by (metis disjoint_iff_not_equal insert_Diff insert_iff) qed have "finite P" using \finite A\ \partitions ?P' A\ finite_elements by fastforce have "card P = Suc (card (P - {p}))" using p_def \finite P\ card.remove by fastforce also have "\ = card ?P'" using \p - {a} \ P\ \finite P\ by simp also have "\ \ card A" using \partitions ?P' A\ insert.hyps(3) by simp also have "\ \ card (insert a A)" by (simp add: card_insert_le \finite A\ ) finally show ?thesis . qed qed subsection {* Operations on Set Partitions *} lemma partitions_union: assumes "A \ B = {}" assumes "partitions P A" assumes "partitions Q B" shows "partitions (P \ Q) (A \ B)" proof (rule partitionsI) fix X assume "X \ P \ Q" from this \partitions P A\ \partitions Q B\ show "X \ {}" by (auto elim: partitionsE) next show "\(P \ Q) = A \ B" using \partitions P A\ \partitions Q B\ by (auto elim: partitionsE) next fix X Y assume "X \ P \ Q" "Y \ P \ Q" "X \ Y" from this assms show "X \ Y = {}" by (elim UnE partitionsE) auto qed lemma partitions_split1: assumes "partitions (P \ Q) A" shows "partitions P (\P)" proof (rule partitionsI) fix p assume "p \ P" from this assms show "p \ {}" using Un_iff partitionsE by auto next show "\P = \P" .. next fix p p' assume a: "p \ P" "p' \ P" "p \ p'" from this assms show "p \ p' = {}" using partitionsE subsetCE sup_ge1 by blast qed lemma partitions_split2: assumes "partitions (P \ Q) A" shows "partitions Q (\Q)" using assms partitions_split1 sup_commute by metis lemma partitions_intersect_on_elements: assumes "partitions P (A \ C)" assumes "\X \ P. \x. x \ X \ C" shows "partitions ((\X. X \ C)  P) C" proof (rule partitionsI) fix p assume "p \ (\X. X \ C)  P" from this assms show "p \ {}" by auto next have "\P = A \ C" using assms by (auto elim: partitionsE) from this show "\((\X. X \ C)  P) = C" by auto next fix p p' assume "p \ (\X. X \ C)  P" "p' \ (\X. X \ C)  P" "p \ p'" from this assms(1) show "p \ p' = {}" by (blast elim: partitionsE) qed lemma partitions_insert_elements: assumes "A \ B = {}" assumes "partitions P B" assumes "f \ A \\<^sub>E P" shows "partitions ((\X. X \ {x \ A. f x = X})  P) (A \ B)" (is "partitions ?P _") proof (rule partitionsI) fix X assume "X \ ?P" from this \partitions P B\ show "X \ {}" by (auto elim: partitionsE) next show "\?P = A \ B" using \partitions P B\ \f \ A \\<^sub>E P\ by (auto elim: partitionsE) next fix X Y assume "X \ ?P" "Y \ ?P" "X \ Y" from \X \ ?P\ obtain X' where X': "X = X' \ {x \ A. f x = X'}" "X' \ P" by auto from \Y \ ?P\ obtain Y' where Y': "Y = Y' \ {x \ A. f x = Y'}" "Y' \ P" by auto from \X \ Y\ X' Y' have "X' \ Y'" by auto from this X' Y' have "X' \ Y' = {}" using \partitions P B\ by (auto elim!: partitionsE) from X' Y' have "X' \ B" "Y' \ B" using \partitions P B\ by (auto elim!: partitionsE) from this \X' \ Y' = {}\ X' Y' \X' \ Y'\ show "X \ Y = {}" using \A \ B = {}\ by auto qed lemma partitions_map: assumes "inj_on f A" assumes "partitions P A" shows "partitions (op  f  P) (f  A)" proof - { fix X Y assume "X \ P" "Y \ P" "f  X \ f  Y" moreover from assms have "\p\P. \p'\P. p \ p' \ p \ p' = {}" and "inj_on f (\P)" by (auto elim!: partitionsE) ultimately have "f  X \ f  Y = {}" unfolding inj_on_def by auto (metis IntI empty_iff rev_image_eqI)+ } from assms this show "partitions (op  f  P) (f  A)" by (auto intro!: partitionsI elim!: partitionsE) qed lemma set_of_partitions_map: assumes "inj_on f A" shows "op  (op  f)  {P. partitions P A} = {P. partitions P (f  A)}" proof (rule set_eqI') fix x assume "x \ op  (op  f)  {P. partitions P A}" from this \inj_on f A\ show "x \ {P. partitions P (f  A)}" by (auto intro: partitions_map) next fix P assume "P \ {P. partitions P (f  A)}" from this have "partitions P (f  A)" by auto from this have mem: "\X x. X \ P \ x \ X \ x \ f  A" by (auto elim!: partitionsE) have "op  (f \ the_inv_into A f)  P = op  f  op  (the_inv_into A f)  P" by (simp add: image_comp comp_image) moreover have "P = op  (f \ the_inv_into A f)  P" proof (rule set_eqI') fix X assume "X \ P" moreover from this mem have in_range: "\x\X. x \ f  A" by auto moreover have "X = (f \ the_inv_into A f)  X" proof (rule set_eqI') fix x assume "x \ X" show "x \ (f \ the_inv_into A f)  X" proof (rule image_eqI) from in_range \x \ X\ assms show "x = (f \ the_inv_into A f) x" by (auto simp add: f_the_inv_into_f[of f]) from \x \ X\ show "x \ X" by assumption qed next fix x assume "x \ (f \ the_inv_into A f)  X" from this obtain x' where x': "x' \ X \ x = f (the_inv_into A f x')" by auto from in_range x' have f: "f (the_inv_into A f x') \ X" by (subst f_the_inv_into_f[of f]) (auto intro: \inj_on f A$$ from x' \X \ P\ f show "x \ X" by auto qed ultimately show "X \ op  (f \ the_inv_into A f)  P" by auto next fix X assume "X \ op  (f \ the_inv_into A f)  P" moreover { fix Y assume "Y \ P" from this \inj_on f A\ mem have "\x\Y. f (the_inv_into A f x) = x" by (auto simp add: f_the_inv_into_f) from this have "(f \ the_inv_into A f)  Y = Y" by force } ultimately show "X \ P" by auto qed ultimately have P: "P = op  f  op  (the_inv_into A f)  P" by simp have A_eq: "A = the_inv_into A f  f  A" by (simp add: assms) from \inj_on f A\ have "inj_on (the_inv_into A f) (f  A)" using \partitions P (f  A)\ by (simp add: inj_on_the_inv_into) from this have "op  (the_inv_into A f)  P \ {P. partitions P A}" using \partitions P (f  A)\ by (subst A_eq, auto intro!: partitions_map) from P this show "P \ op  (op  f) ` {P. partitions P A}" by (rule image_eqI) qed end
 # -*- shell-script -*- # Get email when automated build fails. May be empty. # values: "email1 email2 .. emailn" NOTIFY="lukas.bulwahn@gmail.com" # Participate in frequent (nightly) build (only for small submissions) # values: "yes" "no" FREQUENT="yes"
 @article{spivey-2008, author = "Michael Z. Spivey", title = "A Generalized Recurrence for {Bell} Numbers", journal = "Journal of Integer Sequences", year = "2008", volume = "11", issue = "2", note = "Electronic copy available at https://cs.uwaterloo.ca/journals/JIS/VOL11/Spivey/spivey25.pdf" } @inproceedings{bell-numbers, title = "A000110: Bell or exponential numbers: number of ways to partition a set of n labeled elements.", author = "N. J. A. Sloane", booktitle = "The On-Line Encyclopedia of Integer Sequences", editors = "N. J. A. Sloane", note = "https://oeis.org/A000110" }
 \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \, \, \, \, %\ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \begin{document} \title{Spivey's Generalized Recurrence for Bell Numbers} \author{Lukas Bulwahn} \maketitle \begin{abstract} This entry defines the Bell numbers~\cite{bell-numbers} as the cardinality of set partitions for a carrier set of given size, and derives Spivey's generalized recurrence relation for Bell numbers~\cite{spivey-2008} following his elegant and intuitive combinatorial proof. As the set construction for the combinatorial proof requires construction of three intermediate structures, the main difficulty of the formalization is handling the overall combinatorial argument in a structured way. The introduced proof structure allows us to compose the combinatorial argument from its subparts, and supports to keep track how the detailed proof steps are related to the overall argument. To obtain this structure, this entry uses set monad notation for the set construction's definition, introduces suitable predicates and rules, and follows a repeating structure in its Isar proof. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} \nocite{*} \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End:
 ... ... @@ -14,6 +14,7 @@ ArrowImpossibilityGS AutoFocus-Stream Automatic_Refinement BDD Bell_Numbers_Spivey BinarySearchTree Binomial-Heaps Binomial-Queues ... ...
 Archive of Formal Proofs

Spivey's Generalized Recurrence for Bell Numbers

Title: Spivey's Generalized Recurrence for Bell Numbers
Author: Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com)
Submission date: 2016-05-04
Abstract: This entry defines the Bell numbers as the cardinality of set partitions for a carrier set of given size, and derives Spivey's generalized recurrence relation for Bell numbers following his elegant and intuitive combinatorial proof.

As the set construction for the combinatorial proof requires construction of three intermediate structures, the main difficulty of the formalization is handling the overall combinatorial argument in a structured way. The introduced proof structure allows us to compose the combinatorial argument from its subparts, and supports to keep track how the detailed proof steps are related to the overall argument. To obtain this structure, this entry uses set monad notation for the set construction's definition, introduces suitable predicates and rules, and follows a repeating structure in its Isar proof.

BibTeX:
@article{Bell_Numbers_Spivey-AFP,
author  = {Lukas Bulwahn},
title   = {Spivey's Generalized Recurrence for Bell Numbers},
journal = {Archive of Formal Proofs},
month   = may,
year    = 2016,
note    = {\url{http://isa-afp.org/entries/Bell_Numbers_Spivey.shtml},
Formal proof development},
ISSN    = {2150-914x},
}