1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\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
|
