CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to define a supremum on a set?

I'm trying to describe a type system of a programming language. It has a common subtype for any types (VoidType) and a common supertype for any 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"

I'm trying to instantinate type as 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

Could you suggest how to define a supremum function Sup :: OCL.type set ⇒ OCL.type?

Upvotes: 0

Views: 147

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5078

The type OCL.type is finite, so all sets of type OCL.type set are finite, too. Moreover, there is also a top element in your hierarchy. Therefore, you can define the Sup operation simply by folding sup over the given set. The locale comm_monoid_set provides the necessary infrastructure. First, instantiate the type classes semilattice_sup and order_top. Then interpret comm_monoid_set:

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

This generates the folded sup operation over sets under the name ocl.F. So,

definition "Sup_ocl = ocl.F id"

gives you a definition for the Sup operation. This is a general construction that works for any finite upper semilattice with a top element. But it will not give you any dedicated setup for reasoning about the OCL.type hierarchy in particular. You'll have to derive appropriate rules yourself.

Upvotes: 1

Related Questions