# [isabelle] how to state that a function is well-defined?

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] how to state that a function is well-defined?
*From*: John Wickerson <johnwickerson at cantab.net>
*Date*: Fri, 1 Nov 2013 18:41:03 +0000
*Authentication-results*: jackal.aluminati.org (amavisd-new); dkim=pass header.i=@cantab.net

This is a really basic question, and I'll probably kick myself once somebody tells me the answer.
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.
Thanks!
john

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*