expand_list : list_tactic -> proof
If a list-tactic solves the current goal list (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. That level of goals 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 list-tactic applied is a validating version of the list-tactic given. It ensures that the justification of the list-tactic does provide a proof of the goals from the subgoals generated by the tactic. It will cause failure if this is not so. The tactical VALID_LT performs this validation.
For a description of the subgoal package, see set_goal.
> expand_list (ALLGOALS CONJ_TAC) ; OK.. NO_PROOFSException- NO_PROOFS raised > g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`; > val it = Proof manager status: 1 proof. 1. Incomplete: Initial goal: (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]) : proofs > expand CONJ_TAC; OK.. 2 subgoals: > val it = TL [1; 2; 3] = [2; 3] HD [1; 2; 3] = 1 : proof > expand_list (ALLGOALS (REWRITE_TAC[listTheory.HD,listTheory.TL])) ; OK.. val it = Initial goal proved. |- (HD [1; 2; 3] = 1) /\ (TL [1; 2; 3] = [2; 3]): proof