(*
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 \