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 \<ge> 0"
proof (cases n)
  case 0
  thus "maximum_except n b i \<ge> 0" unfolding maximum_except_def by simp
next
  case (Suc m)
  with maximum_non_negative
  show "maximum_except n b i \<ge> 0" unfolding maximum_except_def by simp
qed

subsection {* Choice of highest bidder *}

definition highest_bidder :: "participants \<Rightarrow> real_vector \<Rightarrow> participant" where
  "highest_bidder n b \<equiv> \<some> i. in_range n i \<and> 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 "\<exists> i. in_range n i \<and> maximum n b = b i" unfolding bids_def by simp
  hence "in_range n (highest_bidder n b) \<and> 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 \<in> 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 \<Rightarrow> allocation" where
  "highest_bidder_wins n b i \<equiv> 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 \<Rightarrow> payments" where
  "second_price_payments n b i
    \<equiv> 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 \<in> 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 \<noteq> 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 "\<exists> i. in_range n i
      \<and> second_price_auction_winner n b (highest_bidder_wins n)
        (second_price_payments n) i
      \<and> (\<forall> j. in_range n j \<and> j \<noteq> i
        \<longrightarrow> 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