如何让 typedef 类型从类型类的母类型继承运算符

发布答案后续问题

Brian 提供了答案，并建议使用提升和转移的解决方案。然而，我找不到足够的关于举重和转移的教程信息，无法知道如何调整他的答案来完成我需要做的事情。

在这里，我在黑暗中工作，并使用给出的答案作为即插即用模板来提出这个后续问题。

我最初的代码中的命令，typedef trivAlg = "{x::sT. x = emS}"给我一个新类型，它是母类型的子集sT.

我有我的会员运营商consts inP :: "sT => sT => bool"，所以在我对提升和转移的天真的看法中，因为我monoid_add0 已被定义为常数emS::sT，我可以做出这样的声明，(emS::sT) inP emS，我想做这样的事情：

theorem "~((0::trivAlg) inP 0)"

所以，我尝试使用提升来让我的操作员inP使用类型trivAlg像这样：

lift_definition inP_trivAlg :: "trivAlg => trivAlg => bool"
  is "% x y. (x inP y)" 
  by simp

theorem "~((0::trivAlg) inP 0)"

theorem "(emS::trivAlg) = emS"

但是，我的使用发生了类型冲突theorem因为我使用的类型sT and trivAlg不兼容。

如果可以添加答案以向我展示如何获得我的inP使用类型trivAlg我会很感激。或者，也许我离题太远了。

（原始）问题的预备知识

我有我的类型sT，代表“一切都是集合”。到目前为止，我所有的常量和运算符都已用单一类型定义sT。例如，我的空集、成员运算符和联合运算符的定义如下：

consts emS :: "sT"
consts inP :: "sT => sT => bool"
consts geU :: "sT => sT"

我现在正在做一些早期调查，看看我是否可以绑我的sT进入广义组团体.thy http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/Groups.html.

来自霍尔文件 http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/document.pdf，我试图从 Groups 的 4.2、4.3 和 4.4 节以及 Nat 的 15.2 和 15.3 节中获取示例。

在这里，我几乎要问我的问题了，但我不知道我是否在问一个聪明的问题。我认为我知道的是，解决方案可能仅涉及语言环境、子语言环境和解释，而不是类型类。

我一直在看一点语言环境.pdf http://isabelle.in.tum.de/website-Isabelle2013/dist/Isabelle2013/doc/locales.pdf and 类.pdf http://isabelle.in.tum.de/website-Isabelle2013/dist/Isabelle2013/doc/classes.pdf，所以我知道语言环境和类是交织在一起的。我也一直在看伊萨尔数学库 http://slawekk.wordpress.com/2013/02/25/isarmathlib-1-8-0-released/查看那里如何使用语言环境、子语言环境和解释。

问题

我的问题是，通过下面我的微不足道的代数结构，trivAlg，这是一个新类型，定义为typedef，我如何使用类型类进行设置，以便我可以使用我的常量，例如emS, inP, and geU上面列出了类型的元素trivAlg?

列出下面的代码后，我会询问一些有关特定代码行的问题团体.thy http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/Groups.html.

The Code

typedef trivAlg = "{x::sT. x = emS}"
  by auto

instantiation trivAlg :: zero
begin
definition trivAlg_zero:
  "0 = Abs_trivAlg emS"
instance ..
end

instantiation trivAlg :: monoid_add
begin
definition plus_trivAlg:
  "m + n = (Abs_trivAlg emS)" 
instance proof
  fix n m q :: trivAlg
  show "(n + m) + q = n + (m + q)"
    by(metis plus_trivAlg)
  show "0 + n = n"
    apply(induct n) apply(auto)
    by(metis plus_trivAlg)
  show "n + 0  = n"
    apply(induct n) apply(auto)
    by(metis plus_trivAlg)
qed
end

theorem
  "((n::trivAlg) + m) + q = n + (m + q)"
  by(metis plus_trivAlg)

theorem
  "((0::trivAlg) + 0) = 0"
  by(metis monoid_add_class.add.left_neutral)

关于 Groups.thy 的后续问题

Groups.thy 中的第 151 到 155 行有以下代码：

class semigroup_add = plus +
  assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"

sublocale semigroup_add < add!: semigroup plus proof
qed (fact add_assoc) 

没有一份文档教我如何使用类、区域设置、子区域设置和解释，所以我不知道它到底告诉我什么。

如果我想使用semigroup_add这是在 Groups.thy 中，我可以选择将其用作类型类还是语言环境吗？

获取type对应的操作trivAlg，可能最简单的方法是使用 Isabelle 的 Lifting 套餐；然后您可以使用 Transfer 包来证明类实例。这是一个例子：

typedef trivAlg = "{x::sT. x = emS}"
  by auto

setup_lifting type_definition_trivAlg

instantiation trivAlg :: zero
begin
lift_definition zero_trivAlg :: "trivAlg" is "emS" .
instance ..
end

instantiation trivAlg :: monoid_add
begin
lift_definition plus_trivAlg :: "trivAlg => trivAlg => trivAlg"
  is "% x y. emS"
by simp

instance proof
  fix n m q :: trivAlg
  show "(n + m) + q = n + (m + q)"
    by transfer simp
  show "0 + n = n"
    by transfer simp
  show "n + 0  = n"
    by transfer simp
qed
end