*To*: Roger H. <s57076 at hotmail.com>*Subject*: Re: [isabelle] Partial functions basics*From*: John Wickerson <johnwickerson at cantab.net>*Date*: Thu, 9 Jan 2014 17:41:47 +0000*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DUB124-W39CC062195AB276AD815958FB00@phx.gbl>*References*: <DUB124-W39CC062195AB276AD815958FB00@phx.gbl>

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! > > > > >

**Follow-Ups**:**Re: [isabelle] Partial functions basics***From:*Andrew Boyton

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

- Previous by Date: [isabelle] Partial functions basics
- Next by Date: Re: [isabelle] Partial functions basics
- Previous by Thread: [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