如何隐藏定义的常量

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。另见the Isabelle/Isar Reference Manual，第105页。