# Theory CombinatorialAuction

```(*
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 ‹VCG auction: definitions and theorems›

theory CombinatorialAuction

imports
UniformTieBreaking

begin

subsection ‹Definition of a VCG auction scheme, through the pair @{term "(vcga, vcgp)"}›

(* b is a bid vector and participants is the set of all participants present in b *)
abbreviation "participants b == Domain (Domain b)"

(* goods is the list of goods auctioned *)
abbreviation "goods == sorted_list_of_set o Union o Range o Domain"

(* The seller is represented as integer 0, the other particants as integers 1, ..., n *)
abbreviation "seller == (0::integer)"

(* allAllocations' and allAllocations'' are variants of allAllocations. All three formulations are equivent. *)
abbreviation "allAllocations' N Ω ==
injectionsUniverse ∩ {a. Domain a ⊆ N & Range a ∈ all_partitions Ω}"

abbreviation "allAllocations'' N Ω == allocationsUniverse ∩ {a. Domain a ⊆ N & ⋃(Range a) = Ω}"

lemma allAllocationsEquivalence:
"allAllocations N Ω = allAllocations' N Ω & allAllocations N Ω = allAllocations'' N Ω"
using allocationInjectionsUnivervseProperty allAllocationsIntersection by metis

lemma allAllocationsVarCharacterization:
"(a ∈ allAllocations'' N Ω) = (a ∈ allocationsUniverse& Domain a ⊆ N & ⋃(Range a) = Ω)"
by force

(* remove the seller from the set of all allocations *)
abbreviation "soldAllocations N Ω == (Outside' {seller}) ` (allAllocations (N ∪ {seller}) Ω)"

(* soldAllocations' and soldAllocations'' are variants of soldAllocations reflecting the different
formulations of allAllocations. soldAllocations''' is yet another variant. These variants are
used since for different proofs different variants are easier to use. *)
abbreviation "soldAllocations' N Ω == (Outside' {seller}) ` (allAllocations' (N ∪ {seller}) Ω)"
abbreviation "soldAllocations'' N Ω == (Outside' {seller}) ` (allAllocations'' (N ∪ {seller}) Ω)"
abbreviation "soldAllocations''' N Ω ==
allocationsUniverse ∩ {aa. Domain aa⊆N-{seller} & ⋃(Range aa)⊆Ω}"
lemma soldAllocationsEquivalence:
"soldAllocations N Ω = soldAllocations' N Ω &
soldAllocations' N Ω = soldAllocations'' N Ω"
using allAllocationsEquivalence by metis

corollary soldAllocationsEquivalenceVariant:
"soldAllocations = soldAllocations'  &
soldAllocations' = soldAllocations'' &
soldAllocations = soldAllocations''"
using soldAllocationsEquivalence by metis

lemma allocationSellerMonotonicity:
"soldAllocations (N-{seller}) Ω ⊆ soldAllocations N Ω"
using Outside_def by simp

lemma allocationsUniverseCharacterization:
"(a ∈ allocationsUniverse) = (a ∈ allAllocations'' (Domain a) (⋃(Range a)))"
by blast

lemma allocationMonotonicity:
assumes "N1 ⊆ N2"
shows "allAllocations'' N1 Ω ⊆ allAllocations'' N2 Ω"
using assms by auto

lemma allocationWithOneParticipant:
assumes "a ∈ allAllocations'' N Ω"
shows "Domain (a -- x) ⊆ N-{x}"
using assms Outside_def by fastforce

lemma soldAllocationIsAllocation:
assumes "a ∈ soldAllocations N Ω"
shows "a ∈ allocationsUniverse"
proof -
obtain aa where "a  =aa -- seller & aa ∈ allAllocations (N∪{seller}) Ω"
using assms by blast
then have "a ⊆ aa & aa ∈ allocationsUniverse"
unfolding Outside_def using allAllocationsIntersectionSubset by blast
then show ?thesis using subsetAllocation by blast
qed

lemma soldAllocationIsAllocationVariant:
assumes "a ∈ soldAllocations N Ω"
shows "a ∈ allAllocations'' (Domain a) (⋃(Range a))"
proof -
show ?thesis using assms soldAllocationIsAllocation
by auto blast+
qed

lemma onlyGoodsAreSold:
assumes "a ∈ soldAllocations'' N Ω"
shows "⋃ (Range a) ⊆ Ω"
using assms Outside_def by blast

lemma soldAllocationIsRestricted:
"a ∈ soldAllocations'' N Ω =
(∃aa. aa -- (seller) = a  ∧  aa ∈ allAllocations'' (N ∪ {seller}) Ω)"
by blast

(* Note that +* enlarges the function by one additional pair *)
lemma restrictionConservation:
"(R +* ({x}×Y)) -- x = R -- x"
unfolding Outside_def paste_def by blast

assumes "a ∈ allocationsUniverse" "Domain a ⊆ N-{seller}" "⋃ (Range a) ⊆ Ω"
shows "a ∈ soldAllocations'' N Ω"
proof -
let ?i = "seller"
let ?Y = "{Ω-⋃ (Range a)}-{{}}"
let ?b = "{?i}×?Y"
let ?aa = "a∪?b"
let ?aa' = "a +* ?b"
have
1: "a ∈ allocationsUniverse" using assms(1) by fast
have "?b ⊆ {(?i,Ω-⋃(Range a))} - {(?i, {})}" by fastforce
then have
2: "?b ∈ allocationsUniverse"
using allocationUniverseProperty subsetAllocation by (metis(no_types))
have
3: "⋃ (Range a) ∩ ⋃ (Range ?b) = {}" by blast
have
4: "Domain a ∩ Domain ?b ={}" using assms by fast
have "?aa ∈ allocationsUniverse" using 1 2 3 4 by (rule allocationUnion)
then have "?aa ∈ allAllocations'' (Domain ?aa) (⋃ (Range ?aa))"
unfolding allocationsUniverseCharacterization by metis
then have "?aa ∈ allAllocations'' (N∪{?i}) (⋃ (Range ?aa))"
using allocationMonotonicity assms paste_def by auto
moreover have "Range ?aa = Range a ∪ ?Y" by blast
then moreover have "⋃ (Range ?aa) = Ω"
using Un_Diff_cancel Un_Diff_cancel2 Union_Un_distrib Union_empty Union_insert
by (metis (lifting, no_types) assms(3) cSup_singleton subset_Un_eq)
moreover have "?aa' = ?aa" using 4 by (rule paste_disj_domains)
ultimately have "?aa' ∈ allAllocations'' (N∪{?i}) Ω" by simp
moreover have "Domain ?b ⊆ {?i}" by fast
have "?aa' -- ?i = a -- ?i" by (rule restrictionConservation)
moreover have "... = a" using Outside_def assms(2) by auto
ultimately show ?thesis using soldAllocationIsRestricted by auto
qed

lemma allocationCharacterization:
"a ∈ allAllocations N Ω  =
(a ∈ injectionsUniverse & Domain a ⊆ N & Range a ∈ all_partitions Ω)"
by (metis (full_types) posssibleAllocationsRelCharacterization)

(* The lemmas lm01, lm02, lm03, and lm04 are used in order to prove
lemma soldAllocationVariantEquivalence   *)
lemma lm01:
assumes "a ∈ soldAllocations'' N Ω"
shows "Domain a ⊆ N-{seller} & a ∈ allocationsUniverse"
proof -
let ?i = "seller"
obtain aa where
0: "a = aa -- ?i & aa ∈ allAllocations'' (N ∪ {?i}) Ω"
using assms(1) soldAllocationIsRestricted by blast
then have "Domain aa ⊆ N ∪ {?i}" using allocationCharacterization by blast
then have "Domain a ⊆ N - {?i}" using 0 Outside_def by blast
moreover have "a ∈ soldAllocations N Ω" using assms soldAllocationsEquivalenceVariant by metis
then moreover have "a ∈ allocationsUniverse" using soldAllocationIsAllocation by blast
ultimately show ?thesis by blast
qed

corollary lm02:
assumes "a ∈ soldAllocations'' N Ω"
shows "a ∈ allocationsUniverse & Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω"
proof -
have "a ∈ allocationsUniverse" using assms lm01 [of a] by blast
moreover have "Domain a ⊆ N-{seller}" using assms lm01 by blast
moreover have "⋃ (Range a) ⊆ Ω" using assms onlyGoodsAreSold by blast
ultimately show ?thesis by blast
qed

corollary lm03:
"(a ∈ soldAllocations'' N Ω) =
(a ∈ allocationsUniverse & a ∈ {aa. Domain aa ⊆ N-{seller} & ⋃ (Range aa) ⊆ Ω})"
(is "?L = ?R")
proof -
have "(a∈soldAllocations'' N Ω) =
(a∈allocationsUniverse& Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω)"
using lm02 allocatedToBuyerMeansSold by (metis (mono_tags))
then have "?L = (a∈allocationsUniverse& Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω)" by fast
moreover have "... = ?R" using mem_Collect_eq by (metis (lifting, no_types))
ultimately show ?thesis by auto
qed

corollary lm04:
"a ∈ soldAllocations'' N Ω =
(a∈ (allocationsUniverse ∩ {aa. Domain aa ⊆ N-{seller} & ⋃ (Range aa) ⊆ Ω}))"
using lm03 by (metis (mono_tags) Int_iff)

corollary soldAllocationVariantEquivalence:
"soldAllocations'' N Ω = soldAllocations''' N Ω"
(is "?L=?R")
proof -
{
fix a
have "a ∈ ?L = (a ∈ ?R)" by (rule lm04)
}
thus ?thesis by blast
qed

(* We use lm05 in order to show a variant for soldAllocations without ''' *)
lemma lm05:
assumes "a ∈ soldAllocations''' N Ω"
shows "a -- n ∈ soldAllocations''' (N-{n}) Ω"
proof -
let ?bb = seller
let ?d = Domain
let ?r = Range
let ?X1 = "{aa. ?d aa ⊆ N-{n}-{?bb} & ⋃(?r aa)⊆Ω}"
let ?X2 = "{aa. ?d aa ⊆ N-{?bb} & ⋃(?r aa) ⊆ Ω}"
have "a∈?X2" using assms(1) by fast
then have
0: "?d a ⊆ N-{?bb} & ⋃(?r a) ⊆ Ω" by blast
then have "?d (a--n) ⊆ N-{?bb}-{n}"
using outside_reduces_domain by (metis Diff_mono subset_refl)
moreover have "... = N-{n}-{?bb}" by fastforce
ultimately have "?d (a--n) ⊆ N-{n}-{?bb}" by blast
moreover have "⋃ (?r (a--n)) ⊆ Ω"
unfolding Outside_def using 0 by blast
ultimately have "a -- n ∈ ?X1" by fast
moreover have "a--n ∈ allocationsUniverse"
using assms(1) Int_iff allocationsUniverseOutside by (metis(lifting,mono_tags))
ultimately show ?thesis by blast
qed

lemma allAllocationsEquivalenceExtended:
"soldAllocations =  soldAllocations' &
soldAllocations' = soldAllocations'' &
soldAllocations'' = soldAllocations'''"
using soldAllocationVariantEquivalence soldAllocationsEquivalenceVariant by metis

(* The following corollary shows that an allocation is invariant to subtracting a single bidder.
This is used a fundamental step to prove the non-negativity of price in VCG. *)
corollary soldAllocationRestriction:
assumes "a ∈ soldAllocations N Ω"
shows "a -- n ∈ soldAllocations (N-{n}) Ω"
proof -
let ?A' = soldAllocations'''
have "a ∈ ?A' N Ω" using assms allAllocationsEquivalenceExtended by metis
then have "a -- n ∈ ?A' (N-{n}) Ω" by (rule lm05)
thus ?thesis using allAllocationsEquivalenceExtended by metis
qed

corollary allocationGoodsMonotonicity:
assumes "Ω1 ⊆ Ω2"
shows "soldAllocations''' N Ω1 ⊆ soldAllocations''' N Ω2"
using assms by blast

corollary allocationGoodsMonotonicityVariant:
assumes "Ω1 ⊆ Ω2"
shows "soldAllocations'' N Ω1 ⊆ soldAllocations'' N Ω2"
proof -
have "soldAllocations'' N Ω1 = soldAllocations''' N Ω1"
by (rule soldAllocationVariantEquivalence)
moreover have "... ⊆ soldAllocations''' N Ω2"
using assms(1) by (rule allocationGoodsMonotonicity)
moreover have "... = soldAllocations'' N Ω2" using soldAllocationVariantEquivalence by metis
ultimately show ?thesis by auto
qed

(* maximalStrictAllocationsAlg are the allocations maximizing the revenue. They also include the
unallocated goods assigned to the seller (bidder 0).*)
abbreviation "maximalStrictAllocations N Ω b == argmax (sum b) (allAllocations ({seller}∪N) Ω)"

(* randomBids builds up a bid vector from a random number so that bidding with this bid vector
resolves any ties. Details are defined in UniformTieBreaking.thy *)
abbreviation "randomBids N Ω b random == resolvingBid (N∪{seller}) Ω b random"

(* vcgas gives the one-element set with the winning allocation after tie breaking.
(argmax∘sum) b ... determines the set of all maximal allocations.
(argmax∘sum) (randomBids ...) restricts that by tie-breaking to a singleton.
Outside' {seller} removes the seller from the only allocation in the singleton.   *)
abbreviation "vcgas N Ω b r  ==
Outside' {seller} `((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations (N ∪ {seller}) (set Ω))))"

(* Takes the element out of the one elemnt set (vcgas ...) *)
abbreviation "vcga N Ω b r == the_elem (vcgas N Ω b r)"

(* alternative definition of vcga *)
abbreviation "vcga' N Ω b r ==
(the_elem (argmax (sum (randomBids N Ω b r))
(maximalStrictAllocations N (set Ω) b)))
-- seller"

(* The following three auxiliary lemmas, lm06, lm07, and lm08 are used to prove lemma
vcgaEquivalence as well as in the theorem that cardinality of vcgas is one.*)
lemma lm06:
assumes "card ((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) = 1"
shows "vcga N Ω b r =
(the_elem ((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations ({seller}∪N) (set Ω)))))
-- seller"
using assms cardOneTheElem by auto

corollary lm07:
assumes "card ((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) = 1"
shows "vcga N Ω b r = vcga' N Ω b r"
(is "?l = ?r")
proof -
have "?l = (the_elem ((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations ({seller}∪N) (set Ω)))))
-- seller"
using assms by (rule lm06)
moreover have "... = ?r" by force
ultimately show ?thesis by blast
qed

lemma lm08:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "card ((argmax∘sum) (randomBids N Ω bids random)
((argmax∘sum) bids (allAllocations (N∪{seller}) (set Ω)))) = 1"
(is "card ?l=_")
proof -
let ?N = "N∪{seller}"
let ?b' = "randomBids N Ω bids random"
let ?s = sum
let ?a = argmax
let ?f = "?a ∘ ?s"
have
1: "?N≠{}" by auto
have
2: "finite ?N" using assms(3) by simp
have "?a (?s ?b') (?a (?s bids) (allAllocations ?N (set Ω))) =
{chosenAllocation ?N Ω bids random}" (is "?L=?R")
using 1 assms(1) assms(2) 2 by (rule winningAllocationUniqueness)
moreover have "?L= ?f ?b' (?f bids (allAllocations ?N (set Ω)))" by auto
ultimately have "?l = {chosenAllocation ?N Ω bids random}" by simp
moreover have "card ...=1" by simp ultimately show ?thesis by simp
qed

lemma vcgaEquivalence:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcga N Ω b r = vcga' N Ω b r"
using assms lm07 lm08 by blast

(* After showing that the cardinality of vcgas is 1, we know that the_elem to determine vcga
will return a definite value. *)
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "card (vcgas N Ω b r) = 1"
proof -
have "card ((argmax∘sum) (randomBids N Ω b r)
((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) =
1"
(is "card ?X = _") using assms lm08 by blast
moreover have "(Outside'{seller}) ` ?X = vcgas N Ω b r" by blast
ultimately show ?thesis using cardOneImageCardOne by blast
qed

(* The following lemma is a variant of the vcgaDefiniteness theorem. *)
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows  "card (argmax (sum (randomBids N Ω b r))
(maximalStrictAllocations N (set Ω) b)) =
1"
(is "card ?L=_")
proof -
let ?n = "{seller}"
have
1: "(?n ∪ N)≠{}" by simp
have
2: "finite (?n∪N)" using assms(3) by fast
have "terminatingAuctionRel (?n∪N) Ω b r = {chosenAllocation (?n∪N) Ω b r}"
using 1 assms(1) assms(2) 2 by (rule winningAllocationUniqueness)
moreover have "?L = terminatingAuctionRel (?n∪N) Ω b r" by auto
ultimately show ?thesis by auto
qed

theorem winningAllocationIsMaximal:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "the_elem (argmax (sum (randomBids N Ω b r))
(maximalStrictAllocations N (set Ω) b)) ∈
(maximalStrictAllocations N (set Ω) b)"
(is "the_elem ?X ∈ ?R")
proof -
have "card ?X=1" using assms by (rule vcgaDefinitenessVariant)
moreover have "?X ⊆ ?R" by auto
ultimately show ?thesis using cardinalityOneTheElem by blast
qed

corollary winningAllocationIsMaximalWithoutSeller:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcga' N Ω b r ∈ (Outside' {seller})`(maximalStrictAllocations N (set Ω) b)"
using assms winningAllocationIsMaximal by blast

lemma maximalAllactionWithoutSeller:
"(Outside' {seller})`(maximalStrictAllocations N Ω b) ⊆ soldAllocations N Ω"
using Outside_def by force

lemma onlyGoodsAreAllocatedAuxiliary:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcga' N Ω b r ∈ soldAllocations N (set Ω)"
(is "?a ∈ ?A")
proof -
have "?a ∈ (Outside' {seller})`(maximalStrictAllocations N (set Ω) b)"
using assms by (rule winningAllocationIsMaximalWithoutSeller)
thus ?thesis using maximalAllactionWithoutSeller  by fastforce
qed

theorem onlyGoodsAreAllocated:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcga N Ω b r ∈ soldAllocations N (set Ω)"
(is "_∈?r")
proof -
have "vcga' N Ω b r ∈ ?r" using assms by (rule onlyGoodsAreAllocatedAuxiliary)
then show ?thesis using assms vcgaEquivalence by blast
qed

(* Let b be a bid vector such that the seller's bid for each possible set of goods is 0 then
the revenue does not depend on the presence of the seller. *)
corollary neutralSeller:
assumes "∀X. X ∈ Range a ⟶b (seller, X)=0" "finite a"
shows "sum b a = sum b (a--seller)"
proof -
let ?n = seller
have "finite (a||{?n})" using assms restrict_def by (metis finite_Int)
moreover have "∀z ∈ a||{?n}. b z=0" using assms restrict_def by fastforce
ultimately have "sum b (a||{?n}) = 0" using assms by (metis sum.neutral)
thus ?thesis using sumOutside assms(2) by (metis add.comm_neutral)
qed

corollary neutralSellerVariant:
assumes "∀a∈A. finite a & (∀ X. X∈Range a ⟶ b (seller, X)=0)"
shows "{sum b a| a. a∈A} = {sum b (a -- seller)| a. a∈A}"
using assms neutralSeller by (metis (lifting, no_types))

lemma vcgaIsMaximalAux1:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "∃a. ((a ∈ (maximalStrictAllocations N (set Ω) b))  ∧  (vcga' N Ω b r = a -- seller)  &
(a ∈ argmax (sum b) (allAllocations ({seller}∪N) (set Ω))))"
using assms winningAllocationIsMaximalWithoutSeller by fast

lemma vcgaIsMaximalAux2:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
"∀a ∈ allAllocations ({seller}∪N) (set Ω). ∀ X ∈ Range a. b (seller, X)=0"
(is "∀a∈?X. _")
shows "sum b (vcga' N Ω b r) = Max{sum b a| a. a ∈ soldAllocations N (set Ω)}"
proof -
let ?n = seller
let ?s = sum
let ?a = "vcga' N Ω b r"
obtain a where
0: "a ∈ maximalStrictAllocations N (set Ω) b &
?a = a--?n &
(a ∈ argmax (sum b) (allAllocations({seller}∪N)(set Ω)))"
(is "_ & ?a=_ & a∈?Z")
using assms(1,2,3) vcgaIsMaximalAux1 by blast
have
1: "∀a ∈ ?X. finite a & (∀ X. X∈Range a ⟶ b (?n, X)=0)"
using assms(4) List.finite_set allocationFinite by metis
have
2: "a ∈ ?X" using 0 by auto have "a ∈ ?Z" using 0 by fast
then have "a ∈ ?X∩{x. ?s b x = Max (?s b ` ?X)}" using injectionsUnionCommute by simp
then have "a ∈ {x. ?s b x = Max (?s b ` ?X)}" using injectionsUnionCommute by simp
moreover have "?s b ` ?X = {?s b a| a. a∈?X}" by blast
ultimately have "?s b a = Max {?s b a| a. a∈?X}" by auto
moreover have "{?s b a| a. a∈?X} = {?s b (a--?n)| a. a∈?X}"
using 1 by (rule neutralSellerVariant)
moreover have "... = {?s b a| a. a ∈ Outside' {?n}`?X}" by blast
moreover have "... = {?s b a| a. a ∈ soldAllocations N (set Ω)}" by simp
ultimately have "Max {?s b a| a. a ∈ soldAllocations N (set Ω)} = ?s b a" by simp
moreover have "... = ?s b (a--?n)" using 1 2 neutralSeller by (metis (lifting, no_types))
ultimately show "?s b ?a=Max{?s b a| a. a ∈ soldAllocations N (set Ω)}" using 0 by simp
qed

text ‹Adequacy theorem: The allocation satisfies the standard pen-and-paper specification
of a VCG auction. See, for example, \<^cite>‹‹\S~1.2› in "cramton"›.›
theorem vcgaIsMaximal:
assumes "distinct Ω" "set Ω ≠ {}" "finite N" "∀ X. b (seller, X) = 0"
shows "sum b (vcga' N Ω b r) = Max{sum b a| a. a ∈ soldAllocations N (set Ω)}"
using assms vcgaIsMaximalAux2 by blast

corollary vcgaIsAllocationAllocatingGoodsOnly:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcga' N Ω b r ∈ allocationsUniverse & ⋃ (Range (vcga' N Ω b r)) ⊆ set Ω"
proof -
let ?a = "vcga' N Ω b r"
let ?n = seller
obtain a where
0: "?a = a -- seller & a ∈ maximalStrictAllocations N (set Ω) b"
using assms winningAllocationIsMaximalWithoutSeller by blast
then moreover have
1: "a ∈ allAllocations ({?n}∪N) (set Ω)" by auto
moreover have "maximalStrictAllocations N (set Ω) b ⊆ allocationsUniverse"
by (metis (lifting, mono_tags) winningAllocationPossible
allAllocationsUniverse subset_trans)
ultimately moreover have "?a = a -- seller  &  a ∈ allocationsUniverse" by blast
then have "?a ∈ allocationsUniverse" using allocationsUniverseOutside by auto
moreover have "⋃ (Range a) = set Ω" using allAllocationsIntersectionSetEquals 1 by metis
then moreover have "⋃ (Range ?a) ⊆ set Ω" using Outside_def 0 by fast
ultimately show ?thesis using allocationsUniverseOutside Outside_def by blast
qed

(* The price a participant n has to pay is the revenue achieved if n had not participated minus
the value of the goods allocated not to n. *)
abbreviation "vcgp N Ω b r n ==
Max (sum b ` (soldAllocations (N-{n}) (set Ω)))
-  (sum b (vcga N Ω b r -- n))"

(* Since vcga is well-defined the following theorem is trivial. *)
theorem vcgpDefiniteness:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "∃! y. vcgp N Ω b r n = y"

lemma soldAllocationsFinite:
assumes "finite N" "finite Ω"
shows "finite (soldAllocations N Ω)"
using assms allAllocationsFinite finite.emptyI finite.insertI finite_UnI finite_imageI
by metis

text‹The price paid by any participant is non-negative.›
theorem NonnegPrices:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "vcgp N Ω b r n >= (0::price)"
proof -
let ?a = "vcga N Ω b r"
let ?A = soldAllocations
let ?f = "sum b"
have "?a ∈ ?A N (set Ω)" using assms by (rule onlyGoodsAreAllocated)
then have "?a -- n ∈ ?A (N-{n}) (set Ω)" by (rule soldAllocationRestriction)
moreover have "finite (?A (N-{n}) (set Ω))"
using assms(3) soldAllocationsFinite finite_set finite_Diff by blast
ultimately have "Max (?f`(?A (N-{n}) (set Ω))) ≥ ?f (?a -- n)"
(is "?L >= ?R") by (rule maxLemma)
then show "?L - ?R >=0" by linarith
qed

lemma allocationDisjointAuxiliary:
assumes "a ∈ allocationsUniverse" and "n1 ∈ Domain a" and "n2 ∈ Domain a" and "n1 ≠ n2"
shows "a,,n1 ∩ a,,n2 = {}"
proof -
have "Range a ∈ partitionsUniverse" using assms nonOverlapping by blast
moreover have "a ∈ injectionsUniverse & a ∈ partitionValuedUniverse"
using assms by (metis (lifting, no_types) IntD1 IntD2)
ultimately moreover have "a,,n1 ∈ Range a"
using assms by (metis (mono_tags) eval_runiq_in_Range mem_Collect_eq)
ultimately moreover have "a,,n1 ≠ a,,n2"
using assms converse.intros eval_runiq_rel mem_Collect_eq runiq_basic
by (metis (lifting, no_types))
ultimately show ?thesis
using is_non_overlapping_def
by (metis (lifting, no_types) assms(3) eval_runiq_in_Range mem_Collect_eq)
qed

lemma allocationDisjoint:
assumes "a ∈ allocationsUniverse" and "n1 ∈ Domain a" and "n2 ∈ Domain a" and "n1 ≠ n2"
shows "a,,,n1 ∩ a,,,n2 = {}"
using assms allocationDisjointAuxiliary imageEquivalence by fastforce

text‹No good is assigned twice.›
(* We assume implicitely that n1, n2 are participants, Ω a goods list and N the participant set
with "n1 ∈ Domain (vcga' N Ω b r)" "n2 ∈ Domain (vcga' N Ω b r)". However,
formally these assumptions are not needed for the theorem. *)
theorem PairwiseDisjointAllocations:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"  "n1 ≠ n2"
shows "(vcga' N Ω b r),,,n1 ∩ (vcga' N Ω b r),,,n2 = {}"
proof -
have "vcga' N Ω b r ∈ allocationsUniverse"
using vcgaIsAllocationAllocatingGoodsOnly assms by blast
then show ?thesis using allocationDisjoint assms by fast
qed

text ‹Nothing outside the set of goods is allocated.›
theorem OnlyGoodsAllocated:
assumes "distinct Ω" "set Ω ≠ {}" "finite N" "g ∈ (vcga N Ω b r),,,n"
shows "g ∈ set Ω"
proof -
let ?a = "vcga' N Ω b r"
have "?a ∈ allocationsUniverse" using assms(1,2,3) vcgaIsAllocationAllocatingGoodsOnly by blast
then have 1: "runiq ?a" using assms(1,2,3) by blast
have 2: "n ∈ Domain ?a" using assms vcgaEquivalence by fast
with 1 have "?a,,n ∈ Range ?a" using eval_runiq_in_Range by fast
with 1 2 have "?a,,,n ∈ Range ?a" using imageEquivalence by fastforce
then have "g ∈ ⋃ (Range ?a)" using assms vcgaEquivalence by blast
moreover have "⋃ (Range ?a) ⊆ set Ω" using assms(1,2,3) vcgaIsAllocationAllocatingGoodsOnly by fast
ultimately show ?thesis by blast
qed

subsection ‹Computable versions of the VCG formalization›

(*  The computable versions are used to extract code.
Furthermore we prove the equivalence with their classical counterparts. This computes the set of all maximal allocations including the seller. *)
abbreviation "maximalStrictAllocationsAlg N Ω b ==
argmax (sum b) (set (allAllocationsAlg ({seller}∪N) Ω))"

(* This computes the maximal allocation after tie breaking. *)
definition "chosenAllocationAlg N Ω b (r::integer) ==
(randomEl (takeAll (%x. x∈ (argmax ∘ sum) b (set (allAllocationsAlg N Ω)))
(allAllocationsAlg N Ω))
r)"

(* This is the computable version of maxbid in UniformTieBreaking.thy. It takes an allocation,
the bidders and the goods and computes a bid such for each good a bidder bids 1 if they get
that good in allocation a, else they bid 0.*)
definition "maxbidAlg a N Ω == (bidMaximizedBy a N Ω) Elsee 0"

(* This is the completed version of summedBidVectorRel by returning 0 if
summedBidVectorRel is not defined. *)
definition "summedBidVectorAlg bids N Ω == (summedBidVectorRel bids N Ω) Elsee 0"

(* Computable version of tiebids. If computes a bid vector that when the VCG algorithm runs
on it yields the singleton {a}. *)
definition "tiebidsAlg a N Ω == summedBidVectorAlg (maxbidAlg a N Ω) N Ω"

(* Computable version of resolvingBid, that is, is computes the bid vector in random values
that returns the chosen winning allocation *)
definition "resolvingBidAlg N Ω bids random ==
tiebidsAlg (chosenAllocationAlg N Ω bids random) N (set Ω)"

(* The same as above, but adding the seller who receives all unallocated goods. *)
definition "randomBidsAlg N Ω b random == resolvingBidAlg (N∪{seller}) Ω b random"

(* Computable allocation without those participants who do not receive anything. *)
definition "vcgaAlgWithoutLosers N Ω b r ==
(the_elem (argmax (sum (randomBidsAlg N Ω b r))
(maximalStrictAllocationsAlg N Ω b)))
-- seller"

(* Adding losers to an arbitrary allocation *)
abbreviation "addLosers participantset allocation == (participantset × {{}}) +* allocation"

(* Computable version of vcga. It computes the winning allocation incl. losers. *)
definition "vcgaAlg N Ω b r = addLosers N (vcgaAlgWithoutLosers N Ω b r)"

(* Computable version of soldAllocations *)
abbreviation "soldAllocationsAlg N Ω ==
(Outside' {seller}) ` set (allAllocationsAlg (N ∪ {seller}) Ω)"

(* Computable version of vcgp, which computes the prices each participant has to pay. Note that
losers do not pay anything, hence vcgaAlgWithoutLosers is here equivalent to vcgaAlg.
The price a participant n has to pay is the revenue achieved if n had not participated minus
the value of the goods allocated not to n.*)
definition "vcgpAlg N Ω b r n (winningAllocation::allocation) =
Max (sum b ` (soldAllocationsAlg (N-{n}) Ω)) -
(sum b (winningAllocation -- n))"

lemma functionCompletion:
assumes "x ∈ Domain f"
shows "toFunction f x = (f Elsee 0) x"
unfolding toFunctionWithFallbackAlg_def by (metis assms toFunction_def)

(* This technical lemma shows the equivalence of Elsee and toFunction inside a sum expression
under certain assumptions. It is used for the proof of the bridging theorem that
the two versions of the definition of maximalStrictAllocations are equivalent.*)
lemma lm09:
assumes "fst pair ∈ N" "snd pair ∈ Pow Ω - {{}}"
shows "sum (%g. (toFunction (bidMaximizedBy a N Ω))  (fst pair, g))
(finestpart (snd pair)) =
sum (%g. ((bidMaximizedBy a N Ω) Elsee 0) (fst pair, g))
(finestpart (snd pair))"
proof -
let ?f1 = "%g.(toFunction (bidMaximizedBy a N Ω))(fst pair, g)"
let ?f2 = "%g.((bidMaximizedBy a N Ω) Elsee 0)(fst pair, g)"
{
fix g assume "g ∈ finestpart (snd pair)"
then have
0: "g ∈ finestpart Ω" using assms finestpartSubset  by (metis Diff_iff Pow_iff in_mono)
have "?f1 g = ?f2 g"
proof -
have "⋀x⇩1 x⇩2. (x⇩1, g) ∈ x⇩2 × finestpart Ω ∨ x⇩1 ∉ x⇩2" by (metis 0 mem_Sigma_iff)
then have "(pseudoAllocation a <| (N × finestpart Ω)) (fst pair, g) =
maxbidAlg a N Ω (fst pair, g)"
unfolding toFunctionWithFallbackAlg_def maxbidAlg_def
by (metis (no_types) domainCharacteristicFunction UnCI assms(1) toFunction_def)
thus ?thesis unfolding maxbidAlg_def by blast
qed
}
thus ?thesis using sum.cong by simp
qed

(* lm10, lm11, lm12, l13 are variants of lm09 *)
corollary lm10:
assumes "pair ∈ N × (Pow Ω - {{}})"
shows  "summedBid (toFunction (bidMaximizedBy a N Ω)) pair =
summedBid ((bidMaximizedBy a N Ω) Elsee 0) pair"
proof -
have "fst pair ∈ N" using assms by force
moreover have "snd pair ∈ Pow Ω - {{}}" using assms(1) by force
ultimately show ?thesis using lm09 by blast
qed

corollary lm11:
"∀ pair ∈ N × (Pow Ω - {{}}).
summedBid (toFunction (bidMaximizedBy a N Ω)) pair =
summedBid ((bidMaximizedBy a N Ω) Elsee 0) pair"
using lm10 by blast

corollary lm12:
"(summedBid (toFunction (bidMaximizedBy a N Ω))) ` (N × (Pow Ω - {{}}))=
(summedBid ((bidMaximizedBy a N Ω) Elsee 0)) ` (N × (Pow Ω - {{}}))"
(is "?f1 ` ?Z = ?f2 ` ?Z")
proof -
have "∀ z ∈ ?Z. ?f1 z = ?f2 z" by (rule lm11)
thus ?thesis by (rule functionEquivalenceOnSets)
qed

corollary lm13:
"summedBidVectorRel (toFunction (bidMaximizedBy a N Ω)) N Ω =
summedBidVectorRel ((bidMaximizedBy a N Ω) Elsee 0) N Ω"
using lm12 by metis

corollary maxbidEquivalence:
"summedBidVectorRel (maxbid a N Ω) N Ω =
summedBidVectorRel (maxbidAlg a N Ω) N Ω"
unfolding maxbidAlg_def using lm13 by metis

lemma summedBidVectorEquivalence:
assumes "x ∈ (N × (Pow Ω - {{}}))"
shows "summedBidVector (maxbid a N Ω) N Ω x = summedBidVectorAlg (maxbidAlg a N Ω) N Ω x"
(is "?f1 ?g1 N Ω x = ?f2 ?g2 N Ω x")
proof -
let ?h1 = "maxbid a N Ω"
let ?h2 = "maxbidAlg a N Ω"
have "summedBidVectorRel ?h1 N Ω = summedBidVectorRel ?h2 N Ω"
using maxbidEquivalence by metis
moreover have "summedBidVectorAlg ?h2 N Ω = (summedBidVectorRel ?h2 N Ω) Elsee 0"
unfolding summedBidVectorAlg_def by fast
ultimately have " summedBidVectorAlg ?h2 N Ω=summedBidVectorRel ?h1 N Ω Elsee 0" by simp
moreover have "... x = (toFunction (summedBidVectorRel ?h1 N Ω)) x"
using assms functionCompletion summedBidVectorCharacterization by (metis (mono_tags))
ultimately have "summedBidVectorAlg ?h2 N Ω x = (toFunction (summedBidVectorRel ?h1 N Ω)) x"
by (metis (lifting, no_types))
thus ?thesis by simp
qed

(* TPTP ? *)
corollary chosenAllocationEquivalence:
assumes "card N > 0" and "distinct Ω"
shows  "chosenAllocation N Ω b r = chosenAllocationAlg N Ω b r"
using assms allAllocationsBridgingLemma
by (metis (no_types) chosenAllocationAlg_def comp_apply)

corollary tiebidsBridgingLemma:
assumes "x ∈ (N × (Pow Ω - {{}}))"
shows "tiebids a N Ω x = tiebidsAlg a N Ω x"
(is "?L=_")
proof -
have "?L = summedBidVector (maxbid a N Ω) N Ω x" by fast
moreover have "...= summedBidVectorAlg (maxbidAlg a N Ω) N Ω x"
using assms by (rule summedBidVectorEquivalence)
ultimately show ?thesis unfolding tiebidsAlg_def by fast
qed

definition "tiebids'=tiebids"
corollary tiebidsBridgingLemma':
assumes "x ∈ (N × (Pow Ω - {{}}))"
shows "tiebids' a N Ω x = tiebidsAlg a N Ω x"
using assms tiebidsBridgingLemma tiebids'_def by metis

abbreviation "resolvingBid' N G bids random ==
tiebids' (chosenAllocation N G bids random) N (set G)"

lemma resolvingBidEquivalence:
assumes "x ∈ (N × (Pow (set Ω) - {{}}))"  "card N > 0" "distinct Ω"
shows "resolvingBid' N Ω b r x = resolvingBidAlg N Ω b r x"
using assms chosenAllocationEquivalence tiebidsBridgingLemma' resolvingBidAlg_def by metis

lemma sumResolvingBidEquivalence:
assumes "card N > 0" "distinct Ω" "a ⊆ (N × (Pow (set Ω) - {{}}))"
shows "sum (resolvingBid' N Ω b r) a = sum (resolvingBidAlg N Ω b r) a"
(is "?L=?R")
proof -
have "∀x∈a. resolvingBid' N Ω b r x = resolvingBidAlg N Ω b r x"
using assms resolvingBidEquivalence by blast
thus ?thesis using sum.cong by force
qed

lemma resolvingBidBridgingLemma:
assumes "card N > 0" "distinct Ω" "a ⊆ (N × (Pow (set Ω) - {{}}))"
shows "sum (resolvingBid N Ω b r) a = sum (resolvingBidAlg N Ω b r) a"
(is "?L=?R")
proof -
have "?L=sum (resolvingBid' N Ω b r) a" unfolding tiebids'_def by fast
moreover have "...=?R"
using assms by (rule sumResolvingBidEquivalence)
ultimately show ?thesis by simp
qed

lemma allAllocationsInPowerset:
"allAllocations N Ω ⊆ Pow (N × (Pow Ω - {{}}))"
by (metis PowI allocationPowerset subsetI)

corollary resolvingBidBridgingLemmaVariant1:
assumes "card N > 0" "distinct Ω" "a ∈ allAllocations N (set Ω)"
shows "sum (resolvingBid N Ω b r) a = sum (resolvingBidAlg N Ω b r) a"
proof -
have "a ⊆ N × (Pow (set Ω) - {{}})" using assms(3) allAllocationsInPowerset by blast
thus ?thesis using assms(1,2) resolvingBidBridgingLemma by blast
qed

corollary resolvingBidBridgingLemmaVariant2:
assumes "finite N" "distinct Ω" "a ∈ maximalStrictAllocations N (set Ω) b"
shows "sum (randomBids N Ω b r) a = sum (randomBidsAlg N Ω b r) a"
proof -
have "card (N∪{seller}) > 0" using assms(1) sup_eq_bot_iff insert_not_empty
by (metis card_gt_0_iff finite.emptyI finite.insertI finite_UnI)
moreover have "distinct Ω" using assms(2) by simp
moreover have "a ∈ allAllocations (N∪{seller}) (set Ω)" using assms(3) by fastforce
ultimately show ?thesis unfolding randomBidsAlg_def by (rule resolvingBidBridgingLemmaVariant1)
qed

corollary tiebreakingGivesSingleton:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "card (argmax (sum (randomBidsAlg N Ω b r))
(maximalStrictAllocations N (set Ω) b)) =
1"
proof -
have "∀ a ∈ maximalStrictAllocations N (set Ω) b.
sum (randomBids N Ω b r) a = sum (randomBidsAlg N Ω b r) a"
using assms(3,1) resolvingBidBridgingLemmaVariant2 by blast
then have "argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocations N (set Ω) b) =
argmax (sum (randomBids N Ω b r)) (maximalStrictAllocations N (set Ω) b)"
using argmaxEquivalence by blast
moreover have "card ... = 1" using assms by (rule vcgaDefinitenessVariant)
ultimately show ?thesis by simp
qed

theorem maximalAllocationBridgingTheorem:
assumes "finite N" "distinct Ω"
shows "maximalStrictAllocations N (set Ω) b = maximalStrictAllocationsAlg N Ω b"
proof -
let ?N = "{seller} ∪ N"
have "card ?N>0" using assms(1)
by (metis (full_types) card_gt_0_iff finite_insert insert_is_Un insert_not_empty)
thus ?thesis using assms(2) allAllocationsBridgingLemma by metis
qed

theorem vcgaAlgDefinedness:
assumes "distinct Ω" "set Ω ≠ {}" "finite N"
shows "card (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocationsAlg N Ω b)) = 1"
proof -
have "card (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocations N (set Ω) b)) = 1"
using assms by (rule tiebreakingGivesSingleton)
moreover have "maximalStrictAllocations N (set Ω) b = maximalStrictAllocationsAlg N Ω b"
using assms(3,1) by (rule maximalAllocationBridgingTheorem)
ultimately show ?thesis by metis
qed

end

```