isabelle - “应用（规则）”或“证明”使用什么规则？

Question

当我apply (rule)在应用脚本中使用时，通常会选择适当的规则。这同样适用proof于结构化证明。我在哪里可以了解/查找使用的规则的名称？

Answer 1

您可以尝试rule_trace如下使用：

lemma "a ∧ b"
  using [[rule_trace]]
  apply rule

这将显示在输出中：

rules:
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
proof (prove): step 2

goal (2 subgoals):
 1. a
 2. b

如果需要规则的名称，您可以尝试使用find_theorems; 我不确定它们是否可以直接确定。

Answer 2

声明为Pure.intro/ intro/ iff（或其变体之一?）的所有!内容都被视为默认引入规则（即，如果没有链接当前事实）。同样，声明为Pure.elim//的所有内容都被视为默认消除规则（即，如果当前事实被链接）elim。iff通常后面的声明优先于前面的声明（至少如果使用相同类型的声明......混合，例如，Pure.intro?withintro等，可能会产生不同的结果）。

然而，这只是回答了原则上考虑什么样的规则。我不知道直接找出应用了哪个规则的方法。但是find_theorems intro在您想知道的直线上方直接找到正确的规则是相对简单的。例如，

lemma "A & B"
find_theorems intro
proof

将向您显示所有可以作为引入规则应用于目标的规则A & B。其中之一是应用的默认规则proof（您将通过获得的子目标识别它）。

对于消除规则，您可以使用，例如，

lemma assumes "A | B" shows "P"
using assms
find_theorems elim
proof

Answer 3

其他答案已经告诉您如何确定应用了哪些引理rule。注意proof不是调用的rule，而是方法default。大多数时候，default与 做相同rule的事情，但例如证明它调用的语言环境谓词unfold_locales。

我不知道有什么方法可以看到那里实际发生了什么。