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
>
> Nonetheless, if you really want to tinker with const names, there are at
> least two possibilities: (1) abbreviations or (2) name space aliases.
>
> For example:
>
>   abbreviation "cauchy ≡ Real.cauchy"
>
>   setup ‹Sign.const_alias @{binding cauchy} @{const_name Real.cauchy}›
>
> The alias is more low-level -- you normally don't do that to avoid mass
> confusion in libraries, which explains why there is no Isar command for
> that. It reverse the effect of 'hide' more precisely, though.
>
>
>         Makarius




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