(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Manfred Kerber * Christoph Lange * Colin Rowat * Makarius Wenzel 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 {* Fully specified single good auctions (with tie-breaking) *} theory SingleGoodAuctionTieBreaker (* TODO CL: consider renaming as per https://github.com/formare/auctions/issues/16 *) imports Main "~~/src/HOL/Library/Order_Relation" SingleGoodAuction begin (* CL: CR commented that a tie-breaker may even be employed on the highest level of ranking bids: There's nothing, in principle, to prevent design of an auction in which the value of a bid is not the first element in the lexicographical order - or even, presumably - in which the scoring rule calculates a weighted average of a number of factors. *) text{* Helps to determine whether one participant should be preferred over another one in the case of a draw. t x y = True should result in x being (strictly) preferred. *} type_synonym tie_breaker = "participant \ participant \ bool" text{* Is a tie-breaker well-behaved on a given set of participants? I.e. is it a strict linear order? *} definition wb_tie_breaker_on :: "tie_breaker \ participant set \ bool" where "wb_tie_breaker_on t N \ strict_linear_order_on N {(a::participant, b::participant) . {a, b} \ N \ t a b}" (* old version for tie_breaker = "participant \ real", to be used with < "card (tie_breaker ` N) = card N" *) (* CL: code provided by Le_J (http://stackoverflow.com/a/16690357/2397768) – how to prove strict linear order in a concrete case: *) (* lemma "strict_linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} \ {1::nat, 2} \ a < b}" unfolding strict_linear_order_on_def partial_order_on_def preorder_on_def irrefl_def total_on_def trans_def antisym_def by auto *) end