CODEWITHSUNDEEP
isabelle
corny
corny

Reputation: 7852

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

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?

Upvotes: 7

Views: 500

Answers (3)

Lars Noschinski
Lars Noschinski

Reputation: 3667

The other answers already tell you how to determine which lemmas are applied by rule. Note that proof does not call the rule, but the method default. Most of the time, default does the same as rule, but e.g. to prove a locale predicate it calls unfold_locales.

I don't know of any method to see what actually happens there.

Upvotes: 3

davidg
davidg

Reputation: 6027

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.

Upvotes: 5

chris
chris

Reputation: 5038

Everything that is declared as Pure.intro/intro/iff (or one of its ? or ! variants) is considered as default introduction rule (i.e., if no current facts are chained in). Similarly, everything that is declared as Pure.elim/elim/iff is considered as default elimination rule (i.e., if current facts are chained in). Usually later declarations take precedence over earlier ones (at least if the same kind of declaration is used... mixing, e.g., Pure.intro? with intro, etc., might turn out differently).

However, this just answers what kind of rules are considered in principle. I don't know a way to directly find out which rule was applied. But it is relatively straight-forward to find the correct rule by find_theorems intro directly above the line you were wondering about. E.g.,

lemma "A & B"
find_theorems intro
proof

will show you all rules that could be applied as introduction rule to the goal A & B. One of them is the default rule applied by proof (you will recognize it by the subgoals you obtained).

For elimination rules you can use, e.g.,

lemma assumes "A | B" shows "P"
using assms
find_theorems elim
proof

Upvotes: 3

Related Questions