Re: [isabelle] undefined & None
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and