isabelle - 伊莎贝尔的糟糕理论导入

Question

以下给出 bad theory import "Multivariate_Analysis"

imports Multivariate_Analysis

进口 Main工作正常，如何导入模块？

Answer 1

对于理论导入，您通常必须指定理论文件的完整或相对路径。所以对于 Multivariate_Analysis ，这是 <path to isabelle distrib>/src/HOL/Multivariate_Analysis/Multivariate_Analysis .只有当理论已经是 session 图像的一部分时，才能省略路径。如Main是默认图像的一部分 HOL ，您可以在没有路径的情况下导入它。从带有或不带有路径的 session 图像中导入理论是否更好，意见分歧。

该路径还可能包含环境变量，如 $ISABELLE_HOME或 $AFP ，用户可以在他们的本地设置文件中进行设置，以便理论适用于不同的安装。对于 Isabelle 发行版中的所有内容，习惯使用 ~~ Isabelle 分发文件夹的路径。

总之，您的导入应如下所示:

theory My_Theory
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin

如 Multivariate_Analysis是一个相当大的模块，但更改默认 session 图像可能是明智的，这样所有这些理论都不会在 Isabelle/jEdit 的每次启动时重新加载。您可以通过指定 -l HOL-Multivariate_Analysis 来做到这一点。在调用时的命令行或通过在理论面板中选择此 session 并重新启动 Isabelle/jEdit。

更新:自 Isabelle2017 以来，最好通过 session 名称而不是相对路径名称从其他 session 导入理论。那就是
理论 Multivariate_Analysis将被导入为

theory My_Theory
imports "HOL-Multivariate_Analysis.Multivariate_Analysis"
begin