Menu
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?
876
Every statement must be justified. A justification can refer to prior lines of the proof, the hypothesis and/or previously proven statements from the book. Cases are often required to complete a proof which has statements with an "or" in them.
The rules of inference (also known as inference rules) are a logical form or guide consisting of premises (or hypotheses) and draws a conclusion. A valid argument is when the conclusion is true whenever all the beliefs are true, and an invalid argument is called a fallacy as noted by Monroe Community College.
A valid argument is one where the conclusion follows from the truth values of the premises. Rules of Inference provide the templates or guidelines for constructing valid arguments from the statements that we already have.
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.
131
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
