Soundness proof and code generation for combinatorial first-price auction

[clange]

As discussed with @rowatc: redo what we did for the combinatorial VCG mechanism (in CombinatorialVickreyAuction.thy) for the first-price combinatorial auction, in the following steps:

• add variant of payment function
• generate code
• adapt soundness proof (which, at this point, still remains to be written for nVCG)
  Keep track of the time these things took.