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

Simplifier

• simp rewrites the goal using the simplifier (for more information, refer to the cookbook section on the simplifier). This method never fails except when it cannot perform any simplification at all.
• simp_all is like simp, but acts on all goals

You can find a list of useful simpsets here.

Classical Automation

• blast is a Tableaux prover that is good at predicate logic and set theory. It can take claset modifiers like intro, dest, elim. It can occasionally solve goals involving equality, but generally handles equality rather poorly compared to methods that use the simplifier. However, for purely ‘logical’ goals that do not require rewriting, it can often be superior.
• fastforce and force perform both classical proof search using the claset and rewriting using the simplifier. They differ in which heuristic the classical search uses.
• auto is similar to fastforce/force, but does not try quite as hard. It also acts on all goals and never fails (unless it cannot do anything). It uses a variant of blast internally to close prove goals. Two numeric parameters can be used to steer auto's proof search: in auto b d, b specifies the search depth of blast and d specifies the number of classical proof steps to be taken. The defaults are b = 4 and d = 2, and typically it is more helpful to modify d—if one wants to use these modifiers at all.
• auto2 TODO

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

• metis and meson are automated theorem provers for first-order logic. They are sometimes suggested by sledgehammer or try0. Unlike most other Isabelle automation, they do not use any fact database (like the claset), so they will usually require the user to pass many low-level facts explicitly to them, which makes them impractical to use manually (as opposed to generated by sledgehammer). However, there are occasional cases where fairly big (but logically simple) goals can easily be solved by metis and meson but not by any of Isabelle's other methods.
• smt (an Isabelle wrapper around the Z3 SMT solver) also needs to be given relevant facts manually and is sometimes suggested by sledgehammer. Unlike the previous two, however, it also knows some things about linear arithmetic and a few other things.
• satx uses an external proof-producing SAT solver, replaying its proof in Isabelle
• argo is a prover for propositional logic with equality and linear arithmetic

Less Relevant Methods

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

• fast, slow, and best are classical provers with different heuristics and roughly the same field of applications as blast.
• slowsimp and bestsimp are variants of fastforce with different heuristics.

Summary

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

• assumption solves the goal with one of the premises
• subst performs single-step rewriting of the goal with a given equation. Optional arguments can be used to rewrite the premises instead, or to specify the position to rewrite.
• rewrite is essentially a more powerful version of subst. It allows one to use term patterns to specify the position where the rewriting should be applied. It needs to be imported from HOL-Library.Rewrite. Some instructive examples can be found in HOL-ex.Rewrite_Examples.
• rule performs a single resolution step (it ‘applies’ a rule to the current goal, reasoning backwards)
• drule and frule peform a single step of foward reasoning (they ‘apply’ a rule to one of the premises, yielding a new premise). The difference is that drule deletes the premise that is being transformed, whereas frule does not.
• erule applies resolution of a rule with the goal and with one of the premises being consumed by the first assumption of the rule. An optional numeric argument can be used to consume more than one premise. It is more or less equivalent to rule, assumption. This is often useful for elimination rules (e.g. case analyses or rules written in the fixes ... assume ... obtains ... format).
• intro applies resolution with the given rules repeatedly.
• elim applies elimination with the given rules repeatedly.
• safe applies safe rules from the claset only. This is typically used to split conjunctions in goals with several subgoals, or to split conjunctions in the assumptions by several assumptions, or to prove set equivalence by proving membership in both directions. However, sometimes it can do a bit too much (e.g. x ∈ {a} becomes x ∉ {} ⟹ x = a). In those cases, using the intro/elim methods by hand is preferable.
• clarsimp is similar to safe but also invokes the simplifier. You can think of it as a less aggressive version of auto.
• clarify TODO: What does clarify do precisely

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.

Transfer

TODO

Special-Purpose Automation

Termination

• relation can be used in manual termination proofs by giving a suitable well-founded relation by hand (often used in combination with measure or <*lex*>/<*mlex*>).
• lexicographic_order attempts to prove termination of a multivariate function automatically by finding a lexicographic combination of termination measures.
• size_change is a more sophisticated termination method TODO what does it do

Arithmetic

• linarith solves linear arithmetic goals on natural numbers, integers, and reals. It deals with disjunctions by performing a case distinction, so if the goal contains many disjunctions, this becomes prohibitively slow.
• smt also supports linear arithmetic and often deals with disjunctions much better than linarith.
• presburger solves Presburger arithmetic goals. It can be very useful to prove goals involving divisibility and mod on naturals and integers, but in practice it is often prohibitively slow on all but very small goals. TODO link
• arith was created to become a wrapper tactic for all kinds of arithmetic decision procedures, but in practice, it only calls linarith and presburger at the moment.

Polynomials

• sos can prove polynomial inequalities using sum-of-squares witnesses. It is complete for univariate polynomials, but the witness search can often take quite long for larger ones.
• sturm can prove various things about univariate real polynomials, such as non-negativity, number of roots, etc.

Other

• measurable proves measurability of functions and sets
• pratt can prove that a number is prime using prime certificates. This works even for fairly large primes. TODO link AFP
• master_theorem can prove asymptotic relations for divide-and-conquer recurrences corresponding to a generalised version of the Master Theorem. TODO link AFP
• approximation proves inequalities on various real-valued functions using interval arithmetic. TODO link
• real_asymp proves various asymptotic properties of concrete real-valued functions, such limits, ‘Big-O’, and asymptotic equivalence
• eval_winding provides support for evaluating winding numbers of paths in the complex plane in many practically relevant cases TODO link AFP