我想在 Isabelle 中构建一种类型层次结构：
B is of type A ( B::A )
C and D are of type of B (C,D ::B)
E and F are of type of C (E,F ::C)
在 Isabelle 中进行编码的最佳方式是什么？有没有直接的方法来定义这个层次结构，或者我需要一个解决方法。我应该去哪里看？
PS：假设 A..F 都是抽象的，并且在每种类型上都定义了一些函数）
谢谢
【问题讨论】：
标签： isabelle
（第一个注意：在我看来，正如您一直在使用的那样，“抽象”一词没有明确的含义。用于定义类型的 Isabelle 关键字可用于定义，如我所见，要么抽象或具体类型，或可以同时考虑的类型，例如'a list。）
（第二个注意：这里，我考虑了你在其他问题中与面向对象编程的比较。至于编程语言和逻辑语言，应该注意，我只是一个观察者。）
对我自己来说，这一切都变得模糊不清，在我看来，我不再清楚区分术语和类型，因此 Rene Thiemann 等答案有助于让我想起这一点。
不过，我知道的不多，我可以简单地认为您的短语“类型层次结构”与“类型类层次结构”同义，并且进一步与“排序层次结构”同义。这让我可以很高兴地为您的问题提供答案，尽管其他人的接受可能是不稳定的。
当然，在 Isabelle 词汇表中，类型和排序不是同义词，但在 Isabelle/HOL 中，它们是密不可分的，因为每个 HOL 术语都有一个排序。 （一个危险的说法，因为在HOL中使用了prop类型，也许我仍然不明白空排序是什么。）：
'a::type的区别
Isabelle 通过语言环境提供继承（以及其他方式？），其中类型类是（或包含）语言环境：
我创建了 5 个类型类来满足您的要求，至少简单地说。每个人都有自己的身份功能。 + 符号是神奇的继承符号。
declare [[show_sorts, show_consts]]
(*The 5 type classes.*)
class cA =
fixes idA :: "'a => 'a"
assumes idA_is_id: "idA x = x"
class cB = cA +
fixes idB :: "'a => 'a"
assumes idB_is_id: "idB x = x"
class cC = cB +
fixes idC :: "'a => 'a"
assumes idC_is_id: "idC x = x"
class cD = cB +
fixes idD :: "'a => 'a"
assumes idD_is_id: "idD x = x"
class cE = cC +
fixes idE :: "'a => 'a"
assumes idE_is_id: "idE x = x"
class cF = cC +
fixes idF :: "'a => 'a"
assumes idF_is_id: "idF x = x"
有效：
(*Any of type class cB, cC, cD, and cF can be used where cA can be used.*)
term "idA (x::'a::cA)"
term "idA (x::'a::cB)"
term "idA (x::'a::cC)"
term "idA (x::'a::cD)"
term "idA (x::'a::cE)"
term "idA (x::'a::cF)"
更多继承示例：
(*Use of idC shows that cE inherited all of what's in cC.*)
term "idC :: ('a::cC => 'a::cC)"
term "idC :: ('a::cE => 'a::cE)"
term "idC (x::'a::cE)"
(*But here, there's a type sort clash, because cC didn't inherit from cE. *)
term "idE :: ('a::cC) => ('a::cC)"
现在，通过将 nat 实例化为类型类 cF 添加一些具体性：
(*It took me over an hour to see I was using 'idA_cA' instead of 'idA_nat'.
99% of the battle can be learning the syntax.*)
instantiation nat :: "{cF}"
begin
definition idA_nat :: "nat => nat" where "idA_nat == id"
definition idB_nat :: "nat => nat" where "idB_nat == id"
definition idC_nat :: "nat => nat" where "idC_nat == id"
definition idF_nat :: "nat => nat" where "idF_nat == id"
instance (*proof. Use 'proof' and see 4 subgoals: the need for 4 id functions.*)
by(default, auto simp add: idA_nat_def idB_nat_def idC_nat_def idF_nat_def)
end
(*When I instantiated nat as cF, I had to instantiate nat as cA, cB, and cC,
because I had not previously done so. Normally, you would be adding useful
'fixes' and 'assumes' with each type class, and proving useful theorems about
them.*)
value "idA (0::nat)"
value "idB (0::nat)"
value "idC (0::nat)"
value "idF (0::nat)"
(*You have to show that a type satisfies all of the 'fixes' and 'assumes'
of a type class. But additional proved theorems, you get those for free.
That's the great benefit of type classes. You may have 20 types that
you instantiate as a type class, but you only have to prove 'extraneous'
theorems once, that being for the type class, based on the 'fixes' and
'assumes' (and other things defined with other keywords).*)
我仍然会定期尝试学习如何正确使用 Isabelle 词汇。所以，我在看关键字subclass：
subclass，第 97 页 isar-ref.pdf
我不妨证明cF 是cA 的子类，以说明一点：
context cF
begin
subclass cA ..
end
cA 是 cF 的子类，反之亦然？好吧，如果我没有在 isar-ref.pdf 中的子类定义中替换 c 和 d，我就不会已经承诺了。
接触语言的本质，无论是逻辑还是编程，你都会发现它们都没有给你一切，所以你最终想要它们分别给你的一切。
您可以轻松地在 C++ 中定义对象，但尝试在 C++ 中定义代数数据类型。
你可以：
但这并不像 Isabelle/HOL 那样简单，它类似于 Haskell，而且我尝试过的变通方法的模式匹配能力甚至不接近。
但是，嘿，我完全支持我们想要的所有这些东西的最终融合。
【讨论】：
至少在 Isabelle/HOL 中，这直接是不可能的，因为术语和类型之间存在严格的分离，:: 在左侧使用术语，在左侧使用 typ右侧。
所以，当写B :: A 时，B 是一个术语，A 是一个类型。那么，就不可能写C :: B了。
我不确定，但也许您的设置可以直接在 Isabelle/ZF 中建模。
关于变通方法，您可以按集合交换类型并改用成员资格:
的::。然后就可以写了
context
fixes A B C D E F
assumes
"B : A"
"C : B" "D : B"
"E : C" "F : C"
begin
...
end
但是你没有得到类型检查器的支持，A 的类型为 'a set set set。
希望这会有所帮助。
【讨论】：