[isabelle-dev] top and bot
brianh at cs.pdx.edu
Sat May 1 17:22:54 CEST 2010
Every time I use the overloaded constants "top" and "bot" (defined in
Orderings.thy), Isabelle prints them out as "top_class.top" and
"bot_class.bot", instead of just "top" and "bot". I find this
annoying, so I tried to find out the reason for this.
Here are the class definitions from Orderings.thy that introduce "top"
class top = preorder +
fixes top :: 'a
assumes top_greatest [simp]: "x \<le> top"
class bot = preorder +
fixes bot :: 'a
assumes bot_least [simp]: "bot \<le> x"
The problem is that the definition of class top defines *two*
constants named "top" - "Orderings.top", which is the name of the
locale predicate, and "Orderings.top_class.top", which is the name of
the overloaded constant. But the name of the locale predicate is
totally inaccessible, since "Orderings.top" parses as "top_class.top"
(I guess the "top_class" part of the qualified name is flagged as
optional). This means that I can't even hide the locale predicate with
"hide_const Orderings.top" - the effect is to hide the wrong constant.
There is a similar situation with class finite in Finite_Set.thy, but
there a workaround is possible due to the fact that the constant
"finite" is defined separately from the class definition. The same
trick won't work here.
Can anyone suggest a workaround for this, or will it be necessary to
change the names of the classes to be distinct from the constant
More information about the isabelle-dev