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
* ISC License (1-clause BSD License)
See LICENSE file for details
(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

lemma allocatedToBuyerMeansSold: 
  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. *)
theorem vcgaDefiniteness: 
  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. *)
lemma vcgaDefinitenessVariant: 
  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" 
  using assms vcgaDefiniteness by simp

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