(*
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 second price single good auction *}
theory FullySpecifiedSecondPriceAuction
imports
SingleGoodAuction
SingleGoodAuctionTieBreaker
SecondPriceAuction
UniqueMaximum
begin
(* fs = fully specified *)
definition fs_spa_pred :: "participant set \ bids \ tie_breaker \ allocation \ payments \ bool"
where
"fs_spa_pred N b t x p \
wb_tie_breaker_on t N \
spa_admissible_input N b \
(\i \ N . i = the (arg_max_tb_req_wb N t b) \ second_price_auction_winner_outcome N b x p i \
(\j \ N . j \ i \ second_price_auction_loser_outcome N x p j))"
text{* convenience function to compute the winner of a fully specified second price auction with tie-breaking *}
fun fs_spa_winner_req_wb :: "participant set \ bids \ tie_breaker \ participant"
where "fs_spa_winner_req_wb N b t = the (arg_max_tb_req_wb N t b)"
fun fs_spa_winner :: "participant set \ bids \ tie_breaker \ participant"
where "fs_spa_winner N b t = arg_max_tb N t b"
lemma fs_spa_winner_wb:
assumes "wb_tie_breaker_on t N" shows "fs_spa_winner N b t = fs_spa_winner_req_wb N b t"
using assms by simp
text{* convenience function to compute the allocation of a fully specified second price auction with tie-breaking *}
fun fs_spa_allocation_req_wb :: "participant set \ bids \ tie_breaker \ allocation"
where "fs_spa_allocation_req_wb N b t = (let winner = fs_spa_winner_req_wb N b t in
(\ i . if (i = winner) then 1 else 0))"
fun fs_spa_allocation :: "participant set \ bids \ tie_breaker \ allocation"
where "fs_spa_allocation N b t = (let winner = fs_spa_winner N b t in
(\ i . if (i = winner) then 1 else 0))"
lemma fs_spa_allocation_wb:
assumes "wb_tie_breaker_on t N" shows "fs_spa_allocation N b t = fs_spa_allocation_req_wb N b t"
using assms by simp
text{* convenience function to compute the payments of a fully specified second price auction with tie-breaking *}
fun fs_spa_payments_req_wb :: "participant set \ bids \ tie_breaker \ payments"
where "fs_spa_payments_req_wb N b t = (let winner = fs_spa_winner_req_wb N b t in
(\ i . if (i = winner) then maximum (N - {i}) b else 0))"
fun fs_spa_payments :: "participant set \ bids \ tie_breaker \ payments"
where "fs_spa_payments N b t = (let winner = fs_spa_winner N b t in
(\ i . if (i = winner) then maximum (N - {i}) b else 0))"
lemma fs_spa_payments_wb:
assumes "wb_tie_breaker_on t N" shows "fs_spa_payments N b t = fs_spa_payments_req_wb N b t"
using assms by simp
text{* The definitions of the computable functions @{text fs_spa_allocation} and @{text fs_spa_payments}
are consistent with how we defined the outcome of a fully specified second price auction
with tie-breaking in @{text fs_spa_pred}. *}
lemma fs_spa_pred_allocation_payments:
fixes N :: "participant set"
and b :: bids
and t :: tie_breaker
and x :: allocation
and p :: payments
shows "fs_spa_pred N b t x p \
wb_tie_breaker_on t N \
spa_admissible_input N b \
eq N x (fs_spa_allocation_req_wb N b t) \
eq N p (fs_spa_payments_req_wb N b t)" (is "?fs_spa_pred \ ?alloc_pay")
proof
assume "?fs_spa_pred"
then have "wb_tie_breaker_on t N \ spa_admissible_input N b"
and outcome: "\i \ N . i = fs_spa_winner_req_wb N b t \
x i = 1 \ (\j \ N . j \ i \ x j = 0) \
p i = maximum (N - {i}) b \ (\j \ N . j \ i \ p j = 0)"
unfolding fs_spa_pred_def
second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def
by auto
then show "?alloc_pay"
using fs_spa_allocation_req_wb.simps fs_spa_payments_req_wb.simps unfolding eq_def by smt
next
assume "?alloc_pay"
then have wb_tie: "wb_tie_breaker_on t N"
and admissible: "spa_admissible_input N b"
and outcome: "let winner = fs_spa_winner_req_wb N b t in
(\i \ N . x i = (if (i = winner) then 1 else 0)) \
(\i \ N . p i = (if (i = winner) then maximum (N - {i}) b else 0))"
unfolding eq_def
by simp_all
from wb_tie admissible have winner_range: "fs_spa_winner_req_wb N b t \ N"
using arg_max_def arg_max_tb_imp_arg_max fs_spa_winner_req_wb.simps maximum_defined_def spa_admissible_input_def
mem_Collect_eq
by smt
with outcome have "let winner = fs_spa_winner_req_wb N b t in
x winner = 1 \ (\j \ N . j \ winner \ x j = 0) \
p winner = maximum (N - {winner}) b \ (\j \ N . j \ winner \ p j = 0)" by metis
with wb_tie admissible winner_range show "?fs_spa_pred"
unfolding fs_spa_pred_def
second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def
using fs_spa_winner_req_wb.simps by metis
qed
lemma fs_spa_is_spa :
fixes N :: "participant set"
and b :: bids
and t :: tie_breaker
and x :: allocation
and p :: payments
assumes "fs_spa_pred N b t x p"
shows "spa_pred N b x p"
proof -
from assms have wb_tie: "wb_tie_breaker_on t N" and card: "card N > 1" and bids: "bids N b" and
def_unfolded: "(\i \ N . i = the (arg_max_tb_req_wb N t b) \ second_price_auction_winner_outcome N b x p i \
(\j \ N . j \ i \ second_price_auction_loser_outcome N x p j))"
unfolding fs_spa_pred_def spa_admissible_input_def by auto
then obtain winner
where fs_spa_winner: "winner \ N \ winner = the (arg_max_tb_req_wb N t b) \
second_price_auction_winner_outcome N b x p winner"
and spa_loser: "\j \ N . j \ winner \ second_price_auction_loser_outcome N x p j" by blast
have spa_winner: "winner \ N \ winner \ arg_max N b \ second_price_auction_winner_outcome N b x p winner"
proof -
from fs_spa_winner have range: "winner \ N"
and determination: "winner = the (arg_max_tb_req_wb N t b)"
and spa_winner_outcome: "second_price_auction_winner_outcome N b x p winner"
by auto
from card have maximum_defined: "maximum_defined N" unfolding maximum_defined_def by simp
with wb_tie determination have "winner \ arg_max N b" using arg_max_tb_imp_arg_max by simp
with range and spa_winner_outcome show ?thesis by simp
qed
with card bids spa_loser have "card N > 1 \ bids N b \ (\i \ N. i \ arg_max N b \ second_price_auction_winner_outcome N b x p i \
(\j \ N . j \ i \ second_price_auction_loser_outcome N x p j))" by blast
then show ?thesis unfolding spa_admissible_input_def spa_pred_def by simp
qed
text{* alternative definition for easier currying *}
definition fs_spa_pred' :: "tie_breaker \ participant set \ bids \ allocation \ payments \ bool"
where "fs_spa_pred' t N b x p = fs_spa_pred N b t x p"
end