isabelle - 如何使 find_theorems 更具体

Question

我试图在 Isabelle (2021) 中找到一个定理，效果如下：

lemma "A ⟹ B ⟹ A ∧ B"

到目前为止，我已经尝试使用以下模式：

find_theorems "_ ⟹ _ ⟹ _ ∧ _"

但它显然会返回很多结果，因为模式太抽象了。各种占位符_可以表示彼此非常不同的事物。

我想知道是否有任何方法可以在搜索中更具体，以表示某些占位符是相同的。例如，下面的假设示例能否在 Isabelle 的搜索工具中实现？

find_theorems "_1 ⟹ _2 ⟹ _1 ∧ _2"

（表示所有_1s 都是同一个变量，所有_2s 都是相同的，等等）

标签： isabelle

Answer 1

正如我在评论中提到的，find_theorems也将模式作为类似于is. 所以任何形式的'？可以使用后跟字符串（以及可选的数字 [1]）。

find_theorems "?A \<Longrightarrow> ?B \<Longrightarrow> ?A \<and> ?B"
(*
  "?A ⟹ ?B ⟹ ?A ∧ ?B"

found 1 theorem(s):
•  HOL.conjI: ?P ⟹ ?Q ⟹ ?P ∧ ?Q
*)

[1] 通常需要注意的是，“?A0”和“?A”指的是相同的模式。