basic_prover : (simpset -> 'a -> term -> thm) -> simpset -> 'a -> term -> thm

- SYNOPSIS
- The basic prover use function used in the simplifier.
- DESCRIPTION
- 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.