Theory FirstPrice

(*
Auction Theory Toolbox (http://formare.github.io/auctions/)

Authors:
* Marco B. Caminati http://caminati.co.nr
* Manfred Kerber <mnfrd.krbr@gmail.com>
* Christoph Lange <math.semantic.web@gmail.com>
* Colin Rowat <c.rowat@bham.ac.uk>

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

section ‹First-price auction: adapted from VCG auction›

theory FirstPrice

imports
CombinatorialAuction


begin

(* In a first price auction we use the same allocation algorithm as in a VCG auction. 
   The price a winning bidder has to pay is given by evaluating b with respect to the bidder
   and the set he/she gets. *)
abbreviation "firstPriceP N Ω b r n ==
  b (n, winningAllocationAlg N Ω r b,, n)"

(* The non-negativity of prices follows immediately from the assumptions that all bids are
   non-negative. *)
theorem NonnegFirstPrices:
   assumes "∀ X. b (n, X) ≥ 0" 
   shows "firstPriceP N Ω b r n ≥ 0" 
   using assms by blast
end