/usr/share/hol88-2.02.19940316/help/ENTRIES/expand.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | \DOC expand
\TYPE {expand : (tactic -> void)}
\SYNOPSIS
Applies a tactic to the current goal, stacking the resulting subgoals.
\DESCRIBE
The function {expand} is part of the subgoal package. It may be abbreviated by
the function {e}. It applies a tactic to the current goal to give a new proof
state. The previous state is stored on the backup list. If the tactic produces
subgoals, the new proof state is formed from the old one by removing the
current goal from the goal stack and adding a new level consisting of its
subgoals. The corresponding justification is placed on the justification stack.
The new subgoals are printed. If more than one subgoal is produced, they are
printed from the bottom of the stack so that the new current goal is printed
last.
If a tactic solves the current goal (returns an empty subgoal list), then its
justification is used to prove a corresponding theorem. This theorem is
incorporated into the justification of the parent goal and printed. If the
subgoal was the last subgoal of the level, the level is removed and the parent
goal is proved using its (new) justification. This process is repeated until a
level with unproven subgoals is reached. The next goal on the goal stack then
becomes the current goal. This goal is printed. If all the subgoals are proved,
the resulting proof state consists of the theorem proved by the justifications.
The tactic applied is a validating version of the tactic given. It ensures that
the justification of the tactic does provide a proof of the goal from the
subgoals generated by the tactic. It will cause failure if this is not so. The
tactical {VALID} performs this validation.
For a description of the subgoal package, see {set_goal}.
\FAILURE
{expand tac} fails if the tactic {tac} fails for the top goal. It will diverge
if the tactic diverges for the goal. It will fail if there are no unproven
goals. This could be because no goal has been set using {set_goal} or because
the last goal set has been completely proved. It will also fail in cases when
the tactic is invalid.
\EXAMPLE
{
#expand CONJ_TAC;;
OK..
evaluation failed no goals to expand
#g "(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])";;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])"
() : void
#expand CONJ_TAC;;
OK..
2 subgoals
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#expand (REWRITE_TAC[HD]);;
OK..
goal proved
|- HD[1;2;3] = 1
Previous subproof:
"TL[1;2;3] = [2;3]"
() : void
#expand (REWRITE_TAC[TL]);;
OK..
goal proved
|- TL[1;2;3] = [2;3]
|- (HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])
Previous subproof:
goal proved
() : void
}
\noindent In the following example an invalid tactic is used. It is invalid
because it assumes something that is not on the assumption list of the goal.
The justification adds this assumption to the assumption list so the
justification would not prove the goal that was set.
{
#set_goal([],"1=2");;
"1 = 2"
() : void
#expand (REWRITE_TAC[ASSUME "1=2"]);;
OK..
evaluation failed Invalid tactic
}
\USES
Doing a step in an interactive goal-directed proof.
\SEEALSO
b, backup, backup_limit, e, expandf, g, get_state, p, print_state, r,
rotate, save_top_thm, set_goal, set_state, top_goal, top_thm, VALID.
\ENDDOC
|