Re: [isabelle] [isabelle-dev] Partial functions (fwd)



This also belongs to isabelle-users.

It does not make any sense to post questions both to isabelle-users and isabelle-dev at the same time -- it just causes confusion.


	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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.