On Mon, May 3, 2010 at 4:55 AM, Florian Haftmann
florian.haftm...@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
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
