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.


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