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



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.