什么是Isabelle/HOL亚型？Isar命令产生什么子类型？

Question

我想知道Isabelle/HOL亚型.我解释一下为什么在我对上一个SO问题的部分回答中对我来说很重要:

基本上,我只有一种类型,所以如果我可以通过子类型利用HOL类型的力量,它可能对我有用.

我已经在Isabelle文档,Web和Isabelle邮件列表中进行了搜索.使用"子类型"这个词虽然不多,但它似乎并不是伊莎贝尔词汇中非常重要的一部分.

部分地,我只想知道如何正确使用"子类型"这个词.我不想在Isabelle中调用一个不属于子类型的子类型.

根据Wiki,子类型是特定于语言的:

重要的最后部分; 命令请

有人能给我一个创建Isar子类型的Isar命令列表吗？我正在调查typedef,正如上面提到的问题所解释的那样.我倾向于称之为子类型,但isar-ref.pdf在解释命令时不使用"子类型".

如果有其他方法可以创建Isabelle/HOL亚型,我想知道.

Answer 1

Isabelle/HOL在可替代性方面没有亚型.这意味着如果你需要一个类型的值a,那么你必须提供一个类型的值a- 你不能与另一种类型相处b.特别是,Isabelle没有子类型的概念,其中子类型的值满足一些额外的属性.

有一些方法可以模拟子类型的某些方面,这就是使用概念子类型的地方:

类型参数的替换允许您有时创建子类型的错觉.该record包使用这个扩展记录,例如,人们可以使用扩展记录q代替非扩展记录的r.在内部,其他字段q被填充到r记录类型的泛化的附加类型参数中.从技术上讲,没有子类型多态性发生; 因此,延长记录的顺序很重要.
typedef引入了一种新类型,t其类型Universe是某些现有HOL类型值的非空子集a.有时,这被称为t子类型a,但您没有可替代性.你总是要明确提及嵌入射Rep_t时要使用的值t作为一个a.无论您是使用typedef其他方式还是通过其他方式定义您的类型,任何内射函数都可以作为这样的强制.
Isabelle参考手册(第12.4节)中描述的强制性子类型使Isabelle推断并自动插入此类强制.这只适用于类型和子类型都是没有参数的类型构造函数.使用declare [[coercion_enabled]]启用强制分型,并与注册您的强制功能declare [[coercion Rep_t]].因此,您不必自己插入嵌入函数.

Andreas，这是另一个我对需要和想要的东西有模糊的想法的例子，开发人员很久以前就以成熟的形式考虑并实现了这个想法。第12.4节使用短语“强制性子类型化”。可以根据Isabelle / HOL中的使用方式专门定义“子类型” ...当在文档中使用一个单词但从未定义过一个单词，并且具有非标准含义时，我可以转动轮子...但是击中这2个最后一句话。现在，我看到“强制输入”已全部说明，甚至可以在Wiki中解决。我的意识提高了。@Lars，感谢您将“写入”澄清为“插入”。 (2认同)