1\DOC expand
2
3\TYPE {expand : tactic -> proof}
4
5\SYNOPSIS
6Applies a tactic to the current goal, stacking the resulting subgoals.
7
8\DESCRIBE
9The function {expand} is part of the subgoal package.  It may be abbreviated by
10the function {e}.  It applies a tactic to the current goal to give a new proof
11state. The previous state is stored on the backup list. If the tactic produces
12subgoals, the new proof state is formed from the old one by removing the
13current goal from the goal stack and adding a new level consisting of its
14subgoals. The corresponding justification is placed on the justification stack.
15The new subgoals are printed. If more than one subgoal is produced, they are
16printed from the bottom of the stack so that the new current goal is  printed
17last.
18
19If a tactic solves the current goal (returns an empty subgoal list), then its
20justification is used to prove a corresponding theorem. This theorem is
21incorporated into the justification of the parent goal and printed. If the
22subgoal was the last subgoal of the level, the level is removed and the parent
23goal is proved using  its (new) justification. This process is repeated until a
24level with unproven subgoals is reached. The next goal on the goal stack then
25becomes the current goal. This goal is printed. If all the subgoals are proved,
26the resulting proof state consists of the theorem proved by the justifications.
27
28The tactic applied is a validating version of the tactic given. It ensures that
29the justification of the tactic does provide a proof of the goal from the
30subgoals generated by the tactic. It will cause failure if this is not so. The
31tactical {VALID} performs this validation.
32
33For a description of the subgoal package, see  {set_goal}.
34
35\FAILURE
36{expand tac} fails if the tactic {tac} fails for the top goal. It will diverge
37if the tactic diverges for the goal. It will fail if there are no unproven
38goals. This could be because no goal has been set using {set_goal} or because
39the last goal set has been completely proved. It will also fail in cases when
40the tactic is invalid.
41
42\EXAMPLE
43{
44- expand CONJ_TAC;
45- expand CONJ_TAC;
46OK..
47NO_PROOFS! Uncaught exception:
48! NO_PROOFS
49
50- g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;
51> val it =
52    Proof manager status: 1 proof.
53    1. Incomplete:
54         Initial goal:
55         (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])
56
57     : proofs
58
59- expand CONJ_TAC;
60OK..
612 subgoals:
62> val it =
63    TL [1; 2; 3] = [2; 3]
64
65
66    HD [1; 2; 3] = 1
67
68     : proof
69
70- expand (REWRITE_TAC[listTheory.HD]);
71OK..
72
73Goal proved.
74|- HD [1; 2; 3] = 1
75
76Remaining subgoals:
77> val it =
78    TL [1; 2; 3] = [2; 3]
79
80     : proof
81
82- expand (REWRITE_TAC[listTheory.TL]);
83OK..
84
85Goal proved.
86|- TL [1; 2; 3] = [2; 3]
87> val it =
88    Initial goal proved.
89    |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) : proof
90}
91In the following example an invalid tactic is used. It is invalid
92because it assumes something that is not on the assumption list of the goal.
93The justification adds this assumption to the assumption list so the
94justification would not prove the goal that was set.
95{
96- g `1=2`;
97> val it =
98    Proof manager status: 2 proofs.
99    2. Completed: |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3])
100    1. Incomplete:
101         Initial goal:
102         1 = 2
103
104     : proofs
105- expand (REWRITE_TAC[ASSUME (Term `1=2`)]);
106OK..
107
108Exception raised at Tactical.VALID:
109Invalid tactic
110! Uncaught exception:
111! HOL_ERR
112}
113
114Note that an invalid tactic may "succeed".
115Thus, where {tac1} is invalid, and {tac2} is valid (and both succeed),
116{FIRST [tac1, tac2]} is invalid.  For example, where
117theorem {uth} is {[p] |- q} and {uth'} is {[p'] |- q}
118
119{
1201 subgoal:
121val it =
122
123q
124------------------------------------
125  p
126:
127   proof
128
129> e (FIRST (map ACCEPT_TAC [uth', uth])) ;
130OK..
131
132Exception raised at Tactical.VALID:
133Invalid tactic [...]
134
135> e (FIRST (map (VALID o ACCEPT_TAC) [uth', uth])) ;
136OK..
137
138Goal proved.
139 [p] |- q
140}
141
142\USES
143Doing a step in an interactive goal-directed proof.
144
145\SEEALSO
146proofManagerLib.set_goal, proofManagerLib.restart,
147proofManagerLib.backup,proofManagerLib.restore, proofManagerLib.save,
148proofManagerLib.set_backup,proofManagerLib.expand, proofManagerLib.expandf,
149proofManagerLib.flatn,proofManagerLib.p,proofManagerLib.top_thm,
150proofManagerLib.top_goal, Tactical.VALID, Tactical.VALIDATE
151
152\ENDDOC
153