Re: [isabelle] domain of function
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and