mk_prover : ('a -> conv) -> ('a -> thm list -> 'a) -> 'a -> prover

Construct a prover from applicator and state augmentation function.

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 mk_prover app aug where app: 'a -> conv is an application operation to prove a term using the context of type 'a and aug : 'a -> thm list -> 'a is an augmentation operation to add whatever representation of the theorem list in the state of the prover is chosen, gives a canonical prover of this form. The crucial point is that the type 'a is invisible in the resulting prover, so different provers can maintain their state in different ways. (In the trivial case, one might just use thm list for the state, and appending for the augmentation.)

Does not normally fail unless the functions provided are abnormal.

This is mostly for experts wishing to customize 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.

apply_prover, augment, SIMP_CONV, SIMP_RULE, SIMP_TAC.