[isabelle-dev] An ARBITRARY question
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
[isabelle-dev] An ARBITRARY question
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
[isabelle-dev] An ARBITRARY question
On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote: I also think that two would be better than three; technically undefined is the same as arbitrary Then what is the point of undefined_fun: undefined x = undefined in HOL.thy? Best, Tjark
[isabelle-dev] An ARBITRARY question
Then what is the point of undefined_fun: undefined x = undefined in HOL.thy? This is essentially pointless and is so soon to be dropped that I didn't take the effort to even point out to it in my emails, taking the risk that somebody would have a look a the source ;-) Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20081003/577547fb/attachment.pgp
[isabelle-dev] An ARBITRARY question
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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20081002/0bf82e20/attachment.pgp
[isabelle-dev] An ARBITRARY question
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
