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