0

以下代码不进行类型检查：

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

为什么这样？我错过了使用解释的东西吗？我怀疑我在这里需要一个新类型包装器之类的东西......

4

1 回答 1

1

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

如果您使用小于来实例化order选项类型的类型类，那么您可以使用映射，因为函数空间以逐点顺序实例化。然而，地图上的排序只会在语义上等价于，而不是在句法上，因此现有的关于 的定理都不适用，反之亦然。此外，您的理论将与其他人的不同实例化的理论不兼容。NoneSome xmonoorder<=⊆⇩m⊆⇩m<=orderoption

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

于 2016-06-24T15:44:36.343 回答