(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Marco B. Caminati http://caminati.co.nr * Manfred Kerber <mnfrd.krbr@gmail.com> * Christoph Lange <math.semantic.web@gmail.com> * Colin Rowat <c.rowat@bham.ac.uk> 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) *) section ‹Partitions of sets› theory Partitions imports SetUtils begin text ‹ We define the set of all partitions of a set (@{term all_partitions}) in textbook style, as well as a computable function @{term all_partitions_list} to algorithmically compute this set (then represented as a list). This function is suitable for code generation. We prove the equivalence of the two definition in order 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. › text ‹@{term P} is a family of non-overlapping sets.› definition is_non_overlapping where "is_non_overlapping P = (∀ X∈P . ∀ Y∈ P . (X ∩ Y ≠ {} ⟷ X = Y))" (* alternative, less concise formalisation: "is_non_overlapping P = (∀ ec1 ∈ P . ec1 ≠ {} ∧ (∀ ec2 ∈ P - {ec1}. ec1 ∩ ec2 = {}))" *) text ‹A subfamily of a non-overlapping family is also a non-overlapping family› lemma subset_is_non_overlapping: assumes subset: "P ⊆ Q" and non_overlapping: "is_non_overlapping Q" shows "is_non_overlapping P" (* CL: The following takes 387 ms with Isabelle2013-1-RC1: by (metis is_non_overlapping_def non_overlapping rev_subsetD subset). MC: possibly useful for TPTP *) 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 non_overlapping unfolding is_non_overlapping_def by force } then show ?thesis unfolding is_non_overlapping_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. MC: possibly useful for TPTP *) text ‹The family that results from removing one element from an equivalence class of a non-overlapping family is not otherwise a member of the family.› lemma remove_from_eq_class_preserves_disjoint: fixes elem::'a and X::"'a set" and P::"'a set set" assumes non_overlapping: "is_non_overlapping P" and eq_class: "X ∈ P" and elem: "elem ∈ X" shows "X - {elem} ∉ P" using assms Int_Diff is_non_overlapping_def Diff_disjoint Diff_eq_empty_iff Int_absorb2 insert_Diff_if insert_not_empty by (metis) text ‹Inserting into a non-overlapping family @{term P} a set @{term X}, which is disjoint with the set partitioned by @{term P}, yields another non-overlapping family.› lemma non_overlapping_extension1: fixes P::"'a set set" and X::"'a set" assumes partition: "is_non_overlapping P" and disjoint: "X ∩ ⋃ P = {}" and non_empty: "X ≠ {}" shows "is_non_overlapping (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_non_overlapping_def by fast next assume "Y = Z" then show "Y ∩ Z ≠ {}" using Y_Z_in_ext_P partition non_empty unfolding is_non_overlapping_def by auto qed } then show ?thesis unfolding is_non_overlapping_def by force qed text ‹An element of a non-overlapping family has no intersection with any other of its elements.› lemma disj_eq_classes: fixes P::"'a set set" and X::"'a set" assumes "is_non_overlapping 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_non_overlapping_def by fast then have "x ∈ {}" using other_eq_class by fast } then show ?thesis by blast qed text ‹The empty set is not element of a non-overlapping family.› lemma no_empty_in_non_overlapping: assumes "is_non_overlapping p" shows "{} ∉ p" (* CL: The following takes 36 ms with Isabelle2013-1-RC1: by (metis Int_iff all_not_in_conv assms is_non_overlapping_def). MC: possibly useful for TPTP *) using assms is_non_overlapping_def by fast text ‹@{term P} is a partition of the set @{term A}. The infix notation takes the form ``noun-verb-object''› definition is_partition_of (infix "partitions" 75) where "is_partition_of P A = (⋃ P = A ∧ is_non_overlapping P)" text ‹No partition of a non-empty set is empty.› lemma non_empty_imp_non_empty_partition: assumes "A ≠ {}" and "P partitions A" shows "P ≠ {}" using assms unfolding is_partition_of_def by fast text ‹Every element of a partitioned set ends up in one element in the partition.› lemma elem_in_partition: assumes in_set: "x ∈ A" and part: "P partitions A" obtains X where "x ∈ X" and "X ∈ P" using part in_set unfolding is_partition_of_def is_non_overlapping_def by (auto simp add: UnionE) text ‹Every element of the difference of a set @{term A} and another set @{term B} ends up in an element of a partition of @{term A}, but not in an element of the partition of @{term "{B}"}.› lemma diff_elem_in_partition: assumes x: "x ∈ A - B" and part: "P partitions A" shows "∃ S ∈ P - { B } . x ∈ S" (* Sledgehammer in Isabelle2013-1-RC1 can't do this within the default time limit. MC: possibly useful for TPTP *) proof - from part x obtain X where "x ∈ X" and "X ∈ P" by (metis Diff_iff elem_in_partition) with x have "X ≠ B" by fast with ‹x ∈ X› ‹X ∈ P› show ?thesis by blast qed text ‹Every element of a partitioned set ends up in exactly one set.› lemma elem_in_uniq_set: assumes in_set: "x ∈ A" and part: "P partitions A" shows "∃! X ∈ P . x ∈ X" proof - from assms obtain X where *: "X ∈ P ∧ x ∈ X" by (rule elem_in_partition) blast moreover { fix Y assume "Y ∈ P ∧ x ∈ Y" then have "Y = X" using part in_set * unfolding is_partition_of_def is_non_overlapping_def by (metis disjoint_iff_not_equal) } ultimately show ?thesis by (rule ex1I) qed text ‹A non-empty set ``is'' a partition of itself.› lemma set_partitions_itself: assumes "A ≠ {}" shows "{A} partitions A" unfolding is_partition_of_def is_non_overlapping_def (* CL: the following takes 48 ms on my machine with Isabelle2013: by (metis Sup_empty Sup_insert assms inf_idem singletonE sup_bot_right). MC: possibly useful for TPTP *) 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 "{} partitions {}" unfolding is_partition_of_def is_non_overlapping_def by fast text ‹Any partition of the empty set is empty.› lemma emptyset_part_emptyset2: assumes "P partitions {}" shows "P = {}" using assms unfolding is_partition_of_def is_non_overlapping_def by fastforce text ‹Classical set-theoretical definition of ``all partitions of a set @{term A}''› definition all_partitions where "all_partitions A = {P . P partitions A}" 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 text ‹inserts an element new\_el into a specified set S inside a given family 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 a non-overlapping family of sets yields another non-overlapping family.› lemma non_overlapping_extension2: fixes new_el::'a and P::"'a set set" and X::"'a set" assumes non_overlapping: "is_non_overlapping P" and class_element: "X ∈ P" and new: "new_el ∉ ⋃ P" shows "is_non_overlapping (insert_into_member new_el P X)" proof - let ?Y = "insert new_el X" have rest_is_non_overlapping: "is_non_overlapping (P - {X})" using non_overlapping subset_is_non_overlapping by blast have *: "X ∩ ⋃ (P - {X}) = {}" using non_overlapping class_element by (rule disj_eq_classes) from * have non_empty: "?Y ≠ {}" by blast from * have disjoint: "?Y ∩ ⋃ (P - {X}) = {}" using new by force have "is_non_overlapping (insert ?Y (P - {X}))" using rest_is_non_overlapping disjoint non_empty by (rule non_overlapping_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_equivalence: 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 characterization 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 set::"'a set" shows "⋃ (insert_into_member elem P set) = ⋃ (insert (set ∪ {elem}) (P - {set}))" (* CL: The following takes 12 ms in Isabelle2013-1-RC1: by (metis insert_into_member_def). MC: possibly useful for TPTP *) unfolding insert_into_member_def by fast text ‹Assuming that @{term P} is a partition of a set @{term S}, and @{term "new_el ∉ S"}, the function defined below yields all possible partitions of @{term "S ∪ {new_el}"} that are coarser than @{term P} (i.e.\ not splitting classes that already exist in @{term P}). These comprise one partition with a class @{term "{new_el}"} and all other classes unchanged, as well as all partitions obtained by inserting @{term new_el} into one class of @{term P} at a time. While we use the definition to build coarser partitions of an existing partition P, the definition itself does not require P to be a partition.› 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 class ‹{new_el}› and leaving all previous 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 class of ‹P› at a time.› ((insert_into_member new_el P) ` P)" 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 class ‹{new_el}› and leaving all previous 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 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_equivalence: 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_equivalence 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 classes, is non\_overlapping.› lemma non_overlapping_extension3: fixes elem::'a and P::"'a set set" and Q::"'a set set" assumes P_non_overlapping: "is_non_overlapping P" and new_elem: "elem ∉ ⋃ P" and Q_coarser: "Q ∈ coarser_partitions_with elem P" shows "is_non_overlapping 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_non_overlapping new_elem non_overlapping_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 non_overlapping_extension2 P_non_overlapping 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 one of the necessary criteria 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 characterization 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 class of the partition obtained by removing an element @{term elem} from an original partition @{term P} using @{const partition_without} equals some class of @{term P}, reduced by @{term elem}.› lemma super_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 class of sets obtained by removing an element from a non-overlapping class is another non-overlapping clas.› lemma non_overlapping_without_is_non_overlapping: fixes elem::'a and P::"'a set set" assumes "is_non_overlapping P" shows "is_non_overlapping (partition_without elem P)" (is "is_non_overlapping ?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_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_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_non_overlapping_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_non_overlapping_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 non_overlapping: "is_non_overlapping 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 of which elem is not a member *) 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 classes,of which elem is not a member, form a partition *) have elem_neq_classes_part: "is_non_overlapping ?elem_neq_classes" using subset_is_non_overlapping non_overlapping by blast have elem_eq_wrt_P: "?elem_eq ∈ ?remove_elem ` P" using elem_eq_class' by blast { (* consider a class W, of which elem is not a member *) fix W assume W_eq_class: "W ∈ ?elem_neq_classes" then have "elem ∉ W" using elem_eq_class elem_eq_class' non_overlapping is_non_overlapping_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 Y_elem_eq elem_neq_classes_id image_Un by metis finally have Q_wrt_elem: "?Q = ?elem_neq_classes ∪ {?elem_eq} - {{}}" . have "?elem_eq = {} ∨ ?elem_eq ∉ P" using elem_eq_class elem_eq_class' non_overlapping Diff_Int_distrib2 Diff_iff empty_Diff insert_iff unfolding is_non_overlapping_def by metis then have "?elem_eq ∉ P" using non_overlapping no_empty_in_non_overlapping 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 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_in_non_overlapping 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_in_non_overlapping non_overlapping non_overlapping_without_is_non_overlapping 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_equivalence: 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 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_equivalence 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) in form of a set› 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) in form of a 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_non_overlapping (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_non_overlapping_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_in_non_overlapping remove_code(1)) qed with ps_list distinct show ?thesis by (metis (full_types) distinct.simps(2) distinct_removeAll) qed qed text ‹The classical definition @{const all_partitions} and the algorithmic (constructive) definition @{const all_partitions_list} are equivalent.› lemma all_partitions_equivalence': 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: "P partitions (set (x # xs))" unfolding all_partitions_def .. then have is_non_overlapping: "is_non_overlapping 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 "?P_without_x partitions (set xs)" unfolding is_partition_of_def using is_non_overlapping non_overlapping_without_is_non_overlapping 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_non_overlapping 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_equivalence 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_equivalence 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 "Q partitions (set xs)" unfolding all_partitions_def .. then have "is_non_overlapping Q" and Q_covers: "⋃ Q = set xs" unfolding is_partition_of_def by simp_all then have P_partition: "is_non_overlapping P" using non_overlapping_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 "P partitions (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)" using UnionE comp_def imageE by auto 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_non_overlapping (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 classical definition @{const all_partitions} and the algorithmic (constructive) definition @{const all_partitions_list} are equivalent. This is a front-end theorem derived from @{thm all_partitions_equivalence'}; 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_equivalence' by blast text ‹The function that we will be using in practice to compute all partitions of a set, a set-oriented front-end 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)" end