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



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.