什么规则"适用(规则)"或"证明"使用？

Question

当我apply (rule)在apply-script中使用时,通常会选择适当的规则.这同样适用于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; 我不确定他们是否可以直接确定.