Email Gateway (Aug 19 2022 at 16:06): Email Gateway (Aug 19 2022 at 16:06):From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,
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?
Many thanks,
Wenda
Email Gateway (Aug 19 2022 at 16:07):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 16:07):From: Brian Huffman <huffman.brian.c@gmail.com>
Hi Wenda,
I had two reasons for hiding those constants:
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.
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.
Last updated: Apr 25 2024 at 08:20 UTC