在 Isabelle 中定义带参数的子类

Question

documentation on typeclasses in Isabelle（第 3.5 节）通过给出缺失公理的证明，解释了如何定义额外的子类关系 "after the fact"。有没有办法在子类除了公理之外还加参数的时候做这个？

例如，假设我有以下类:

class setoid =
fixes eq :: "'a ⇒ 'a ⇒ bool" (infix "≈" 50)
assumes eq_refl : "∀x. x ≈ x"
and eq_symm : "∀x y. x ≈ y ⟶ y ≈ x"
and eq_trans : "∀x y z. x ≈ y ⟶ y ≈ z ⟶ x ≈ z"

class preorder =
fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≲" 50)
assumes le_refl : "∀x. x ≲ x"
and le_trans : "∀x y z. x ≲ y ⟶ y ≲ z ⟶ x ≲ z"

当我们对称其不等式时，每个预序都应该是一个 setoid：

definition (in preorder) peq :: "'a ⇒ 'a ⇒ bool"
where "peq x y ≡ (x ≲ y) ∧ (y ≲ x)"

然而，以下失败：

subclass (in preorder) setoid

错误 exception TYPE raised: Class preorder lacks parameter(s) "setoid_class.eq" of setoid。但是我想不出一个语法来告诉伊莎贝尔这个缺失的参数应该是我定义的关系peq。

如果我下拉到语言环境而不是类型，我可以做到这一点类（为简洁起见省略了证明）：

interpretation peq_class : setoid peq
proof
show "∀x. peq x x" sorry
show "∀x y. peq x y ⟶ peq y x" sorry
show "∀x y z. peq x y ⟶ peq y z ⟶ peq x z" sorry
qed

但这不允许我将 preorder 用作 setoid，即 interpretation 不像 subclass 或 instantiation。我想要的是能够将一个类型实例化为预序，然后通过不等式的对称化，自动能够在该类型上使用关于 setoids 的定义和定理。我怎样才能做到这一点？

Answer 1

这是 Isabelle 中实现类型 classes 的方式的限制。我不确定以下解决方法是否尽可能短，但它有效：

class eq =
  fixes eq :: "'a ⇒ 'a ⇒ bool" (infix "≈" 50)

class setoid = eq +
  assumes eq_refl : "∀x. x ≈ x"
    and eq_symm : "∀x y. x ≈ y ⟶ y ≈ x"
    and eq_trans : "∀x y z. x ≈ y ⟶ y ≈ z ⟶ x ≈ z"

class preorder =
  fixes le :: "'a ⇒ 'a ⇒ bool" (infix "≲" 50)
  assumes le_refl : "∀x. x ≲ x"
    and le_trans : "∀x y z. x ≲ y ⟶ y ≲ z ⟶ x ≲ z"

class preorder_setoid = preorder + eq +
  assumes eq_def: "x ≈ y ⟷ (x ≲ y) ∧ (y ≲ x)"

subclass (in preorder_setoid) setoid
  apply standard
  unfolding eq_def
  using le_refl le_trans by auto

缺点是您仍然无法自动将 preorder 的任何实例生成为 setoid，但您必须手动执行。对于每个 preorder 个实例，您可以添加一个 preorder_setoid 个实例。所有这些看起来都一样；他们必须根据 eq_def 定义 eq。然后证明是自动的。

Update 正如评论中指出的那样，eq 常量将始终在 eq class 的上下文中进行解释；也就是说，如果没有进一步的类型注释，就无法证明任何有趣的事情。可以告诉类型推断做得更好：

setup {*
  Sign.add_const_constraint (@{const_name "eq"}, SOME @{typ "'a::setoid ⇒ 'a ⇒ bool"})
*}

在 Isabelle 中定义带参数的子类

Defining a subclass with parameters in Isabelle

isabelle