Make combinatorial Vickrey auction and its soundness a special case of reorganised general combinatorial auctions

[clange]

Reorganise and extend some of the code that's currently in CombinatorialVickreyAuction.thy, probably also some of the code in CombinatorialAuction.thy. As a specialisation of the corresponding notions for general combinatorial auctions (#19) there should be

1. a definition of the nVCG auction that is as close to the paper form as possible. This includes the definition of an admissible input (bids, goods, etc.). The functions for the outcome (allocation and payments) we already have, but they may need reorganisation.
2. if necessary, a redefinition of the same in relational form (i.e. input × outcome), and a proof of the equivalence of the two forms (1) and (2)
3. a proof that, in the presence of a tie-breaking function, for any admissible input there is a unique, well-defined outcome, i.e. that the relational representation of the auction is left-total and right-unique (i.e. a function), and that the outcome is well-defined. The notion of what an “admissible input” is probably applies to all combinatorial auctions in the same way, but we might need a specialisation to nVCG. Similarly, the notion of a “well-defined outcome” (e.g. only allocating goods that are for sale) probably applies to all combinatorial auctions, but here we certainly have auction-specific specialisations: some auctions may have negative payments, some (including nVCG in our understanding) may allow for goods not to be allocated. BTW, the “right-unique” part of the proof should be really easy, as the tie-breaker takes care of that.