如何在集合上定义上确界？

Question

我正在尝试描述一种编程语言的类型系统。它具有任何类型的公共子类型 (VoidType) 和任何类型的公共超类型 (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"

我正在尝试将 type 实例化为 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

你能建议如何定义上元函数吗Sup :: OCL.type set ⇒ OCL.type？

Answer 1

类型 OCL.type 是有限的，所以类型 OCL.type set 的所有集合也是有限的。此外，您的层次结构中还有一个顶级元素。因此，您可以简单地通过在给定集上折叠 sup 来定义 Sup 操作。语言环境 comm_monoid_set 提供了必要的基础设施。首先，实例化类型类 semilattice_sup 和 order_top。然后解释 comm_monoid_set:

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

这会在名称 ocl.F 下的集合上生成折叠 sup 操作。所以，

definition "Sup_ocl = ocl.F id"

为您提供了 Sup 操作的定义。这是适用于任何具有顶元素的有限上半格的通用构造。但它不会为您提供任何专门的设置来特别推理 OCL.type 层次结构。您必须自己推导出适当的规则。

如何在集合上定义上确界？

How to define a supremum on a set?

isabelle