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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
<html>
<head><title>PROOF-TREE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h1>PROOF-TREE</h1>proof tree displays
<pre>Major Section: <a href="acl2-doc-major-topics.html">ACL2 Documentation</a>
</pre><p>
A view of ACL2 proofs may be obtained by way of ``proof tree
displays.'' The emacs environment is easily customized to provide
window-based proof tree displays that assist in traversing and
making sense of the proof transcript; see <a href="PROOF-TREE-EMACS.html">proof-tree-emacs</a>.
Proof tree displays may be turned on with the command <code>:</code><code><a href="START-PROOF-TREE.html">start-proof-tree</a></code>
and may be turned off with the command <code>:</code><code><a href="STOP-PROOF-TREE.html">stop-proof-tree</a></code>;
see <a href="START-PROOF-TREE.html">start-proof-tree</a> and see <a href="STOP-PROOF-TREE.html">stop-proof-tree</a>.
<p>
<ul>
<li><h3><a href="CHECKPOINT-FORCED-GOALS.html">CHECKPOINT-FORCED-GOALS</a> -- Cause forcing goals to be checkpointed in proof trees
</h3>
</li>
<li><h3><a href="PROOF-TREE-DETAILS.html">PROOF-TREE-DETAILS</a> -- proof tree details not covered elsewhere
</h3>
</li>
<li><h3><a href="PROOF-TREE-EMACS.html">PROOF-TREE-EMACS</a> -- using emacs with proof trees
</h3>
</li>
<li><h3><a href="PROOF-TREE-EXAMPLES.html">PROOF-TREE-EXAMPLES</a> -- proof tree example
</h3>
</li>
<li><h3><a href="START-PROOF-TREE.html">START-PROOF-TREE</a> -- start displaying proof trees during proofs
</h3>
</li>
<li><h3><a href="STOP-PROOF-TREE.html">STOP-PROOF-TREE</a> -- stop displaying proof trees during proofs
</h3>
</li>
</ul>
Here is an example of a proof tree display, with comments. Lines
marked with ``c'' are considered ``checkpoints,'' i.e., goals whose
scrutiny may be of particular value.
<pre>
( DEFTHM PLUS-TREE-DEL ...) ;currently proving PLUS-TREE-DEL
1 Goal preprocess ;"Goal" creates 1 subgoal by preprocessing
2 | Goal' simp ;"Goal'" creates 2 subgoals by simplification
c 0 | | Subgoal 2 PUSH *1 ;"Subgoal 2" pushes "*1" for INDUCT
++++++++++++++++++++++++++++++ ;first pass thru waterfall completed
c 6 *1 INDUCT ;Proof by induction of "*1" has
| <5 more subgoals> ; created 6 top-level subgoals. At
; this point, one of those 6 has been
; proved, and 5 remain to be proved.
; We are currently working on the
; first of those 5 remaining goals.
</pre>
See <a href="PROOF-TREE-EXAMPLES.html">proof-tree-examples</a> for many examples that contain proof
tree displays. But first, we summarize the kinds of lines that may
appear in a proof tree display. The simplest form of a proof tree
display is a header showing the current event, followed by list of
lines, each having one of the following forms.
<pre>
n <goal> <process> ...
</pre>
Says that the indicated goal created <code>n</code> subgoals using the
indicated process. Here ``...'' refers to possible additional
information.
<pre>
c n <goal> <process> ...
</pre>
As above, but calls attention to the fact that this goal is a
``checkpoint'' in the sense that it may be of particular interest.
Some displays may overwrite ``c'' with ``>'' to indicate the current
checkpoint being shown in the proof transcript.
<pre>
| <goal> ...
| | <k subgoals>
</pre>
Indicates that the goal just above this line, which is pointed to
by the rightmost vertical bar (``|''), has <code>k</code> subgoals, none of which
have yet been processed.
<pre>
| <goal> ...
| | <k more subgoals>
</pre>
As above, except that some subgoals have already been processed.
<pre>
++++++++++++++++++++++++++++++
</pre>
Separates successive passes through the ``waterfall''. Thus, this
``fencepost'' mark indicates the start of a new proof by induction
or of a new forcing round.<p>
See <a href="PROOF-TREE-EXAMPLES.html">proof-tree-examples</a> for detailed examples. To learn how to
turn off proof tree displays or to turn them back on again,
see <a href="STOP-PROOF-TREE.html">stop-proof-tree</a> and see <a href="START-PROOF-TREE.html">start-proof-tree</a>,
respectively. See <a href="CHECKPOINT-FORCED-GOALS.html">checkpoint-forced-goals</a> to learn how to mark
goals as checkpoints that <a href="FORCE.html">force</a> the creation of goals in forcing
rounds. Finally, see <a href="PROOF-TREE-DETAILS.html">proof-tree-details</a> for some points not
covered elsewhere.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
