Take the statement P ⟹ Q ⟹ P ∧ Q as an example. You may prove it with:
lemma dummy: "P ⟹ Q ⟹ P ∧ Q"
proof
assume "P" "Q"
show "P" by fact
show "Q" by fact
qed
Here the proof command chooses some proof method, which generates two subtasks, a proof of P, followed by a proof of Q.
Is there a way for me to find out which method was chosen by proof?
Note: I know the proof method chosen here was rule conjI, my question is for the general case.
As @NieDzejkob already mentioned, the proof method chosen by proof is standard. I'm not an expert in Isabelle/ML, but the following ML snippet traverses the proof term and prints the list of used theorems, which may be helpful in trying to find out the specific theorem used by 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);
›