Re: [isabelle] how to state that a function is well-defined?
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
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
and for an explanation (to an audience without a theorem proving
background) see section 5 of
username/password guest/guest). Note that both are work in progress.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and