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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
\DOC record_proof
\TYPE {record_proof : bool -> void}
\KEYWORDS
proof recording.
\SYNOPSIS
Enable/disable proof recording.
\DESCRIBE
A proof is a list of inference steps. After the proof recorder is
enabled, every inference performed by the system is recorded and
cumulated in an internal buffer. When a proof is completed, the raw
records can then be processed and output to a disk file.
{record_proof} is a low level user function for managing the proof
recorder. It takes a single boolean as its argument. If
this is {true}, it initialises and enables the proof recorder. If it
is {false}, it disables the proof recorder without clearing the proof
recorded since the last time this function is called with the value
{true}.
The current state of the proof recorder can interrogated using the
function {is_recording_proof}. The recorder can be temporarily
disabled and later re-enabled without clearing the internal buffer.
\FAILURE
Never fail.
\EXAMPLE
Below is an example showing how to record an extremely simple proof:
{
#let th = SPEC_ALL ADD_SYM;;
Theorem ADD_SYM autoloading from theory `arithmetic` ...
ADD_SYM = |- !m n. m + n = n + m
th = |- m + n = n + m
#let v = genvar ":num";;
"GEN%VAR%536" : term
#record_proof true;;
() : void
#let th1 = (REFL "SUC(m + n)");;
th1 = |- SUC(m + n) = SUC(m + n)
#let th2 = SUBST [th,v] "SUC(m + n) = SUC ^v" th1;;
th2 = |- SUC(m + n) = SUC(n + m)
#record_proof false;;
() : void
#write_proof_to `ap_term.prf` `ap_term` [] (get_steps());;
() : void
}
The proof consists of two inference steps: the application of the two
primitive inference rules {REFL} and {SUBST}. The function
{write_proof_to} outputs the proof into a file names {ap_term.prf}.
\COMMENTS
This function is used to implement higher level user functions for
recording proof in the library {record_proof}. It is much more
convenient to use those functions than the low level functions
such as {record_proof} directly.
\SEEALSO
is_recording_proof, RecordStep, get_steps,
suspend_recording, resume_recording,
current_proof, current_proof_file,
new_proof_file, close_proof_file, begin_proof, end_proof,
TAC_PROOF, PROVE, prove, prove_thm.
\ENDDOC
|
