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
|
\DOC backup
\TYPE {backup : (void -> void)}
\SYNOPSIS
Restores the proof state, undoing the effects of a previous expansion.
\DESCRIBE
The function {backup} is part of the subgoal package. It allows backing up
from the last state change (caused by calls to {expand}, {set_goal}, {rotate}
and their abbreviations, or to {set_state}). The package maintains a backup
list of previous proof states. A call to {backup} restores the state to the
previous state (which was on top of the backup list). The current state and the
state on top of the backup list are discarded. The maximum number of proof
states saved on the backup list is one greater than the value of the assignable
variable {backup_limit}. This variable is initially set to 12. Adding new proof
states after the maximum is reached causes the earliest proof state on the list
to be discarded. The user may backup repeatedly until the list is exhausted.
The state restored includes all unproven subgoals or, if a goal had been
proved in the previous state, the corresponding theorem. {backup} is
abbreviated by the function {b}. For a description of the subgoal package, see
{set_goal}.
\FAILURE
The function {backup} will fail if the backup list is empty.
\EXAMPLE
{
#g "(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])";;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
() : void
#e CONJ_TAC;;
OK..
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#backup();;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
() : void
#e (REWRITE_TAC[HD;TL]);;
OK..
goal proved
|- (HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])
Previous subproof:
goal proved
() : void
}
\USES
Back tracking in a goal-directed proof to undo errors or try different tactics.
\SEEALSO
b, backup_limit, e, expand, expandf, g, get_state, p, print_state, r,
rotate, save_top_thm, set_goal, set_state, top_goal, top_thm.
\ENDDOC
|
