这个问题与我之前关于 type classes的 SO question 有关。我问这个问题是为了建立一个关于语言环境的未来问题。我不认为类型类适用于我正在尝试做的事情，但是类型类的工作方式让我了解了我想要从语言环境中得到什么。
下面，当我使用大括号符号{0,0}时，它并不代表普通的 HOL 大括号，而是代表0空集。
一些文件，如果你想要的话
- A_i130424a.thy - ASCII 友好的 THY。
- i130424a.thy - 非 ASCII 友好的 THY。
- i130424a_DOC.pdf - 显示行号的 PDF。
- MFZ_DOC.pdf - 与之相关的主要项目。
- 此问题的GitHub 文件夹和MFZ GitHub文件夹。
题前谈话
我描述了我在 THY 中所做的事情（包括在底部），然后我基本上会问，“我可以在这里做些什么来解决这个问题，以便我可以使用类型类吗？”
与上面链接的 SO 问题一样，我试图与Groups.thy semigroup_add联系起来。我所做的是使用创建我的类型的子类型sT，typedef然后尝试将一些基本函数常量和运算符提升到新类型中，例如我的联合运算符geU、我的空集emS、我的无序对集paS和我的成员资格谓词inP.
这不起作用，因为我试图将新类型视为子集。特别是，我的新类型应该表示 set { {0,0} }，它旨在成为平凡半群的一部分，一个只有一个元素的半群。
问题是无序对公理声明如果集合x存在则集合(paS x x)存在，而联合公理声明如果集合x存在则集合(geU x)存在。因此，当我尝试将联合运算符提升到我的新类型中时，证明者神奇地知道我需要证明(geU{0,0} = {0,0})，这是不正确的，但{0,0}我的新类型中只有一个元素，所以它必须是那样的。
问题
我可以解决这个问题吗？在我看来，我将集合和子集与类型和子类型进行比较，我知道它们并不相同。调用我的主要类型sT和我的子类型subT。我需要的是所有使用 type 定义的运算符，sT例如，在被视为sT => sTtypesubT时为 type 工作。使用 type 定义的新运算符和常量，例如 type 的函数，它们会以某种方式工作，就像神奇地应该与这些东西一起工作。 subTsTsubTsubT => subT
发表问题谈话
在这里，我通过 THY 中的行号指出发生了什么。行号将显示在 PDF 和 GitHub 站点上。
在第 21 到 71 行中有四个部分，我将相关的常量、符号和公理组合在一起。
- 类型
sT、隶属谓词inP/PIn和等式公理（21 到 33）。 - 空集
emS/SEm和空集公理（37 到 45）。 - 无序对常数
paS/SPa和无序对公理（49 到 58）。 - 联合常数
geU/UGe和联合公理（62 到 71）。
从第 75 行开始，我创建了一个新类型，typedef然后将其实例化为 type class semigroup_add。
在我尝试提升我的无序对函数{.x,y.}（第 108 行）和我的联合函数(geU x)（第 114 行）之前，没有任何问题。
在 Isar 命令下方，我显示的输出告诉我我需要证明某些集合等于{0,0}，这是无法证明的事实。
这是 ASCII 友好的源代码，我从上面链接的 THY 中删除了一些注释和行：
theory A_i130424a
imports Complex_Main
begin
--"AXIOM (sT type, inP predicate, and the equality axiom)"
typedecl sT ("sT")
consts PIn :: "sT => sT => bool"
notation
PIn ("in'_P") and
PIn (infix "inP" 51) and
PIn (infix "inP" 51)
axiomatization where
Ax_x: "(! x. x inP r <-> x inP s) <-> (r = s)"
--"[END]"
--"AXIOM (emS and the empty set axiom)"
consts SEm :: "sT" ("emS")
notation (input)
SEm ("emS")
axiomatization where
Ax_em [simp]: "(x niP emS)"
--"[END]"
--"AXIOM (paS and the axiom of unordered pairs)"
consts SPa :: "sT => sT => sT"
notation
SPa ("paS") and
SPa ("({.(_),(_).})")
axiomatization where
Ax_pa [simp]: "(x inP {.r,s.}) <-> (x = r | x = s)"
--"[END]"
--"AXIOM (geU and the axiom of unions)"
consts UGe :: "sT => sT"
notation
UGe ("geU") and
UGe ("geU")
axiomatization where
Ax_un: "x inP geU r = (? u. x inP u & u inP r)"
--"[END]"
--"EXAMPLE (A typedef type cannot be treated as a set of type sT)"
typedef tdLift = "{x::sT. x = {.emS,emS.}}"
by(simp)
setup_lifting type_definition_tdLift
instantiation tdLift :: semigroup_add
begin
lift_definition plus_tdLift:: "tdLift => tdLift => tdLift"
is "% x y. {.emS,emS.}" by(simp)
instance
proof
fix n m q :: tdLift
show "(n + m) + q = n + (m + q)"
by(transfer,simp)
qed
end
theorem
"((n::tdLift) + m) + q = n + (m + q)"
by(transfer,simp)
class tdClass =
fixes emSc :: "'a" ("emSk")
fixes inPc :: "'a => 'a => bool" (infix "∈k" 51)
fixes paSc :: "'a => 'a => 'a" ("({.(_),(_).}k)")
fixes geUc :: "'a => 'a" ("⋃k")
instantiation tdLift :: tdClass
begin
lift_definition inPc_tdLift:: "tdLift => tdLift => bool"
is "% x y. x inP y"
by(simp)
lift_definition paSc_tdLift:: "tdLift => tdLift => tdLift"
is "% x y. {.x,y.}"
--"OUTPUT: 1. (!! (sT1 sT2). ([|(sT1 = emS); (sT2 = emS)|] ==> ({.sT1,sT2.} = emS)))"
apply(auto)
--"OUTPUT: 1. ({.emS.} = emS)"
oops
lift_definition geUc_tdLift:: "tdLift => tdLift"
is "% x. geU x"
--"OUTPUT: 1. (!! sT. ((sT = {.emS,emS.}) ==> ((geU sT) = {.emS,emS.})))"
apply(auto)
--"OUTPUT: 1. ((geU {.emS,emS.}) = {.emS,emS.})"
oops
lift_definition emSc_tdLift:: "tdLift"
is "emS"
--"OUTPUT:
exception THM 1 raised (line 333 of drule.ML):
RSN: no unifiers
(?t = ?t) [name HOL.refl]
((emS = {.emS,emS.}) ==> (Lifting.invariant (% x. (x = {.emS,emS.})) emS emS))"
oops
instance ..
end
--"[END]"
end