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