*To*: John Wickerson <johnwickerson at cantab.net>*Subject*: Re: [isabelle] how to state that a function is well-defined?*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Fri, 01 Nov 2013 20:25:05 +0100*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <14EC554F-168D-4867-801D-9DD233B242F9@cantab.net>*Organization*: University of Birmingham*References*: <14EC554F-168D-4867-801D-9DD233B242F9@cantab.net>*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130919 Thunderbird/17.0.9

Hi John, 2013-11-01 19:41 John Wickerson: > How can I state a lemma that simply says my function is "well-defined"? I mean: suppose I define > > definition "foo x == x ! 0" > > I want to say that foo is "well-defined" on all inputs other than the empty list. I'm imagining something like > > lemma "x ≠ [] ⟹ ∃!y. foo x = y" > > but that's true for any foo. I'm not sure what your concrete application is, but we have experienced the same problem in the concrete setting of proving the well-definedness of an auction. To our most general understanding, an auction is a relation of inputs (participants' bids on available goods) to outcomes (an allocation of goods to participants, and a specification of who has to pay how much to the auctioneer). Of such a relation we seek to prove three properties: 1. it is left-total on valid inputs, i.e. for any such input there exists an outcome 2. these outcomes are unique. (1) and (2) means that the auction relation is a function. 3. the outcomes satisfy some additional properties. Note that we call these properties "well-definedness", whereas we use "soundness" to refer to what you call "well-definedness". OK, but one concrete auction for which we'd like to prove this is already stated as a HOL function. This means, taking into account what Larry explained, that (1) and (2) are easy to prove, but that you don't gain much from this close-to-vacuous observation in practice. Thus … 2013-11-01 20:00 Lawrence Paulson: > You may find that some properties of foo only hold for non-empty lists, that’s all. … (3) is indeed the only interesting part of our proof. For the source see https://github.com/formare/auctions/blob/master/isabelle/Auction/CombinatorialVickreyAuctionSoundness.thy, and for an explanation (to an audience without a theorem proving background) see section 5 of https://codex.cs.bham.ac.uk/svn/mmk/formare/pubs/wine2013/130719n-VCG.pdf (use username/password guest/guest). Note that both are work in progress. Cheers, Christoph -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Mathematics in Computer Science Special Issue on “Enabling Domain Experts to use Formalised Reasoning”; submission until 31 October. http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

**References**:**[isabelle] how to state that a function is well-defined?***From:*John Wickerson

- Previous by Date: Re: [isabelle] how to state that a function is well-defined?
- Next by Date: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Previous by Thread: Re: [isabelle] how to state that a function is well-defined?
- Next by Thread: [isabelle] linordered_idom: context affecting time & simp, printing numerals
- Cl-isabelle-users November 2013 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