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 >>
