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会使用您的新名称，而是会使用它们自己的启发式方法来确定哪个是“最佳”名称以输出给用户。

lemmasis的另一个同义词theorems，尽管前者被认为是更标准的方法。