To apply a method (i.e. do a proof step):
apply method
Consider the following rule R, which in Isabelle looks like [| P1; ...; Pn |] ==> Q
P1 ... Pn
---------
Q
Method rule R unifies Q with the current subgoal, replacing it by n new subgoals: instances of P1, ..., Pn.
This is backward reasoning and is appropriate for introduction rules.
Method erule R unifies Q with the current subgoal and simultaneously unifies P1 with some assumption.
The subgoal is replaced by the n - 1 new subgoals of proving instances of P2, ..., Pn , with the matching assumption deleted.
It is appropriate for elimination rules.
The method (rule R, assumption) is similar, but it does not delete an assumption.
Method drule R unifies P1 with some assumption, which it then deletes.
The subgoal is replaced by the n - 1 new subgoals of proving P2, ..., Pn.
An nth subgoal is like the original one but has an additional assumption: an instance of Q.
It is appropriate for destruction rules.
Method frule R is like (drule R) except that the matching assumption is not deleted.
Method insert R adds R to the assumptions.
Method thin_tac "term" removes term from the assumptions (for stuff that you don't need and is getting in the way).
Method subgoal_tac "..." adds the expression to the assumptions, and as a new subgoal (allows you to work from the middle of a proof).
Method intro allI impI repeatedly applies the given introduction rules.
To iterate over possible instantiations when applying a method, use:
back
To specify an instantiation, use the method (we similarly have erule_tac, drule_tac and frule_tac):
rule_tac ?x="foo" and ?y="bar" and ?z="fish" in R
To direct one of these methods to subgoal number i:
rule_tac [i] R
To limit the number of displayed subgoals, use pr n. Use prefer or defer to change ordering of subgoals.
Use + and ? and | to compose methods. Use by to apply the given method, then apply assumption then end the proof:
by (drule mp, (assumption|arith))+?
Variables are either bound or free ('?' qualifiers are
omitted). If you can see question marks or boxes then probably your font does
not support the required mathematical symbols (try this one instead).
| For all | |
| allI: | (⋀x. |
| allE: | ⟦∀x. |
| spec: | ∀x. |
| Exists | |
| exI: | |
| exE: | ⟦∃x. |
| If | |
| impI: | ( |
| impE: | ⟦ |
| mp: | ⟦ |
| And | |
| conjI: | ⟦ |
| conjE: | ⟦ |
| Or | |
| disjI1: | |
| disjI2: | |
| disjE: | ⟦ |
| Sets | |
| Int_lower1: | |
| Int_lower2: | |
| Un_upper1: | |
| Un_upper2: | |
| subset_trans: | ⟦ |
| CollectD: | |
| Misc | |
| ssubst: | ⟦ |
| notnotD: | ¬¬ |
Some of this text is stolen from the Isabelle tutorial.