Auction Theory Toolbox – Isabelle
Files relevant to the Isabelle formalisation
- Source repository on GitHub.
- all-in-one ZIP archive for download
- *.thy: Isabelle formalisation:
- All.thy: loads all theories whose formalisation is stable, for convenience
- General foundations; additions to the Isabelle library:
- Finite_SetUtils.thy: additions to Finite_Set.thy from the library
- HOLUtils.thy: additions to HOL.thy from the library
- ListUtils.thy: additions to List.thy from the library
- Maximum.thy: maximum components of vectors and sets, and their properties
- Partitions.thy: partitions of sets
- PartitionsAlternative.thy: some alternative definitions of partitions (currently unused)
- PartitionsTest.thy: test cases for partitions
- RelationOperators.thy: some additional operators on relations, and their properties
- RelationProperties.thy: further properties of the library operators on relations
- RelationUtils.thy: additions to Relations.thy from the library
- SetUtils.thy: additions to Set.thy from the library
- Vectors.thy: vectors, implemented as functions
- General foundations of static single good auctions, and Vickrey's theorem:
- MaximumTest.thy: some examples for testing Maximum
- SingleGoodAuction.thy: single good auctions
- SingleGoodAuctionTest.thy: some examples for testing SingleGoodAuction
- SingleGoodAuctionProperties.thy: some properties that single good auctions can have
- SecondPriceAuction.thy: second price single good auctions (underspecified; without tie-breaking) and some of their properties
- Vickrey.thy: Vickrey's Theorem: second price auctions are efficient, and truthful bidding is a weakly dominant strategy.
- Soundness checks for static single good auctions:
- SecondPriceAuctionSoundness.thy: soundness proof of the underspecified second price single good auctions without tie-breaking
- UniqueMaximum.thy: determining a unique maximum components of vectors, subject to tie-breaking
- SingleGoodAuctionTieBreaker.thy: tie-breaking rules for single good auctions
- FullySpecifiedSingleGoodAuction.thy: fully specified single good auctions, with tie-breaking rules
- FullySpecifiedSecondPriceAuction.thy: fully specified variant of the second price single good auction
- FullySpecifiedSecondPriceAuctionSoundness.thy: soundness proof of the fully specified variant of the second price single good auction
- FullySpecifiedSecondPriceAuctionCode.thy: wrapper to generate verified code to execute the fully specified second price single good auction
- Static combinatorial auctions, from foundations to soundness checks:
- CombinatorialAuction.thy: definition of general combinatorial auctions
- CombinatorialAuctionProperties.thy: some properties that general combinatorial auctions can have
- CombinatorialAuctionTest.thy: test combinatorial auctions
- CombinatorialAuctionTieBreaker.thy: tie-breakers for combinatorial auctions
- CombinatorialVickreyAuction.thy: definition of the combinatorial Vickrey auction
- CombinatorialVickreyAuction.thy: wrapper to generate verified code to execute the combinatorial Vickrey auction
- CombinatorialVickreyAuctionSoundness.thy: soundness proof (in progress) of the fully specified combinatorial Vickrey auction
- CombinatorialVickreyAuctionTest.thy: tests for the combinatorial Vickrey auction
- *.pdf: exported files (for an old version of Vickrey's theorem at the time of this writing):
- code: executable Scala code generated from the fully specified auctions (in progress)
- Makefile contains rules to regenerate some of the files mentioned above.
How to run
- Obtain Isabelle. Our code is known to work with Isabelle2013-1-RC1.
- Interactive mode: run
isabelle jedit Auction/Vickrey.thy, and agree to loading all of its dependencies. - Batch mode: run
isabelle build -D Auctionand open the generatedAuction/output/document/root.pdf
This page was last modified on 04 October 2013.