\DOC apply_prover

\TYPE {apply_prover : prover -> term -> thm}

\SYNOPSIS
Apply a prover to a term.

\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. These may maintain a state dynamically and augment it as more
theorems become available (e.g. a theorem {p |- p} becomes available when
simplifying the consequent of an implication {`p ==> q`}). In order to allow
maximal flexibility in the data structure used to maintain state, provers are
set up in an `object-oriented' style, where the context is part of the prover
function itself. A call {apply_prover p `tm`} applies the prover with its
current context to attempt to prove the term {tm}.

\FAILURE
The call {apply_prover p} never fails, but it may fail to prove the term.

\USES
Mainly intended for users customizing the simplifier.

\COMMENTS
I learned of this ingenious trick for maintaining context from Don Syme, who
discovered it by reading some code written by Richard Boulton. I was told by
Simon Finn that there are similar ideas in the functional language literature
for simulating existential types.

\SEEALSO
augment, mk_prover, SIMP_CONV, SIMP_RULE, SIMP_TAC.

\ENDDOC

{"subset_name": "curated", "file": "formal/hol/Help/apply_prover.doc"}