[isabelle-dev] top and bot

[Brian Huffman]

On Mon, May 3, 2010 at 4:55 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
>> 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 fact that both class predicate and class operation have the same
> base name is indeed confusing.  Meanwhile it should be possible to
> insert a non-mandatory qualifier into the name binding of the class
> predicate, e.g. "pred", or even "class".  Any objections?

Let me see if I understand your proposal correctly.

Currently, the declaration for class "top" defines two constants:

class predicate: "Orderings.top"
overloaded constant: "Orderings.top_class.top"

In your proposed scheme, these would be changed to

class predicate: "Orderings.pred.top"
overloaded constant: "Orderings.top_class.top"

So in the new system, "term top" would still print out as
"top_class.top". But it would be possible to write "pred.top" to
unambiguously refer to the class predicate (which is not currently
possible), and in turn this would enable us to use the "hide_const"
like this:

hide_const (open) Orderings.pred.top

which would make "top" just print out as "top". Is this right?

It sounds like a sensible idea to me, although we should make sure we
understand how it would affect the situation with class "finite". It
would be best if any change we make avoids ugly workarounds in all
situations ("top"/"bot" as well as "finite").

- Brian