Theory Partitions
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))"
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"
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
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"
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"
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
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}))"
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
(insert {new_el} P)
((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 =
({new_el} # P)
#
(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 - {{}}"
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}"
obtain Y
where elem_eq_class: "elem ∈ Y" and elem_eq_class': "Y ∈ P" using elem ..
let ?elem_neq_classes = "P - {Y}"
have P_wrt_elem: "P = ?elem_neq_classes ∪ {Y}" using elem_eq_class' by blast
let ?elem_eq = "Y - {elem}"
have Y_elem_eq: "?remove_elem ` {Y} = {?elem_eq}" by fast
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
{
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"
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
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)
fix P::"'a set set"
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
fix P::"'a set set"
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)))" .
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