如何隱藏定義的常量

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頁。