proofManagerLib.expand

STRUCTURE

SYNOPSIS

Applies a list-tactic to replace the current goal list.

DESCRIPTION

The function expand_list is part of the subgoal package. It may be abbreviated by the function elt. It applies a tactic to the current goal list (that is, the list of goals produced by the most recent use of expand or expand_list) to give a new proof state. The previous state is stored on the backup list. If the list-tactic produces subgoals, the new proof state is formed from the old one by removing the current goal list from the goal stack and replacing it by the list of subgoals produced by the list-tactic. The corresponding justification is modified accordingly, appropriate to the new goal list. 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 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.

FAILURE

expand_list ltac fails if the tactic ltac fails for the current goal list. It will diverge if the list-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 list-tactic is invalid.

EXAMPLE

> 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

USES

Doing a step in an interactive goal-directed proof, in particular, a step which affects all the subgoals generated by the preceding step.

SEEALSO

set_goal, restart, backup, restore, save, set_backup, expand, expandf, expand_listf, flatn, p, top_thm, top_goal