What rule does 'apply (rule)' or 'proof' use?

isabelle

Solution

You can try using `rule_trace` as follows:

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

which will display in the output:

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

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

If the names of the rules are needed, you can then try using `find_theorems`; I'm not sure if they can be directly determined.

Problem

When I use `apply (rule)` in an apply-script, typically an appropriate rule is selected. The same holds for `proof` in structured proofs. Where can I learn/lookup the name of the rule that was used?

Original source