Re: [isabelle] [isabelle-dev] Partial functions



Hi Roger,

Isabelle/HOL is a logic of total function, so very function is defined for all values of the argument type. So, if you declare the type "nat => nat", it is always defined on all natural numbers. As you have found out yourself, you can create types for subsets of natural numbers, but you won't get happy with that, because all of your formalisation will be cluttered with embeddings of one of these types into another.

The standard way to model partiality is the following: Wrap the return type in "option" and use the value None to denote undefinedness.

For example,

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

Then, "dom f" returns the domain of f as {1,2,3} and "ran f" the range of f. There are a few more operations defined in theory Map, in particular map_of. Option.bind in theory Option is used for function composition.

Best,
Andreas

PS: This is a standard user's topic, so it belongs to the mailing list isabelle-users, not isabelle-dev.

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





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