*To*: Henri DEBRAT <Henri.Debrat at loria.fr>, USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] undefined & None*From*: John Wickerson <johnwickerson at cantab.net>*Date*: Sun, 14 Jul 2013 11:18:05 +0100*In-reply-to*: <84BA764F-548D-4581-8A0C-363F02925A3A@loria.fr>*References*: <42ADB9E3-85FA-4CFE-93BA-2A4CAC36DCA6@loria.fr> <84BA764F-548D-4581-8A0C-363F02925A3A@loria.fr>

Further to Stephan's response... The type of "None" is "T option", for any type T. Suppose T has elements {a,b,c,d}. Then "T option" will contain the elements {None, Some a, Some b, Some c, Some d}. "None" is just an extra element added to the type. "None" is often used when defining partial functions: an input is sent to "None" when the partial function is not defined for that input. But otherwise "None" and the special "undefined" constant are completely unrelated. There are other uses of "None", unrelated to definedness. For instance, None could represent an error in a calculation. A division function might return "Some 10" when asked to divide 50 by 5, and "None" when a division-by-zero is attempted. Another use is to represent natural-numbers-with-infinity. The type "nat" only includes finite numbers, but if you use "nat option" then you can use "None" to stand for infinity. In short, None is just an extra element added to an existing type. john On 14 Jul 2013, at 10:22, Stephan Merz wrote: > Henri, > > On Jul 13, 2013, at 11:17 PM, Henri DEBRAT <Henri.Debrat at loria.fr> wrote: > >> I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom. >> >> In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ? > > grepping for undefined in src/HOL yields > > HOL.thy:axiomatization undefined :: 'a > > As you can see, the constant is not defined but declared as a polymorphic constant for arbitrary type. This is logically unproblematic because types in HOL must be non-empty. The value denotes some unspecified value of arbitrary type, this is sometimes useful when no particular property of the value is required. > > Note that in theory Hilbert_Choice one could actually define > > definition undefined where "(undefined::'a) = Some (x::'a). True" > >> I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not. > > Since "undefined" is polymorphic, it exists for any option type. Defining "undefined :: 'a option" to be None would be more specific than what is required. > > Hope this helps, > > Stephan > >

**Follow-Ups**:**Re: [isabelle] undefined & None***From:*Henri DEBRAT

**References**:**[isabelle] undefined & None***From:*Henri DEBRAT

**Re: [isabelle] undefined & None***From:*Stephan Merz

- Previous by Date: Re: [isabelle] undefined & None
- Next by Date: Re: [isabelle] undefined & None
- Previous by Thread: Re: [isabelle] undefined & None
- Next by Thread: Re: [isabelle] undefined & None
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list