伊莎贝尔：如何获得数据类型继承

Question

手册非常友好地回答了我的第一个问题，但现在我不知所措了。我想定义两种类型，就像在命题演算中一样，我想要一种原子类型和一种更复杂的类型。

datatype atomicType = aa | bb | cc
datatype complexType = combine complexType complexType

基本上这加上能够使用 atomicType 个实例作为 complexType。 Oc 我可以为 complexType 定义另一个构造函数 "Up atomicType"，但是我看不出如何在我的公理中区分这两种类型等等。

Answer 1

通常的解决方案就像您建议的那样：

datatype complexType = combine complexType complexType |
                       atomic atomicType

datatype命令会自动为你生成很多常量。其中一组是 complexType => bool 类型的 "discriminators"。它们可以让您区分您的类型。

datatype complexType = is_combined: combine complexType complexType |
                       is_atomic: atomic atomicType

... 或使用默认名称（在 datatype manual 的 §2.1.5 中描述）。

有了它，你可以写下一个属性喜欢

is_atomic x ==> is_combined (some_operation ...)

Isabelle: How to get datatype Inheritance