Isabelle：Class 的拓扑向量空间

Question

我想用显而易见的方式定义拓扑向量空间的class：

theory foo
imports Real_Vector_Spaces 
begin

class topological_vector = topological_space + real_vector +
  assumes add_cont_fst: "∀a. continuous_on UNIV (λb. a + b)"
  ...

但我收到错误 Type inference imposes additional sort constraint topological_space of type parameter 'a of sort type

我尝试在条件中引入类型约束，看起来像 continuous_on 不想与 class.

的默认类型 'a 匹配

当然我可以通过用等效条件替换连续性来解决这个问题，我只是好奇为什么这不起作用。

Answer 1

在Isabelle/HOL中的一个class定义中，可能只出现一个类型变量（即'a），它具有默认的HOL排序type。因此，不能形式化多参数类型 classes。这也会影响定义inside类型classes，它可能只依赖于一种类型class的参数。例如，您可以在类型 class 上下文 topological_space 中定义一个谓词 cont :: 'a set => ('a => 'a) => bool，如下所示

definition (in topological_space) cont :: "'a set ⇒ ('a ⇒ 'a) ⇒ bool"
where "cont s f = (∀x∈s. (f ---> f x) (at x within s))"

目标 (in topological_space) 告诉类型 class 系统 cont 实际上只依赖于一种类型。因此，在继承自 topological_space.

的其他类型 class 的假设中使用 cont 是安全的

现在，Isabelle/HOL 中的谓词 continuous_on 具有类型 'a set => ('a => 'b) => bool，其中 'a 和 'b 都必须属于 topological_space .因此，continuous_on比cont更通用，因为它允许不同的拓扑空间a和b。相反，continuous_on 不能在任何 one 类型 class 中定义。因此，您也不能在 classes 类型的假设中使用 continuous_on。这个限制并不特定于 continuous_on，它出现在所有类型的态射中，例如mono 用于保序函数，代数结构之间的同态等。单参数类型 classes 无法表达这些东西。

在您的示例中，您会收到错误，因为 Isabelle 将所有出现的类型变量统一为 'a，然后意识到 continuous_on 强制对 'a 进行排序 topological_space，但由于上述原因，您可能不依赖 class 规范中的排序。

不过，可能有一个简单的出路。只需如上所述定义 cont 并在 topological_vector 的假设中使用它而不是 continuous_on。在 class 上下文之外，您可以证明 cont = continuous_on 并使用 continuous_on 而不是 cont 推导原始假设。这使您无法在 class 上下文中进行抽象推理，但这只是一个小限制。

Isabelle：Class 的拓扑向量空间

Isabelle: Class of topological vector spaces

isabelle