set_goal : term list * term -> goalstack

SYNOPSIS

Initializes the subgoal package with a new goal.

DESCRIPTION

The function set_goal initializes the subgoal management package. A proof state of the package consists of either a goal stack and a justification stack if a proof is in progress, or a theorem if a proof has just been completed. set_goal sets a new proof state consisting of an empty justification stack and a goal stack with the given goal as its sole goal. The goal is printed.

FAILURE CONDITIONS

Fails unless all terms in the goal are of type bool.

EXAMPLE

  # set_goal([], `(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]`

USES

Starting an interactive proof session with the subgoal package. The subgoal package implements a simple framework for interactive goal-directed proof. When conducting a proof that involves many subgoals and tactics, the user must keep track of all the justifications and compose them in the correct order. While this is feasible even in large proofs, it is tedious. The subgoal package provides a way of building and traversing the tree of subgoals top-down, stacking the justifications and applying them properly. The package maintains a proof state consisting of either a goal stack of outstanding goals and a justification stack, or a theorem. Tactics are used to expand the current goal (the one on the top of the goal stack) into subgoals and justifications. These are pushed onto the goal stack and justification stack, respectively, to form a new proof state. All preceding proof states are saved and can be returned to if a mistake is made in the proof. The goal stack is divided into levels, a new level being created each time a tactic is successfully applied to give new subgoals. The subgoals of the current level may be considered in any order.

SEE ALSO

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