Theory UniformTieBreaking

```(*
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
(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

```