Basics of the Proof Editor

The proof  editor, red  (for refinement  editor), is invoked when the view command is given on a theorem object. The proof editor window always displays the current node of the proof. When the editor is first entered the current node is the root of the tree; in general, the current node can be changed by going into one of its subgoals or by going to its parent. For convenience there are also ways to jump to the next unproved leaf and to the root of the theorem.

  
Figure: A Sample Proof Editor Window

Figure shows a sample proof editor  window. The parenthesized numbers it contains are referenced below.

1. The header  line names the theorem being edited, t in this case.

2. The map , top 1 2, gives the path from the root to the current node. (If the path is too long to fit on one line it is truncated on the left.) The displayed node is the second child of the first child of the root.

3. The goal's first (and only) hypothesis , a:int, appears under the map.

4. The conclusion  of the goal is the formula to be proved, given the hypotheses. The conclusion is shown to the right of the the sequent arrow, >>. In the example it is

         b:int # ((a=b in int)|((a=b in int) -> void)) in U1.
   

5. The rule  specifies how to refine the goal. In the example the intro rule is used to specify product introduction, since the main connective of the conclusion is the product operator, #.

6. The first subgoal has one hypothesis, a:int, and the conclusion int in U1.

7. The second subgoal has two hypotheses, a:int and b:int, and the conclusion

           ((a=b in int) | ((a=b in int) -> void)) in U1.
   

Notice that lines (2), (6) and (7) have asterisks, which serve as status  indicators. The asterisk in line (2) means that this entire subgoal has the status complete; similarly, the asterisks in lines (6) and (7) mean that the two subgoals also are complete. Other status indicators are # (incomplete), - (bad), and ? (raw).