如何证明原始类型类定义之外的类型类的相关性？

问题描述

我正在尝试其他方法来编写来自 this question 和 Isabelle 2020 的 Rings.thy 的以下证明。（特别是，我添加了 note div_mult_mod_eq[of a b] 行来测试 note 命令的使用：

lemma mod_div_decomp:
  fixes a b
  obtains q r where "q = a div b" and "r = a mod b"
    and "a = q * b + r"
proof -
  from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
  note div_mult_mod_eq[of a b]
  moreover have "a div b = a div b" ..
  moreover have "a mod b = a mod b" ..
  note that ultimately show thesis by blast
qed

但是，如果我将其写在单独的 .thy 文件中，则会在 note 行出现有关类型统一的错误：

Type unification Failed: Variable 'a::{plus,times} not of sort semiring_modulo

Failed to meet type constraint:

Term:  a :: 'a
Type:  ??'a

如果我将整个证明包含在一对类型类 class begin ... end 中，问题就会迎刃而解：

theory "test"
  imports Main 
  HOL.Rings
 begin
  ...

    class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
      assumes div_mult_mod_eq: "a div b * b + a mod b = a"
    begin
     (* ...  inserted proof here *)
    end

 ... 
end

我的问题是：

这是证明关于类型类的定理的正确方法吗？即在不同的文件中编写单独的类定义？

是否总是需要像我一样复制类型类定义？

如果不是，在原始定义位置之外证明关于类型类的定理的正确方法是什么？

解决方法

有两种方法可以证明类型类中的事物（对于 Isabelle/HOL 基本上是 sort = typeclass）：

在类型类的上下文中证明

context semiring_modulo
begin
...
end

（稍微不那么干净）向类型添加排序约束：

lemma mod_div_decomp:
  fixes a b :: "'a :: {semiring_modulo}"
  obtains q r where "q = a div b" and "r = a mod b"
    and "a = q * b + r"

semiring_modulo 包含 plus 和 times，但您也可以键入 {semiring_modulo,plus,times} 以真正拥有它们。

documentation of classes 包含更多示例。

您遇到的问题与 Isabelle 如何实现多态有关。排序代表所有类型的一个子集，我们用一组相交的类来表征它们。通过将排序附加到变量，我们限制了可以实例化该变量的术语空间。看待这个问题的一种方法是假设变量属于某种类型。在您的情况下，类型推断 (+) (*) div mod 显然给了您 {plus,times}，这对于 div_mult_mod_eq 来说是不够的。要进一步限制变量，您可以按照 Mathias 的解释进行显式类型注释。请注意，上面一行中的 simp 应该会遇到同样的问题。

isabelle typeclass