Lemma Collections
The default setup of the simplifier and other automatic proof methods in Isabelle includes lemmas which are considered generally useful and (almost) never make a goal harder to prove (or unprovable). Apart from this default setup, Isabelle offers some collections of lemmas that are useful to prove specific kinds of goals:
| Collection | Usage |
|---|---|
eval_nat_numeral |
simp rules to convert numerals to Suc/Zero notation |
ac_simps |
TODO |
algebra_simps |
simp rules to deal with the classical algebraic structures of groups and rings and fields.
They simplify terms by multiplying everything out (in case of a ring) and bringing sums and products into a canonical form (by ordered rewriting).
As a result, it decides group and ring equalities but also helps with inequalities.
Of course it also works for fields, but it knows nothing about multiplicative inverses or division.
This is catered for by |
field_simps |
simp rules that multiply with denominators in (in)equations if they can be proved to be non-zero (for equations) or positive/negative (for inequations); can be too aggressive and is therefore separate from the more benign algebra_simps. |
sign_simps |
TODO |
DERIV_intros |
TODO |
tendsto_intros |
TODO |