如何使 find_theorems 更具体
How to make find_theorems more specific
我试图在 Isabelle (2021) 中找到一个具有以下效果的定理：
lemma "A ⟹ B ⟹ A ∧ B"
到目前为止，我尝试使用以下模式：
find_theorems "_ ⟹ _ ⟹ _ ∧ _"
但它显然returns很多结果，因为模式太抽象了。各种占位符 _ 可以代表彼此截然不同的事物。
我想知道有没有办法在搜索中更具体一些，表达一些占位符是相同的。比如下面假设的例子在Isabelle的搜索工具中能否实现？
find_theorems "_1 ⟹ _2 ⟹ _1 ∧ _2"
（表示所有的_1都是同一个变量，所有的_2都是一样的等等）
正如我在评论中提到的，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”指的是相同的模式。
我试图在 Isabelle (2021) 中找到一个具有以下效果的定理：
lemma "A ⟹ B ⟹ A ∧ B"
到目前为止，我尝试使用以下模式：
find_theorems "_ ⟹ _ ⟹ _ ∧ _"
但它显然returns很多结果，因为模式太抽象了。各种占位符 _ 可以代表彼此截然不同的事物。
我想知道有没有办法在搜索中更具体一些，表达一些占位符是相同的。比如下面假设的例子在Isabelle的搜索工具中能否实现？
find_theorems "_1 ⟹ _2 ⟹ _1 ∧ _2"
（表示所有的_1都是同一个变量，所有的_2都是一样的等等）
正如我在评论中提到的，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”指的是相同的模式。