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

Question

假设我有一个定理:

theorem non_ASCII_thm_name:
  "True"
  by simp

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

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，尽管前者被认为是更标准的方法。