这个问题关系到我的以前的SO问题类型的类 。 我问这个问题，以建立未来约语言环境的问题。 我不认为类型类会为我想要做的工作，但如何类型类的工作给了我什么，我想出来的语言环境的想法。
下面，当我用大括号标记{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 。
这不工作，因为我试图把新型就像一个子集。 具体地讲，我的新类型应该代表该组{ {0,0} }其意图是琐碎半群的一部分，与只有一个元件的半群。
的问题是，二元集合公理指出，如果设置x存在，则设置(paS xx)存在，并且，如果设置的联合公理状态x存在，则设置(geU x)存在。 所以，当我试图举起我的工会运营商到我的新类型，证明方神奇地知道我需要证明(geU{0,0} = {0,0})这是不正确的，但只有一个元素{0,0}在我的新类型，所以它必须是这样的。
题
我能解决这个问题？ 在我的脑海里，我比较集和亚群的类型和子类型，在那里我知道他们是不一样的。 叫我的主要类型， sT和我的亚型subT 。 我需要的是我所有的运营商已经与类型定义sT ，类型，如sT => sT ，类型工作subT时subT被视为类型sT 。 新的运营商和常量已使用类型定义subT ，如类型的函数subT => 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 ，然后实例作为类型的类semigroup_add 。
有没有问题，直到我试图举起我的二元集合功能{.x,y.} ，线108，和我的工会函数(geU x)线114。
下面伊萨尔命令，我表明，在告诉我，我需要证明，某些集等于输出{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
