1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
\DOC basic_prover
\TYPE {basic_prover : (simpset -> 'a -> term -> thm) -> simpset -> 'a -> term -> thm}
\SYNOPSIS
The basic prover use function used in the simplifier.
\DESCRIBE
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
Never fails, though the later application to a term may fail to prove it.
\SEEALSO
mk_prover, SIMP_CONV, SIMP_RULE, SIMP_TAC.
\ENDDOC
|
