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