(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Christoph Lange * Marco B. Caminati Dually licenced under * Creative Commons Attribution (CC-BY) 3.0 * ISC License (1-clause BSD License) See LICENSE file for details (Rationale for this dual licence: http://arxiv.org/abs/1107.3212) *) header {* Partitions of sets *} theory Partitions imports Main SetUtils begin text {* We define the set of all partitions of a set (@{term all_partitions}) in textbook style, as well as a function @{term all_partitions_list} to algorithmically compute this set (then represented as a list). This function is suitable for code generation. We prove their equivalence to ensure that the generated code correctly implements the original textbook-style definition. For further background on the overall approach, see Caminati, Kerber, Lange, Rowat: \href{http://arxiv.org/abs/1308.1779}{Proving soundness of combinatorial Vickrey auctions and generating verified executable code}, 2013. The algorithmic computation of all partitions of a set works as in the following example: \begin{itemize} \item Set: $\{\a}$\\ Partitions: $\{\{a\}\}$ \item Set: $\{a,b\}$ Partitions: $\{\{a\}, \{b\}\}, \{\{a, b\}\}$ \item Set: $\{a,b,c\}$ Partitions: $\{\{a\}, \{b\}, \{c\}\}, \{\{a,b\}, \{c\}\}, \{\{a,c\}, \{b\}\}, \{\{a\}, \{c,b\}\}, \{\{a,b,c\}\}$ \end{itemize} BTW, the number of partitions of a set (same as the number of equivalence relations on the set) is known as \href{http://en.wikipedia.org/wiki/Bell_number}{Bell number}. *} text {* @{term P} is a partition of some set. *} definition is_partition where "is_partition P = (\ X\P . \ Y\ P . (X \ Y \ {} \ X = Y))" (* alternative, less concise formalisation: "is_partition P = (\ ec1 \ P . ec1 \ {} \ (\ ec2 \ P - {ec1}. ec1 \ ec2 = {}))" *) text {* A subset of a partition is also a partition (but, note: only of a subset of the original set) *} lemma subset_is_partition: assumes subset: "P \ Q" and partition: "is_partition Q" shows "is_partition P" proof - { fix X Y assume "X \ P \ Y \ P" then have "X \ Q \ Y \ Q" using subset by fast then have "X \ Y \ {} \ X = Y" using partition unfolding is_partition_def by force } then show ?thesis unfolding is_partition_def by force qed (* This is not used at the moment, but it is interesting, as the proof was very hard to find for Sledgehammer. *) text {* The set that results from removing one element from an equivalence class of a partition is not otherwise a member of the partition. *} lemma remove_from_eq_class_preserves_disjoint: fixes elem::'a and X::"'a set" and P::"'a set set" assumes partition: "is_partition P" and eq_class: "X \ P" and elem: "elem \ X" shows "X - {elem} \ P" using assms using is_partition_def by (smt Diff_iff Int_Diff Int_absorb Int_commute insertCI) text {* Inserting into a partition @{term P} a set @{term X}, which is disjoint with the set partitioned by @{term P}, yields another partition. *} lemma partition_extension1: fixes P::"'a set set" and X::"'a set" assumes partition: "is_partition P" and disjoint: "X \ \ P = {}" and non_empty: "X \ {}" shows "is_partition (insert X P)" proof - { fix Y::"'a set" and Z::"'a set" assume Y_Z_in_ext_P: "Y \ insert X P \ Z \ insert X P" have "Y \ Z \ {} \ Y = Z" proof assume "Y \ Z \ {}" then show "Y = Z" using Y_Z_in_ext_P partition disjoint unfolding is_partition_def by fast next assume "Y = Z" then show "Y \ Z \ {}" using Y_Z_in_ext_P partition non_empty unfolding is_partition_def by auto qed } then show ?thesis unfolding is_partition_def by force qed text {* An equivalence class of a partition has no intersection with any of the other equivalence classes. *} lemma disj_eq_classes: fixes P::"'a set set" and X::"'a set" assumes "is_partition P" and "X \ P" shows "X \ \ (P - {X}) = {}" proof - { fix x::'a assume x_in_two_eq_classes: "x \ X \ \ (P - {X})" then obtain Y where other_eq_class: "Y \ P - {X} \ x \ Y" by blast have "x \ X \ Y \ Y \ P" using x_in_two_eq_classes other_eq_class by force then have "X = Y" using assms is_partition_def by fast then have "x \ {}" using other_eq_class by fast } then show ?thesis by blast qed text {* In a partition there is no empty equivalence class. *} lemma no_empty_eq_class: assumes "is_partition p" shows "{} \ p" using assms is_partition_def by fast text {* @{term P} is a partition of the set @{term A}. *} definition is_partition_of where "is_partition_of P A = (\ P = A \ is_partition P)" text {* A non-empty set is a partition of itself. *} lemma set_partitions_itself: assumes "A \ {}" shows "is_partition_of {A} A" unfolding is_partition_of_def is_partition_def (* CL: the following takes 48 ms on my machine: by (metis Sup_empty Sup_insert assms inf_idem singletonE sup_bot_right) *) proof show "\ {A} = A" by simp { fix X Y assume "X \ {A}" then have "X = A" by (rule singletonD) assume "Y \ {A}" then have "Y = A" by (rule singletonD) from X = A Y = A have "X \ Y \ {} \ X = Y" using assms by simp } then show "\ X \ {A} . \ Y \ {A} . (X \ Y \ {} \ X = Y)" by force qed text {* The empty set is a partition of the empty set. *} lemma emptyset_part_emptyset1: shows "is_partition_of {} {}" unfolding is_partition_of_def is_partition_def by fast text {* Any partition of the empty set is empty. *} lemma emptyset_part_emptyset2: assumes "is_partition_of P {}" shows "P = {}" using assms is_partition_def is_partition_of_def by fast text {* classical set-theoretical definition of all partitions of a set @{term A}'' *} definition all_partitions where "all_partitions A = {P . is_partition_of P A}" text {* Any non-empty set has at least one partition. *} lemma non_empty_set_has_partitions: assumes "A \ {}" shows "all_partitions A \ {}" (* CL: the following takes 1.32 s on my machine, and it does already use my lemma set_partitions_itself: *) (* unfolding all_partitions_def is_partition_of_def is_partition_def by (smt Int_absorb Int_commute assms empty_def is_partition_of_def mem_Collect_eq set_partitions_itself singleton_conv2) *) (* CL: Without set_partitions_itself, it doesn't work within reasonable time: unfolding all_partitions_def is_partition_of_def is_partition_def sledgehammer (del: set_partitions_itself) *) proof assume "all_partitions A = {}" then have "\ P . \is_partition_of P A" using all_partitions_def by blast moreover have "is_partition_of {A} A" using assms by (rule set_partitions_itself) ultimately show False by simp qed text {* The set of all partitions of the empty set only contains the empty set. We need this to prove the base case of @{term all_partitions_paper_equiv_alg}. *} lemma emptyset_part_emptyset3: shows "all_partitions {} = {{}}" unfolding all_partitions_def using emptyset_part_emptyset1 emptyset_part_emptyset2 by fast (* MC: A further, proof-friendlier way of computing partitions is introduced: everything's a set, except the very initial input, which is a list (of elements) because I don't know how to do recursive definitions on finite sets. CL@MC: There is a predicate Finite_Set.finite, which is defined inductively (search for "inductive finite" in Finite_Set.thy, but it is not defined as an algebraic _datatype_ and therefore doesn't work with recursive _functions_. Then equivalence with all_partitions is inductively shown *) (* MC: update: now I probably would know how to utterly eliminate lists from this. CL@MC: Is this comment still up to date? *) text {* inserts an element into a specified set inside the given set of sets *} definition insert_into_member :: "'a \ 'a set set \ 'a set \ 'a set set" where "insert_into_member new_el Sets S = insert (S \ {new_el}) (Sets - {S})" text {* Using @{const insert_into_member} to insert a fresh element, which is not a member of the set @{term S} being partitioned, into an equivalence class of a partition yields another partition (of -- we don't prove this here -- the set @{term "S \ {new_el}"}). *} lemma partition_extension2: fixes new_el::'a and P::"'a set set" and X::"'a set" assumes partition: "is_partition P" and eq_class: "X \ P" and new: "new_el \ \ P" shows "is_partition (insert_into_member new_el P X)" proof - let ?Y = "insert new_el X" have rest_is_partition: "is_partition (P - {X})" using partition subset_is_partition by blast have *: "X \ \ (P - {X}) = {}" using partition eq_class by (rule disj_eq_classes) from * have non_empty: "?Y \ {}" by blast from * have disjoint: "?Y \ \ (P - {X}) = {}" using new by force have "is_partition (insert ?Y (P - {X}))" using rest_is_partition disjoint non_empty by (rule partition_extension1) then show ?thesis unfolding insert_into_member_def by simp qed text {* inserts an element into a specified set inside the given list of sets -- the list variant of @{const insert_into_member} The rationale for this variant and for everything that depends on it is: While it is possible to computationally enumerate all partitions of a set'' as an @{typ "'a set set set"}, we need a list representation to apply further computational functions to partitions. Because of the way we construct partitions (using functions such as @{term all_coarser_partitions_with} below) it is not sufficient to simply use @{typ "'a set set list"}, but we need @{typ "'a set list list"}. This is because it is hard to impossible to convert a set to a list, whereas it is easy to convert a @{type list} to a @{type set}. *} definition insert_into_member_list :: "'a \ 'a set list \ 'a set \ 'a set list" where "insert_into_member_list new_el Sets S = (S \ {new_el}) # (remove1 S Sets)" text {* @{const insert_into_member_list} and @{const insert_into_member} are equivalent (as in returning the same set). *} lemma insert_into_member_list_alt: fixes new_el::'a and Sets::"'a set list" and S::"'a set" assumes "distinct Sets" shows "set (insert_into_member_list new_el Sets S) = insert_into_member new_el (set Sets) S" unfolding insert_into_member_list_def insert_into_member_def using assms by simp text {* an alternative characterisation of the set partitioned by a partition obtained by inserting an element into an equivalence class of a given partition (if @{term P} \emph{is} a partition) *} lemma insert_into_member_partition1: fixes elem::'a and P::"'a set set" and eq_class::"'a set" (* no need to assume "eq_class \ P" *) shows "\ insert_into_member elem P eq_class = \ insert (eq_class \ {elem}) (P - {eq_class})" unfolding insert_into_member_def by fast (* TODO CL: document for the general case of a non-partition argument as per https://github.com/formare/auctions/issues/20 *) text {* Assuming that @{term P} is a partition of a set @{term S}, and @{term "new_el \ S"}, this function yields all possible partitions of @{term "S \ {new_el}"} that are coarser than @{term P} (i.e.\ not splitting equivalence classes that already exist in @{term P}). These comprise one partition with an equivalence class @{term "{new_el}"} and all other equivalence classes unchanged, as well as all partitions obtained by inserting @{term new_el} into one equivalence class of @{term P} at a time. *} definition coarser_partitions_with ::"'a \ 'a set set \ 'a set set set" where "coarser_partitions_with new_el P = insert (* Let P be a partition of a set Set, and suppose new_el \ Set, i.e. {new_el} \ P, then the following constructs a partition of 'Set \ {new_el}' obtained by inserting a new equivalence class {new_el} and leaving all previous equivalence classes unchanged. *) (insert {new_el} P) (* Let P be a partition of a set Set, and suppose new_el \ Set, then the following constructs the set of those partitions of 'Set \ {new_el}' obtained by inserting new_el into one equivalence class of P at a time. *) ((insert_into_member new_el P)  P)" (* TODO CL: document for the general case of a non-partition argument as per https://github.com/formare/auctions/issues/20 *) text {* the list variant of @{const coarser_partitions_with} *} definition coarser_partitions_with_list ::"'a \ 'a set list \ 'a set list list" where "coarser_partitions_with_list new_el P = (* Let P be a partition of a set Set, and suppose new_el \ Set, i.e. {new_el} \ set P, then the following constructs a partition of 'Set \ {new_el}' obtained by inserting a new equivalence class {new_el} and leaving all previous equivalence classes unchanged. *) ({new_el} # P) # (* Let P be a partition of a set Set, and suppose new_el \ Set, then the following constructs the set of those partitions of 'Set \ {new_el}' obtained by inserting new_el into one equivalence class of P at a time. *) (map ((insert_into_member_list new_el P)) P)" text {* @{const coarser_partitions_with_list} and @{const coarser_partitions_with} are equivalent. *} lemma coarser_partitions_with_list_alt: assumes "distinct P" shows "set (map set (coarser_partitions_with_list new_el P)) = coarser_partitions_with new_el (set P)" proof - have "set (map set (coarser_partitions_with_list new_el P)) = set (map set (({new_el} # P) # (map ((insert_into_member_list new_el P)) P)))" unfolding coarser_partitions_with_list_def .. also have "\ = insert (insert {new_el} (set P)) ((set \ (insert_into_member_list new_el P))  set P)" by simp also have "\ = insert (insert {new_el} (set P)) ((insert_into_member new_el (set P))  set P)" using assms insert_into_member_list_alt by (metis comp_apply) finally show ?thesis unfolding coarser_partitions_with_def . qed text {* Any member of the set of coarser partitions of a given partition, obtained by inserting a given fresh element into each of its equivalence classes, actually is a partition. *} lemma partition_extension3: fixes elem::'a and P::"'a set set" and Q::"'a set set" assumes P_partition: "is_partition P" and new_elem: "elem \ \ P" and Q_coarser: "Q \ coarser_partitions_with elem P" shows "is_partition Q" proof - let ?q = "insert {elem} P" have Q_coarser_unfolded: "Q \ insert ?q (insert_into_member elem P  P)" using Q_coarser unfolding coarser_partitions_with_def by fast show ?thesis proof (cases "Q = ?q") case True then show ?thesis using P_partition new_elem partition_extension1 by fastforce next case False then have "Q \ (insert_into_member elem P)  P" using Q_coarser_unfolded by fastforce then show ?thesis using partition_extension2 P_partition new_elem by fast qed qed text {* Let @{term P} be a partition of a set @{term S}, and @{term elem} an element (which may or may not be in @{term S} already). Then, any member of @{term "coarser_partitions_with elem P"} is a set of sets whose union is @{term "S \ {elem}"}, i.e.\ it satisfies a necessary criterion for being a partition of @{term "S \ {elem}"}. *} lemma coarser_partitions_covers: fixes elem::'a and P::"'a set set" and Q::"'a set set" assumes "Q \ coarser_partitions_with elem P" shows "\ Q = insert elem (\ P)" proof - let ?S = "\ P" have Q_cases: "Q \ (insert_into_member elem P)  P \ Q = insert {elem} P" using assms unfolding coarser_partitions_with_def by fast { fix eq_class assume eq_class_in_P: "eq_class \ P" have "\ insert (eq_class \ {elem}) (P - {eq_class}) = ?S \ (eq_class \ {elem})" using insert_into_member_partition1 by (metis Sup_insert Un_commute Un_empty_right Un_insert_right insert_Diff_single) with eq_class_in_P have "\ insert (eq_class \ {elem}) (P - {eq_class}) = ?S \ {elem}" by blast then have "\ insert_into_member elem P eq_class = ?S \ {elem}" using insert_into_member_partition1 by (rule subst) } then show ?thesis using Q_cases by blast qed text {* Removes the element @{term elem} from every set in @{term P}, and removes from @{term P} any remaining empty sets. This function is intended to be applied to partitions, i.e. @{term elem} occurs in at most one set. @{term "partition_without e"} reverses @{term "coarser_partitions_with e"}. @{const coarser_partitions_with} is one-to-many, while this is one-to-one, so we can think of a tree relation, where coarser partitions of a set @{term "S \ {elem}"} are child nodes of one partition of @{term S}. *} definition partition_without :: "'a \ 'a set set \ 'a set set" where "partition_without elem P = (\X . X - {elem})  P - {{}}" (* Set comprehension notation { x - {elem} | x . x \ P } would look nicer but is harder to do proofs about *) (* We don't need to define partition_without_list. *) text {* alternative characterisation of the set partitioned by the partition obtained by removing an element from a given partition using @{const partition_without} *} lemma partition_without_covers: fixes elem::'a and P::"'a set set" shows "\ partition_without elem P = \ P - {elem}" proof - have "\ partition_without elem P = \ ((\x . x - {elem})  P - {{}})" unfolding partition_without_def by fast also have "\ = \ P - {elem}" by blast finally show ?thesis . qed text {* Any equivalence class of the partition obtained by removing an element @{term elem} from an original partition @{term P} using @{const partition_without} equals some equivalence class of @{term P}, reduced by @{term elem}. *} lemma super_eq_class: assumes "X \ partition_without elem P" obtains Z where "Z \ P" and "X = Z - {elem}" proof - from assms have "X \ (\X . X - {elem})  P - {{}}" unfolding partition_without_def . then obtain Z where Z_in_P: "Z \ P" and Z_sup: "X = Z - {elem}" by (metis (lifting) Diff_iff image_iff) then show ?thesis .. qed text {* The set of sets obtained by removing an element from a partition actually is another partition. *} lemma partition_without_is_partition: fixes elem::'a and P::"'a set set" assumes "is_partition P" shows "is_partition (partition_without elem P)" (is "is_partition ?Q") proof - have "\ X1 \ ?Q. \ X2 \ ?Q. X1 \ X2 \ {} \ X1 = X2" proof fix X1 assume X1_in_Q: "X1 \ ?Q" then obtain Z1 where Z1_in_P: "Z1 \ P" and Z1_sup: "X1 = Z1 - {elem}" by (rule super_eq_class) have X1_non_empty: "X1 \ {}" using X1_in_Q partition_without_def by fast show "\ X2 \ ?Q. X1 \ X2 \ {} \ X1 = X2" proof fix X2 assume "X2 \ ?Q" then obtain Z2 where Z2_in_P: "Z2 \ P" and Z2_sup: "X2 = Z2 - {elem}" by (rule super_eq_class) have "X1 \ X2 \ {} \ X1 = X2" proof assume "X1 \ X2 \ {}" then have "Z1 \ Z2 \ {}" using Z1_sup Z2_sup by fast then have "Z1 = Z2" using Z1_in_P Z2_in_P assms unfolding is_partition_def by fast then show "X1 = X2" using Z1_sup Z2_sup by fast qed moreover have "X1 = X2 \ X1 \ X2 \ {}" using X1_non_empty by auto ultimately show "(X1 \ X2 \ {}) \ X1 = X2" by blast qed qed then show ?thesis unfolding is_partition_def . qed text {* @{term "coarser_partitions_with elem"} is the inverse'' of @{term "partition_without elem"}. *} lemma coarser_partitions_inv_without: fixes elem::'a and P::"'a set set" assumes partition: "is_partition P" and elem: "elem \ \ P" shows "P \ coarser_partitions_with elem (partition_without elem P)" (is "P \ coarser_partitions_with elem ?Q") proof - let ?remove_elem = "\X . X - {elem}" (* function that removes elem out of a set *) obtain Y (* the equivalence class of elem *) where elem_eq_class: "elem \ Y" and elem_eq_class': "Y \ P" using elem .. let ?elem_neq_classes = "P - {Y}" (* those equivalence classes in which elem is not *) have P_wrt_elem: "P = ?elem_neq_classes \ {Y}" using elem_eq_class' by blast let ?elem_eq = "Y - {elem}" (* other elements equivalent to elem *) have Y_elem_eq: "?remove_elem  {Y} = {?elem_eq}" by fast (* those equivalence classes, in which elem is not, form a partition *) have elem_neq_classes_part: "is_partition ?elem_neq_classes" using subset_is_partition partition by blast have elem_eq_wrt_P: "?elem_eq \ ?remove_elem  P" using elem_eq_class' by blast { (* consider an equivalence class W, in which elem is not *) fix W assume W_eq_class: "W \ ?elem_neq_classes" then have "elem \ W" using elem_eq_class elem_eq_class' partition is_partition_def by fast then have "?remove_elem W = W" by simp } then have elem_neq_classes_id: "?remove_elem  ?elem_neq_classes = ?elem_neq_classes" by fastforce have Q_unfolded: "?Q = ?remove_elem  P - {{}}" unfolding partition_without_def using image_Collect_mem by blast also have "\ = ?remove_elem  (?elem_neq_classes \ {Y}) - {{}}" using P_wrt_elem by presburger also have "\ = ?elem_neq_classes \ {?elem_eq} - {{}}" using elem_eq_class' partition_without_def Y_elem_eq elem_neq_classes_id by (smt image_Un) finally have Q_wrt_elem: "?Q = ?elem_neq_classes \ {?elem_eq} - {{}}" . have "?elem_eq = {} \ ?elem_eq \ P" using elem_eq_class elem_eq_class' partition unfolding is_partition_def by (smt Diff_Int_distrib2 Diff_iff Int_absorb empty_Diff insert_iff) then have "?elem_eq \ P" using partition no_empty_eq_class by metis then have elem_neq_classes: "?elem_neq_classes - {?elem_eq} = ?elem_neq_classes" by fastforce show ?thesis proof cases assume "?elem_eq \ ?Q" (* the equivalence class of elem is not a member of ?Q = partition_without elem P *) then have "?elem_eq \ {{}}" using elem_eq_wrt_P Q_unfolded by (metis DiffI) then have Y_singleton: "Y = {elem}" using elem_eq_class by fast then have "?Q = ?elem_neq_classes - {{}}" using Q_wrt_elem by force then have "?Q = ?elem_neq_classes" using no_empty_eq_class elem_neq_classes_part by blast then have "insert {elem} ?Q = P" using Y_singleton elem_eq_class' by fast then show ?thesis unfolding coarser_partitions_with_def by auto next assume True: "\ ?elem_eq \ ?Q" hence Y': "?elem_neq_classes \ {?elem_eq} - {{}} = ?elem_neq_classes \ {?elem_eq}" using no_empty_eq_class partition partition_without_is_partition by force have "insert_into_member elem ({?elem_eq} \ ?elem_neq_classes) ?elem_eq = insert (?elem_eq \ {elem}) (({?elem_eq} \ ?elem_neq_classes) - {?elem_eq})" unfolding insert_into_member_def .. also have "\ = ({} \ ?elem_neq_classes) \ {?elem_eq \ {elem}}" using elem_neq_classes by force also have "\ = ?elem_neq_classes \ {Y}" using elem_eq_class by blast finally have "insert_into_member elem ({?elem_eq} \ ?elem_neq_classes) ?elem_eq = ?elem_neq_classes \ {Y}" . then have "?elem_neq_classes \ {Y} = insert_into_member elem ?Q ?elem_eq" using Q_wrt_elem Y' partition_without_def by force then have "{Y} \ ?elem_neq_classes \ insert_into_member elem ?Q  ?Q" using True by blast then have "{Y} \ ?elem_neq_classes \ coarser_partitions_with elem ?Q" unfolding coarser_partitions_with_def by simp then show ?thesis using P_wrt_elem by simp qed qed text {* Given a set @{term Ps} of partitions, this is intended to compute the set of all coarser partitions (given an extension element) of all partitions in @{term Ps}. *} definition all_coarser_partitions_with :: " 'a \ 'a set set set \ 'a set set set" where "all_coarser_partitions_with elem Ps = \ (coarser_partitions_with elem  Ps)" text {* the list variant of @{const all_coarser_partitions_with} *} definition all_coarser_partitions_with_list :: " 'a \ 'a set list list \ 'a set list list" where "all_coarser_partitions_with_list elem Ps = concat (map (coarser_partitions_with_list elem) Ps)" text {* @{const all_coarser_partitions_with_list} and @{const all_coarser_partitions_with} are equivalent. *} lemma all_coarser_partitions_with_list_alt: fixes elem::'a and Ps::"'a set list list" assumes distinct: "\ P \ set Ps . distinct P" shows "set (map set (all_coarser_partitions_with_list elem Ps)) = all_coarser_partitions_with elem (set (map set Ps))" (is "?list_expr = ?set_expr") proof - have "?list_expr = set (map set (concat (map (coarser_partitions_with_list elem) Ps)))" unfolding all_coarser_partitions_with_list_def .. also have "\ = set  (\ x \ (coarser_partitions_with_list elem)  (set Ps) . set x)" by simp (* This and other intermediate results may not be easy to understand. I obtained them by conflating multiple “by ” steps into one. *) also have "\ = set  (\ x \ { coarser_partitions_with_list elem P | P . P \ set Ps } . set x)" by (simp add: image_Collect_mem) also have "\ = \ { set (map set (coarser_partitions_with_list elem P)) | P . P \ set Ps }" by auto also have "\ = \ { coarser_partitions_with elem (set P) | P . P \ set Ps }" using distinct coarser_partitions_with_list_alt by fast also have "\ = \ (coarser_partitions_with elem  (set  (set Ps)))" by (simp add: image_Collect_mem) also have "\ = \ (coarser_partitions_with elem  (set (map set Ps)))" by simp also have "\ = ?set_expr" unfolding all_coarser_partitions_with_def .. finally show ?thesis . qed text {* all partitions of a set (given as list) *} fun all_partitions_set :: "'a list \ 'a set set set" where "all_partitions_set [] = {{}}" | "all_partitions_set (e # X) = all_coarser_partitions_with e (all_partitions_set X)" text {* all partitions of a set (given as list) *} fun all_partitions_list :: "'a list \ 'a set list list" where "all_partitions_list [] = [[]]" | "all_partitions_list (e # X) = all_coarser_partitions_with_list e (all_partitions_list X)" text {* A list of partitions coarser than a given partition in list representation (constructed with @{const coarser_partitions_with} is distinct under certain conditions. *} lemma coarser_partitions_with_list_distinct: fixes ps assumes ps_coarser: "ps \ set (coarser_partitions_with_list x Q)" and distinct: "distinct Q" and partition: "is_partition (set Q)" and new: "{x} \ set Q" shows "distinct ps" proof - have "set (coarser_partitions_with_list x Q) = insert ({x} # Q) (set (map (insert_into_member_list x Q) Q))" unfolding coarser_partitions_with_list_def by simp with ps_coarser have "ps \ insert ({x} # Q) (set (map ((insert_into_member_list x Q)) Q))" by blast then show ?thesis proof assume "ps = {x} # Q" with distinct and new show ?thesis by simp next assume "ps \ set (map (insert_into_member_list x Q) Q)" then obtain X where X_in_Q: "X \ set Q" and ps_insert: "ps = insert_into_member_list x Q X" by auto from ps_insert have "ps = (X \ {x}) # (remove1 X Q)" unfolding insert_into_member_list_def . also have "\ = (X \ {x}) # (removeAll X Q)" using distinct by (metis distinct_remove1_removeAll) finally have ps_list: "ps = (X \ {x}) # (removeAll X Q)" . have distinct_tl: "X \ {x} \ set (removeAll X Q)" proof from partition have partition': "\x\set Q. \y\set Q. (x \ y \ {}) = (x = y)" unfolding is_partition_def . assume "X \ {x} \ set (removeAll X Q)" with X_in_Q partition show False by (metis partition' inf_sup_absorb member_remove no_empty_eq_class remove_code(1)) qed with ps_list distinct show ?thesis by (metis (full_types) distinct.simps(2) distinct_removeAll) qed qed text {* The paper-like definition @{const all_partitions} and the algorithmic definition @{const all_partitions_list} are equivalent. *} lemma all_partitions_paper_equiv_alg': fixes xs::"'a list" shows "distinct xs \ ((set (map set (all_partitions_list xs)) = all_partitions (set xs)) \ (\ ps \ set (all_partitions_list xs) . distinct ps))" proof (induct xs) case Nil have "set (map set (all_partitions_list [])) = all_partitions (set [])" unfolding List.set.simps(1) emptyset_part_emptyset3 by simp (* Sledgehammer no longer seems to find this, maybe after we have added the "distinct" part to the theorem statement. *) moreover have "\ ps \ set (all_partitions_list []) . distinct ps" by fastforce ultimately show ?case .. next case (Cons x xs) from Cons.prems Cons.hyps have hyp_equiv: "set (map set (all_partitions_list xs)) = all_partitions (set xs)" by simp from Cons.prems Cons.hyps have hyp_distinct: "\ ps \ set (all_partitions_list xs) . distinct ps" by simp have distinct_xs: "distinct xs" using Cons.prems by simp have x_notin_xs: "x \ set xs" using Cons.prems by simp have "set (map set (all_partitions_list (x # xs))) = all_partitions (set (x # xs))" proof (rule equalitySubsetI) -- {* case set \ list *} fix P::"'a set set" (* a partition *) let ?P_without_x = "partition_without x P" have P_partitions_exc_x: "\ ?P_without_x = \ P - {x}" using partition_without_covers . assume "P \ all_partitions (set (x # xs))" then have is_partition_of: "is_partition_of P (set (x # xs))" unfolding all_partitions_def .. then have is_partition: "is_partition P" unfolding is_partition_of_def by simp from is_partition_of have P_covers: "\ P = set (x # xs)" unfolding is_partition_of_def by simp have "is_partition_of ?P_without_x (set xs)" unfolding is_partition_of_def using is_partition partition_without_is_partition partition_without_covers P_covers x_notin_xs by (metis Diff_insert_absorb List.set.simps(2)) with hyp_equiv have p_list: "?P_without_x \ set (map set (all_partitions_list xs))" unfolding all_partitions_def by fast have "P \ coarser_partitions_with x ?P_without_x" using coarser_partitions_inv_without is_partition P_covers by (metis List.set.simps(2) insertI1) then have "P \ \ (coarser_partitions_with x  set (map set (all_partitions_list xs)))" using p_list by blast then have "P \ all_coarser_partitions_with x (set (map set (all_partitions_list xs)))" unfolding all_coarser_partitions_with_def by fast then show "P \ set (map set (all_partitions_list (x # xs)))" using all_coarser_partitions_with_list_alt hyp_distinct by (metis all_partitions_list.simps(2)) next -- {* case list \ set *} fix P::"'a set set" (* a partition *) assume P: "P \ set (map set (all_partitions_list (x # xs)))" have "set (map set (all_partitions_list (x # xs))) = set (map set (all_coarser_partitions_with_list x (all_partitions_list xs)))" by simp also have "\ = all_coarser_partitions_with x (set (map set (all_partitions_list xs)))" using distinct_xs hyp_distinct all_coarser_partitions_with_list_alt by fast also have "\ = all_coarser_partitions_with x (all_partitions (set xs))" using distinct_xs hyp_equiv by auto finally have P_set: "set (map set (all_partitions_list (x # xs))) = all_coarser_partitions_with x (all_partitions (set xs))" . with P have "P \ all_coarser_partitions_with x (all_partitions (set xs))" by fast then have "P \ \ (coarser_partitions_with x  (all_partitions (set xs)))" unfolding all_coarser_partitions_with_def . then obtain Y where P_in_Y: "P \ Y" and Y_coarser: "Y \ coarser_partitions_with x  (all_partitions (set xs))" .. from Y_coarser obtain Q where Q_part_xs: "Q \ all_partitions (set xs)" and Y_coarser': "Y = coarser_partitions_with x Q" .. from P_in_Y Y_coarser' have P_wrt_Q: "P \ coarser_partitions_with x Q" by fast then have "Q \ all_partitions (set xs)" using Q_part_xs by simp then have "is_partition_of Q (set xs)" unfolding all_partitions_def .. then have "is_partition Q" and Q_covers: "\ Q = set xs" unfolding is_partition_of_def by simp_all then have P_partition: "is_partition P" using partition_extension3 P_wrt_Q x_notin_xs by fast have "\ P = set xs \ {x}" using Q_covers P_in_Y Y_coarser' coarser_partitions_covers by fast then have "\ P = set (x # xs)" using x_notin_xs P_wrt_Q Q_covers by (metis List.set.simps(2) insert_is_Un sup_commute) then have "is_partition_of P (set (x # xs))" using P_partition unfolding is_partition_of_def by blast then show "P \ all_partitions (set (x # xs))" unfolding all_partitions_def .. qed moreover have "\ ps \ set (all_partitions_list (x # xs)) . distinct ps" proof fix ps::"'a set list" assume ps_part: "ps \ set (all_partitions_list (x # xs))" have "set (all_partitions_list (x # xs)) = set (all_coarser_partitions_with_list x (all_partitions_list xs))" by simp also have "\ = set (concat (map (coarser_partitions_with_list x) (all_partitions_list xs)))" unfolding all_coarser_partitions_with_list_def .. also have "\ = \ ((set \ (coarser_partitions_with_list x))  (set (all_partitions_list xs)))" by simp finally have all_parts_unfolded: "set (all_partitions_list (x # xs)) = \ ((set \ (coarser_partitions_with_list x)) ` (set (all_partitions_list xs)))" . (* \ = \ { set (coarser_partitions_with_list x ps) | ps . ps \ set (all_partitions_list xs) } (more readable, but less useful in proofs) *) with ps_part obtain qs where qs: "qs \ set (all_partitions_list xs)" and ps_coarser: "ps \ set (coarser_partitions_with_list x qs)" by (smt UnionE comp_def imageE) from qs have "set qs \ set (map set (all_partitions_list (xs)))" by simp with distinct_xs hyp_equiv have qs_hyp: "set qs \ all_partitions (set xs)" by fast then have qs_part: "is_partition (set qs)" using all_partitions_def is_partition_of_def by (metis mem_Collect_eq) then have distinct_qs: "distinct qs" using qs distinct_xs hyp_distinct by fast from Cons.prems have "x \ set xs" by simp then have new: "{x} \ set qs" using qs_hyp unfolding all_partitions_def is_partition_of_def by (metis (lifting, mono_tags) UnionI insertI1 mem_Collect_eq) from ps_coarser distinct_qs qs_part new show "distinct ps" by (rule coarser_partitions_with_list_distinct) qed ultimately show ?case .. qed text {* The paper-like definition @{const all_partitions} and the algorithmic definition @{const all_partitions_list} are equivalent. This is a frontend theorem derived from @{thm all_partitions_paper_equiv_alg'}; it does not make the auxiliary statement about partitions being distinct lists. *} theorem all_partitions_paper_equiv_alg: fixes xs::"'a list" shows "distinct xs \ set (map set (all_partitions_list xs)) = all_partitions (set xs)" using all_partitions_paper_equiv_alg' by blast text {* The function that we will be using in practice to compute all partitions of a set, a set-oriented frontend to @{const all_partitions_list} *} definition all_partitions_alg :: "'a\linorder set \ 'a set list list" where "all_partitions_alg X = all_partitions_list (sorted_list_of_set X)" (* TODO CL: maybe delete as per https://github.com/formare/auctions/issues/21 *) corollary [code_unfold]: fixes X assumes "finite X" shows "all_partitions X = set (map set (all_partitions_alg X))" unfolding all_partitions_alg_def using assms by (metis all_partitions_paper_equiv_alg' sorted_list_of_set) (* all_partitions internally works with a list representing a set (this allows us to use the recursive function all_partitions_list). For a general list we can only guarantee compliance once we establish distinctness. *) end