[isabelle-dev] top and bot

[Brian Huffman]

Hello all,

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"
and "bot":

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
names?

- Brian