set_goal : term list * term -> goalstack
Initializes the subgoal package with a new goal.
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.
# 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]`
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.