如何隐藏已定义的常量

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页.