Well, as the purpose of optionTheory is to augment any type with one more value, for (at least) extreals, it would be equivalent to have that “undefined” thing defined as part of the datatype definition:
val extreal_def = Datatype `extreal = NegInf | PosInf | Normal real | Undefined`; However, once “Undefined” is actually defined, it’s then a disaster to affect almost all arithmetic laws. For a number which is either PosInf nor NegInf, now we can’t say it must be a (Normal x) any more, and many theorems will be broken. To fix it, we have to treat this “Undefined” as something like those NaNs in IEEE 754 standard and define their orders and arithmetic laws, then all these work are unnecessary for formalization of pure math theorems. So I think the key is to make sure that “undefined” thing really undefined, such that whenever it appears, the proof cannot proceed any more, except for syntactic rewriting, which is inevitable in HOL. Keeping ``0 / 0 = 0`` as before, could be another option, but I have concerns to convince mathematicians to accept this fact since I aim at precisely reproduce those pure math proofs under the “same” formal system with math books (except for the subtle differences between ZFC and HOL not affecting the math theories that I’m working with.) —Chun > Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar > <ramana.ku...@cl.cam.ac.uk> ha scritto: > > I'd say one of the stronger ways to get "undefined" is to add an element to > your type representing undefinedness, e.g., make it (/) : real option -> real > option -> real option, where NONE represents "undefined". But then you will > have a lot of bookkeeping to deal with... > I don't suggest this seriously in the case of division -- I would rather > suggest accepting the usual treatment of these partial functions as a small > price for the benefits of working in a logic of (only) total functions. > > On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson <l...@cam.ac.uk > <mailto:l...@cam.ac.uk>> wrote: > None of these attempts make any sense. In HOL and similar systems (including > Isabelle/HOL), it’s *impossible* to arrange for x/0 to be undefined in any > strong sense. Fortunately, it’s consistent and harmless to put x/0 = 0. > > Larry Paulson > > > > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net > > <mailto:hol-info-requ...@lists.sourceforge.net> wrote: > > > > I run some experiments so to check if it is violating any fundamental rule. > > So far it went good. > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info > <https://lists.sourceforge.net/lists/listinfo/hol-info> > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
