header {* Specific allocation and payment functions satisfying the requirements of a
second-price auction *}
theory Vickrey_Extras
imports Vickrey
begin
subsection {* More about @{const maximum_except} *}
lemma maximum_except_non_negative: "maximum_except n b i \ 0"
proof (cases n)
case 0
thus "maximum_except n b i \ 0" unfolding maximum_except_def by simp
next
case (Suc m)
with maximum_non_negative
show "maximum_except n b i \ 0" unfolding maximum_except_def by simp
qed
subsection {* Choice of highest bidder *}
definition highest_bidder :: "participants \ real_vector \ participant" where
"highest_bidder n b \ \ i. in_range n i \ maximum n b = b i"
lemma highest_bidder_is_maximum:
assumes "n > 0" and "bids n b"
shows "in_range n (highest_bidder n b)" and "maximum n b = b (highest_bidder n b)"
proof -
from assms and maximum_is_component
have "\ i. in_range n i \ maximum n b = b i" unfolding bids_def by simp
hence "in_range n (highest_bidder n b) \ maximum n b = b (highest_bidder n b)"
unfolding highest_bidder_def by (rule someI_ex)
thus "in_range n (highest_bidder n b)" and "maximum n b = b (highest_bidder n b)"
by simp_all
qed
lemma highest_bidder_in_arg_max_set:
assumes "n > 0" and "bids n b"
shows "highest_bidder n b \ arg_max_set n b"
unfolding arg_max_set_def
using assms and highest_bidder_is_maximum
by simp
subsection {* Allocation where the highest bidder wins *}
definition highest_bidder_wins :: "participants \ allocation" where
"highest_bidder_wins n b i \ if i = highest_bidder n b then True else False"
lemma highest_bidder_wins_is_allocation:
assumes "n > 0" and "bids n b"
shows "allocation n b (highest_bidder_wins n)"
proof -
from assms have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)
with `bids n b` show "allocation n b (highest_bidder_wins n)"
unfolding allocation_def and highest_bidder_wins_def by simp
qed
subsection {* Second-price payments *}
definition second_price_payments :: "participants \ payments" where
"second_price_payments n b i
\ if i = highest_bidder n b then maximum_except n b i else 0"
lemma second_price_payments_non_negative:
"vickrey_payment n b (second_price_payments n)"
unfolding vickrey_payment_def and second_price_payments_def
using maximum_except_non_negative
by simp
subsection {* @{const highest_bidder_wins} and @{const second_price_payments}
satisfy @{const second_price_auction} *}
lemma highest_bidder_second_price_auction_winner:
assumes "n > 0" and "bids n b"
shows "second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) (highest_bidder n b)"
proof -
from assms
have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)
from assms
have "highest_bidder n b \ arg_max_set n b" by (rule highest_bidder_in_arg_max_set)
with `in_range n (highest_bidder n b)`
show ?thesis
unfolding second_price_auction_winner_def
and highest_bidder_wins_def
and second_price_payments_def
by simp
qed
lemma other_bidders_second_price_auction_loser:
assumes "in_range n i" and "i \ highest_bidder n b"
shows "second_price_auction_loser n b (highest_bidder_wins n)
(second_price_payments n) i"
unfolding second_price_auction_loser_def
and highest_bidder_wins_def
and second_price_payments_def
using assms
by simp
theorem second_price_auction_example:
assumes "n > 0"
shows "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
proof -
{ fix b
assume "bids n b"
with `n > 0`
have "allocation n b (highest_bidder_wins n)"
by (rule highest_bidder_wins_is_allocation)
from `n > 0` and `bids n b`
have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)
from `n > 0` and `bids n b`
have "second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) (highest_bidder n b)"
by (rule highest_bidder_second_price_auction_winner)
with `in_range n (highest_bidder n b)` and other_bidders_second_price_auction_loser
have "\ i. in_range n i
\ second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) i
\ (\ j. in_range n j \ j \ i
\ second_price_auction_loser n b (highest_bidder_wins n)
(second_price_payments n) j)"
by (simp add: exI [of _ "highest_bidder n b"])
note `allocation n b (highest_bidder_wins n)`
and second_price_payments_non_negative [of n b]
and this
}
thus "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
unfolding second_price_auction_def
by simp
qed
theorem second_price_auction_example_equilibrium_weakly_dominant:
assumes "n > 0" and "valuation n v"
shows "equilibrium_weakly_dominant_strategy n v v
(highest_bidder_wins n) (second_price_payments n)"
proof -
from `n > 0`
have "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
by (rule second_price_auction_example)
with `valuation n v`
show "equilibrium_weakly_dominant_strategy n v v
(highest_bidder_wins n) (second_price_payments n)"
by (rule vickreyA)
qed
theorem second_price_auction_example_efficient:
assumes "n > 0" and "valuation n v"
shows "efficient n v v (highest_bidder_wins n)"
proof -
from `n > 0`
have "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
by (rule second_price_auction_example)
with `valuation n v`
show "efficient n v v (highest_bidder_wins n)" by (rule vickreyB)
qed
end