>>> So you suggest using e.g. >>> if EX x. x : A then A >>> else {0} >>> instead of A as the semantic interpretation? >>> Interesting! >> >> Yes, this is exactly the kind of thing I meant. You could use any >> nonempty set you want in place of {0}, of course. > > How about {undefined}, or similar?
IMHO {default} is even the more suitable choice, although it makes no substantial difference. Btw. there is often the situation that, given an Abs :: b => a for a "new" type "a", the user defines a constructor C which then is "total", e.g. for rats: Rat k l := (if l = 0 then Abs_rat 0 1 else Abs_rat k l) or for dlists: Dlist xs := Abs_dlist (remdups xs) This saves some case distinctions in trivial cases. I have called this "totalisation". > You surely know this HOL joke in some form or the other: > > "if default = undefined then SOME x. True else SOME x. False" The original formulation also involved "arbitrary", which we have managed to get rid of finally, but you can still permute the values in the term above in an arbitrary order. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev