*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Tue, 13 Nov 2012 12:08:21 +1300*Cc*: "formare-discuss at cs.bham.ac.uk" <formare-discuss at cs.bham.ac.uk>, isabelle-users at cl.cam.ac.uk*In-reply-to*: <50916DB3.4030707@cs.bham.ac.uk>*References*: <50916DB3.4030707@cs.bham.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

I've had a look at your work, and found it interesting. One thing that I noticed was that you defined what it means to be a second_price_auction, and you proved various things about functions that satisfy this definition, but you never showed that the definition was satisfiable. This isn't an inconsequential detail; at first, I thought you'd got the definition wrong, and that "second_price_auction n x p" implied n < 2. When I tried to prove it, I finally noticed that your allocation and payment functions depend on the set of bids. But it is easy to write definitions that aren't satisfiable, or that imply trivialities. So I decided to prove that your second_price_auction was satisfiable for n > 0. See attached for the proof. Also, you made a comment about removing an element from a set. Given a set A, the set of all the elements of A except x can be written as "A - {x}" I have a feeling that there was something else I was going to comment on, but I should go and have lunch, and write again if I remember it. Tim <><

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

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions***From:*Lawrence Paulson

- Previous by Date: [isabelle] Follow-up [Re: Isabelle operator precedence]
- Next by Date: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Previous by Thread: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Next by Thread: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list