[isabelle] The theory Option

I've been looking at theory Option for some time now, and I've been wondering why it isn't used more often than it is. If you're going to have a type with an extra element called None, an obvious use of this (obvious to me, anyway) would be to interpret None as "undefined." Division of real numbers, for example, could be a function from (real option) x (real option) -> real option, with x/0 = None and None/x = y/None = None. This is in fact exactly how floating point numbers work on computers today, except that there None is called NaN, which is an abbreviation for Not a Number. The advantage of this over the current system of using zero to mean "undefined" is that there you can't tell the difference, after the fact, between a zero meaning "undefined" and a real zero. Another advantage for me is that if I'm trying to explain Isar to mathematicians who are complex analysts or other non-algebraists, as I intend to try to do, it could take a lot of explaining to convince them that defining x/0 to be 0 (rather than None) doesn't lead to absurdities. I've done complex analysis myself (my theorem says that if S and S' are countable dense sets on the complex plane, there exists an entire function taking S onto S') so I should be believable when talking to complex analysts.
Is there a good reason why this wouldn't work in practice?

Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875

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