Comment définir un supremum sur un ensemble?

Question

J'essaie de décrire un système de type d'un langage de programmation. Il a un sous-type commun pour tous types (VoidType) et un super-type commun pour tous types (AnyType):

datatype type = 
    VoidType | 
    AnyType | 
    BooleanType | 
    EBooleanType | 
    RealType | 
    IntegerType | 
    UnlimNatType | 
    StringType 

fun subtype_strict_fun :: "type ⇒ type ⇒ bool" (infix "<:sf" 55) where 
    "_ <:sf VoidType = False" 
| "VoidType <:sf _ = True" 
| "AnyType <:sf _ = False" 
| "_ <:sf AnyType = True" 
| "BooleanType <:sf EBooleanType = True" 
| "IntegerType <:sf RealType = True" 
| "UnlimNatType <:sf IntegerType = True" 
| "UnlimNatType <:sf RealType = True" 
| "_ <:sf _ = False" 

definition subtype_fun :: "type ⇒ type ⇒ bool" (infix "<:f" 55) where 
    "x <:f y ≡ x = y ∨ x <:sf y" 

Je suis en train de instantinate type comme ccpo:

instantiation type :: ccpo 
begin 

definition "less_eq = subtype_fun" 
definition "less = subtype_strict_fun" 

lemma subtype_strict_eq_subtype: 
    "(x <:sf y) = (x <:f y ∧ ¬ y <:f x)" 
    by (cases x; cases y; simp add: subtype_fun_def) 

lemma subtype_refl: 
    "x <:f x" 
    by (simp add: subtype_fun_def) 

lemma subtype_trans: 
    "x <:f y ⟹ y <:f z ⟹ x <:f z" 
    by (cases x; cases y; cases z; simp add: subtype_fun_def) 

lemma subtype_antisym: 
    "x <:f y ⟹ y <:f x ⟹ x = y" 
    by (cases x; cases y; simp add: subtype_fun_def) 

instance 
    apply intro_classes 
    apply (simp add: less_eq_type_def less_type_def subtype_strict_eq_subtype) 
    apply (simp add: less_eq_type_def less_type_def subtype_refl) 
    apply (metis less_eq_type_def subtype_trans) 
    apply (metis less_eq_type_def subtype_antisym) 

end 

Pouvez-vous suggérer comment définir une fonction supremum Sup :: OCL.type set ⇒ OCL.type?

Answer 1

Le type OCL.type est fini, donc tous les ensembles de type OCL.type set sont également finis. De plus, il y a aussi un élément supérieur dans votre hiérarchie. Par conséquent, vous pouvez définir l'opération Sup simplement en pliant sup sur l'ensemble donné. Les paramètres régionaux comm_monoid_set fournissent l'infrastructure nécessaire. D'abord, instanciez les classes de type semilattice_sup et order_top. Puis interpréter comm_monoid_set:

interpretation ocl': abel_semigroup sup "top :: OCL.type" <proof> 
interpretation ocl: comm_monoid_set sup "top :: OCL.type" <proof> 

Cela génère l'opération sup repliée sur des ensembles sous le nom ocl.F. Ainsi,

definition "Sup_ocl = ocl.F id" 

vous donne une définition pour l'opération Sup. C'est une construction générale qui fonctionne pour tout semilattice supérieur fini avec un élément supérieur. Mais il ne vous donnera aucune configuration dédiée pour raisonner sur la hiérarchie OCL.type en particulier. Vous devrez vous-même dériver des règles appropriées.