(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Marco B. Caminati http://caminati.co.nr * Manfred Kerber <mnfrd.krbr@gmail.com> * Christoph Lange <math.semantic.web@gmail.com> * Colin Rowat <c.rowat@bham.ac.uk> 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) *) section ‹Termination theorem for uniform tie-breaking› theory UniformTieBreaking imports StrictCombinatorialAuction Universes "HOL-Library.Code_Target_Nat" begin subsection ‹Uniform tie breaking: definitions› text‹Let us repeat the general context. Each bidder has made their bids and the VCG algorithm up to now allocates goods to the higher bidders. If there are several high bidders tie breaking has to take place. To do tie breaking we generate out of a random number a second bid vector so that the same algorithm can be run again to determine a unique allocation. To this end, we associate to each allocation the bid in which each participant bids for a set of goods an amount equal to the cardinality of the intersection of the bid with the set she gets in this allocation. By construction, the revenue of an auction run using this bid is maximal on the given allocation, and this maximal is unique. We can then use the bid constructed this way @{term tiebids} to break ties by running an auction having the same form as a normal auction (that is why we use the adjective ``uniform''), only with this special bid vector.› (* omega pair is a tool to compute cardinalities of pairs, e.g. for a pair made of a participant 1 and a set of goods {11,12,13}, the result will be the set of pairs: {(1,{11}), (1,{12}), (1,{13})}. *) abbreviation "omega pair == {fst pair} × (finestpart (snd pair))" (* pseudo allocation is like an allocation, but without uniqueness of the elements allocated *) definition "pseudoAllocation allocation == ⋃ (omega ` allocation)" (* some abbreviation to defined tiebids below *) abbreviation "bidMaximizedBy allocation N G == pseudoAllocation allocation <|| ((N × (finestpart G)))" (* functional version of the above *) abbreviation "maxbid a N G == toFunction (bidMaximizedBy a N G)" (* For bidding the cardinality of the second element of a single pair, i.e., (bidder, goods) → ((bidder, goods), bid) *) abbreviation "summedBid bids pair == (pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair)))" (* returns just the bid in the above *) abbreviation "summedBidSecond bids pair == sum (%g. bids (fst pair, g)) (finestpart (snd pair))" (* apply summedBid to each possible pair *) abbreviation "summedBidVectorRel bids N G == (summedBid bids) ` (N × (Pow G - {{}}))" (* functional version of above *) abbreviation "summedBidVector bids N G == toFunction (summedBidVectorRel bids N G)" (* tiebids returns a bid vector that when the VCG algorithm runs on it yields the singleton {allocation}. Functional version *) abbreviation "tiebids allocation N G == summedBidVector (maxbid allocation N G) N G" (* relational version of the above *) abbreviation "Tiebids allocation N G == summedBidVectorRel (real∘maxbid allocation N G) N G" (* Assumed we have a list and a random we take the random-th element of the list. However, if the random number is bigger than the list is long we take it modulo the length of the list *) definition "randomEl list (random::integer) = list ! ((nat_of_integer random) mod (size list))" value "nat_of_integer (-3::integer) mod 2" (* The randomEl taken out of a list is in the list *) lemma randomElLemma: assumes "set list ≠ {}" shows "randomEl list random ∈ set list" using assms by (simp add: randomEl_def) (* The chosen allocation takes the random-th element of all possible winning allocations. This is done by taking the element given by randomEl list random defined above. *) abbreviation "chosenAllocation N G bids random == randomEl (takeAll (%x. x∈(winningAllocationsRel N (set G) bids)) (allAllocationsAlg N G)) random" (* find the bid vector in random values that returns the chosen winning allocation *) abbreviation "resolvingBid N G bids random == tiebids (chosenAllocation N G bids random) N (set G)" subsection ‹Termination theorem for the uniform tie-breaking scheme› corollary winningAllocationPossible: "winningAllocationsRel N G b ⊆ allAllocations N G" using injectionsFromEmptyAreEmpty mem_Collect_eq subsetI by auto lemma subsetAllocation: assumes "a ∈ allocationsUniverse" "c ⊆ a" shows "c ∈ allocationsUniverse" proof - have "c=a-(a-c)" using assms(2) by blast thus ?thesis using assms(1) reducedAllocation by (metis (no_types)) qed lemma lm001: assumes "a ∈ allocationsUniverse" shows "a outside X ∈ allocationsUniverse" using assms reducedAllocation Outside_def by (metis (no_types)) corollary lm002: "{x}×({X}-{{}}) ∈ allocationsUniverse" using allocationUniverseProperty pairDifference by metis (* TPTP? *) corollary lm003: "{(x,{y})} ∈ allocationsUniverse" proof - have "⋀x1. {} - {x1::'a × 'b set} = {}" by simp thus "{(x, {y})} ∈ allocationsUniverse" by (metis (no_types) allocationUniverseProperty empty_iff insert_Diff_if insert_iff prod.inject) qed corollary lm004: "allocationsUniverse ≠ {}" using lm003 by fast corollary lm005: "{} ∈ allocationsUniverse" using subsetAllocation lm003 by (metis (lifting, mono_tags) empty_subsetI) lemma lm006: assumes "G ≠ {}" shows "{G} ∈ all_partitions G" using all_partitions_def is_partition_of_def is_non_overlapping_def assms by force lemma lm007: assumes "n ∈ N" shows "{(G,n)} ∈ totalRels {G} N" using assms by force lemma lm008: assumes "n∈N" shows "{(G,n)} ∈ injections {G} N" using assms injections_def singlePairInInjectionsUniverse by fastforce corollary lm009: assumes " G≠{}" "n∈N" shows "{(G,n)} ∈ possible_allocations_rel G N" proof - have "{(G,n)} ∈ injections {G} N" using assms lm008 by fast moreover have "{G} ∈ all_partitions G" using assms lm006 by metis ultimately show ?thesis by auto qed corollary lm010: assumes "N ≠ {}" "G≠{}" shows "allAllocations N G ≠ {}" using assms lm009 by (metis (opaque_lifting, no_types) equals0I image_insert insert_absorb insert_not_empty) corollary lm011: assumes "N ≠ {}" "finite N" "G ≠ {}" "finite G" shows "winningAllocationsRel N G bids ≠ {} & finite (winningAllocationsRel N G bids)" using assms lm010 allAllocationsFinite argmax_non_empty_iff by (metis winningAllocationPossible rev_finite_subset) lemma lm012: "allAllocations N {} ⊆ {{}}" using emptyset_part_emptyset3 rangeEmpty characterizationallAllocations mem_Collect_eq subsetI vimage_def by metis lemma lm013: assumes "a ∈ allAllocations N G" "finite G" shows "finite (Range a)" using assms elementOfPartitionOfFiniteSetIsFinite by (metis allocationReverseInjective) corollary allocationFinite: assumes "a ∈ allAllocations N G" "finite G" shows "finite a" using assms finite_converse Range_converse imageE allocationProperty finiteDomainImpliesFinite lm013 by (metis (erased, lifting)) lemma lm014: assumes "a ∈ allAllocations N G" "finite G" shows "∀ y ∈ Range a. finite y" using assms is_partition_of_def allocationInverseRangeDomainProperty by (metis Union_upper rev_finite_subset) (* Note that allocations are strict, that is, all goods are allocated to the bidders at this point. Later we will have the seller as participant 0 getting all goods not allocated *) corollary lm015: assumes "a ∈ allAllocations N G" "finite G" shows "card G = sum card (Range a)" using assms cardSumCommute lm013 allocationInverseRangeDomainProperty by (metis is_partition_of_def) subsection ‹Results on summed bid vectors› lemma lm016: "summedBidVectorRel bids N G = {(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair)))| pair. pair ∈ N × (Pow G-{{}})}" by blast (* Note that || stands for restriction, here to an allocation a *) corollary lm017: "{(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ (N × (Pow G-{{}})) } || a = {(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ (N × (Pow G-{{}})) ∩ a}" by (metis restrictionVsIntersection) corollary lm018: "(summedBidVectorRel bids N G) || a = {(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ (N × (Pow G - {{}})) ∩ a}" (is "?L = ?R") proof - let ?l = summedBidVectorRel let ?M = "{(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ N × (Pow G-{{}})}" have "?l bids N G = ?M" by (rule lm016) then have "?L = (?M || a)" by presburger moreover have "... = ?R" by (rule lm017) ultimately show ?thesis by simp qed lemma lm019: "(summedBid bids) ` ((N × (Pow G - {{}})) ∩ a) = {(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ (N × (Pow G - {{}})) ∩ a}" by blast corollary lm020: "(summedBidVectorRel bids N G) || a = (summedBid bids) ` ((N × (Pow G - {{}})) ∩ a)" (is "?L=?R") proof - let ?l=summedBidVectorRel let ?p=summedBid let ?M="{(pair, sum (%g. bids (fst pair, g)) (finestpart (snd pair))) | pair. pair ∈ (N × (Pow G - {{}})) ∩ a}" have "?L = ?M" by (rule lm018) moreover have "... = ?R" using lm019 by blast ultimately show ?thesis by simp qed (* the function made by (summedBid bids) is always injective, that is, also with domain UNIV *) lemma summedBidInjective: "inj_on (summedBid bids) UNIV" using fst_conv inj_on_inverseI by (metis (lifting)) (* restrict above to any set X *) corollary lm021: "inj_on (summedBid bids) X" using fst_conv inj_on_inverseI by (metis (lifting)) (* relationship between different formalizations of summedBid *) lemma lm022: "sum snd (summedBidVectorRel bids N G) = sum (snd ∘ (summedBid bids)) (N × (Pow G - {{}}))" using lm021 sum.reindex by blast (* remember: omega of (1,{11,12,13}) is {(1,{11}), (1,{12}), (1,{13})} *) corollary lm023: "snd (summedBid bids pair) = sum bids (omega pair)" using sumCurry by force (* restatement of the above *) corollary lm024: "snd ∘ summedBid bids = (sum bids) ∘ omega" using lm023 by fastforce lemma lm025: assumes "finite (finestpart (snd pair))" shows "card (omega pair) = card (finestpart (snd pair))" using assms by force corollary lm026: assumes "finite (snd pair)" shows "card (omega pair) = card (snd pair)" using assms cardFinestpart card_cartesian_product_singleton by metis lemma lm027: assumes "{} ∉ Range f" "runiq f" shows "is_non_overlapping (omega ` f)" proof - let ?X="omega ` f" let ?p=finestpart { fix y1 y2 assume "y1 ∈ ?X ∧ y2 ∈ ?X" then obtain pair1 pair2 where "y1 = omega pair1 & y2 = omega pair2 & pair1 ∈ f & pair2 ∈ f" by blast then moreover have "snd pair1 ≠ {} & snd pair1 ≠ {}" using assms by (metis rev_image_eqI snd_eq_Range) ultimately moreover have "fst pair1 = fst pair2 ⟷ pair1 = pair2" using assms runiq_basic surjective_pairing by metis ultimately moreover have "y1 ∩ y2 ≠ {} ⟶ y1 = y2" using assms by fast ultimately have "y1 = y2 ⟷ y1 ∩ y2 ≠ {}" using assms notEmptyFinestpart by (metis Int_absorb Times_empty insert_not_empty) } thus ?thesis using is_non_overlapping_def by (metis (lifting, no_types) inf_commute inf_sup_aci(1)) qed lemma lm028: assumes "{} ∉ Range X" shows "inj_on omega X" proof - let ?p=finestpart { fix pair1 pair2 assume "pair1 ∈ X & pair2 ∈ X" then have "snd pair1 ≠ {} & snd pair2 ≠ {}" using assms by (metis Range.intros surjective_pairing) moreover assume "omega pair1 = omega pair2" then moreover have "?p (snd pair1) = ?p (snd pair2)" by blast then moreover have "snd pair1 = snd pair2" by (metis finestPart nonEqualitySetOfSets) ultimately moreover have "{fst pair1} = {fst pair2}" using notEmptyFinestpart by (metis fst_image_times) ultimately have "pair1 = pair2" by (metis prod_eqI singleton_inject) } thus ?thesis by (metis (lifting, no_types) inj_onI) qed lemma lm029: assumes "{} ∉ Range a" "∀X ∈ omega ` a. finite X" "is_non_overlapping (omega ` a)" shows "card (pseudoAllocation a) = sum (card ∘ omega) a" (is "?L = ?R") proof - have "?L = sum card (omega ` a)" unfolding pseudoAllocation_def using assms by (simp add: cardinalityPreservation) moreover have "... = ?R" using assms(1) lm028 sum.reindex by blast ultimately show ?thesis by simp qed lemma lm030: "card (omega pair)= card (snd pair)" using cardFinestpart card_cartesian_product_singleton by metis corollary lm031: "card ∘ omega = card ∘ snd" using lm030 by fastforce (* set image of omega on a set of pair is called pseudoAllocation *) corollary lm032: assumes "{} ∉ Range a" "∀ pair ∈ a. finite (snd pair)" "finite a" "runiq a" shows "card (pseudoAllocation a) = sum (card ∘ snd) a" proof - let ?P=pseudoAllocation let ?c=card have "∀ pair ∈ a. finite (omega pair)" using finiteFinestpart assms by blast moreover have "is_non_overlapping (omega ` a)" using assms lm027 by force ultimately have "?c (?P a) = sum (?c ∘ omega) a" using assms lm029 by force moreover have "... = sum (?c ∘ snd) a" using lm031 by metis ultimately show ?thesis by simp qed corollary lm033: assumes "runiq (a^-1)" "runiq a" "finite a" "{} ∉ Range a" "∀ pair ∈ a. finite (snd pair)" shows "card (pseudoAllocation a) = sum card (Range a)" using assms sumPairsInverse lm032 by force corollary lm034: assumes "a ∈ allAllocations N G" "finite G" shows "card (pseudoAllocation a) = card G" proof - have "{} ∉ Range a" using assms by (metis emptyNotInRange) moreover have "∀ pair ∈ a. finite (snd pair)" using assms lm014 finitePairSecondRange by metis moreover have "finite a" using assms allocationFinite by blast moreover have "runiq a" using assms by (metis (lifting) Int_lower1 in_mono allocationInjectionsUnivervseProperty mem_Collect_eq) moreover have "runiq (a^-1)" using assms by (metis (mono_tags) injections_def characterizationallAllocations mem_Collect_eq) ultimately have "card (pseudoAllocation a) = sum card (Range a)" using lm033 by fast moreover have "... = card G" using assms lm015 by metis ultimately show ?thesis by simp qed corollary lm035: assumes "pseudoAllocation aa ⊆ pseudoAllocation a ∪ (N × (finestpart G))" "finite (pseudoAllocation aa)" shows "sum (toFunction (bidMaximizedBy a N G)) (pseudoAllocation a) - (sum (toFunction (bidMaximizedBy a N G)) (pseudoAllocation aa)) = card (pseudoAllocation a) - card (pseudoAllocation aa ∩ (pseudoAllocation a))" using assms subsetCardinality by blast corollary lm036: assumes "pseudoAllocation aa ⊆ pseudoAllocation a ∪ (N × (finestpart G))" "finite (pseudoAllocation aa)" shows "int (sum (maxbid a N G) (pseudoAllocation a)) - int (sum (maxbid a N G) (pseudoAllocation aa)) = int (card (pseudoAllocation a)) - int (card (pseudoAllocation aa ∩ (pseudoAllocation a)))" using differenceSumVsCardinality assms by blast lemma lm037: "pseudoAllocation {} = {}" unfolding pseudoAllocation_def by simp corollary lm038: assumes "a ∈ allAllocations N {}" shows "(pseudoAllocation a) = {}" unfolding pseudoAllocation_def using assms lm012 by blast corollary lm039: assumes "a ∈ allAllocations N G" "finite G" "G ≠ {}" shows "finite (pseudoAllocation a)" proof - have "card (pseudoAllocation a) = card G" using assms(1,2) lm034 by blast thus "finite (pseudoAllocation a)" using assms(2,3) by fastforce qed corollary lm040: assumes "a ∈ allAllocations N G" "finite G" shows "finite (pseudoAllocation a)" using assms finite.emptyI lm039 lm038 by (metis (no_types)) lemma lm041: assumes "a ∈ allAllocations N G" "aa ∈ allAllocations N G" "finite G" shows "(card (pseudoAllocation aa ∩ (pseudoAllocation a)) = card (pseudoAllocation a)) = (pseudoAllocation a = pseudoAllocation aa)" proof - let ?P=pseudoAllocation let ?c=card let ?A="?P a" let ?AA="?P aa" have "?c ?A=?c G & ?c ?AA=?c G" using assms lm034 by (metis (lifting, mono_tags)) moreover have "finite ?A & finite ?AA" using assms lm040 by blast ultimately show ?thesis using assms cardinalityIntersectionEquality by (metis(no_types,lifting)) qed (* alternative definition for omega *) lemma lm042: "omega pair = {fst pair} × {{y}| y. y ∈ snd pair}" using finestpart_def finestPart by auto (* variant of above *) lemma lm043: "omega pair = {(fst pair, {y})| y. y ∈ snd pair}" using lm042 setOfPairs by metis lemma lm044: "pseudoAllocation a = ⋃ {{(fst pair, {y})| y. y ∈ snd pair}| pair. pair ∈ a}" unfolding pseudoAllocation_def using lm043 by blast lemma lm045: "⋃ {{(fst pair, {y})| y. y ∈ snd pair}| pair. pair ∈ a} = {(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ a}" by blast corollary lm046: "pseudoAllocation a = {(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ a}" unfolding pseudoAllocation_def using setOfPairsEquality by fastforce lemma lm047: assumes "runiq a" shows "{(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ a} = {(x, Y)| Y x. Y ∈ finestpart (a,,x) & x ∈ Domain a}" (is "?L=?R") using assms Domain.DomainI fst_conv functionOnFirstEqualsSecond runiq_wrt_ex1 surjective_pairing by (metis(opaque_lifting,no_types)) corollary lm048: assumes "runiq a" shows "pseudoAllocation a = {(x, Y)| Y x. Y ∈ finestpart (a,,x) & x ∈ Domain a}" unfolding pseudoAllocation_def using assms lm047 lm046 by fastforce corollary lm049: "Range (pseudoAllocation a) = ⋃ (finestpart ` (Range a))" unfolding pseudoAllocation_def using lm046 rangeSetOfPairs unionFinestPart by fastforce corollary lm050: "Range (pseudoAllocation a) = finestpart (⋃ (Range a))" using commuteUnionFinestpart lm049 by metis lemma lm051: "pseudoAllocation a = {(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ a}" using lm044 lm045 by (metis (no_types)) lemma lm052: "{(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ a} = {(x, {y})| x y. y ∈ ⋃ (a``{x}) & x ∈ Domain a}" by auto lemma lm053: "pseudoAllocation a = {(x, {y})| x y. y ∈ ⋃ (a``{x}) & x ∈ Domain a}" (is "?L=?R") proof - have "?L={(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ a}" by (rule lm051) moreover have "... = ?R" by (rule lm052) ultimately show ?thesis by simp qed lemma lm054: "runiq (summedBidVectorRel bids N G)" using graph_def image_Collect_mem domainOfGraph by (metis(no_types)) corollary lm055: "runiq (summedBidVectorRel bids N G || a)" unfolding restrict_def using lm054 subrel_runiq Int_commute by blast lemma summedBidVectorCharacterization: "N × (Pow G - {{}}) = Domain (summedBidVectorRel bids N G)" by blast corollary lm056: assumes "a ∈ allAllocations N G" shows "a ⊆ Domain (summedBidVectorRel bids N G)" proof - let ?p=allAllocations let ?L=summedBidVectorRel have "a ⊆ N × (Pow G - {{}})" using assms allocationPowerset by (metis(no_types)) moreover have "N × (Pow G - {{}}) = Domain (?L bids N G)" using summedBidVectorCharacterization by blast ultimately show ?thesis by blast qed corollary lm057: "sum (summedBidVector bids N G) (a ∩ (Domain (summedBidVectorRel bids N G))) = sum snd ((summedBidVectorRel bids N G) || a)" using sumRestrictedToDomainInvariant lm055 by fast corollary lm058: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum snd ((summedBidVectorRel bids N G) || a)" proof - let ?l=summedBidVector let ?L=summedBidVectorRel have "a ⊆ Domain (?L bids N G)" using assms by (rule lm056) then have "a = a ∩ Domain (?L bids N G)" by blast then have "sum (?l bids N G) a = sum (?l bids N G) (a ∩ Domain (?L bids N G))" by presburger thus ?thesis using lm057 by auto qed corollary lm059: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum snd ((summedBid bids) ` ((N × (Pow G - {{}})) ∩ a))" (is "?X=?R") proof - let ?p = summedBid let ?L = summedBidVectorRel let ?l = summedBidVector let ?A = "N × (Pow G - {{}})" let ?inner2 = "(?p bids)`(?A ∩ a)" let ?inner1 = "(?L bids N G)||a" have "?R = sum snd ?inner1" using assms lm020 by (metis (no_types)) moreover have "sum (?l bids N G) a = sum snd ?inner1" using assms by (rule lm058) ultimately show ?thesis by simp qed corollary lm060: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum snd ((summedBid bids) ` a)" (is "?L=?R") proof - let ?p=summedBid let ?l=summedBidVector have "?L = sum snd ((?p bids)`((N × (Pow G - {{}}))∩ a))" using assms by (rule lm059) moreover have "... = ?R" using assms allocationPowerset Int_absorb1 by (metis (no_types)) ultimately show ?thesis by simp qed corollary lm061: "sum snd ((summedBid bids) ` a) = sum (snd ∘ (summedBid bids)) a" using sum.reindex lm021 by blast corollary lm062: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum (snd ∘ (summedBid bids)) a" (is "?L=?R") proof - let ?p = summedBid let ?l = summedBidVector have "?L = sum snd ((?p bids)` a)" using assms by (rule lm060) moreover have "... = ?R" using assms lm061 by blast ultimately show ?thesis by simp qed corollary lm063: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum ((sum bids) ∘ omega) a" (is "?L=?R") proof - let ?inner1 = "snd ∘ (summedBid bids)" let ?inner2="(sum bids) ∘ omega" let ?M="sum ?inner1 a" have "?L = ?M" using assms by (rule lm062) moreover have "?inner1 = ?inner2" using lm023 assms by fastforce ultimately show "?L = ?R" using assms by metis qed corollary lm064: assumes "a ∈ allAllocations N G" shows "sum (summedBidVector bids N G) a = sum (sum bids) (omega` a)" proof - have "{} ∉ Range a" using assms by (metis emptyNotInRange) then have "inj_on omega a" using lm028 by blast then have "sum (sum bids) (omega ` a) = sum ((sum bids) ∘ omega) a" by (rule sum.reindex) moreover have "sum (summedBidVector bids N G) a = sum ((sum bids) ∘ omega) a" using assms lm063 by (rule Extraction.exE_realizer) ultimately show ?thesis by presburger qed lemma lm065: assumes "finite (snd pair)" shows "finite (omega pair)" using assms finite.emptyI finite.insertI finite_SigmaI finiteFinestpart by (metis(no_types)) corollary lm066: assumes "∀y∈(Range a). finite y" shows "∀y∈(omega ` a). finite y" using assms lm065 imageE finitePairSecondRange by fast corollary lm067: assumes "a ∈ allAllocations N G" "finite G" shows "∀x∈(omega ` a). finite x" using assms lm066 lm014 by (metis(no_types)) corollary lm068: assumes "a ∈ allAllocations N G" shows "is_non_overlapping (omega ` a)" proof - have "runiq a" by (metis (no_types) assms image_iff allocationRightUniqueRangeDomain) moreover have "{} ∉ Range a" using assms by (metis emptyNotInRange) ultimately show ?thesis using lm027 by blast qed lemma lm069: assumes "a ∈ allAllocations N G" "finite G" shows "sum (sum bids) (omega` a) = sum bids (⋃ (omega ` a))" using assms sumUnionDisjoint2 lm068 lm067 by (metis (lifting, mono_tags)) corollary lm070: assumes "a ∈ allAllocations N G" "finite G" shows "sum (summedBidVector bids N G) a = sum bids (pseudoAllocation a)" (is "?L = ?R") proof - have "?L = sum (sum bids) (omega `a)" using assms lm064 by blast moreover have "... = sum bids (⋃ (omega ` a))" using assms lm069 by blast ultimately show ?thesis unfolding pseudoAllocation_def by presburger qed lemma lm071: "Domain (pseudoAllocation a) ⊆ Domain a" unfolding pseudoAllocation_def by fastforce corollary lm072: assumes "a ∈ allAllocations N G" shows "Domain (pseudoAllocation a) ⊆ N & Range (pseudoAllocation a) = finestpart G" using assms lm071 allocationInverseRangeDomainProperty lm050 is_partition_of_def subset_trans by (metis(no_types)) corollary lm073: assumes "a ∈ allAllocations N G" shows "pseudoAllocation a ⊆ N × finestpart G" proof - let ?p = pseudoAllocation let ?aa = "?p a" let ?d = Domain let ?r = Range have "?d ?aa ⊆ N" using assms lm072 by (metis (lifting, mono_tags)) moreover have "?r ?aa ⊆ finestpart G" using assms lm072 by (metis (lifting, mono_tags) equalityE) ultimately have "?d ?aa × (?r ?aa) ⊆ N × finestpart G" by auto then show "?aa ⊆ N × finestpart G" by auto qed subsection ‹From Pseudo-allocations to allocations› (* pseudoAllocationInv inverts pseudoAllocation *) abbreviation "pseudoAllocationInv pseudo == {(x, ⋃ (pseudo `` {x}))| x. x ∈ Domain pseudo}" lemma lm074: assumes "runiq a" "{} ∉ Range a" shows "a = pseudoAllocationInv (pseudoAllocation a)" proof - let ?p="{(x, Y)| Y x. Y ∈ finestpart (a,,x) & x ∈ Domain a}" let ?a="{(x, ⋃ (?p `` {x}))| x. x ∈ Domain ?p}" have "∀x ∈ Domain a. a,,x ≠ {}" by (metis assms eval_runiq_in_Range) then have "∀x ∈ Domain a. finestpart (a,,x) ≠ {}" by (metis notEmptyFinestpart) then have "Domain a ⊆ Domain ?p" by force moreover have "Domain a ⊇ Domain ?p" by fast ultimately have 1: "Domain a = Domain ?p" by fast { fix z assume "z ∈ ?a" then obtain x where "x ∈ Domain ?p & z=(x , ⋃ (?p `` {x}))" by blast then have "x ∈ Domain a & z=(x , ⋃ (?p `` {x}))" by fast then moreover have "?p``{x} = finestpart (a,,x)" using assms by fastforce moreover have "⋃ (finestpart (a,,x))= a,,x" by (metis finestPartUnion) ultimately have "z ∈ a" by (metis assms(1) eval_runiq_rel) } then have 2: "?a ⊆ a" by fast { fix z assume 0: "z ∈ a" let ?x="fst z" let ?Y="a,,?x" let ?YY="finestpart ?Y" have "z ∈ a & ?x ∈ Domain a" using 0 by (metis fst_eq_Domain rev_image_eqI) then have 3: "z ∈ a & ?x ∈ Domain ?p" using 1 by presburger then have "?p `` {?x} = ?YY" by fastforce then have "⋃ (?p `` {?x}) = ?Y" by (metis finestPartUnion) moreover have "z = (?x, ?Y)" using assms by (metis "0" functionOnFirstEqualsSecond surjective_pairing) ultimately have "z ∈ ?a" using 3 by (metis (lifting, mono_tags) mem_Collect_eq) } then have "a = ?a" using 2 by blast moreover have "?p = pseudoAllocation a" using lm048 assms by (metis (lifting, mono_tags)) ultimately show ?thesis by auto qed corollary lm075: assumes "a ∈ runiqs ∩ Pow (UNIV × (UNIV - {{}}))" shows "(pseudoAllocationInv ∘ pseudoAllocation) a = id a" proof - have "runiq a" using runiqs_def assms by fast moreover have "{} ∉ Range a" using assms by blast ultimately show ?thesis using lm074 by fastforce qed lemma lm076: "inj_on (pseudoAllocationInv ∘ pseudoAllocation) (runiqs ∩ Pow (UNIV × (UNIV - {{}})))" proof - let ?ne="Pow (UNIV × (UNIV - {{}}))" let ?X="runiqs ∩ ?ne" let ?f="pseudoAllocationInv ∘ pseudoAllocation" have "∀a1 ∈ ?X. ∀ a2 ∈ ?X. ?f a1 = ?f a2 ⟶ id a1 = id a2" using lm075 by blast then have "∀a1 ∈ ?X. ∀ a2 ∈ ?X. ?f a1 = ?f a2 ⟶ a1 = a2" by auto thus ?thesis unfolding inj_on_def by blast qed corollary lm077: "inj_on pseudoAllocation (runiqs ∩ Pow (UNIV × (UNIV - {{}})))" using lm076 inj_on_imageI2 by blast lemma lm078: "injectionsUniverse ⊆ runiqs" using runiqs_def Collect_conj_eq Int_lower1 by metis lemma lm079: "partitionValuedUniverse ⊆ Pow (UNIV × (UNIV - {{}}))" using is_non_overlapping_def by force corollary lm080: "allocationsUniverse ⊆ runiqs ∩ Pow (UNIV × (UNIV - {{}}))" using lm078 lm079 by auto corollary lm081: "inj_on pseudoAllocation allocationsUniverse" using lm077 lm080 subset_inj_on by blast corollary lm082: "inj_on pseudoAllocation (allAllocations N G)" proof - have "allAllocations N G ⊆ allocationsUniverse" by (metis (no_types) allAllocationsUniverse) thus "inj_on pseudoAllocation (allAllocations N G)" using lm081 subset_inj_on by blast qed lemma lm083: assumes "card N > 0" "distinct G" shows "winningAllocationsRel N (set G) bids ⊆ set (allAllocationsAlg N G)" using assms winningAllocationPossible allAllocationsBridgingLemma by (metis(no_types)) corollary lm084: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" shows "winningAllocationsRel N (set G) bids ∩ set (allAllocationsAlg N G) ≠ {}" proof - let ?w = winningAllocationsRel let ?a = allAllocationsAlg let ?G = "set G" have "card N > 0" using assms by (metis card_gt_0_iff) then have "?w N ?G bids ⊆ set (?a N G)" using lm083 by (metis assms(3)) then show ?thesis using assms lm011 by (metis List.finite_set le_iff_inf) qed (* -` is the reverse image *) lemma lm085: "X = (%x. x ∈ X) -`{True}" by blast corollary lm086: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" shows "(%x. x∈winningAllocationsRel N (set G) bids)-`{True} ∩ set (allAllocationsAlg N G) ≠ {}" using assms lm084 lm085 by metis lemma lm087: assumes "P -` {True} ∩ set l ≠ {}" shows "takeAll P l ≠ []" using assms nonEmptyListFiltered filterpositions2_def by (metis Nil_is_map_conv) corollary lm088: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" shows "takeAll (%x. x ∈ winningAllocationsRel N (set G) bids) (allAllocationsAlg N G) ≠ []" using assms lm087 lm086 by metis corollary lm089: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" shows "perm2 (takeAll (%x. x ∈ winningAllocationsRel N (set G) bids) (allAllocationsAlg N G)) n ≠ []" using assms permutationNotEmpty lm088 by metis (* The chosen allocation is in the set of possible winning allocations *) corollary lm090: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" shows "chosenAllocation N G bids random ∈ winningAllocationsRel N (set G) bids" proof - have "⋀x⇩_{1}b_x x. set x⇩_{1}= {} ∨ (randomEl x⇩_{1}b_x::('a × 'b set) set) ∈ x ∨ ¬ set x⇩_{1}⊆ x" by (metis (no_types) randomElLemma subsetCE) thus "winningAllocationRel N (set G) ((∈) (randomEl (takeAll (λx. winningAllocationRel N (set G) ((∈) x) bids) (allAllocationsAlg N G)) random)) bids" by (metis lm088 assms(1) assms(2) assms(3) assms(4) takeAllSubset set_empty) qed (* The following lemma proves a property of maxbid, which in the following will be proved to maximize the revenue. a and aa are allocations. *) lemma lm091: assumes "finite G" "a ∈ allAllocations N G" "aa ∈ allAllocations N G" shows "real(sum(maxbid a N G)(pseudoAllocation a)) - sum(maxbid a N G)(pseudoAllocation aa) = real (card G) - card (pseudoAllocation aa ∩ (pseudoAllocation a))" proof - let ?p = pseudoAllocation let ?f = finestpart let ?m = maxbid let ?B = "?m a N G" have "?p aa ⊆ N × ?f G" using assms lm073 by (metis (lifting, mono_tags)) then have "?p aa ⊆ ?p a ∪ (N × ?f G)" by auto moreover have "finite (?p aa)" using assms lm034 lm040 by blast ultimately have "real(sum ?B (?p a)) - sum ?B (?p aa) = real(card (?p a))-card(?p aa ∩ (?p a))" using differenceSumVsCardinalityReal by fast moreover have "... = real (card G) - card (?p aa ∩ (?p a))" using assms lm034 by (metis (lifting, mono_tags)) ultimately show ?thesis by simp qed lemma lm092: "summedBidVectorRel bids N G = graph (N × (Pow G-{{}})) (summedBidSecond bids)" unfolding graph_def using lm016 by blast lemma lm093: assumes "x∈X" shows "toFunction (graph X f) x = f x" using assms by (metis graphEqImage toFunction_def) corollary lm094: assumes "pair ∈ N × (Pow G-{{}})" shows "summedBidVector bids N G pair = summedBidSecond bids pair" using assms lm093 lm092 by (metis(mono_tags)) (* type conversion to real commutes *) lemma lm095: "summedBidSecond (real ∘ ((bids:: _ => nat))) pair = real (summedBidSecond bids pair)" by simp lemma lm096: assumes "pair ∈ N × (Pow G-{{}})" shows "summedBidVector (real∘(bids:: _ => nat)) N G pair = real (summedBidVector bids N G pair)" using assms lm094 lm095 by (metis(no_types)) (* TPTP?*) corollary lm097: assumes "X ⊆ N × (Pow G - {{}})" shows "∀pair ∈ X. summedBidVector (real ∘ (bids::_=>nat)) N G pair = (real ∘ (summedBidVector bids N G)) pair" proof - { fix esk48⇩_{0}:: "'a × 'b set" { assume "esk48⇩_{0}∈ N × (Pow G - {{}})" hence "summedBidVector (real ∘ bids) N G esk48⇩_{0}= real (summedBidVector bids N G esk48⇩_{0})" using lm096 by blast hence "esk48⇩_{0}∉ X ∨ summedBidVector (real ∘ bids) N G esk48⇩_{0}= (real ∘ summedBidVector bids N G) esk48⇩_{0}" by simp } hence "esk48⇩_{0}∉ X ∨ summedBidVector (real ∘ bids) N G esk48⇩_{0}= (real ∘ summedBidVector bids N G) esk48⇩_{0}" using assms by blast } thus "∀pair∈X. summedBidVector (real ∘ bids) N G pair = (real ∘ summedBidVector bids N G) pair" by blast qed corollary lm098: assumes "aa ⊆ N × (Pow G-{{}})" shows "sum ((summedBidVector (real ∘ (bids::_=>nat)) N G)) aa = real (sum ((summedBidVector bids N G)) aa)" (is "?L=?R") proof - have "∀ pair ∈ aa. summedBidVector (real ∘ bids) N G pair = (real ∘ (summedBidVector bids N G)) pair" using assms by (rule lm097) then have "?L = sum (real∘(summedBidVector bids N G)) aa" using sum.cong by force then show ?thesis by simp qed corollary lm099: assumes "aa ∈ allAllocations N G" shows "sum ((summedBidVector (real ∘ (bids::_=>nat)) N G)) aa = real (sum ((summedBidVector bids N G)) aa)" using assms lm098 allocationPowerset by (metis(lifting,mono_tags)) corollary lm100: assumes "finite G" "a ∈ allAllocations N G" "aa ∈ allAllocations N G" shows "real (sum (tiebids a N G) a) - sum (tiebids a N G) aa = real (card G) - card (pseudoAllocation aa ∩ (pseudoAllocation a))" (is "?L=?R") proof - let ?l=summedBidVector let ?m=maxbid let ?s=sum let ?p=pseudoAllocation let ?bb="?m a N G" let ?b="real ∘ (?m a N G)" have "real (?s ?bb (?p a)) - (?s ?bb (?p aa)) = ?R" using assms lm091 by blast then have 1: "?R = real (?s ?bb (?p a)) - (?s ?bb (?p aa))" by simp have " ?s (?l ?b N G) aa = ?s ?b (?p aa)" using assms lm070 by blast moreover have "... = ?s ?bb (?p aa)" by fastforce moreover have "(?s (?l ?b N G) aa) = real (?s (?l ?bb N G) aa)" using assms(3) by (rule lm099) ultimately have 2: "?R = real (?s ?bb (?p a)) - (?s (?l ?bb N G) aa)" by (metis 1) have "?s (?l ?b N G) a=(?s ?b (?p a))" using assms lm070 by blast moreover have "... = ?s ?bb (?p a)" by force moreover have "... = real (?s ?bb (?p a))" by fast moreover have "?s (?l ?b N G) a = real (?s (?l ?bb N G) a)" using assms(2) by (rule lm099) ultimately have "?s (?l ?bb N G) a = real (?s ?bb (?p a))" by simp thus ?thesis using 2 by simp qed corollary lm101: assumes "finite G" "a ∈ allAllocations N G" "aa ∈ allAllocations N G" "x = real (sum (tiebids a N G) a) - sum (tiebids a N G) aa" shows "x <= card G & x ≥ 0 & (x=0 ⟷ a = aa) & (aa ≠ a ⟶ sum (tiebids a N G) aa < sum (tiebids a N G) a)" proof - let ?p = pseudoAllocation have "real (card G) >= real (card G) - card (?p aa ∩ (?p a))" by force moreover have "real (sum (tiebids a N G) a) - sum (tiebids a N G) aa = real (card G) - card (pseudoAllocation aa ∩ (pseudoAllocation a))" using assms lm100 by blast ultimately have 1: "x=real(card G)-card(pseudoAllocation aa∩(pseudoAllocation a))" using assms by force then have 2: "x ≤ real (card G)" using assms by linarith have 3: "card (?p aa) = card G & card (?p a) = card G" using assms lm034 by blast moreover have "finite (?p aa) & finite (?p a)" using assms lm040 by blast ultimately have "card (?p aa ∩ ?p a) ≤ card G" using Int_lower2 card_mono by fastforce then have 4: "x ≥ 0" using assms lm100 1 by linarith have "card (?p aa ∩ (?p a)) = card G ⟷ (?p aa = ?p a)" using 3 lm041 4 assms by (metis (lifting, mono_tags)) moreover have "?p aa = ?p a ⟶ a = aa" using assms lm082 inj_on_def by (metis (lifting, mono_tags)) ultimately have "card (?p aa ∩ (?p a)) = card G ⟷ (a=aa)" by blast moreover have "x = real (card G) - card (?p aa ∩ (?p a))" using assms lm100 by blast ultimately have 5: "x = 0 ⟷ (a=aa)" by linarith then have "aa ≠ a ⟶ sum (tiebids a N G) aa < real (sum (tiebids a N G) a)" using 1 4 assms by auto thus ?thesis using 2 4 5 unfolding of_nat_less_iff by force qed (* If for an arbitrary allocation a we compute tiebids for it then the corresponding revenue is strictly maximal. *) corollary lm102: assumes "finite G" "a ∈ allAllocations N G" "aa ∈ allAllocations N G" "aa ≠ a" shows "sum (tiebids a N G) aa < sum (tiebids a N G) a" using assms lm101 by blast lemma lm103: assumes "N ≠ {}" "finite N" "distinct G" "set G ≠ {}" "aa ∈ (allAllocations N (set G))-{chosenAllocation N G bids random}" shows "sum (resolvingBid N G bids random) aa < sum (resolvingBid N G bids random) (chosenAllocation N G bids random)" proof - let ?a="chosenAllocation N G bids random" let ?p=allAllocations let ?G="set G" have "?a ∈ winningAllocationsRel N (set G) bids" using assms lm090 by blast moreover have "winningAllocationsRel N (set G) bids ⊆ ?p N ?G" using assms winningAllocationPossible by metis ultimately have "?a ∈ ?p N ?G" using lm090 assms winningAllocationPossible rev_subsetD by blast then show ?thesis using assms lm102 by blast qed (* putting together the two rounds in the auction, first using the bids, then the random values. *) abbreviation "terminatingAuctionRel N G bids random == argmax (sum (resolvingBid N G bids random)) (argmax (sum bids) (allAllocations N (set G)))" text‹Termination theorem: it assures that the number of winning allocations is exactly one› theorem winningAllocationUniqueness: assumes "N ≠ {}" "distinct G" "set G ≠ {}" "finite N" shows "terminatingAuctionRel N G (bids) random = {chosenAllocation N G bids random}" proof - let ?p = allAllocations let ?G = "set G" let ?X = "argmax (sum bids) (?p N ?G)" let ?a = "chosenAllocation N G bids random" let ?b = "resolvingBid N G bids random" let ?f = "sum ?b" let ?t=terminatingAuctionRel have "∀aa ∈ (allAllocations N ?G)-{?a}. ?f aa < ?f ?a" using assms lm103 by blast then have "∀aa ∈ ?X-{?a}. ?f aa < ?f ?a" using assms lm103 by auto moreover have "finite N" using assms by simp then have "finite (?p N ?G)" using assms allAllocationsFinite by (metis List.finite_set) then have "finite ?X" using assms by (metis finite_subset winningAllocationPossible) moreover have "?a ∈ ?X" using lm090 assms by blast ultimately have "finite ?X & ?a ∈ ?X & (∀aa ∈ ?X-{?a}. ?f aa < ?f ?a)" by force moreover have "(finite ?X & ?a ∈ ?X & (∀aa ∈ ?X-{?a}. ?f aa < ?f ?a)) ⟶ argmax ?f ?X = {?a}" by (rule argmaxProperty) ultimately have "{?a} = argmax ?f ?X" using injectionsFromEmptyIsEmpty by presburger moreover have "... = ?t N G bids random" by simp ultimately show ?thesis by simp qed text ‹The computable variant of Else is defined next as Elsee.› definition "toFunctionWithFallbackAlg R fallback == (% x. if (x ∈ Domain R) then (R,,x) else fallback)" notation toFunctionWithFallbackAlg (infix "Elsee" 75) end