augment : prover -> thm list -> prover

Augments a prover's context with new theorems.

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 augment p thl maps a prover p to a new prover with theorems thl added to the initial state.

Never fails unless the prover is 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, mk_prover, SIMP_CONV, SIMP_RULE, SIMP_TAC.