One creates definitions and theorems in two stages. First, one creates a slot in the library where the new object is to be stored by issuing the create command followed by the name of the object, the kind of the object and a place for the name ( top, bottom or before or after another name). The general form of the ``create'' command is create name kind place. An example of such a command follows.
create t1 thm topThe result is the display of
? t1 THMas a new library entry. The system does not recognize this as an object but rather as a place where the object t1 will eventually reside. The mark ? is called a status mark. The status of an object can be any one of the following:
The second stage in creating an object involves invoking the proof and text editors on the library object created in the first stage described above. One does so by asking to view the object: view name. Issuing view t1 results in a new window as shown in figure . If an object were present, it would appear in the window; at this stage, however, no object has been created, so one sees ? top. Since the object being edited is a theorem, the new window produced is a view of the proof editor, or refinement editor; if the object were a definition, then the system invokes the text editor. Definitions will be discussed at greater length in the next section. The refinement editor is a editor for tree--structured objects and is used for building proof trees. It is discussed in detail in chapter 4; at present it may be viewed as the place where theorems are displayed.
Figure: Appearance of the Screen after the Proof Editor Is Invoked
To enter a theorem statement at this stage, one invokes the text editor (ted) by pressing the select key, SEL ,SEL } or by clicking the left key on the mouse with the mouse cursor in < main proof goal>. This opens a new window as shown in figure . These windows can of course be repositioned, resized or elided (moved off to the edge of the screen) .
Figure: Appearance of the Screen after the Text Editor Is Invoked
One can now enter text into the text editor. As an example, suppose one were to type >> 0=0 in int. This becomes the statement of the theorem t1 and makes the trivial assertion that 0=0. The >> symbol is our notation for the logical turnstile, and the phrase in int appears because every statement of equality must be with respect to some type. One can now leave the text editor by pressing ; the statement now appears in the proof--editing window. If one were trying to prove this theorem, one would at this stage start using the proof facilities to build the proof; this process is discussed in detail in chapter 4. For the present, one can simply exit from this window with . The result is a new library entry for t1. The screen now looks like figure .
Figure: Appearance of Screen after Creating a Theorem
The status mark # indicates that this is an incomplete but syntactically correct object.