*To*: Roger H. <s57076 at hotmail.com>*Subject*: Re: [isabelle] [isabelle-dev] Partial functions*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 22 May 2013 13:44:33 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DUB124-W45D4B252949F10C4E01E678FA90@phx.gbl>*References*: <DUB124-W34753CEAC4B5C9BEBFCF9B8FA90@phx.gbl> <DUB124-W45D4B252949F10C4E01E678FA90@phx.gbl>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

Hi Roger,

For example, definition f :: "nat => nat option" where "f x = (if x : {1,2,3} then Some .... else None)"

Best, Andreas

On 22/05/13 13:35, Roger H. wrote:

Hallo, i want to create a datatype that allows me to write functions from a nat subset to another nat subset. for example i wanna be able to write: definition f: {1,2,3} => {4,5} 1 -->4, 2-->4, 3-->5 or another one: definition g : {6,8} => {2,3,4} So the thing i want to somehow parametrize is "which subset of the nat im using each time as domain and range" , I thought about creating a new datatype : 'a nat The problem with this is that 'a is instantiated with datatypes, and not sets like {1,2,3}. Following solutions are bad: 1. Everytime i want declare a new function, i have to declare by "typedef" the nat subsets i want as domain and range 2. definition f : "nat => nat" where "f x = (if x : {1,2,3} then .... else undefined) This second approach is bad, cause i dont want the domain to be decided as late as the second line of the declaration, cause after this i want to be able to program a selector "domain f" that returns me the domain of f, thats why i want the domain of f to be somehow incapsulated (parametrized) in the first line "f: nat =>nat " so that i can use it later. What would you do in this situation? Many thanks! _______________________________________________ isabelle-dev mailing list isabelle-dev at in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

- Previous by Date: Re: [isabelle] Partial functions
- Next by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Previous by Thread: Re: [isabelle] Partial functions
- Next by Thread: [isabelle] THE-operator
- Cl-isabelle-users May 2013 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