apply_prover : prover -> term -> thm

Apply a prover to a term.

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.

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

Mainly intended for users customizing the simplifier.

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.

augment, mk_prover, SIMP_CONV, SIMP_RULE, SIMP_TAC.