# Re: [isabelle] domain of function

Dear Hidetsune,

`unfortunately, modelling partial functions with arbitrary is rather
``counter-intuitive and weak. Since arbitrary is an (unspecified)
``element from the underlying type, it is not possible to determine the
``domain of such a function. The function could be undefined at point x,
``or it could map x to a value that coincides with the (unspecified)
``value of arbitrary.
`

`If you want to deal with partial functions seriously, you will have to
``make the domain explicit. I can think of two ways of dealing with
``this. You can either make the function a pair (f, A) where A is the
``domain of f. Or you let f be of type 'a => 'b option, and x is in the
``domain of f iff f x = None. Both are precise but not convenient to
``deal with, I'm afraid.
`
Clemens

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