[isabelle-dev] An ARBITRARY question

[Tobias Nipkow]

You can prove "hd [] = undefined" and in fact "hd [] = last []", just as
an example. This is a feature of primrec and function. But you cannot
prove "hd [] = arbitrary".

Tobias

Lawrence Paulson schrieb:
> Apologies for that garbled message. I meant,
> 
>     What is the difference between undefined and arbitrary?
> 
> Larry
> 
> On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
> 
>> "undefined" and "default" are used in a specific way. If you do not want
>> that functionality (and accidental equalities), "arbitrary" is a good
>> alternative.
>>
>> Tobias
>>
>> Florian Haftmann schrieb:
>>> Some years ago two further constants were introduces into HOL.thy:
>>> "undefined" and "default".  The idea then was to divide the role of
>>> classical "arbitrary" on two shoulders:  "undefined" should be
>>> unspecified an could be used to fake partiality, whereas "default" would
>>> be overloaded and could be instantiated on arbitrary types, which is
>>> useful e.g. for proof extraction.  Meanwhile the code dealing with
>>> unspecified case clauses and missing primrec equations etc. has already
>>> switched from "arbitrary" to "undefined".
>>>
>>> I would suggest to walk through and drop any remaining occurence of
>>> "arbitrary" by "undefined".
>>>
>>> But perhaps "arbitrary" is too deep-rooted in HOL tradition to just get
>>> rid of it.  Any further arguments against?
>>>
>>>     Florian
>>>
>>>
>>>
>>> ------------------------------------------------------------------------
>>>
>>> _______________________________________________
>>> Isabelle-dev mailing list
>>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>