isabelle - 'apply (rule)'或 'proof'使用什么规则？

Question

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

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；我不确定是否可以直接确定它们。