从Isabelle/HOL到HOL的自动转换

Question

我在Isabelle/HOL中有一些定义和定理，并且需要在HOL中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有程序可以(半自动)执行这样的翻译？

如果由于某些原因不能做到这一点，请解释原因，因为这对我来说是一项重要的学习。

Answer 1

从理论上讲，您应该能够轻松地在HOL实现之间移动定理和定义，这一想法是OpenTheory项目的动机。不幸的是，在实践中，Isabelle的HOL实现与其他实现完全不同，并且在每个OpenTheory页面上，Isabelle目前只能使用OpenTheory导入定理，并且不能导出它们。