(* 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 {* Maximum components of vectors (unique thanks to tie-breaking), and their properties *} theory UniqueMaximum imports Maximum FullySpecifiedSingleGoodAuction begin text{* the index of the single maximum component *} fun arg_max_l_tb :: "(participant list) \ tie_breaker \ bids \ participant" where "arg_max_l_tb [] t b = 0" (* in practice we will only call the function with lists of at least one element *) | "arg_max_l_tb [x] t b = x" | "arg_max_l_tb (x # xs) t b = (let y = arg_max_l_tb xs t b in if (b x > b y) then x (* TODO CL: Once this works, make 'highest bid' just a special case of tie-breaking, and allow for custom chains of tie-breaking functions to be defined. *) else if (b x = b y \ t x y) then x else y)" fun arg_max_tb :: "participant set \ tie_breaker \ bids \ participant" where "arg_max_tb N t b = arg_max_l_tb (sorted_list_of_set N) t b" (* TODO CL: once proving properties of the list-based implementation of this function starts to hurt, follow Lars Noschinski's advice to use the list-based implementation for code generation only, and otherwise use an equivalent set-based definition. http://stackoverflow.com/questions/16702866/defining-an-arg-max-like-function-over-finite-sets-and-proving-some-of-its-pr#comment24451608_16707012 *) fun arg_max_tb_req_wb :: "participant set \ tie_breaker \ bids \ participant" where "arg_max_tb_req_wb N t b = (if (wb_tie_breaker_on t N) then Some (arg_max_tb N t b) else None)" lemma arg_max_tb_wb: assumes "wb_tie_breaker_on t N" shows "arg_max_tb N t b = the (arg_max_tb_req_wb N t b)" using assms by simp (* uncomment for testing: value "arg_max_tb {2::nat, 4, 6} (* the participant indices *) op> (* the tie breaking function *) (\ i . nth [27::real, 42, 42] (i div 2 - 1::nat))" *) text{* The highest bidder, determined by tie-breaking using @{term arg_max_tb}, is one member of the set of all highest bidders, determined using @{term arg_max}. *} lemma arg_max_tb_imp_arg_max : fixes N :: "participant set" and t :: tie_breaker and b :: bids assumes defined: "maximum_defined N" and wb_tie: "wb_tie_breaker_on t N" shows "the (arg_max_tb_req_wb N t b) \ arg_max N b" (* A proof could be indirect by assuming that arg_max_tb N t b is not in the set, i.e., that the arg_max_tb offers less or more, and bring this to a contradiction.*) proof - def Nsort \ "sorted_list_of_set N" from defined have finite: "finite N" and ne: "N \ {}" unfolding maximum_defined_def by (simp_all add: card_gt_0_iff) from finite Nsort_def sorted_list_of_set have distinct: "distinct Nsort" by fast from finite ne Nsort_def have "Nsort \ []" by simp then have stmt_list: "distinct Nsort \ arg_max_l_tb Nsort t b \ arg_max (set Nsort) b" proof (induct Nsort rule: list_nonempty_induct) case single { fix x have "arg_max_l_tb [x] t b \ arg_max (set [x]) b" unfolding arg_max_def maximum_def Nsort_def by simp } then show ?case .. next case cons (* CL: How can I use the cons.*, that I'm getting here, below? *) fix x xs assume a1: "xs \ []" and a2: "distinct xs \ arg_max_l_tb xs t b \ arg_max (set xs) b" from a1 have mdxs: "maximum_defined (set xs)" unfolding maximum_defined_def by (metis List.finite_set card_gt_0_iff set_empty2) from a1 have mdxs': "maximum_defined (set (x # xs))" unfolding maximum_defined_def by (metis List.finite_set card_gt_0_iff list.distinct(1) set_empty) show "distinct (x # xs) \ arg_max_l_tb (x # xs) t b \ arg_max (set (x # xs)) b" proof assume distinct': "distinct (x # xs)" def i \ "arg_max_l_tb (x # xs) t b" with a1 have "i = (let y = arg_max_l_tb xs t b in if (b x > b y) then x else if (b x = b y \ t x y) then x else y)" by (metis arg_max_l_tb.simps(2,3) neq_Nil_conv) then have i_unf: "i = (let y = arg_max_l_tb xs t b in if (b x > b y \ b x = b y \ t x y) then x else y)" by smt show "i \ arg_max (set (x # xs)) b" proof (cases "i = arg_max_l_tb xs t b") case True (* the maximum is the same as before *) with a2 distinct' have ams: "i \ arg_max (set xs) b" by simp with mdxs have i_in: "i \ (set xs)" unfolding arg_max_def using maximum_is_component by simp then have i_in': "i \ (set (x # xs))" by simp from i_unf True have "\ (b x > b i \ b x = b i \ t x i)" by (smt distinct' distinct.simps(2) i_in) then have 1: "b x \ b i" by auto from ams have "b i = maximum (set xs) b" unfolding arg_max_def by simp with maximum_is_greater_or_equal mdxs have "\ j \ (set xs) . b i \ b j" by (metis (full_types)) with 1 have "\ j \ (set (x # xs)) . b i \ b j" by simp with maximum_sufficient mdxs' i_in' have "b i = maximum (set (x # xs)) b" by metis with i_in' show ?thesis unfolding arg_max_def by simp next case False (* the newly inserted element x is the maximum *) def y \ "arg_max_l_tb xs t b" with i_unf have yi: " i = (if (b x > b y \ b x = b y \ t x y) then x else y)" by auto from y_def False have "i \ y" unfolding i_def by simp with yi have bi: "(b x > b y \ b x = b y \ t x y) \ i = x" by smt from y_def a2 distinct' have ams: "y \ arg_max (set xs) b" by simp with mdxs have y_in: "y \ (set xs)" unfolding arg_max_def using maximum_is_component by simp then have y_in': "y \ (set (x # xs))" by simp from ams have "b y = maximum (set xs) b" unfolding arg_max_def by simp with maximum_is_greater_or_equal mdxs have "\ j \ (set xs) . b y \ b j" by (metis (full_types)) with bi have "\ j \ (set xs) . b x \ b j" by auto (* because b x \ b y *) then have "\ j \ (set (x # xs)) . b x \ b j" by simp with maximum_sufficient mdxs' have "b x = maximum (set (x # xs)) b" by (metis distinct' distinct.simps(2) distinct_length_2_or_more) with bi show ?thesis unfolding arg_max_def by simp qed qed qed from Nsort_def `finite N` have "N = set Nsort" by simp from Nsort_def wb_tie have "the (arg_max_tb_req_wb N t b) = arg_max_l_tb Nsort t b" by simp with distinct stmt_list have "the (arg_max_tb_req_wb N t b) \ arg_max (set Nsort) b" by simp with `N = set Nsort` show ?thesis by simp qed end