isabelle - 如何隐藏定义的常量

Question

当我导入带有定义常量（用于递归函数或定义）f的理论文件时，如何在当前理论文件中隐藏这样的常量？换句话说，我想确保这f是一个自由变量。我不想更改导入的文件。

Answer 1

这正是该hide_const命令的目的。例如，

hide_const f

将从当前上下文中完全删除定义的常量f（从而使其不可访问）。如果你使用

hide_const (open) f

相反，只有基本名称被隐藏（即，f），但限定名称（例如，A.f如果f在理论上定义A）仍然有效。

类、类型和事实有类似的命令：hide_class、hide_type和hide_fact. 另见Isabelle/Isar 参考手册，第 105 页。