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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
\DOC MakeProof
\TYPE {MakeProof : step list -> line list}
\KEYWORDS
proof recording.
\LIBRARY
record_proof
\SYNOPSIS
Convert a inference step list to a proof line list.
\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 are converted into a list of proof lines as in Hilbert's style
proofs. These lines are then output to a disk file.
{MakeProof} is the conversion function for transforming the step list
into proof line list. The ML type {step} represents the inference
steps. There are 52 constructors for the type {step}. Each
constructor associates with a different kind of inferences. Each step
contains the actual arguments of the call of the inference rule. As
shown in the example below, the first step in the step list returned
by {get_steps} is a substitution, i.e. the rule {SUBST}. This
particular rule takes a list of theorem-term pairs, a term and a
theorem as its argument.
The ML type {line} represents a proof line as in Hilbert's style
proofs. Each line has a line number, a theorem which is the result of
applying the inference rule, and a justification which indicates the
inference rule to be applied together with its arguments. If an
argument is a theorem, it is represented by a number. This number
refers to the theorem in the line having the given line number.
\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%385" : 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)
#get_steps();;
[SubstStep([(|- m + n = n + m, "GEN%VAR%385")],
"SUC(m + n) = SUC GEN%VAR%385",
|- SUC(m + n) = SUC(m + n));
ReflStep"SUC(m + n)"]
: step list
#MakeProof it;;
[Line(-1, |- m + n = n + m, Hypothesis);
Line(1, |- SUC(m + n) = SUC(m + n), Refl"SUC(m + n)");
Line(2,
|- SUC(m + n) = SUC(n + m),
Subst([(-1, "GEN%VAR%385")], "SUC(m + n) = SUC GEN%VAR%385", 1))]
: line list
}
The proof consists of two inference steps: the application of the two
primitive inference rules {REFL} and {SUBST}. The step list is in the
reverse order of the inferences, i.e. the first element is the last
inference. All arguments to the inference rule are presented in the
steps explicitly. The line list generated by the function {MakeProof}
is in the order of the proof. The last line, Line 2, corresponds to
the substitution step. The theorems are replaced by line numbers. They
indicate the line where the theorems are found.
\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 this low level function directly.
\SEEALSO
get_steps, write_line, write_thm_list, write_env,
write_proof_add_to, write_proof_to, write_last_proof,
current_proof, current_proof_file,
new_proof_file, close_proof_file, begin_proof, end_proof,
TAC_PROOF, PROVE, prove, prove_thm
\ENDDOC
|
