CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to define a class instance of type_synonym?

type is an instance of semilattice_sup class:

datatype type = BType | IType | AType

instantiation type :: semilattice_sup
begin
end

I'm trying to declare type × bool type as an instance of this class too:

type_synonym stype = "type × bool"

instantiation stype :: semilattice_sup
begin
end

But I get the following error:

Bad type name: "stype"

How to define a class instance of type_synonym?

Upvotes: 2

Views: 257

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8258

You can't. In fact, there is already an instance of semilattice_sup for the product type in Product_Order in HOL-Library, so if type has an semilattice_sup instance, then so does type × bool (if you include Product_Order. Note that this is the pointwise order, not the lexicographic one.

If you need another order or something very specific to your type, you can also define an entirely new type with typedef:

typedef type' = "UNIV :: (type × bool) set"
  by auto

That gives you morphisms Abs_type' and Rep_type' to convert between type' and type × bool, and since this is a completely new type, you can provide type class instances for it.

For the sake of completeness, type classes are implemented with locales, and you can interpret the type class locale manually, giving you all the definitions and lemmas from the type class, but of course, the integration with the type class framework will not work. For one, type × bool will not be of the sort semilattice_sup. Still, occasionally, this can be a viable solution:

interpretation type_bool: semilattice_sup mysup myle myless
proof

(where mysup, myle, myless are sup, ≤, < for type × bool, which you have to provide and then prove that they fulfil the axioms. The names are, of course, completely arbitrary, including type_bool)

Upvotes: 3

Related Questions