Theory FirstPrice

Auction Theory Toolbox (

* Marco B. Caminati
* Manfred Kerber <>
* Christoph Lange <>
* Colin Rowat <>

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:

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

theory FirstPrice



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