[isabelle-dev] top and bot

[Makarius]

On Mon, 3 May 2010, Brian Huffman wrote:

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

If the qualifier for the class constant is made mandatory, one can get 
along without hide_const (hide operations are always something like a 
workaround).  For example:

ML {*
   fun definition (b, t) =
     Theory_Target.init NONE #> Local_Theory.define ((b, NoSyn), (Attrib.empty_binding, t))
     #> #2 #> Local_Theory.exit #> ProofContext.theory_of
*}

setup {* definition (Binding.qualify false "foo_class" @{binding foo}, @{term True}) *}
setup {* definition (Binding.qualify true "class" @{binding foo}, @{term True}) *}

term foo            -- "foo_class.foo printed as foo"
term foo_class.foo  -- "as above"
term class.foo      -- "printed as class.foo"


 	Makarius