[isabelle-dev] An ARBITRARY question

[Tobias Nipkow]

"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