Theory StrictCombinatorialAuction

(*
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 ‹Definitions about those Combinatorial Auctions which are strict (i.e., which assign all the available goods)›

theory StrictCombinatorialAuction
imports Complex_Main
  Partitions
  MiscTools

begin

subsection ‹Types›

type_synonym index = "integer"
type_synonym participant = index
type_synonym good = "integer"
type_synonym goods = "good set"
type_synonym price = real
type_synonym bids3 = "((participant × goods) × price) set"
type_synonym bids = "participant ⇒ goods ⇒ price"
type_synonym allocation_rel = "(goods × participant) set"
type_synonym allocation = "(participant × goods) set" 
type_synonym payments = "participant ⇒ price"
type_synonym bidvector = "(participant × goods) ⇒ price"
abbreviation "bidvector (b::bids) == case_prod b"
abbreviation "proceeds (b::bidvector) (allo::allocation) == sum b allo"
abbreviation "winnersOfAllo (a::allocation) == Domain a"
abbreviation "allocatedGoods (allo::allocation) == ⋃ (Range allo)"

(* possible_allocations_rel defines all possible allocations of a set of goods G to a set of participants N: 
  injective functions that map sets of goods to their potential buyers, i.e.\ participants.
  Here, we assume that everything gets allocated, i.e. that there is no free disposal.
  This assumption facilitates the paper↔algorithm equivalence proof for injective functions.
*)
fun possible_allocations_rel 
  where "possible_allocations_rel G N = Union { injections Y N | Y . Y ∈ all_partitions G }" 

(* The following abbreviations duplicate the corresponding definitions in RelationProperties.thy. This is done since typically abbreviations are efficient in theorem proving, however, not in code extraction. *)

abbreviation "is_partition_of' P A == (⋃ P = A ∧ is_non_overlapping P)"
abbreviation "all_partitions' A == {P . is_partition_of' P A}"

abbreviation "possible_allocations_rel' G N == Union{injections Y N | Y . Y ∈ all_partitions' G}"
abbreviation allAllocations where 
  "allAllocations N G == converse ` (possible_allocations_rel G N)"

text ‹algorithmic version of @{const possible_allocations_rel}›
fun possible_allocations_alg :: "goods ⇒ participant set ⇒ allocation_rel list"
  where "possible_allocations_alg G N = 
         concat [ injections_alg Y N . Y ← all_partitions_alg G ]"

abbreviation "allAllocationsAlg N G == 
              map converse (concat [(injections_alg l N) . l ← all_partitions_list G])"



subsection ‹VCG mechanism›

(* N is the set of bidders, G the set of goods, and b the bidvector *)
abbreviation "winningAllocationsRel N G b == 
              argmax (sum b) (allAllocations N G)"

(* t is a tie breaking function *)
abbreviation "winningAllocationRel N G t b == t (winningAllocationsRel N G b)"

(* This is the computational version of winningAllocationsRel *)
abbreviation "winningAllocationsAlg N G b == argmaxList (proceeds b) (allAllocationsAlg N G)"

(* This is the computational version of winningAllocationRel *)
definition "winningAllocationAlg N G t b == t (winningAllocationsAlg N G b)"

text ‹payments›

text ‹alpha is the maximum sum of bids of all bidders except bidder ‹n›'s bid, computed over all possible allocations of all goods,
  i.e. the value reportedly generated by value maximization when solved without n's bids›
abbreviation "alpha N G b n == Max ((sum b)`(allAllocations (N-{n}) G))"

(* computational version of alpha *)
abbreviation "alphaAlg N G b n == Max ((proceeds b)`(set (allAllocationsAlg (N-{n}) (G::_ list))))"

(* revenue with participant n removed from winning allocation *)
abbreviation "remainingValueRel N G t b n == sum b ((winningAllocationRel N G t b) -- n)"

(* computational version of remainingValueRel *)
abbreviation "remainingValueAlg N G t b n == proceeds b ((winningAllocationAlg N G t b) -- n)"

(* function to determine payments for each participant *)
abbreviation "paymentsRel N G t == (alpha N G) - (remainingValueRel N G t)"

(* computational version of paymentsRel *)
definition "paymentsAlg N G t == (alphaAlg N G) - (remainingValueAlg N G t)"

end