*To*: Wenda Li <wl302 at cam.ac.uk>*Subject*: Re: [isabelle] How to "unhide" constants in Isabelle*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Sat, 13 Sep 2014 09:22:16 -0700*Cc*: Makarius <makarius at sketis.net>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1409131652030.52395@lxbroy10.informatik.tu-muenchen.de>*References*: <561fdf8c271564ae066fd8c9682d9027@cam.ac.uk> <alpine.LNX.2.00.1409131652030.52395@lxbroy10.informatik.tu-muenchen.de>

On Sat, Sep 13, 2014 at 7:57 AM, Makarius <makarius at sketis.net> wrote: > On Sat, 13 Sep 2014, Wenda Li wrote: > >> I am using constants such as Real.Real, Real.cauchy and Real.vanishes in >> my theory. However, as some implementation details of reals are hidden by >> the statement >> >> hide_const (open) vanishes cauchy positive Real >> >> in "Real.thy", I have to use "Real.cauchy" instead of "cauchy" in my >> files, which is slightly annoying. Is there a way to "unhide" those >> constants in my files to make it more convenient? > > > I guess Brian Huffman had good reasons to hide these implementation details > when he introduced that in 2010 here: > http://isabelle.in.tum.de/repos/isabelle/rev/e05e1283c550#l4.1482 Hi Wenda, I had two reasons for hiding those constants: 1. More general versions of them are defined in later theories. If you import Complex_Main, you get predicates like "Cauchy X" and "X ----> 0" which work for arbitrary metric spaces. Currently we fail to provide an instance "rat :: metric_space" in the standard library (and we should probably add one) but it's not hard to define one yourself, with "dist x y = of_rat (abs (x - y))". Then "Real.cauchy X" is equivalent to "Cauchy X", "Real.vanishes X" is equivalent to "X ----> 0", and "Real.Real X" is equivalent to "lim (%n. of_rat (X n))". We have invested much more effort in providing a useful collection of theorems about these more general constants. 2. To discourage users from relying on implementation details of the real number type. If at some point in the future we decide to change to a different construction of the reals again, the constants and theorems used in the construction may change or disappear. If despite these reasons you still want to use the hidden constants from Real.thy, then you are welcome to use one of the workarounds that Makarius suggests. - Brian

**References**:**[isabelle] How to "unhide" constants in Isabelle***From:*Wenda Li

**Re: [isabelle] How to "unhide" constants in Isabelle***From:*Makarius

- Previous by Date: Re: [isabelle] How to "unhide" constants in Isabelle
- Next by Date: Re: [isabelle] PolyML "Insufficient memory" exception while building images
- Previous by Thread: Re: [isabelle] How to "unhide" constants in Isabelle
- Next by Thread: [isabelle] Still no smt commands allowed in AFP submissions?
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list