isabelle - 我可以为一个定理定义多个名称吗？

Question

假设我有一个定理:

theorem non_ASCII_thm_name:
  "True"
  by simp

我想为 non_ASCII_thm_name 定义一个 ASCII 名称类似 notation命令。例如，像这样:

notation non_ASCII_thm_name ("ASCII_thm_name")

Isar 命令 notation和 abbreviation只能与常量一起使用。是否有允许我这样做的 Isar 命令？

最好，我希望我的 Isar 命令提供的只是同义词。例如，如果我使用 sledgehammer ，最好只存在一个定理， non_ASCII_thm_name ，所以 sledgehammer没有使用额外的事实 ASCII_thm_name .

Answer 1

部分解决方案是使用以下命令:

lemmas ASCII_thm_name = non_ASCII_thm_name

这将定义一个名为 ASCII_thm_name 的新定理。这将与 non_ASCII_thm_name 相同.

遗憾的是不能保证诸如 find_theorems 之类的工具。将使用您的新名称，但会使用他们自己的启发式方法来确定哪个是输出回用户的“最佳”名称。
lemmas 的另一种同义词是 theorems ，虽然前者被认为是更标准的方法。