这个问题与我之前的SO问题有关类型类。我问这个问题是为了设置一个有关语言环境的未来问题。我不认为类型类适合我想要做的事情，但是类型类的工作方式让我了解了我想要从语言环境中得到什么。
下面，当我使用大括号表示法时{0,0}，它不代表普通的 HOL 大括号，并且0代表空集。
一些文件，如果你想要的话
-
A_i130424a.thy- ASCII 友好的 THY。
-
i130424a.thy- 非 ASCII 友好的 THY。
-
i130424a_DOC.pdf- PDF 显示行号。
-
MFZ_DOC.pdf- 与此相关的主要项目。
-
此问题的 GitHub 文件夹 and MFZ GitHub folder.
提问前谈话
我在 THY 中描述了我正在做的事情（我将其包含在底部），然后我基本上会问：“我可以在这里做些什么来解决这个问题，以便我可以使用类型类吗？”
正如上面链接的SO问题一样，我试图结合团体.thy semigroup_add。我所做的是创建我的类型的子类型sT using typedef，然后我尝试将一些基本的函数常量和运算符提升为新类型，例如我的联合运算符geU，我的空集emS，我的无序配对集paS，以及我的隶属谓词inP.
这不起作用，因为我试图将新类型视为子集。特别是，我的新类型应该代表集合{ {0,0} }，它是平凡半群的一部分，即只有一个元素的半群。
问题是无序对公理指出如果设置x存在，则设置(paS x x)存在，并且联合公理指出，如果设置x存在，则设置(geU x)存在。因此，当我尝试将联合运算符提升为新类型时，证明者神奇地知道我需要证明(geU{0,0} = {0,0})，这不是真的，但只有一个元素{0,0}在我的新类型中，所以它必须是这样的。
Question
我可以解决这个问题吗？在我看来，我将集合和子集与类型和子类型进行比较，我知道它们并不相同。调用我的主要类型sT和我的亚型subT。我需要的是所有已用类型定义的运算符sT，类型如sT => sT, 为类型工作subT when subT被视为类型sT。使用类型定义的新运算符和常量subT，例如类型的函数subT => subT，这会以某种方式解决，就像事情神奇地应该与这些东西一起工作一样。
发表问题谈话
在这里，我通过 THY 中的行号指出发生了什么。行号将显示在 PDF 和 GitHub 网站上。
在第 21 行到第 71 行中，我在四个部分中组合了相关常数、符号和公理。
- Type
sT, 隶属谓词inP/PIn，以及等式公理（21 至 33）。
- 空集
emS/SEm和空集公理（37 到 45）。
- 无序对常数
paS/SPa和无序对公理（49 到 58）。
- 联合常数
geU/UGe和联合公理（62 至 71）。
从第 75 行开始，我创建了一个新类型typedef然后将其实例化为类型类semigroup_add.
在我尝试提升无序对函数之前没有任何问题{.x,y.}，第 108 行，以及我的 union 函数(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
