# Re: [isabelle] [isabelle-dev] Partial functions

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: Re: [isabelle] [isabelle-dev] Partial functions
*From*: Gottfried Barrow <gottfried.barrow at gmx.com>
*Date*: Fri, 25 Oct 2013 01:34:17 -0500
*In-reply-to*: <519CAFA1.8040804@inf.ethz.ch>
*References*: <DUB124-W34753CEAC4B5C9BEBFCF9B8FA90@phx.gbl> <DUB124-W45D4B252949F10C4E01E678FA90@phx.gbl> <519CAFA1.8040804@inf.ethz.ch>
*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 5/22/2013 6:44 AM, Andreas Lochbihler wrote:

For example,
definition f :: "nat => nat option" where
"f x = (if x : {1,2,3} then Some .... else None)"

`Then, "dom f" returns the domain of f as {1,2,3} and "ran f" the range
``of f. There are a few more operations defined in theory Map, in
``particular map_of. Option.bind in theory Option is used for function
``composition.
`

On 5/22/2013 6:50 AM, Manuel Eberl wrote:

You can find out the domain/range of such a partial function using dom
and ran. For instance, "dom f" is defined as {a. f a ≠ None}.

`I was looking at how to do a partial function with option, so I was
``looking at this old email thread.
`

`The two statements above make it sound like it should be easy to get
``"dom f = {1,2,3}".
`
I do this:
theorem "(dom f) = {1,2,3}"
apply(unfold dom_def)

`And I get a goal: "{a. f a ≠ None} = {1, 2, 3}", with no easy automatic
``proof.
`
Is there something simple I'm supposed to do get "(dom f) = {1,2,3}"?
Thanks,
GB

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