Comment définir une instance de classe de type_synonym?

Question

type est une instance de classe semilattice_sup:

datatype type = BType | IType | AType 

instantiation type :: semilattice_sup 
begin 
end 

Je suis en train de déclarer type × bool le type comme une instance de cette classe aussi:

type_synonym stype = "type × bool" 

instantiation stype :: semilattice_sup 
begin 
end 

Mais je reçois l'erreur suivante:

Bad type name: "stype" 

Comment définir une instance de classe de type_synonym?

Answer 1

Vous ne pouvez pas. En fait, il est déjà une instance de semilattice_sup pour le type de produit Product_Order dans HOL-bibliothèque, donc si type a un fait alors par exemple, semilattice_sup si type × bool (si vous incluez Product_Order. Notez que ceci est l'ordre de pointwise, non celui lexicographique

Si vous avez besoin d'un autre ordre ou quelque chose de très spécifique à votre type, vous pouvez également définir un type entièrement nouveau avec typedef.

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

Cela vous donne morphismes Abs_type' et Rep_type' pour convertir entre type' et type × bool, et comme il s'agit d'un type complètement nouveau, vous pouvez lui fournir des instances de classe de type. Par souci d'exhaustivité, les classes de types sont implémentées avec les locales, et vous pouvez interpréter les paramètres régionaux des classes de type manuellement, vous donnant toutes les définitions et les lemmes de la classe type, mais bien sûr, l'intégration avec le framework de classe de type ne fonctionnera pas. Pour un, type × bool ne sera pas du type semilattice_sup. Pourtant, de temps en temps, cela peut être une solution viable:

interpretation type_bool: semilattice_sup mysup myle myless 
proof 

(où mysup, myle, myless sont sup, ≤, < pour type × bool, que vous devez fournir, puis prouver qu'ils remplissent les axiomes les noms. sont, bien sûr, complètement arbitraires, y compris type_bool)