'未定义的常量：“eq”simpdata.ML'同时尝试在 Isabelle/HOL 的 scala-isabelle 中加载 Imperative_Quicksort 理论

如何解决'未定义的常量：“eq”simpdata.ML'同时尝试在 Isabelle/HOL 的 scala-isabelle 中加载 Imperative_Quicksort 理论

我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle 来加载和解析 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html - Imperative_Quicksort.thy。我正在使用 IntelliJ 的 scala-isabelle 代码（源路径是 C:\Workspace-IntelliJ\scala-isabelle）：

val isabelleHome = "C:\\Homes\\Isabelle2020\\Isabelle2020"
    // Differs from example in README: we skip building to make tests faster
    val setup = Isabelle.Setup(isabelleHome = Path.of(isabelleHome),logic = "HOL",build=false)
    implicit val isabelle: Isabelle = new Isabelle(setup)

    // Load the Isabelle/HOL theory "Main" and create a context object
    //val ctxt = Context("Main")
    //val ctxt = Context("Imperative_Quicksort")
    //val ctxt = Context("C:\\Homes\\Isabelle2020\\Isabelle2020\\src\\HOL\\Imperative_HOL\\ex\\Imperative_Quicksort")
    val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

这种配置在加载一些必需的理论时会给出奇怪的错误信息，例如

Exception in thread "main" de.unruh.isabelle.control.IsabelleException: No such file: "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/Old_Datatype.thy"
The error(s) above occurred for theory "HOL-Library.Old_Datatype" (line 10 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/Countable.thy")
(required by "HOL.Imperative_HOL.ex.Imperative_Quicksort" via "HOL.Imperative_HOL.ex.Imperative_HOL" via "HOL.Imperative_HOL.ex.Array" via "HOL.Imperative_HOL.ex.Heap_Monad" via "HOL.Imperative_HOL.ex.Heap" via "HOL-Library.Countable")
    at de.unruh.isabelle.control.Isabelle.de$unruh$isabelle$control$Isabelle$$parseIsabelle(Isabelle.scala:268)

我的猜测是 - 使用引号导入的理论会给出此类错误消息，我通过将所需的理论复制到 C:\Workspace-IntelliJ\scala-isabelle 中来逐一解决此类错误消息。不好，但我正在尝试加载这个理论，所以 - 如果它有效，那就没问题。

最后需要 simpldata.ML，但 Isabelle 源 (ZF / sequents / HOL/Tools / FOL / FOLP) 中有 5 个 simpdata.ML。我从 FOL 复制（因为 FOL.thy 需要 simpdata.ML）但现在我有错误消息：

Exception in thread "main" de.unruh.isabelle.control.IsabelleException: Failed to load theory "ZF.Bool" (unresolved "ZF.pair")
...
Undefined constant: "eq" (line 12 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/simpdata.ML")completionline=12offset=313end_offset=315file=/cygdrive/c/Workspace-IntelliJ/scala-isabelle/simpdata.MLid=258:2:::IFOL.eq::constant:IFOL.eq::Pure.eq::constant:Pure.eq
At command "ML_file" (line 11 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/pair.thy")
    at de.unruh.isabelle.control.Isabelle.de$unruh$isabelle$control$Isabelle$$parseIsabelle(Isabelle.scala:268)

我尝试复制其他 simpldata.ML，但它们为不同的未定义常量提供了类似的消息。那么 - eq 有什么问题？我的猜测是这是非常基本的功能。

如何解决此undefined eq？通过其他一些进口？但是 FOL/simpdata.ML 没有任何导入，也没有报告缺少某些源文件。如何从这里开始？

我的意图是将 Imperative_Quicksort 作为 Context scala-isabelle 变量加载，然后我将尝试反映/消化生成的 Context 类树，我将使用图神经网络来编码这个类树（我想这代表了Imperative_Quicksort理论的抽象语法树）。

我知道有 Isabelle 邮件组，但这是一个非常技术性的问题，所以 - 它可以/应该在这里解决。

添加了 1 个事实

simpdata.ML 只是包含在 FOL.thy 中的包含文件

ML_file \<open>simpdata.ML\<close>

因此，simpdata.ML 使用封闭 FOL.thy 文件的导入和定义，并且它确实具有 eq 定义（在 simpdata.ML 中使用之前大约有 100 行）：

ML \<open>
  structure Blast = Blast
  (
    structure Classical = Cla
    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
    val equality_name = \<^const_name>\<open>eq\<close>
    val not_name = \<^const_name>\<open>Not\<close>
    val notE = @{thm notE}
    val ccontr = @{thm ccontr}
    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
  );
  val blast_tac = Blast.blast_tac;
\<close>

所以，也许某些加载顺序有问题...

解决方法

似乎有 2 个理论文件（pair.thy 和 FOL.thy - 我已复制到我的 IntelliJ 工作区）使用了它们各自目录中的 simpdata.ML 包含。所以 - 我已经将 pair.thy 的 simpdata.ML 复制为 simpdata_pair.ML 并将 pair.thy 中的 include 命令修改为：

ML_file \<open>simpdata_pair.ML\<close>

这解决了我的问题，并允许我继续导入理论，这是一种有趣的方式。