basic_prover : (simpset -> 'a -> term -> thm) -> simpset -> 'a -> term -> thm
The basic prover use function used in the simplifier.
The HOL Light simplifier (e.g. as invoked by SIMP_TAC) allows provers of type
prover to be installed into simpsets, to automatically dispose of
side-conditions. There is another component of the simpset that controls how
these are applied to unproven subgoals arising in simplification. The
basic_prover function, which is used in all the standard simpsets, simply
tries to simplify the goals with the rewrites as far as possible, then tries
the provers one at a time on the resulting subgoals till one succeeds.
- FAILURE CONDITIONS
Never fails, though the later application to a term may fail to prove it.
- SEE ALSO
mk_prover, SIMP_CONV, SIMP_RULE, SIMP_TAC.