e : tactic -> goalstack

SYNOPSIS

Applies a tactic to the current goal, stacking the resulting subgoals.

DESCRIPTION

The function e is part of the subgoal package. 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 adding a new level consisting of its subgoals. 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 CONDITIONS

e 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

  # g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;;
  val it : goalstack = 1 subgoal (1 total)

  `HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`

  # e CONJ_TAC;;
  val it : goalstack = 2 subgoals (2 total)

  `TL [1; 2; 3] = [2; 3]`

  `HD [1; 2; 3] = 1`

  # e (REWRITE_TAC[HD]);;
  val it : goalstack = 1 subgoal (1 total)

  `TL [1; 2; 3] = [2; 3]`

  # e (REWRITE_TAC[TL]);;
  val it : goalstack = No subgoals

USES

Doing a step in an interactive goal-directed proof.

SEE ALSO

b, g, p, r, set_goal, top_goal, top_thm.