[isabelle-dev] An ARBITRARY question

[Lawrence Paulson]

What is the difference between  willundefined 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