# Re: [isabelle] Partial functions basics

```It might be useful to point out that find_consts can be useful for times like this. It's like a very simplified version of Hoogle [1].

You need to generalise what you are searching for, (not nat ⇀ nat but 'a ⇀ 'b), but it finds what you are after.

find_consts "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ 'a ⇀ 'b"

gives

searched for:
"('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ 'a ⇀ 'b"

found 2 constant(s):

Quickcheck_Exhaustive.cps_plus ::
"(('a ⇒ term list option)
⇒ term list option)
⇒ (('a ⇒ term list option)
⇒ term list option)
⇒ ('a ⇒ term list option)
⇒ term list option"
"('a ⇒ 'b option)
⇒ ('a ⇒ 'b option) ⇒ 'a ⇒ 'b option"

The second, Map.map_add is the one you want, and you can then command click on it to give the definition. ("Map_add" is "++".)

Regards
Andrew

On 10 Jan 2014, at 4:41 am, John Wickerson <johnwickerson at cantab.net> wrote:

> Hi Roger,
>
> For this you want "f ++ g". Such things are defined in Map.thy -- see here:
>
> http://isabelle.in.tum.de/library/HOL/HOL/Map.html
>
> Best wishes,
> John
>
> On 9 Jan 2014, at 17:21, Roger H. <s57076 at hotmail.com> wrote:
>
>> Hi,
>>
>> how can i make "f ∪ g"?
>>
>> definition f :: "nat ⇀ nat" where
>> "f = [1 ↦ 0, 2 ↦ 5]"
>> definition g :: "nat ⇀ nat" where
>> "g = [3 ↦ 7, 4 ↦ 9]"
>> definition f_union_g :: "nat ⇀ nat" where
>> "f_union_g = [1 ↦ 0, 2 ↦ 5, 3 ↦ 7, 4 ↦ 9]"
>>
>> So how should i define f_union_g?
>>
>> And generally in what class.thy can i find such operators on partial functions?
>>
>> Thank you!
>>
>>
>>
>>
>>
>
>

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
```

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