[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 email@example.com
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