*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] [isabelle-dev] Partial functions (fwd)*From*: Makarius <makarius at sketis.net>*Date*: Thu, 23 May 2013 11:39:54 +0200 (CEST)*Cc*: "Roger H." <s57076 at hotmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

This also belongs to isabelle-users.

Makarius ---------- Forwarded message ---------- Date: Wed, 22 May 2013 13:50:45 +0200 From: Manuel Eberl <eberlm at in.tum.de> To: isabelle-dev at mailbroy.informatik.tu-muenchen.de Subject: Re: [isabelle-dev] Partial functions Hallo, partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is an abbreviation for 'a ⇒ 'b option. There is syntax such as "[1 ↦ 2, 3 ↦ 4]", meaning, basically, "λx. if x = 1 then Some 2 else if x = 3 then Some 4 else None". There is also update syntax for such function, such as "f(1 ↦ 3)", meaning "λx. if x = 1 then 3 else f x". You could therefore write something like definition f :: "nat ⇀ nat" where "f = [1 ↦ 4, 2 ↦ 4, 3 ↦ 5]" You can find out the domain/range of such a partial function using dom and ran. For instance, "dom f" is defined as {a. f a ≠ None}. If you want to apply such a function, you can either do "case f x of None ⇒ … | Some y ⇒ …", or you can simply write "the (f x)". "the" takes an option value and extracts the "y" out of a "Some y" or returns "undefined" if the option value is "None". I hope that answers your question. Cheers, Manuel 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

_______________________________________________ isabelle-dev mailing list isabelle-dev at in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

- Previous by Date: Re: [isabelle] SOME-operator
- Next by Date: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Previous by Thread: Re: [isabelle] Set of functions
- Next by Thread: [isabelle] Isabelle/HOL, the book
- 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