Theory CombinatorialAuctionCodeExtraction

```(*
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: Scala code extraction›

theory CombinatorialAuctionCodeExtraction

imports
CombinatorialAuction

(* The following theories are needed for the extraction of Scala code *)
"HOL-Library.Code_Target_Nat"
"HOL-Library.Code_Target_Int"

begin

(* Next we define some auxiliary functions to facilitate pretty printing in Scala *)
(* allocationPrettyPrint transforms sets into lists *)
definition "allocationPrettyPrint a =
{map (%x. (x, sorted_list_of_set(a,,x))) ((sorted_list_of_set ∘ Domain) a)}"

(* We define bids in Scala as lists of three elements: (participants, goods, bid). To use our
vcga algorithm we need the bid vector to be a function from pairs (participant, {goods}) to
the corresponding bid. Bid2funcBid does this conversion. singleBidConverter is a corresponding
helper function. *)

abbreviation "singleBidConverter x == ((fst x, set ((fst o snd) x)), (snd o snd) x)"
definition "Bid2funcBid b = set (map singleBidConverter b) Elsee (0::integer)"

(* participantsSet extracts the participants from a bid vector. *)
definition "participantsSet b = fst ` (set b)"

(* goodsList extracts the goods from a bid vector. *)
definition "goodsList b = sorted_list_of_set (Union ((set o fst o snd) `(set b)))"

(* payment is a wrapper to reuse the allocation so that it is computed only once. *)
definition "payments b r n (a::allocation) =
vcgpAlg ((participantsSet b)) (goodsList b) (Bid2funcBid b) r n (a::allocation)"

(* Isabelle will export code for the vcgaAlg and payments as well as all other functions
necessary for the computation and write it to a file of choice, in this case the file
VCG.scala *)
export_code vcgaAlg payments allocationPrettyPrint in Scala module_name VCG
file ‹VCG-withoutWrapper.scala›

end

(* At this moment in time the code generated works well under Linux. However, there is a naming
conflict in Windows originating from conflating nat and Nat as well as sup_set and Sup_set.
In order to make the code runnable under Windows as well, it is possible to universally
replace, e.g., Nat by NNat and Sup_set by SSup_set. The following shell command may be