Lemma Collections

From Isabelle Community Wiki
Jump to: navigation, search

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, which are useful to prove specific kinds of goals.

Collection Usage
eval_nat_numeral simp rules to convert numerals to Suc/Zero notation
algebra_simps The rules deal with the classical algebraic structures of groups, rings and family. 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.

field_simps These rules 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.
ac_simps associativity and commutativity simplification rules