(*
Auction Theory Toolbox (http://formare.github.io/auctions/)
Authors:
* Christoph Lange
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 {* Alternative definitions of partitions of a set, which we are not currently using *}
theory PartitionsAlternative
imports
Main
Finite_Set
Partitions (* not strictly needed at this point, but useful for searching applicable theorems and for generalisations*)
begin
section {* Unused alternative definitions by Christoph Lange *}
text {* @{term E} is the set of all equivalence relations on the set @{term X}. *}
definition isEquivSet :: "('a \ 'a) set set \ 'a set \ bool"
where "isEquivSet E X \ (\ e . e \ E \ equiv X e)"
text {* another set-theoretical, non-computable definition of ``all partitions of a set @{term A}'':
the set of all quotients of @{term A} w.r.t.\ some equivalence relation @{term R} *}
definition all_partitions_wrt_equiv :: "'a set \ 'a set set set"
where "all_partitions_wrt_equiv A = { P . (* all sets P such that \ *)
(* thought we'd need something like this for computability:
P \ Pow (Pow A) (* P is a set of subsets of A,
i.e. a subset of the set of all subsets of A,
i.e. a subset of the powerset of A,
i.e. a member of the powerset of the powerset of A.
We need this only for computability; otherwise 'P = A // e' would do the job. *)
\ *)
(\ R . (* There is an R such that \ *)
equiv A R (* R is an equivalence relation on A *)
\ P = A // R (* and P is the partition of A w.r.t. R. *)
) }"
text {* an entirely list-based algorithm, which serves as an alternative to
@{const all_partitions_list}, @{const all_coarser_partitions_with_list},
@{const coarser_partitions_with_list}, @{const insert_into_member_list} *}
fun all_partitions_fun_list :: "'a list \ 'a set list list"
where "all_partitions_fun_list [] = []"
| "all_partitions_fun_list [x] = [[{x}]]" (* singleton case is special, not sufficiently covered by [] and x#xs *)
| "all_partitions_fun_list (x # xs) = (let xs_partitions = all_partitions_fun_list xs in
concat [
(* inserting x into each equivalence class (one at a time) \ *)
[ P[i := {x} \ P ! i] . i \ map nat [0..(int (List.length P) - 1)] ]
. P \ xs_partitions (* \ of each partition of xs *) ]
@ [ {x} # P . P \ xs_partitions] (* and adding the {x} singleton equivalence class to each partition of xs: *)
)"
text {* frontend to @{const all_partitions_fun_list}, turns the @{typ "'a set list list"}
returned by that function into a @{typ "'a set set set"} *}
fun all_partitions_fun :: "'a\linorder set \ 'a set set set"
where "all_partitions_fun A = set (map set (all_partitions_fun_list (sorted_list_of_set A)))"
end