Proof Methods

To get started, have a look at Chained facts and proof methods. It introduces the concept of chained facts as well as simple and proper methods. Moreover, it talks about the behaviour of the methods intro/elim, rule/erule, - and insert.

Below, you can find a list of methods and their description. In the following, all methods only act on the first subgoal unless otherwise stated and fail if they cannot solve the goal, unless stated otherwise.

General-Purpose Automation


You can find a list of useful simpsets here.

Classical Automation

The following methods are a bit more specialised, but still useful in some cases:

Less Relevant Methods

The following methods are not used much these days and you can probably safely ignore them:


The most widely used and useful methods are simp/simp_all and auto. Since they never fail, they are also very useful for exploration: a usual pattern in writing Isabelle proofs is to do apply auto and inspect the proof state to see which goals are ‘left over’. One can then give additional facts to the methods or prove remaining goals separately until nothing remains.

If there is a goal that auto should be able to solve but somehow cannot, force often works because it tries a bit harder. Despite its name, fastforce is usually not really faster than force. Which of them is better in any given case seems to be quite random, and it usually does not matter.

One-Step Methods

All of these except drule, frule, erule are often useful even in high-level proofs, especially when used as the first step of a proof. They are often used as the initial proof method, and the goals they produce are then ‘finished off’ using e.g. auto.



Special-Purpose Automation