小智 5
如果您从看到该短语的地方引用一点，那会更好。我知道“模式匹配”，也知道“商类型”，但是我不知道“商类型”。
我不希望先澄清一下，然后再等待，所以我选择了三个词中的两个，即“商类型”。如果我走错了道路，那仍然是一个值得探讨的话题，并且是Isabelle / HOL的重要组成部分。
有quotient_type关键字，它允许您定义具有等价关系的新类型。
它是商包的一部分，从isar-ref.pdf的第248页开始进行描述。碰巧有一个Wiki页面Quotient_type。
Brian Hufmann和Ond？ej Kun？ar给出了更复杂的描述。转至Kun？ar的网页，查看两个PDF ，它们分别为Isabelle / HOL中的 “ 提升和传递：商数的模块化设计”。
碰巧，提升类型和商类型是紧密相关的，并且不容易理解，这就是为什么我像现在这样尝试在这里和那里进行一些研究以获得更好的理解。
您可以先查看Int.thy。
对于商类型，您需要一个等价关系，该关系定义一个集合，并且intrel用于定义type的集合int。
definition intrel :: "(nat * nat) => (nat * nat) => bool" where
"intrel = (%(x, y) (u, v). x + v = u + y)"
这是基于自然数的整数的经典定义。整数是自然数的有序对（以及如下所述的集合），按该定义它们是相等的。
例如，非正式地，(2,3) = (4,5)因为2 + 5 = 4 + 3。
我很无聊，您在等好东西。这是其中一部分的使用quotient_type：
quotient_type int = "nat * nat" / "intrel"
morphisms Rep_Integ Abs_Integ
如果您想动脑筋，并且真正了解正在发生的事情，那这两种态射就可以发挥作用。quotient_type生成了许多函数和简化规则，您必须做很多工作才能找到全部内容，例如使用find_theorems命令。
的Abs功能抽象的有序对到int。检查这些：
lemma "Abs_Integ(1,0) = (1::int)"
by(metis one_int_def)
lemma "Abs_Integ(x,0) + Abs_Integ(y,0) ? (0::int)"
by(smt int_def)
他们表明int，在引擎盖下，确实是有序的一对。
现在，我展示这些态射的显式类型，以及Abs_int和Rep_int，它们int不仅显示为有序对，而且显示为一组有序对。
term "Abs_int :: (nat * nat) set => int"
term "Abs_Integ :: (nat * nat) => int"
term "Rep_int :: int => (nat * nat) set"
term "Rep_Integ :: int => (nat * nat)"
我再无聊，但我有情感上的需要显示更多示例。如果有序对的组成部分相差一个，则两个正整数相等，例如：
lemma "Abs_Integ(1,0) = Abs_Integ(3,2)"
by(smt nat.abs_eq split_conv)
lemma "Abs_Integ(4,3) = Abs_Integ(3,2)"
by(smt nat.abs_eq split_conv)
如果添加Abs_Integ(4,3)和，您会期望什么Abs_Integ(3,2)？这个：
lemma "Abs_Integ(2,3) + Abs_Integ(3,4) = Abs_Integ(2 + 3, 3 + 4)"
by(metis plus_int.abs_eq plus_int_def split_conv)
即plus_int在证明在Int.thy定义，上线44。
lift_definition plus_int :: "int => int => int"
is "%(x, y) (u, v). (x + u, y + v)"
这解除了什么？这会让我“花几天时间”进行这种解释，而我才刚刚开始了解一点。
该find_theorems节目有很多东西隐藏起来，我说：
thm "plus_int.abs_eq"
find_theorems name: "Int.plus_int*"
还有更多示例，但这些示例要强调的是，在引擎的引擎盖下，一个int关系作为集合返回到一个等效类中，在intrel上面，我在上面使用它来定义集合：
term "Abs_int::(nat * nat) set => int"
term "Abs_int {(x,y). x + 3 = 2 + y}" (*(2,3)*)
term "Abs_int {(x,y). x + 4 = 3 + y}" (*(3,4)*)
lemma "Abs_int {(x,y). x + 3 = 2 + y} = Abs_int {(x,y). x + 100 = 99 + y}"
by(auto)
这auto证明很容易，但有没有神奇的未来通过我对这个下一个，尽管它的简单。
lemma "Abs_int {(x,y). x + 3 = 2 + y} + Abs_int {(x,y). x + 4 = 3 + y}
= Abs_int {(x,y). x + 7 = 5 + y}"
apply(auto simp add: plus_int.abs_eq plus_int_def intrel_def)
oops
我可能要做的只是默认情况下使用不是简化规则的东西。
如果quotient_type不是您要谈论的“商户类型模式”，那么至少通过查看上面所有find_theorems返回的内容Int.plus_int*，我可以从中得到一些启示。