*To*: John Wickerson <johnwickerson at cantab.net>*Subject*: Re: [isabelle] Partial functions basics*From*: Andrew Boyton <Andrew.Boyton at nicta.com.au>*Date*: Thu, 9 Jan 2014 23:26:09 +0000*Accept-language*: en-AU, en-US*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, "Roger H." <s57076 at hotmail.com>*In-reply-to*: <75BFEEB2-E851-4A3C-A2C8-0083058DDFE6@cantab.net>*References*: <DUB124-W39CC062195AB276AD815958FB00@phx.gbl> <75BFEEB2-E851-4A3C-A2C8-0083058DDFE6@cantab.net>*Thread-index*: AQHPDWAHBTBcY6qIFkmOY4pfu4SrcJp78PyAgABgN4A=*Thread-topic*: [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.

**Follow-Ups**:**Re: [isabelle] Partial functions basics***From:*Tjark Weber

**References**:**[isabelle] Partial functions basics***From:*Roger H .

**Re: [isabelle] Partial functions basics***From:*John Wickerson

- Previous by Date: Re: [isabelle] Partial functions basics
- Next by Date: Re: [isabelle] Partial functions basics
- Previous by Thread: Re: [isabelle] Partial functions basics
- Next by Thread: Re: [isabelle] Partial functions basics
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list