Re: [isabelle] undefined & None



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





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