*To*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 13 Nov 2012 11:08:20 +0000*Cc*: "formare-discuss at cs.bham.ac.uk" <formare-discuss at cs.bham.ac.uk>, isabelle-users at cl.cam.ac.uk, Christoph LANGE <c.lange at cs.bham.ac.uk>*In-reply-to*: <50A18165.7090304@gmail.com>*References*: <50916DB3.4030707@cs.bham.ac.uk> <50A18165.7090304@gmail.com>

"But it is easy to write definitions that aren't satisfiable, or that imply trivialities." I agree absolutely. People often imagine that it's impossible to make a mistake if you use a formal proof assistant, but erroneous definitions and unrealistic models are commonplace. Larry Paulson On 12 Nov 2012, at 23:08, "Tim (McKenzie) Makarios" <tjm1983 at gmail.com> wrote: > I've had a look at your work, and found it interesting. > > One thing that I noticed was that you defined what it means to be a > second_price_auction, and you proved various things about functions that > satisfy this definition, but you never showed that the definition was > satisfiable. > > This isn't an inconsequential detail; at first, I thought you'd got the > definition wrong, and that "second_price_auction n x p" implied n < 2. > When I tried to prove it, I finally noticed that your allocation and > payment functions depend on the set of bids. But it is easy to write > definitions that aren't satisfiable, or that imply trivialities. > > So I decided to prove that your second_price_auction was satisfiable for > n > 0. See attached for the proof. > > Also, you made a comment about removing an element from a set. Given a > set A, the set of all the elements of A except x can be written as > "A - {x}" > > I have a feeling that there was something else I was going to comment > on, but I should go and have lunch, and write again if I remember it. > > Tim > <>< > <Vickrey_Extras.thy>

**References**:**Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions***From:*Tim (McKenzie) Makarios

- Previous by Date: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Date: [isabelle] Automatic derivation of a total order on datatypes
- Previous by Thread: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Next by Thread: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list