使用有部分地图的订购区域

Question

以下代码未打字：

type_synonym env = "char list ⇀ val"
interpretation map: order "op ⊆⇩m :: (env ⇒ env ⇒ bool)" "(λa b. a ≠ b ∧ a ⊆⇩m b)"
by unfold_locales (auto intro: map_le_trans simp: map_le_antisym)
lemma
  assumes "mono (f :: env ⇒ env)"
  shows "True"
by simp

伊莎贝尔（Isabelle）在引理时抱怨以下错误：

Type unification failed: No type arity option :: order
Type error in application: incompatible operand type
Operator:  mono :: (??'a ⇒ ??'b) ⇒ bool
Operand:   f :: (char list ⇒ val option) ⇒ char list ⇒ val option

为什么呢？我错过了使用这种解释的东西吗？我怀疑我在这里需要类似newtype包装的东西...

Answer 1

当您解释与类型类相对应的order之类的语言环境时，您只能在该语言环境的上下文中得到证明的定理。但是，常数mono仅在类型类中定义。原因是mono的类型包含两个类型变量，而类型类中的Locales内部只有一个变量。您可以注意到这一点，因为您的解释没有map.mono。

如果您将None的选项类型类型类型order实例化，则可以将mono用于映射，因为函数空间将order实现CC_9。但是，地图上的<=排序仅在语义上等同于⊆⇩m，而不是语法，因此有关⊆⇩m的现有定理都不适用于<=，反之亦然。此外，您的理论将与其他人不兼容，以 option实例化order。

因此，我建议您没有类型类。谓词monotone明确采用要使用的订单。这是更多的写作，但是最后，您比类型类更灵活。例如，您可以编写monotone (op ⊆⇩m) (op ⊆⇩m) f来表达f是环境的单调转换。