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



I’m afraid that this concept of "well-defined” does not exist in higher-order logic. You may find that some properties of foo only hold for non-empty lists, that’s all.

Larry Paulson


On 1 Nov 2013, at 18:41, John Wickerson <johnwickerson at cantab.net> wrote:

> 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.