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"
Map.map_add ::
  "('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 "++".)

Note that map_add does right overloading, and is thus not an associative operator.

Regards
Andrew

[1]: http://www.haskell.org/hoogle/


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.