(* 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 {* Tie-breakers in Combinatorial Auctions *} theory CombinatorialAuctionTieBreaker imports CombinatorialAuction begin text {* This formalisation includes suggestions from two participants in a \href{http://stackoverflow.com/questions/18806628/why-is-my-definition-of-a-function-that-chooses-an-element-from-a-finite-set-inc}{discussion at StackOverflow}. *} section {* Types *} type_synonym tie_breaker_rel = "allocation_rel set \ allocation_rel" type_synonym tie_breaker_alg = "allocation_rel list \ allocation_rel" (* CL: probably not needed, neither for close-to-paper nor for computable version type_synonym tie_breaker_fun = "allocation_fun set \ allocation_fun" *) text {* A well-defined tie-breaker is a \href{http://en.wikipedia.org/wiki/Choice_function}{choice function} that selects one element out of a set of allocations. *} definition tie_breaker :: "tie_breaker_rel \ bool" where "tie_breaker t \ (\ X . X \ {} \ t X \ X)" text {* break ties by preferring an arbitrary existing allocation using the choice operator *} definition tie_breaker_choice :: "tie_breaker_rel" where "tie_breaker_choice x = (SOME y . y \ x)" text {* @{const tie_breaker_choice} is a valid tie-breaker. *} lemma "tie_breaker tie_breaker_choice" unfolding tie_breaker_def tie_breaker_choice_def by (metis (lifting) all_not_in_conv some_eq_ex) (* TODO CL: when proving paper\algorithm equivalence w.r.t. tie-breakers, we need to make the assumption, that the "set" tie-breaker and the "list" tie-breaker select the same allocation. *) text {* trivial algorithmic tie breaker: take the first element of a list *} definition tie_breaker_example_alg :: tie_breaker_alg where "tie_breaker_example_alg = hd" end