如何找到"proof"命令选择的证明方法

Question

以语句P ⟹ Q ⟹ P ∧ Q为例。你可以证明它：

lemma dummy: "P ⟹ Q ⟹ P ∧ Q" 
proof
  assume "P" "Q"
  show "P" by fact
  show "Q" by fact
qed

这里proof命令选择了一些证明方法，它生成两个子任务，一个P的证明，然后是Q的证明。

有没有办法让我找出 proof 选择了哪种方法？

注意：我知道这里选择的证明方法是rule conjI，我的问题是针对一般情况。

Answer 1

正如@NieDzejkob 已经提到的，proof 选择的证明方法是 standard。我不是 Isabelle/ML 方面的专家，但以下 ML 片段遍历证明项并打印使用的定理列表，这可能有助于找出 standard 使用的特定定理：

ML_command ‹
  val thm = @{thm dummy};
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
  val all_thms = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] [];
  writeln (commas_quote all_thms);
›

如何找到"proof"命令选择的证明方法

How to find the proof method chosen by the "proof" command

isabelle