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

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.



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