[isabelle-dev] Partial functions

Roger H. s57076 at hotmail.com
Wed May 22 13:35:55 CEST 2013


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!

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130522/40b524ae/attachment.html>

More information about the isabelle-dev mailing list