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