The HOL window Library

Jim Grundy

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

November 1992 \begin{matrix}c \\ ◯ \end{matrix} Jim Grundy 1992

Contents

1 Statement of Rights 3

2 The window Library 5 2.1 Window Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Getting Started . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Transforming the Focus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.4 Opening subwindows . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.5 Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.5.1 Windows on the Context . . . . . . . . . . . . . . . . . . . . . . . . 11 2.6 Conjectures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.7 Window Stacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2.7.1 The xlabel Library Component . . . . . . . . . . . . . . . . . . . . 15 2.8 Batch Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.9 The tactic Library Component . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.10 Adding New Window Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.11 Adding New Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

2.11.1 Relative Strengths . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.12 Future Changes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.13 Bugs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

3 ML Functions in the window Library 25

4 Pre-proved Theorems 95 4.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 4.2 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

Index 96 2 Contents

Chapter 1

Statement of Rights

Jim Grundy, hereafter referred to as ‘the Author’, retains the copyright and all other legal rights to the software contained in the window library, hereafter referred to as ‘the Software’. The Software is made available free of charge on an ‘as is’ basis. No guarantee, either express or implied, of maintenance, reliability, merchantability or suitability for any purpose is made by the Author.

The user is granted the right to make personal or internal use of the Software provided that both:

1. The Software is not used for commercial gain.

2. The user shall not hold the Author liable for any consequences arising from use of the Software.

The user is granted the right to further distribute the Software provided that both:

1. The Software and this statement of rights is not modified.

2. The Software does not form part or the whole of a system distributed for commercial gain.

The user is granted the right to modify the Software for personal or internal use provided that all of the following conditions are observed:

1. The user does not distribute the modified software.

2. The modified software is not used for commercial gain.

3. The Author retains all rights to the modified software.

Anyone seeking a licence to use this software for commercial purposes is invited to contact the Author.

4 Chapter 1. Statement of Rights

The window Library

This manual describes the use of the window library. The window library has been provided to facilitate a style of reasoning called window inference. Window inference should prove more useful than goal directed reasoning in situations where very fine grain manipulations are required, when a proof is more easily progressed forwards than backwards, or when a proof makes extensive use of contextual information. Users interested in transformational design, refinement and equational reasoning should find the window library interesting.

For more details on window inference, see:

Jim Grundy. Window Inference in the HOL System. In Phil J. Windley, Mylar Archer, Karl N. Levitt and Jeff J. Joyce, editors, The Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, University of California at Davis, 28–30 August 1991. IEEE Computer Society / ACM SIGDA, IEEE Computer Society Press, 10662 Los Vaqueros Circle, PO Box 3014, Los Alamitos CA 907020-1264, United States, 1992.

2.1 Window Inference

Window inference is a style of reasoning where the user may transform an expression by restricting attention to a subexpression and transforming it. While restricting attention to a subexpression, the user can transform the subexpression without affecting the remainder of the enclosing expression. Also, while transforming a subexpression, the user can make assumptions based on the context of the subexpression. For example, suppose a user wishes to transform the expression "A /\ B"; this may be done by transforming "A" under the assumption "B". It is possible to assume "B" while transforming "A", because were "B" false, the enclosing expression "A /\ B" would be false regardless of "A". Using contextual information in the transformation of subexpressions adds a degree of complexity to the proof tree. The advantage of the window inference technique is that the user is shielded from this added complexity.

In the window inference style of proof, a user starts with an expression "P" and transforms it to "Q" such that "Q R P" for some relation "R"^{1}; thus creating a proof that |- Q R P. Such a proof need be neither strictly forward nor backward. Window inference encompasses both backward and forward reasoning. The user may start with the expression "P" and transform it to "T"(true) while preserving the relation "==>". Such a process would build the theorem |- T ==> P, and would constitute a backward proof of "P". Alternatively, the user may start with the expression "T" and transform it to "P" while preserving the relation "<=="^{2}. Such a process would build the theorem |- P <== T, and would constitute a forward proof of "P".

1"R" denotes an infix, reflexive, transitive relation.

2.2 Getting Started

Before you can use window inference in HOL you must load the window library. To load the window library, issue the following command:

 load_library `window`;;

It is not always possible to load the window library. This is because the library contains a small theory called win. If you have loaded another theory before attempting to load the window library, and you are not in draft mode, then you will not be able to load the window library. If this happens, a new function load_window is defined which can be used to complete the loading process if HOL is placed in draft mode.

Within a window inference system reasoning is conducted with a stack of windows. Each window is comprised of a focus, f, that is the expression to be transformed, a set of formulae Γ called the assumptions, that can be assumed true in the context of the focus, and a relation R that must relate the focus and the expression to which it is transformed. (Note that the type of the focus is not restricted to :bool as is the case with goals in the subgoal package.) Such a window will be written as follows.

{! Γ \atop R * f}

To begin using the system, you create a window stack which contains a single window. The focus of that window should be the expression you want to transform, the assumptions of the window should be those things you wish to assume, and the relation of the window should be the relation you wish to preserve as you transform the focus. For example, suppose you wish to find something that implies "(A /\ (B /\ C)) /\ D" under the assumption "~C". To create such a stack, you should use the command:

    BEGIN_STACK : string -> term -> term list -> thm list -> void

The first parameter is the name that will be associated with the stack. The second parameter is a term containing both the focus and the relation to be preserved. The third parameter is the list of terms that you wish to assume. The last parameter is a list of theorems that might be relevant to the proof. The function of the last parameter will be explained in section 2.5, until then we will give this parameter the empty list.

2PMI_DEF |- !a, b.  (a <== b) = (b ==> a)

1

    #BEGIN_STACK `intro` "(==>) ((A /\ (B /\ C)) /\ D)" ["~C"] [];;
        ! ~C
    ==> * (A /\ B /\ C) /\ D
    () : void

As a side effect the BEGIN_STACK command prints the top window of the stack. To print the top window at any time use the PRINT_STACK command.

    PRINT_STACK : void -> void

Initially the user may choose one of "=", "==>" or "<==" as the relation to be preserved by a window. However the system can be tailored to preserve any reflexive, transitive relation. Details of how to declare a new relation for use with the system are given in section 2.11.

Each window holds a theorem. To obtain the theorem held by the current window use the following command:

    WIN_THM : void -> thm

Initially (before you have transformed the focus) this theorem will simply state that the original focus of the window is related to itself.

2

    #WIN_THM();;
    |- (A /\ B /\ C) /\ D ==> (A /\ B /\ C) /\ D

2.3 Transforming the Focus

Once you have a window the next thing you want to do is transform it. Each transformation of a focus f_{n} to f_{n+1} must be justified by a theorem of the following form:

Γ |- f_{n+1} R f_{n}

Where Γ is some subset of the assumptions of the window, and R is the relation which is being preserved by the window. The relation could, in fact, be any relation which the system knows to be as strong as R. The system already knows that equality is as strong as any reflexive relation. For the definition of stronger see section 2.11.

To take a theorem of the form above and use it to transform a window, use the command:

    TRANSFORM_WIN : thm -> void

To make life easier, the following commands are provided for transforming the focus of a window. These commands automatically generate a theorem of the correct form and use it to transform the window:^{3}

    MATCH_TRANSFORM_WIN: thm -> void
    REWRITE_WIN : thm list -> void
    PURE_REWRITE_WIN : thm list -> void
    CONVERT_WIN : conv -> void
    RULE_WIN : (thm -> thm) -> void
    THM_RULE_WIN : (thm -> thm) -> void
    FOC_RULE_WIN : (term -> thm) -> void
    TACTIC_WIN : tactic -> void

We shall stick to using rewriting in our examples because its function should be familiar. We can rewrite the focus of the window created in the previous section with the assumption of that window.

3

    #PURE_REWRITE_WIN [ASSUME "~C"];;
        ! ~C
    ==> * (A /\ B /\ F) /\ D
    () : void
    #WIN_THM ();;
    ~C |- (A /\ B /\ F) /\ D ==> (A /\ B /\ C) /\ D

If you decide that the last thing you did was a mistake, then you can use the UNDO command to undo it.

    UNDO : void -> void

2.4 Opening subwindows

If you wish to concentrate your attention on some subterm of the focus, you should open a window on that subterm. This is accomplished with the command:

    OPEN_WIN : path -> void

OPEN_WIN takes as an argument a path that describes the position of the desired subterm within the focus. A path is a list made up of the following constructors: RATOR, RAND and BODY. You should think of using each element in the list to select an ever decreasing subterm until the list is exhausted.

For example, if we wished to concentrate on the subterm "B /\ F" in the previous window, we should open a subwindow at [RATOR; RAND; RAND]:

3Other versions of rewriting are described in chapter 3.

4

    #OPEN_WIN [RATOR; RAND; RAND];;
        ! ~C
        ! D
        ! A
    ==> * B /\ F
    () : void

A subwindow will have all the assumptions of the parent window, plus any additional assumptions which follow from the context of the subwindow. The one exception to this rule is when a window is opened inside the body of an abstraction. In this case, all assumptions with free occurrences of the variable bound by the abstraction will be hidden. (In the future this may be handled by renaming.)

The relation in the subwindow may not be the same as the relation in the parent window. The system will choose the weakest relation for the subwindow which it knows will preserve the relation of the parent window. To learn how the system makes these choices refer to section 2.10.

Having got a subwindow you will want to transform it, and then close it. To close a subwindow, use the function:

    CLOSE_WIN : void -> void

We continue our example by transforming the subwindow with rewriting, and then closing it. Once back in the parent window, we check the theorem proved so far.

5

    #REWRITE_WIN [];;
        ! ~C
        ! D
        ! A
    ==> * F
    () : void
    #CLOSE_WIN ();;
        ! ~C
    ==> * (A /\ F) /\ D
    () : void
    #WIN_THM ();;
    ~C |- (A /\ F) /\ D ==> (A /\ B /\ C) /\ D

If opening a particular window proves to be a mistake, you can return to the parent window with the UNDO_WIN command.

    UNDO_WIN : void -> void

Alternatively, you can use the UNDO command if the OPEN_WIN was the last command you made.

2.5 Lemmas

The window stack can hold a set of theorems which are considered relevant to the current problem. The last parameter of the CREATE_WIN command is the initial list of theorems which should be considered relevant to the window stack. In section 2.2 we created a window with an empty list of relevant theorems.

If the hypotheses of a theorem are a subset of the assumptions of a window, then that theorem is said to be applicable in the context of that window. When a window is printed, the conclusions of those theorems held by the stack that are applicable to the window are printed with the assumptions of the window. Such conclusions are called the lemmas of the window. Lemmas may be used in the same way as the assumptions. We will refer to lemmas and assumptions collectively as the context of a window. When printed, lemmas are prefixed with ‘|’ rather than ‘!’ to distinguish them from assumptions.

As an example, suppose we wish to simplify the term "A /\ B" given that we have a theorem a_then_b which states that A |- B. We create a window stack which has a window with "A /\ B" as its focus, and which stores the theorem A |- B in the stack as a potentially relevant theorem.

1

    #BEGIN_STACK `lemma-ex` "(=) (A /\ B)" [] [a_then_b];;
    = * A /\ B
    () : void

If we now open a subwindow on "B" we enter a context in which the stored theorem is applicable. We can then use the conclusion of the stored theorem to rewrite the focus of the subwindow.

2

    #OPEN_WIN [RAND];;
      ! A
      | B
    = * B
    () : void
    #REWRITE_WIN [ASSUME "B:bool"];;
      ! A
      | B
    = * T
    () : void
    #CLOSE_WIN ();;
    = * A /\ T
    () : void

You can add more theorems to the set of relevant theorems during the course of a proof by using the ADD_THEOREM command.

    ADD_THEOREM : thm -> void

\underline{2.5. Lemmas 11}

You can also recover the list of theorems held by the window stack for use with another proof by using the LEMMA_THMS command.

    LEMMA_THMS : void -> thm list

2.5.1 Windows on the Context

Sometimes you might want to make use of a fact that follows indirectly from the context of a window. To allow this style of reasoning we provide a command for opening subwindows on subterms in the context. You can now open a window on some fact in the context and attempt to derive a new fact from it. When you close such a window a theorem is added to the set of theorems held by the window stack so that the fact you derived becomes a lemma.

The command to open a subwindow in the context is:

    OPEN_CONTEXT : term -> path -> void

The first parameter is the term in the context you wish to open a window on, the second is the path to the desired focus within that term. More often than not, the path will be empty (denoting the entire expression).

For example, consider the window below:

1

    #PRINT_STACK ();;
        ! A = Z
        ! (A /\ B) /\ A
    ==> * (Z /\ B) /\ A
    () : void

If we open a subwindow on the first "A" in the assumption "(A /\ B) /\ A, we can use the assumption "A = Z" to rewrite the "A" to a "Z". The resulting lemma could then be used to simplify the focus to "T".

2

    #OPEN_CONTEXT "(A /\ B) /\ A" [RATOR; RAND; RATOR; RAND];;
        ! A = Z
        ! (A /\ B) /\ A
        ! A
        ! B
    <== * A
    () : void

Note that we are now preserving the relation "<==", this is because we are trying to derive a new fact that follows from the assumption we opened a subwindow on.

3

    #REWRITE_WIN [ASSUME "A:bool = Z:bool"];;
        ! A = Z
        ! (A /\ B) /\ A
        ! A
        ! B
    <== * Z
    () : void
    #CLOSE_WIN ();;
        ! A = Z
        ! (A /\ B) /\ A
        | (Z /\ B) /\ A
    ==> * (Z /\ B) /\ A
    () : void

2.6 Conjectures

The window stack carries with it a set of goals, called suppositions, which the user supposes to be true. A supposition of the form P ?- C means that the user believes that "C" follows from "P". Initially the set of suppositions associated with the window stack is empty. Suppositions can be added to the stack with the command:

    ADD_SUPPOSE : (goal -> void)

The command CONJECTURE "C" is a shorthand for adding a supposition with conclusion "C" and assumptions the same as those of the current window.

    CONJECTURE : (term -> void)

If the premises of any supposition are a subset of the assumptions of a window, then that supposition is said to be applicable in the context of that window. When a window is printed, the conclusions of those suppositions which are held by the stack and which are applicable are printed with the assumptions and lemmas of the window. The conclusions of such suppositions are called the conjectures of the window. Conjectures are part of the context of a window. When printed, conjectures are prefixed with ‘?’ to distinguish them from the other elements of the context.

Conjectures may be used like the other elements of the context, except once used a conjecture must be proved. Once a conjecture has been used, its prefix will change from ‘?’ to ‘$’. If you have used a conjecture in a subwindow, and that conjecture is not part of the context of the parent window, or if the subwindow is inside the body of the abstraction and the variable bound by the abstraction occurs free in the conjecture, then that conjecture must be proved before you can be allowed to close the subwindow. Such conjectures are called bad conjectures. Bad conjectures are prefixed with ‘@’. A list of the bad conjectures of the current window can be obtained with the command:

    BAD_CONJECTURES : void -> term list

All conjectures used at the very bottom of the window stack are considered bad because they appear as extra assumptions in the theorem held by that window.

Consider the window below:

1

    #BEGIN_STACK `suppose-ex` "(=) ((A \/ ~A) \/ B)" [] [];;
    = * (A \/ ~A) \/ B
    () : void

If we assume that we can prove "A \/ ~A", we can simplify the focus, and then return to prove our assumption later.

2

    #CONJECTURE "A \/ ~A";;
      ? A \/ ~A
    = * (A \/ ~A) \/ B
    () : void
    #REWRITE_WIN [ASSUME "A \/ ~A"];;
      @ A \/ ~A
    = * T
    () : void
    #WIN_THM ();;
    A \/ ~A |- T = (A \/ ~A) \/ B

If you open a subwindow in the context of a window, and in that subwindow you use a conjecture, when you return to the parent window you may find that the conjecture is no longer considered to have been used. This is because the conjecture has not been used to transform the focus of this window. However, if you use the lemma generated by the subwindow, all conjectures used in generating that lemma will then be considered to have been used.

To remove a usage of a conjecture, you must introduce a lemma that is the same as the conjecture. You can do this by adding a theorem to the set of relevant theorems directly, by deriving the desired lemma from the context (using the conjecture to derive the required lemma will not work), or by using the command ESTABLISH.

    ESTABLISH : term -> void

ESTABLISH "C" opens a new subwindow with "C" as its focus and "==>" as the relation it preserves. If you can transform the focus of this subwindow to "T" and then close the window, "C" will become a lemma in the parent window.

So, to continue our example, we must now prove the conjecture we have used:

3

 #ESTABLISH "A \/ ~A";;
     ? A \/ ~A
 ==> * A \/ ~A
 () : void
 #REWRITE_WIN [EXCLUDED_MIDDLE];;
     ? A \/ ~A
 ==> * T
 () : void
 #CLOSE_WIN ();;
   | A \/ ~A
 = * T
 () : void
 #WIN_THM ();;
 |- T = (A \/ ~A) \/ B

2.7 Window Stacks

We have already used the BEGIN_STACK command introduced in section 2.2 to create a window stack. It is possible to work with several window stacks at the same time. When you create a new stack with BEGIN_STACK it becomes the current stack. You can set the current stack to another stack by using the command SET_STACK:

    SET_STACK : string -> void

The first parameter of SET_STACK is the name of the stack that you wish to be the current stack.

If you have finished working with a particular stack, it can be destroyed with the

END_STACK command.
    END_STACK : string -> void

The first parameter of the END_STACK command is the name of the stack you wish to destroy. It is possible, and in fact usual, to destroy the current stack, leaving yourself with no current stack.

The command CURRENT_NAME returns the name of the current stack, if there is one.

    CURRENT_NAME : string -> void

The ALL_STACKS command can be used to find out the names of all the stacks in the system.

    ALL_STACKS : void -> void

2.7.1 The xlabel Library Component

If you are running the HOL and the window system from within an Xterminal (an X windows pseudo-terminal), then the xlabel library component may be of help to you. The xlabel library component will set the title bar of the Xterminal to contain the name of the current stack, and maintain the title whenever the the current stack is changed. To load the xlabel component, first load the library as described in section 2.2, then type the following:

 load_library `window:xlabel`;;

2.8 Batch Proof

Once you have completed a proof with the window system, you may wish to reuse part or all of that proof. Until now, the proof has been developed as a series of operations on a stack of windows. Proofs can be repeated noninteractively without using the window stack. Each of the interactive commands we have seen so far (except the undo and stack related commands) has a batch equivalent. The batch commands have the same name as their interactive counterparts, except they are in lowercase.

A batch command to transform a window takes the original window as an argument and returns the transformed window. All such commands will have the basic type :window -> window. Batch analogues to commands which create subwindows have an argument of the transformation function to apply to the subwindow. They then take the original parent window as an argument, open a subwindow in the parent, apply the transformation function to the subwindow, and close the subwindow, returning the transformed parent window. All of these commands will have the basic type

:(window -> window) -> window -> window. The batch commands use of the ML run-

time stack mirrors the use of the window stack during interactive proof.

As an illustration of batch proof, we now repeat the first proof of section 2.2.

1

    #let w1 = create_win "(==>) (A /\ (B /\ C))" ["~C"] [] [];;
    w1 = (|- A /\ B /\ C ==> A /\ B /\ C, ["~C"], [], []) : window

The create_win command creates a window with the specified relation and focus. Its other parameters specify lists of assumptions to make and theorems that might be relevant to the window. create_win is the noninteractive analogue of BEGIN_STACK.

2

    #let w2 = ((pure_rewrite_win [ASSUME "~C"]) CB
    #          (open_win [RAND] (rewrite_win []))) w1;;
    w2 = (~C |- A /\ F ==> A /\ B /\ C, ["~C"], [], []) : window
    #win_thm w2;;
    ~C |- A /\ F ==> A /\ B /\ C

(Note that CB is new to release 2.0 of HOL: f CB g = g o f.) Since this particular combination of commands is quite common, the one command transform has been created for this situation.

    transform : (term -> term list -> thm list -> (window -> window) -> thm

transform creates a window, transforms it and returns the resulting theorem.

1

    #transform "(==>) (A /\ (B /\ C))" ["~C"] []
    #          ((pure_rewrite_win [ASSUME "~C"]) CB
    #           (open_win [RAND] (rewrite_win [])));;
    ~C |- A /\ F ==> A /\ B /\ C

To interface between interactive and batch proof the following functions are provided:

    TOP_WIN : void -> window
    APPLY_TRANSFORM : (window -> window) -> void

TOP_WIN returns the window on the top of the window stack. APPLY_TRANSFORM applies a window transformation function to the top of the stack. All the interactive transformation commands can be described with APPLY_TRANSFORM. For example,

   REWRITE_WIN thms = APPLY_TRANSFORM (rewrite_win thms)

2.9 The tactic Library Component

Most proof done with HOL uses the subgoal package. For most applications the subgoal package remains the most appropriate tool. However it is possible to mix the two proof styles. If you would like to use window inference from within the subgoal package you should load the tactic library component as follows:

 load_library `window:tactic`;;

The tactic library component contains the following functions for mixing the window inference and subgoal proof styles:

    BEGIN_STACK_TAC : string -> path -> thm list -> tactic
    END_STACK_TAC : tactic
    open_TAC : path -> thm list -> (window -> window) -> tactic

BEGIN_STACK_TAC and END_STACK_TAC are for interactive use only and should be used to develop a proof. Once developed, a proof can be repeated with open_TAC. The idea behind these tactics is to open a window inside the current goal, so as to transform some subterm of the goal. The path parameter of both OPEN_TAC and open_TAC is the path through the goal to the focus of the required subwindow. The list of theorems is the list of theorems that might be relevant to the proof.

Here is a simple interactive example. Suppose we had as our current goal the term

"A /\ B /\ F".

1

    #set_goal ([], "A /\ B /\ F");;
    "A /\ B /\ F"
    () : void

If we wanted to rewrite just the subterm "B /\ F" to "F" we can do this by opening a window on the subterm.

2

    #expand (BEGIN_STACK_TAC `tac-ex` [RAND] []);;
    OK..
    ==> * B /\ F
    "A /\ B /\ F"
    () : void

Having opened at window on the desired subterm we can rewrite it without effecting the remainder of the goal.

3

    #REWRITE_WIN [];;
    ==> * F
    () : void

The END_STACK_TAC tactic then takes the reasoning done in the window stack and applies it to the goal. END_STACK_TAC, will not work if you have made any changes to the goal since creating the stack.

4

    #expand (END_STACK_TAC `tac-ex`);;
    ==> * F
    OK..
    "A /\ F"
    () : void

The same example is repeated here with the window inference performed noninteractively.

1

    #set_goal ([], "A /\ (B /\ F)");;
    "A /\ B /\ F"
    () : void
    #expand (open_TAC [RAND] [] (rewrite_win []));;
    OK..
    "A /\ F"
    () : void

2.10 Adding New Window Rules

To allow the opening and closing of subwindows, the system chains together several inference rules on behalf of the user. These rules are called window rules and the system keeps them in a data base together with some information about them.

The system has a full set of rules for opening and closing subwindows on HOL terms. These rules are capable of preserving the following relations: "=", "==>" and "<==". The rules in the system exploit the contextual information available when windowing on the positions marked with ‘_’ in the following terms: "_/\_", "_\/_", "_==>_", "_<==_", "_=>_|_", "(_._)_", and let_=_in_. However, if you would like the system to preserve other relations, or exploit the contextual information available inside other terms, then you will have to add some rules to the database.

Each window rule must be of type :term -> (thm -> thm). A rule should take, the focus of the parent window and the theorem held by the child window, and return the theorem required to transform the parent window. For example, the window rule IMP_CONJ1_CLOSE as defined below is used when opening a subwindow at "A" in "A /\ B" while preserving "==>" in the parent window.

          B |- A' ==> A
   ---------------------------  IMP_CONJ1_CLOSE "A /\ B"
    |- (A' /\ B) ==> (A /\ B)

Each rule in the system is packaged with the following information:

• The path from the focus of the parent window to the focus of the child window. In

     the case of IMP_CONJ1_CLOSE this is [RATOR; RAND].

• A function from the focus of the parent window to bool. The function is true iff the rule is applicable to the focus. IMP_CONJ1_CLOSE only works on conjunctions, so it is stored with the function is_conj.

• A function which takes the focus of the parent window and the relation that we want to preserve in the parent window, and returns the relation that this rule will preserve in the child window. IMP_CONJ1_CLOSE always preserves "==>" in the child window.

• A function which takes the focus of the parent window and the relation that we want to preserve in the parent window, and returns the relation that this rule will preserve in the parent window. IMP_CONJ1_CLOSE always preserves "==>" in the parent window.

• A function which takes the focus and assumptions of the parent window, and returns the assumptions of the child window.

The assumptions of a window are represented by a list of theorems each of which has just one hypothesis. An assumption a is typically represented by the theorem a |- a. However, consider a window with focus "a /\ b /\ c". If you were to open a subwindow at "a" in such a window, you might expect the subwindow to have two new assumptions, "b" and "c". However a batch command would probably expect that when opening a window at the first operand of a conjunction, it would gain the second operand of the conjunction (namely "b /\ c") as an assumption. To avoid this a conflict of expectations, the following theorems should be added when opening the window: b /\ c |- b and b /\ c |- c. The system then knows that "b /\ c" can be assumed true, and that from that it can derive the "b" and "c". Only the conclusions of these theorems (namely "b" and "c") will be displayed as assumptions to the user during interactive proof.

• A function which takes the focus of the parent window and returns the list of variables which appear bound in the parent window, but which are free in the child window. That is, if the window rule opens inside the body of an abstraction, it returns the list of variables bound by the abstraction, otherwise the empty list is returned.

To add a window rule to the system, use the function store_rule.

store_rule : window_rule -> void

Where window_rule is defined as:

lettype window_rule = (  path
                    #  (term -> bool)
                    #  (term -> term -> term)
                    #  (term -> term -> term)
                    #  (term -> ((thm list) -> (thm list)))
                    #  (term -> (term list))
                    #  (term -> (thm -> thm))
                    );;

Namely, a tuple of those components just described, and the window rule itself. For example, IMP_CONJ1_CLOSE was added to the system with the following command:

store_rule   (   [RATOR; RAND]
           ,   is_conj
           ,   (\foc.\rel. "==>")
           ,   (\foc.\rel. "==>")
           ,   (\foc.\hyps. (SMASH (ASSUME (rand foc)))@hyps)
           ,   (\foc. [])

                ,   IMP_CONJ1_CLOSE
                );;

(Note that SMASH is new inference rule introduced by the window library. SMASH is similar

to CONJUNCTS.)

When opening a window it will usually be the case that there are several possible lists of window rules which could have been chained together to open a window at the required position. The system uses the following heuristics to decide which of two potential lists of rules is the better:

1. The system considers the child window which would result from using each of possible lists of rules.

• If the relation required to be preserved by one child window is known to be weaker than that required by the other, the list of rules which produced the window with the weaker relation is chosen.

• Otherwise, the list of rules which produced the child window with the most hypotheses is chosen.

2. If step 1 can not distinguish between the lists of rules then the choice between them is somewhat arbitrary. In such a case the lists are compared one rule at a time until one is found which is regarded as being more specific than the other.

• Rules which follow a longer path are regarded as more specific.

• Rules which preserve a weaker relation in the parent window are regarded as more specific.

• Rules which preserve a weaker relation in the child window are regarded as more specific.

• Rules which create more assumptions in the child window are regarded as more specific.

• Rules which were more recently added to the system are regarded as more specific.

2.11 Adding New Relations

Before the window library can be used to preserve a relation, the system must know that the relation is reflexive and transitive. The system is already aware that the following relations are reflexive and transitive: "=", "==>" and "<==".

To tell the system that some relation is reflexive and transitive, use add_relation.

    add_relation : (thm # thm) -> void

add_relation takes a pair of theorems, which should be of the same form as EQ_REFL and EQ_TRANS and stores these theorems for use by the system. For example, to tell the system that implication was reflexive and transitive we defined two theorems IMP_REFL_THM and IMP_TRANS_THM of the following form:

   IMP_REFL_THM = |- !x. x ==> x
   IMP_TRANS_THM = |- !x y z. (x ==> y) /\ (y ==> z) ==> x ==> z

and then issued the command:

   add_relation (IMP_REFL_THM, IMP_TRANS_THM);;

2.11.1 Relative Strengths

We say that some relation, r_{1}, is stronger than another relation, r_{2}, if whenever some x and y are related by r_{1} they are also related by r_{2}. Note that stronger is a reflexive relation.

If the system knows that r_{1} is stronger than r_{2} then it will allow you use theorems of the form

|- f_{n+1} r_{1} f_{n}

to transform the focus of a window which is supposed to be preserving the relation r_{2}. Furthermore, if you ask the system to open a subwindow in the focus of a window which is supposed to be preserving the relation r_{2}, and the system has no window rule for that case, it can substitute a window rule which preserves r_{1}.

Every relation used with the window library must be reflexive. From this we can deduce that equality is stronger than any relation that can be used with system. The window library knows this, so, when adding some new relation, there is no need to state that equality is stronger than it. However, if you plan on adding two new relations to the system, say "r1" and "r2", such that "r1" is stronger than "r2", you will need to tell the system about that.

First you should prove the following theorem WEAKEN_r1_r2:

    WEAKEN_r1_r2 = |- !x y. (x r1 y) ==> (x r2 y)

then call add_weak to add the theorem to the system:

    add_weak : thm -> void

as in:

   add_weak WEAKEN_r1_r2;;

2.12 Future Changes

Some changes to the window library are currently being considered. These changes include:

• The window rules for opening inside the body of abstractions may be changed so that they rename bound variables rather than hiding assumptions in which the bound variables occur.

• I may add the ability to weaken the premises of a supposition. This would be an alternative to compelling the user to prove used conjectures.

• It may be possible to specify a path to a subterm with pattern matching.

• Some functions which are currently considered internal to the system may be documented in future releases.

The window library is still work in progress. It has been released to solicit comment as much as to provide a service. As people begin to use the software I expect various infelicities to be brought to light. It is my intention to keep the interface fluid for the first couple to releases so that I can capitalise on the feedback I get from people’s experiences with using it. While I hope that the vast majority of the code is bug-free, I will not be too surprised to learn otherwise. If you do have a suggestion for improving the system, or find a bug, please contact me. I will endeavour to provide bug fixes as soon as possible. When reporting a bug, please be sure to tell me which versions of the window inference system and HOL you are using. The constant window_version contains the version number of the window system. I can be contacted at:

Jim Grundy

University of Cambridge  phone: +44 223 33 4760
Computer Laboratory fax: +44 223 33 4678
New Museums Site  telex: CAMSPLG 81240
Pembroke Street  email: jg@cl.cam.ac.uk

Cambridge CB2 3QG UNITED KINGDOM

2.13 Bugs

Opening a window inside a let expression will not work properly for let expressions involving tuples of variables or which use the and construct.

\underline{2.13. Bugs 23}

Acknowledgements

I would like to thank Andy Gordon, Mats Larsson, Laurent Thery and Joakim von Wright, all of whom have found bugs in earlier versions of the system, and suggested many improvements.

24 Chapter 2. The window Library

ML Functions in the window Library

This chapter provides documentation on most the ML functions that are made available in HOL when the window library is loaded. This documentation is also available online via the help facility. The documentation does not extend to functions which are considered to be internal to the window library. Entries for the internal functions do appear in the online help.

 add_relation

add_relation : ((thm # thm) -> void)

Synopsis

Declares a new relation for use with the window system.

Description

Before the window inference system can be used to preserve a given relation, the system must know that the relation is reflexive and transitive. Initially the system knows about the reflexivity and transitivity of equality, implication and backward implication. To inform the system of the reflexivity and transitivity of some new relation, NEW, the user should first prove to new theorems NEW_REFL_THM and NEW_TRANS_THM. These theorems should have a form analogous to that of IMP_REFL_THM and IMP_TRANS_THM respectively. The user should then execute the following command:

 add_relation (NEW_REFL_THM,NEW_TRANS_THM) .

Failure

Never fails.

See also

EQ_REFL, EQ_TRANS, IMP_REFL_THM, IMP_TRANS_THM, PMI_REFL_THM, PMI_TRANS_THM,
add_weak.

 ADD_SUPPOSE

ADD_SUPPOSE : (goal -> void)

Synopsis

Add a supposition to the set associated with the window stack.

Description

ADD_SUPPOSE (p ?- c) adds the supposition (p ?- c) to the set of suppositions associated with the window stack. The supposition will not be added if some stronger (alpha equivalent conclusion, fewer assumptions) theorem or supposition is already held by the stack. A limited amount of resolution is also performed on the theorems and supposition of a window after each addition. For example, if (q ?- p) were already a supposition and the supposition (p ?- c) was added, then the supposition (q ?- c) would be inferred.

Failure

Fails if there is no current window stack.

See also

add_suppose, CONJECTURE, ADD_THEOREM, ESTABLISH

 add_suppose

add_suppose : (goal -> window -> window)

Synopsis

Add a supposition to the set associated with a window.

Description

add_suppose (p ?- c) adds the supposition (p ?- c) to the set of suppositions associated with a window. The supposition will not be added if some stronger (equivalent conclusion, subset of assumptions) theorem or supposition is already held by the window. A limited amount of resolution is also performed on the theorems and supposition of a window after each addition. For example, if (q ?- p) were already a supposition and the supposition (p ?- c) was added, then the supposition (q ?- c) would be inferred.

Failure

Never fails.

See also

ADD_SUPPOSE, conjecture, add_theorem, establish

 ADD_THEOREM

ADD_THEOREM : (thm -> void)

Synopsis

Add a theorem to the set of theorems relevant to the window stack.

Description

ADD_THEOREM (a |- c) adds the theorem (a |- c) to the set of theorems considered relevant to the window stack. The theorem will not be added if a stronger (alpha-equivalent conclusion, subset of assumptions) theorem is already held by the stack. When each theorem is added, a limited amount of resolution is performed. For example if the theorem (b |- a) is already held by the system, and the theorem (a |- c) was added, then the theorem (b |- c) would be inferred.

Failure

Fails if there is no currrent window stack.

See also

add_theorem

 add_theorem

add_theorem : (thm -> window -> window)

Synopsis

Add a theorem to the set of theorems relevant to a window.

Description

add_theorem (a |- c) adds the theorem (a |- c) to the set of theorems considered relevant to a window. The theorem will not be added if a stronger (alpha-equivalent conclusion, fewer assumptions) theorem is already held by the window. When each theorem is added, a limited amount of resolution is performed. For example if the theorem (b |- a) is already held by the system, and the theorem (a |- c) was added, then the theorem (b |- c) would be inferred.

Failure

Never fails.

See also

ADD_THEOREM

 add_weak

add_weak : (thm -> void)

Synopsis

Adds a weakening rule to the window system tables.

Description

The window inference system can compensate for a missing window rule in its database by substituting a rule which preserves a relation which is stronger than the one the user wanted to preserve. To do this the system must know how to weaken a theorem where two terms are related by the stronger relation to a theorem where the two terms are related by the required relation.

The system already knows that equality is stronger than any reflexive relation, and how to weaken a theorem which relates terms by equality to a theorem which relates the terms by any reflexive relation. Suppose you would like the system to know that the relation "S" is stronger than the relation "R". First you should define the following theorem:

   WEAK_SR |- !x y. (x S y) ==> (x R y)

Next you add this theorem with the command add_weak WEAK_SR. From this information system maintains lists of which relationships may be substituted for which. Suppose we had added to the system rules for weakening "S" to "R" and "R" to "Q", the system can infer that both "R" and "S" can be used as substitutes for "Q", but "R" is preferable since it is the weaker of the two relations.

Failure

add_weak will fail if you try to add a rule which duplicates information already stored or inferred by the system. add_weak will fail if you try to add a rule which would create a cycle in the list of possible substitutes for a relation. add_weak will fail if you try to add a rule which would create a branch in the list of possible substitutes for a relation.

See also

add_relation.

 disp_hypotheses

disp_hypotheses : (window -> term list)

Synopsis

The hypotheses of a window - as displayed interactively.

Description

This is the list of things that may be assumed in the context of a window. disp_hypotheses returns the hypotheses in the form that they will be printed when the window library is used interactively.

Example

   #BEGIN_STACK `hyp-ex` "= ((A /\ B) /\ C)" [] [];;
   = * (A /\ B) /\ C
   () : void
   #OPEN_WIN [RAND];;
     ! B
     ! A
   = * C
   () : void
  #disp_hypotheses (TOP_WIN ());;
  ["A"; "B"] : term list

Failure

Never fails.

See also

hyp_thms, hypotheses, all_hypotheses, context

 ALL_STACKS

ALL_STACKS : (void -> string list)

Synopsis

Lists all the available stacks.

Description

ALL_STACKS () lists the names of all the stacks recorded in the system. That is all those stacks created by BEGIN_STACK and BEGIN_STACK_TAC, and not yet destroyed by END_STACK or END_STACK_TAC. You may use SET_STACK to make any one of these stacks the current stack.

Failure

Never fails.

See also

create_win, BEGIN_STACK, END_STACK, SET_STACK, CURRENT_NAME

 APPLY_TRANSFORM

APPLY_TRANSFORM : ((window -> window) -> void)

Synopsis

Apply a window transforming function to the top window.

Description

APPLY_TRANSFORM fn transforms the window on top of the window stack by applying fn to it.

Failure

Fails if the window stack is empty.

 ASM_REWRITE_WIN

ASM_REWRITE_WIN :  (thm list -> void)

asm rewrite win 31

Synopsis

Repeatedly rewrite top focus with the context, theorems and basic rewritings.

Failure

ASM_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may fail to terminate if thms describe a circular rewriting.

See also

GEN_REWRITE_WIN, REWRITE_WIN, PURE_REWRITE_WIN, PURE_ONCE_REWRITE_WIN,
ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 asm_rewrite_win

asm_rewrite_win :  (thm list -> window -> window)

Synopsis

Repeatedly rewrite the focus with context, theorems and basic rewritings.

Failure

asm_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms, or the context, describe a circular rewriting.

See also

gen_rewrite_win, pure_rewrite_win, rewrite_win, pure_once_rewrite_win,
once_rewrite_win, pure_asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 BAD_CONJECTURES

BAD_CONJECTURES : (void -> term list)

Synopsis

The conjectures of a window which have been used and that are not available in the parent window.

Description

BAD_CONJECTURES () returns the set of conjectures which have been used to transform the window on top of the window stack, and which are not in the context of the parent window below. These conjectures are called bad because the top window can not be closed if it has any bad conjectures.

Failure

Comments

If there is only one window on the window stack, all of its used conjectures are considered bad.

See also

used_conjectures, ESTABLISH, establish, PRINT_WIN

 BEGIN_STACK

BEGIN_STACK : (string -> term -> term list -> thm list -> void)

Synopsis

Create a window stack.

Description

BEGIN_STACK `name` "r f" hyps thms creates a new window stack containing a single window with: focus "f", relation "r", hypotheses hyps, relevant theorems thms and suppositions []. The new stack has the name `name` and is made the current stack.

Failure

BEGIN_STACK `name` "r f" hyps thms fails if there already exists a window stack called

`name`.

Uses

Use this command to start an interactive reasoning session.

See also

create_win, END_STACK, SET_STACK, ALL_STACKS, CURRENT_NAME

 BEGIN_STACK_TAC

BEGIN_STACK_TAC : (string -> path -> thm list -> tactic)

Synopsis

Open a subwindow on the current goal of the subgoals package.

Description

The tactic BEGIN_STACK_TAC name path thms leaves the current goal unchanged, but as a side-effect it creates a new window stack called name. The focus of the top (and only) window of this new stack is the selected subterm of the goal. The window will have the assumptions of the goal as it’s assumptions, as well as any assumptions which follow from it’s context. The window will have thms as it’s set of relevant theorems. The relation preserved by the window will be such that if goal is the current goal, the window can be used to transform goal to goal', generating the theorem (H |- goal' ==> goal). When the stack is ended with END_STACK_TAC name the goal will be transformed from goal to

goal'.

Failure

BEGIN_STACK_TAC name path thms will fail if the goal stack is empty, if path denotes a position which is not present in the current goal, or these already exists a window stack called name.

Example

#set_goal ([], "A \/ (B \/ F)");;
"A \/ B \/ F"
() : void
#e (BEGIN_STACK_TAC `tac` [RAND] []);;
OK..
! ~A
==> * B \/ F
"A \/ B \/ F"
() : void
#REWRITE_WIN [];;
! ~A
==> * B
() : void
#e (END_STACK_TAC `tac`);;
OK..
"A \/ B"
() : void

Comments

BEGIN_STACK_TAC is for interactive use only. For noninteractive applications use open_TAC.

See also

open_TAC, END_STACK_TAC

 bound

bound : (window -> term list)

Synopsis

The list of variables bound by a window.

Description

bound w returns the list of variables which are said to be bound by the window w. This is list list of variables which appear to be free in w, but are bound in the its parent window.

Example

    #letref b = [] : term list;;
    b = [] : term list
    #open_win
       [BODY]
       (\w. b:=bound w; w)
   (create_win "= (\x:num.x + y)" [] []) ;;
    (|- (\x. x + y) = (\x. x + y), [], [], [], ["x"]) : window
    #b;;
    ["x"] : term list

Failure

Never fails.

See also

 CLOSE_WIN

CLOSE_WIN : (void -> void)

Synopsis

Pop the top window from the stack and transform the parent window.

Description

CLOSE_WIN () removes the top window from the window stack and uses the theorem in that window to transform the parent window. CLOSE_WIN is used to close subwindows

opened by the GEN_OPEN_WIN, OPEN_WIN, OPEN_CONTEXT and ESTABLISH commands.

Failure

CLOSE_WIN () will fail if the stack is empty or is only one window deep. Other possible failures depend on the command used to open the window.

36 Chapter 3. ML Functions in the window Library

Example

#BEGIN_STACK `example` "(==>) (A /\ (B /\ F))" [] [];;
==> * A /\ B /\ F
() : void
#OPEN_WIN [rand];;
    ! A
==> * B /\ F
() : void
#REWRITE_WIN [];;
    ! A
==> * F
() : void
#CLOSE_WIN [];;
==> * A /\ F
() : void

See also

GEN_OPEN_WIN, gen_open_win, OPEN_WIN, open_context, OPEN_CONTEXT, establish,
ESTABLISH

 CONJECTURE

CONJECTURE : (term -> void)

Synopsis

Add a conjecture to the top window on the window stack.

Description

The command CONJECTURE "c" is a short-hand way of adding a supposition to the window stack. CONJECTURE "c" works like ADD_SUPPOSE (p ?- c) where "p" represents the hypotheses of the top window on the stack.

Failure

Fails if there is no current window stack.

See also

conjecture, ADD_SUPPOSE, ADD_THEOREM, ESTABLISH

 conjecture
conjecture : (term -> window -> window)

Synopsis

Add a conjecture to a window.

Description

The command conjecture "c" is a short-hand way of adding a supposition to a window. conjecture "c" works like add_suppose (p ?- c) where "p" represents the hypotheses of the window.

Failure

Never fails.

See also

add_suppose, ADD_SUPPOSE, add_theorem, ADD_THEOREM, establish
 conjectures
conjectures : (window -> term list)

Synopsis

The conjectures of a window.

Description

These are the conclusions of the suppositions of the window which have as their premises a subset of the hypotheses and lemmas of the window. The conjectures of a window are a set of terms which the user believes to the true in the context of the window, but which have not yet been proven.

Failure

Never fails.

See also

used_conjectures, BAD_CONJECTURES

 context

context : (window -> term list)

Synopsis

The context of a window.

Description

context w retuns all the hypotheses, lemmas, and conjectures that may be assumed in the context of the window w.

Failure

Never fails.

See also

all_hypotheses, lemmas, conjectures

 CONVERT_WIN

CONVERT_WIN :  (conv -> void)

Synopsis

Apply a conversion to the focus of the top window.

Description

If the focus of the top window is "f", and applying a conversion c to "f" yields the theorem (|- f = f'), then CONVERT_WIN c transforms the focus of the top window from

"f" to "f'".

Failure

CONVERT_WIN c if the window stack is empty. CONVERT_WIN c will fail if the hypotheses of the theorem returned when c is applied to the focus of the top window are not a subset of the context of the window.

See also

transform_win, TRANSFORM_WIN, convert_win, rule_win, RULE_WIN, thm_rule_win,
THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN, tactic_win, TACTIC_WIN, rewrite_win,
REWRITE_WIN

 convert_win

convert_win :  (conv -> window -> window)

Synopsis

Apply a conversion to the focus of a window.

Description

If the focus of the window, win, is "f", and applying a conversion c to "f" yields

(|- f = f'), then CONVERT_WIN c win transforms the focus of win from "f" to "f'".

Failure

convert_win c win will fail if the hypotheses of the theorem returned when c is applied to the focus of the window are not a subset of the context of win.

See also

transform_win, TRANSFORM_WIN, CONVERT_WIN, rewrite_win, REWRITE_WIN

 create_win

create_win : (term -> term list -> thm list -> window)

Synopsis

Create a window.

Description

create_win "r f" hyps thms creates a window with: focus "f", relation "r", hypotheses hyps and relevant theorems thms.

Failure

Never fails.

Uses

Use this command to create an initial window for reasoning with.

See also

transform, BEGIN_STACK

 CURRENT_NAME
CURRENT_NAME : (void -> string)

Synopsis

Returns the name of the current window stack.

Failure

Fails if there is no current window stack.

See also

create_win, BEGIN_STACK, END_STACK, SET_STACK, ALL_STACKS
 dest_pmi
dest_pmi : (term -> (term # term))

Synopsis

Breaks apart a backward implication into antecedent and consequent.

Description

dest_pmi is a term destructor for backward negations. dest_pmi "t1 <== t2" returns

("t1","t2").

Comments

Unlike dest_imp, dest_pmi does not consider negation to be a special case of implication.

Failure

Fails if the term is not a backward implication.

See also

dest_imp, PMI_DEF.
 all_hypotheses
all_hypotheses : (window -> term list)

Synopsis

The hypotheses of a window - in all their forms.

Description

This is the list of things that may be assumed in the context of a window. all_hypotheses returns the hypotheses in both the noninteractive and interactive forms.

Example

   #BEGIN_STACK `hyp-ex` "= ((A /\ B) /\ C)" [] [];;
   = * (A /\ B) /\ C
   () : void
   #OPEN_WIN [RAND];;
     ! B
     ! A
   = * C
   () : void
  #all_hypotheses (TOP_WIN ());;
  ["A /\ B"; "A"; "B"] : term list

Failure

Never fails.

See also

hyp_thms, hypotheses, disp_hypotheses, context

 empty_rules

empty_rules : (void -> void)

Synopsis

Deletes all window rules from the system’s tables.

Description

The system maintains a table of window rules for opening subwindows. This command is used to purge that table. You may wish to use this command if you do not whish to use those rules that are loaded by the system by default. You may also wish to use this command if you have added an erroneous rule to the systems tables with the store_rule command. To reload the default entries in the table you should reload the following

segments of the window library: basic_close, eq_close, imp_close and pmi_close.

Failure

Never fails.

See also

store_rule

 END_STACK

END_STACK : (string -> void)

Synopsis

Destroys a window stack.

Description

END_STACK `name` destroyes the window stack with name `name`. If `name` is the name of the current stack, then END_STACK `name` leaves you with no current stack.

Failure

END_STACK `name` fails if there is no stack called `name`.

See also

create_win, BEGIN_STACK, SET_STACK, ALL_STACKS, CURRENT_NAME

 END_STACK_TAC

END_STACK_TAC : (string -> tactic)

Synopsis

Closes a subwindow opened on the current goal of the subgoals package.

Description

END_STACK_TAC name closes all the subwindows on the window stack called name and returns to the parent window of the stack. The theorem in this window is used to generate a theorem of the form (H |- goal' ==> goal) where goal is the current goal of the subgoal package. The current goal is transformed from goal to goal' and the named stacked ended.

Failure

END_STACK_TAC will fail if you have done any other tactical reasoning since opening the window with BEGIN_STACK_TAC. END_STACK_TAC will also fail if there are any used conjectures in the current window. END_STACK_TAC will fail if the named stack was not created

with BEGIN_STACK_TAC.

Example

   #set_goal ([], "A \/ (B \/ F)");;
   "A \/ B \/ F"
   () : void
   #e (BEGIN_STACK_TAC `tac` [RAND] []);;
   OK..
       ! ~A
   ==> * B \/ F
   "A \/ B \/ F"
   () : void
   #REWRITE_WIN [];;
       ! ~A
   ==> * B
   () : void
   #e (END_STACK_TAC `tac`);;
   OK..
   "A \/ B"
   () : void

Comments

END_STACK_TAC is for interactive use only. For noninteractive applications use open_TAC.

See also

BEGIN_STACK_TAC, open_TAC

 equiv_tm

equiv_tm : term

Synopsis

The boolean constant ”=:bool -¿ (bool -¿ bool)”.

See also

imp_tm, pmi_tm.

 ESTABLISH

ESTABLISH : (term -> void)

Synopsis

Prove a new lemma. (Also used to establish the truth of conjectures.)

Description

ESTABLISH tm pushes a subwindow with focus tm onto the window stack. If tm is a conjecture in the parent window, it (and any lemmas that depend on it) will be removed from the subwindow. The relationship preserved in the subwindow is "==>". The user should then transform the focus of the subwindow from tm to "T"(true). The subwindow should then be closed making tm a lemma of the parent window.

Failure

ESTABLISH will fail if the window stack is empty. Attempts to use CLOSE_WIN on a window opened by ESTABLISH and whose focus has not been transformed to "T" will fail. If the focus can not be proven you can abandon the proof attempt with UNDO_WIN.

Example

#PRINT_WIN ();;
= * f
() : void
#ESTABLISH A \/ ~A;;
==> * A \/ ~A
() : void
#REWRITE_WIN [EXCLUDED_MIDDLE];;
==> * T
() : void
#CLOSE_WIN ();;
  | A \/ ~A
= * f
() : void

See also

GEN_OPEN_WIN, gen_open_win, open_win, OPEN_WIN, CLOSE_WIN, open_context,
OPEN_CONTEXT, establish

 establish

establish : (term -> (window -> window) -> window -> window)

Synopsis

Prove a new lemma. (Also used to establish the truth of conjectures.)

Description

establish tm fn win opens a subwindow with focus tm. If tm is a conjecture in the parent window, it (and any lemmas that depend on it) will be removed from the subwindow. The relationship preserved in the subwindow is "==>". fn is then used to transform the focus of the subwindow from tm to "T"(true). The subwindow is then closed and tm becomes a lemma in the parent window. The parent window with the new lemma is returned as the result.

Failure

establish tm fn win will fail if fn does not transform tm to "T" in the subwindow.

See also

open_win, OPEN_WIN, CLOSE_WIN, open_context, OPEN_CONTEXT, ESTABLISH,
gen_open_win, GEN_OPEN_WIN

 EXISTS_PMI

EXISTS_PMI : (term -> thm -> thm)

Synopsis

Existentially quantifies the antecedent and consequent of backward implication.

Description

When applied to a variable x and a theorem A |- t1 <== t2, the inference rule EXISTS_PMI returns the theorem A |- (?x. t1) <== (?x. t2), provided x is not free in the assumptions.

         A |- t1 <== t2
   --------------------------  EXISTS_IMP "x"   [where x is not free in A]
    A |- (?x.t1) <== (?x.t2)

Failure

Fails if the theorem is a backward implication, or if the term is not a variable, or if the term is a variable but is free in the assumption list.

See also

EXISTS_EQ, EXISTS_IMP, PMI_DEF.

 FILTER_ASM_REWRITE_WIN

FILTER_ASM_REWRITE_WIN :  ((term -> bool) -> thm list -> void)

Synopsis

Selectively rewrite the focus with context, theorems and basic rewritings.

Description

FILTER_ASM_REWRITE_WIN p thms repeatedly rewrites the focus of the top window on the current stack with thms, a list of basic rewritings and those theorems in the context of the window, the conclusions of which satisfy the predicate p.

Failure

Fails if there is no current stack.

FILTER_ASM_REWRITE_WIN p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms, or the selected terms in the context, describe a circular rewriting.

See also

ASM_REWRITE_WIN, GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN,
PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN,
PURE_ONCE_ASM_REWRITE_WIN, ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 filter_asm_rewrite_win

filter_asm_rewrite_win : ((term- bool)->thm list->window->window)

Synopsis

Selectively rewrite the focus with context, theorems and basic rewritings.

Description

filter_asm_rewrite_win p thms repeatedly rewrites the focus of a window with thms, a list of basic rewritings and those theorems in the context of the window, the conclusions of which satisfy the predicate p.

Failure

filter_asm_rewrite_win p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms, or the selected terms in the context, describe a circular rewriting.

See also

asm_rewrite_win, gen_rewrite_win, pure_rewrite_win, rewrite_win,
pure_once_rewrite_win, once_rewrite_win, pure_asm_rewrite_win,
pure_once_asm_rewrite_win, once_asm_rewrite_win, filter_pure_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 FILTER_ONCE_ASM_REWRITE_WIN

FILTER_ONCE_ASM_REWRITE_WIN :  ((term -> bool) -> thm list -> void)

48 Chapter 3. ML Functions in the window Library

Synopsis

Rewrite the focus with selected terms of the context, theorems and basics.

Description

FILTER_ONCE_ASM_REWRITE_WIN p thms rewrites the focus of a window with thms, those

theorems in the context of the window, the conclusions of which satisfy the predicate p, and a list of basic rewrites.

Failure

FILTER_ONCE_ASM_REWRITE_WIN p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window.

See also

ASM_REWRITE_WIN, GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN,
PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN,
PURE_ONCE_ASM_REWRITE_WIN, ONCE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ASM_REWRITE_WIN, FILTER_PURE_ONCE_ASM_REWRITE_WIN
 filter_once_asm_rewrite_win
filter_once_asm_rewrite_win:((term->bool)->thm list->window->window)

Synopsis

Rewrite the focus with selected terms of the context, theorems and basics.

Description

filter_once_asm_rewrite_win p thms rewrites the focus of a window with thms, those

theorems in the context of the window, the conclusions of which satisfy the predicate p, and a list of basic rewrites.

Failure

filter_once_asm_rewrite_win p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window.

See also

asm_rewrite_win, gen_rewrite_win, pure_rewrite_win, rewrite_win,
pure_once_rewrite_win, once_rewrite_win, pure_asm_rewrite_win,
pure_once_asm_rewrite_win, once_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_asm_rewrite_win, filter_pure_once_asm_rewrite_win

 FILTER_PURE_ASM_REWRITE_WIN
FILTER_PURE_ASM_REWRITE_WIN : ((term -> bool) -> thm list -> void)

Synopsis

Repeatedly rewrite the focus with selected terms of the context and theorems.

Description

FILTER_PURE_ASM_REWRITE_WIN p thms repeatedly rewrites the focus of of the top window on the current stack with thms and those theorems in the context of the window, the conclusions of which satisfy the predicate p.

Failure

Fails if there is not current stack.

FILTER_PURE_ASM_REWRITE_WIN p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms, or the selected terms in the context, describe a circular rewriting.

See also

ASM_REWRITE_WIN, GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN,
PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN,
PURE_ONCE_ASM_REWRITE_WIN, ONCE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN
 filter_pure_asm_rewrite_win
filter_pure_asm_rewrite_win:((term->bool)->thm list->window->window)

Synopsis

Repeatedly rewrite the focus with selected terms of the context and theorems.

Description

filter_pure_asm_rewrite_win p thms repeatedly rewrites the focus of a window with thms and those theorems in the context of the window, the conclusions of which satisfy the predicate p.

Failure

filter_pure_asm_rewrite_win p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms, or the selected terms in the context, describe a circular rewriting.

See also

asm_rewrite_win, gen_rewrite_win, pure_rewrite_win, rewrite_win,
pure_once_rewrite_win, once_rewrite_win, pure_asm_rewrite_win,
pure_once_asm_rewrite_win, once_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 FILTER_PURE_ONCE_ASM_REWRITE_WIN

FILTER_PURE_ONCE_ASM_REWRITE_WIN : ((term -> bool) -> thm list -> void)

Synopsis

Rewrite the focus with selected terms of the context and a list of theorems.

Description

FILTER_PURE_ONCE_ASM_REWRITE_WIN p thms rewrites the focus of the top window of the

current stack with thms and those theorems in the context of the window, the conclusions of which satisfy the predicate p.

Failure

Fails if there is no current stack.

  FILTER_PURE_ONCE_ASM_REWRITE_WIN p thms will fail if the hypotheses of any of the

theorems in thms are not a subset of the conjectures of the window.

See also

ASM_REWRITE_WIN, GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN,
PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN,
PURE_ONCE_ASM_REWRITE_WIN, ONCE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 filter_pure_once_asm_rewrite_win

filter_pure_once_asm_rewrite_win:(term->bool)->thm list->window->window

\underline{FOCUS 51}

Synopsis

Rewrite the focus with selected terms of the context and a list of theorems.

Description

filter_pure_once_asm_rewrite_win p thms rewrites the focus of a window with thms and

those theorems in the context of the window, the conclusions of which satisfy the predicate

p.

Failure

filter_pure_once_asm_rewrite_win p thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window.

See also

asm_rewrite_win, gen_rewrite_win, pure_rewrite_win, rewrite_win,
pure_once_rewrite_win, once_rewrite_win, pure_asm_rewrite_win,
pure_once_asm_rewrite_win, once_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_asm_rewrite_win, filter_once_asm_rewrite_win

 FOCUS

FOCUS : (void -> term)

Synopsis

The focus of the top window of the current window stack.

Failure

Fails if there is no current window stack.

See also

focus

 focus

focus : (window -> term)

Synopsis

The focus of a window.

Failure

See also

FOCUS

 FOC_RULE_WIN

FOC_RULE_WIN :  ((term -> thm) -> void)

Synopsis

Apply an inference rule to the focus of the top window.

Description

Assuming RULE is an inference rule of the following form:

   ------------- RULE "f"
    H |- f' R f

FOC_RULE_WIN RULE can be used to transform the focus of the top window from f to f', providing the window is supposed to preserve "R" or some weaker relation.

Failure

RULE_WIN r will fail if there is no current window stack or if the assumpitions of the theorem generated by r are not ab subset of the context of the top window. RULE_WIN r will fail if the top window is not supposed to preserve some relation which is equal to or weaker than "R.

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, thm_rule_win,
THM_RULE_WIN, rule_win, RULE_WIN, tactic_win, TACTIC_WIN, foc_rule_win,
rewrite_win, REWRITE_WIN

 foc_rule_win

foc_rule_win :  ((term -> thm) -> window -> window)

Synopsis

Apply an inference rule to the focus of a window.

Description

Assuming RULE is an inference rule of the following form:

   ------------- RULE "f"
    H |- f' R f

foc_rule_win RULE can be used to transform the focus of a window from f to f', providing the window is supposed to preserve "R" or some weaker relation.

Comments

The actual type displayed by the system is ”:(conv -¿ window -¿ window)”.

Failure

rule_win r will fail if the window is not supposed to preserve some relation which is equal to or weaker than "<==". rule_win r will fail if the hypotheses of the theorem produced by r are not a subset of the context of the window.

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, rule_win, RULE_WIN,
thm_rule_win, THM_RULE_WIN, FOC_RULE_WIN, tactic_win, TACTIC_WIN, rewrite_win,
REWRITE_WIN.

 GEN_OPEN_WIN

GEN_OPEN_WIN : (win_path -> void)

Synopsis

Apply some transformation to a subwindow of the top window window.

Description

GEN_OPEN_WIN wpath fn opens a subwindow on the top window at the position described by wpath. wpath can take one of two forms. If wpath is of the form FOCUS p then it indicates a subterm of the focus. In such cases GEN_OPEN_WIN wpth behaves like OPEN_WIN p. If wpath is of the form CONTEXT_PATH (t,p) then it indicates a subterm of the context. In such

cases GEN_OPEN_WIN wpth behaves like OPEN_CONTEXT t p.

See also

GEN_OPEN_WIN, open_win, open_context, OPEN_WIN, OPEN_CONTEXT, CLOSE_WIN

 gen_open_win

gen_open_win : (win_path -> (window -> window) -> window -> window)

Synopsis

Apply some transformation to a subwindow of a window.

Description

gen_open_win wpath fn win opens a subwindow inside win at the position described by wpath. wpath can take one of two forms. If wpath is of the form FOCUS p then it indicates a subterm of the focus. In such cases gen_open_win wpth behaves like open_win p. If wpath is of the form CONTEXT_PATH (t,p) then it indicates a subterm of the context. In such

cases gen_open_win wpth behaves like open_context t p.

See also

GEN_OPEN_WIN, open_win, open_context, OPEN_WIN, OPEN_CONTEXT, CLOSE_WIN

 GEN_REWRITE_WIN

gen_rewrite_win : ((conv -> conv) -> thm list -> thm list -> void)

Synopsis

Rewrites the window, selecting terms according to a user-specified strategy.

Description

Rewriting in HOL is based on the use of equational theorems as left-to-right replacements on the subterms of an object theorem. This replacement is mediated by the use of REWR_CONV, which finds matches between left-hand sides of given equations in a term and applies the substitution.

Equations used in rewriting are obtained from the theorem lists given as arguments to the function. These are at first transformed into a form suitable for rewriting. Conjunctions are separated into individual rewrites. Theorems with conclusions of the form "~t" are transformed into the corresponding equations "t = F". Theorems "t" which are not equations are cast as equations of form "t = T".

If a theorem is used to rewrite the object theorem, its assumptions are added to the assumptions of the returned theorem, unless they are alpha-convertible to existing assumptions. The matching involved uses variable instantiation. Thus, all free variables are generalized, and terms are instantiated before substitution. Theorems may have universally quantified variables.

The theorems with which rewriting is done are divided into two groups, to facilitate implementing other rewriting tools. However, they are considered in an order-independent fashion. (That is, the ordering is an implementation detail which is not specified.)

The search strategy for finding matching subterms is the first argument to the rule. Matching and substitution may occur at any level of the term, according to the specified search strategy: the whole term, or starting from any subterm. The search strategy also specifies the depth of the search: recursively up to an arbitrary depth until no matches occur, once over the selected subterm, or any more complex scheme.

Failure

GEN_REWRITE_WIN fails if the search strategy fails. It may also cause a non-terminating sequence of rewrites, depending on the search strategy used.

Uses

This rule is used in the system to implement all other window rewriting, and may provide a user with a method to fine-tune rewriting of windows.

Example

As an example, rewrite_win could be implemented as

    gen_rewrite_win TOP_DEPTH_CONV basic_rewrites

which specifies that matches should be searched recursively starting from the whole term of the theorem, and basic_rewrites must be added to the user defined set of theorems employed in rewriting.

See also

PURE_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN,
PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 gen_rewrite_win

gen_rewrite_win:((conv->conv)->thm list->thmlist->window->window)

Synopsis

Rewrites a window, selecting terms according to a user-specified strategy.

Description

Rewriting in HOL is based on the use of equational theorems as left-to-right replacements on the subterms of an object theorem. This replacement is mediated by the use of REWR_CONV, which finds matches between left-hand sides of given equations in a term and applies the substitution.

Equations used in rewriting are obtained from the theorem lists given as arguments to the function. These are at first transformed into a form suitable for rewriting. Conjunctions are separated into individual rewrites. Theorems with conclusions of the form "~t" are transformed into the corresponding equations "t = F". Theorems "t" which are not equations are cast as equations of form "t = T".

If a theorem is used to rewrite the object theorem, its assumptions are added to the assumptions of the returned theorem, unless they are alpha-convertible to existing assumptions. The matching involved uses variable instantiation. Thus, all free variables are generalized, and terms are instantiated before substitution. Theorems may have universally quantified variables.

The theorems with which rewriting is done are divided into two groups, to facilitate implementing other rewriting tools. However, they are considered in an order-independent fashion. (That is, the ordering is an implementation detail which is not specified.)

The search strategy for finding matching subterms is the first argument to the rule. Matching and substitution may occur at any level of the term, according to the specified search strategy: the whole term, or starting from any subterm. The search strategy also specifies the depth of the search: recursively up to an arbitrary depth until no matches occur, once over the selected subterm, or any more complex scheme.

Failure

gen_rewrite_win fails if the search strategy fails. It may also cause a non-terminating sequence of rewrites, depending on the search strategy used.

Uses

This rule is used in the system to implement all other window rewriting, and may provide a user with a method to fine-tune rewriting of windows.

Example

As an example, rewrite_win could be implemented as

    gen_rewrite_win TOP_DEPTH_CONV basic_rewrites

which specifies that matches should be searched recursively starting from the whole term of the theorem, and basic_rewrites must be added to the user defined set of theorems employed in rewriting.

GET MAX HIST 57

See also

pure_rewrite_win, rewrite_win, pure_once_rewrite_win, once_rewrite_win,
pure_asm_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 GET_MAX_HIST
GET_MAX_HIST: (void -> int)

Synopsis

Returns the maximum history size that can be stored for a window stack.

Failure See also

UNDO, REDO, SET_MAX_HIST
 hypotheses
hypotheses : (window -> term list)

Synopsis

The set of hypotheses of a window.

Description

This is the list of things that may be assumed in the context of a window. hypotheses may not present these things in the same way as they are printed interactively. Use disp_hyposesthese to get the set of hypotheses that are printed for interactive use.

Example

   #BEGIN_STACK `hyp-ex` "= ((A /\ B) /\ C)" [] [];;
   = * (A /\ B) /\ C
   () : void
   #OPEN_WIN [RAND];;
     ! B
     ! A
   = * C
   () : void
   #hypotheses (TOP_WIN ());;
   ["A /\ B"] : term list

Failure

Never fails.

See also

hyp_thms, disp_hypotheses, all_hypotheses, context

 hyp_thms

hyp_thms : (window -> thm list)

Synopsis

The theorems infered from the context of a window.

Description

hyp_thms w is the list of theorems which are infered from the context of w. The conclusions of these theorems are the hypotheses of the window.

\underline{IMP PMI 59}

Example

#BEGIN_STACK `hyp-ex` "= ((A /\ B) /\ C)" [] [];;
= * (A /\ B) /\ C
() : void
#OPEN_WIN [RAND];;
  ! B
  ! A
= * C
() : void
#hyp_thms (TOP_WIN ());;
[A /\ B |- A; A /\ B |- B] : thm list

Failure

Never fails.

See also

hypotheses, disp_hypotheses, all_hypothese

IMP_PMI

IMP_PMI : (thm -> thm)

Synopsis

Changes a forward implication into a backward implication.

Description

H |- t ==> u
--------------  IMP_PMI
H |- u <== t

Failure

IMP_PMI will fail if its argument is not an implication.

See also

PMI_IMP, PMI_DEF

 IMP_PMI_CONV
IMP_PMI_CONV : (term -> thm)

Synopsis

Changes a forward implication into a backward implication.

Example

#IMP_PMI_CONV "A ==> B";;
|- (A ==> B) = (B <== A)

Failure

IMP_PMI_CONV will fail if its argument is not an implication.

See also

PMI_IMP, IMP_PMI, PMI_IMP_CONV, PMI_DEF
 IMP_REFL
IMP_REFL : conv

Synopsis

Returns a theorem expressing the reflexivity of implication.

Description

------------ IMP_REFL "t"
 |- t ==> t

See also

REFL, PMI_REFL
 imp_tm
imp_tm : term

\underline{is pmi 61}

Synopsis

The boolean constant ”==¿”.

See also

equiv_tm, pmi_tm.

 is_pmi

is_pmi : (term -> bool)

Synopsis

Tests a term to see if it is a backward implication.

Description

is_pmi "t1 <== t2" returns true. If the argument is not a backward implication it returns

false.

Comments

Unlike is_imp, is_pmi does not consider negation to be a special case of implication.

Failure

Never fails.

See also

is_imp, PMI_DEF

 is_trueimp

is_trueimp : (term -> bool)

Synopsis

Tests a term to see if it is an implication.

Description

is_trueimp "t1 ==> t2" returns true. If the argument is not an implication it returns

false.

62 Chapter 3. ML Functions in the window Library

Failure

Never fails.

See also

is_imp, is_pmi
 lemmas
lemmas : (window -> term list)

Synopsis

The lemmas of a window.

Description

The list of conclusions of those theorems which are relevant to the window and the assumptions of which are a subset of the hypotheses of the window. The lemmas of a window are a list of terms which are known to be true in the context of the window.

Failure

Never fails.

See also

theorems
 LEMMA_THMS
LEMMA_THMS : (void -> thm list)

Synopsis

The set of theorems recorded as being relevant to the window stack.

Failure

Fails if there is not current window stack.

See also

lemma_thms

 lemma_thms

lemma_thms : (window -> thm list)

Synopsis

The set of theorems recorded as being relevant to this window.

Failure

Never fails.

See also

LEMMA_THMS, lemmas

 load_window

load_window : (void -> void)

Synopsis

Finishes loading the window library.

Description

If when the user attempts to load the window library the system is unable to load the theory win, then loading is aborted and the function load_window defined. If at some later time the user loads the theory win or places the system in draft mode, then the call load_library () can be used to complete the loading of the window library.

Comments

The function load_window is only defined if the initial attempt to load the window library did not succeed.

Failure

Fails if the theory win is not the parent theory and the system is not in draft mode.

See also

 MATCH_TRANSFORM_WIN
MATCH_TRANSFORM_WIN : (thm -> void)

Synopsis

Transform the focus of the current window.

Description

MATCH_TRANSFORM_WIN (H |- !x1...xn. g R f) specialises the quantified variables x1 ...

xn and then instantiates the free variables so that f matches the focus of the current window. The focus is then transformed to g (with the same substitutions applied).

Failure

TRANSFORM_WIN (H |- g R f) will fail if f can not be instantiated to the focus of the window. TRANSFORM_WIN (H |- g R f) will fail if H is not a subset of the context of the window. TRANSFORM_WIN (H |- g R f) will fail if R is not equal to or stronger than the relation that the window is supposed to maintain.

See also

transform_win, TRANSFORM_WIN, match_transform_win, convert_win, CONVERT_WIN,
rule_win, RULE_WIN, thm_rule_win, THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN,
tactic_win, TACTIC_WIN, rewrite_win, REWRITE_WIN

 match_transform_win

match_transform_win : (thm -> window -> window)

Synopsis

Transform the focus of a window.

Description

match_transform_win (H |- !x1...xn. g R f) specialises the quantified variables x1 ...

xn and then instantiates the free variables so that f matches the focus of window. The focus is then transformed to g (with the same substitutions applied).

Failure

transform_win (H |- g R f) will fail if f can not be instantiated to the focus of the window. transform_win (H |- g R f) will fail if H is not a subset of the context of the window. transform_win (H |- g R f) will fail if R is not equal to or stronger than the relation that the window is supposed to maintain.

See also

transform_win, TRANSFORM_WIN, MATCH_TRANSFORM_WIN, convert_win, CONVERT_WIN,
rule_win, RULE_WIN, thm_rule_win, THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN,
tactic_win, TACTIC_WIN, rewrite_win, REWRITE_WIN

 ONCE_ASM_REWRITE_WIN

ONCE_ASM_REWRITE_WIN :  (thm list -> void)

Synopsis

Rewrite the top focus with the context, a list of theorems and basic rewritings.

Failure

ONCE_ASM_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN,
ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN,
PURE_ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 once_asm_rewrite_win

once_rewrite_win :  (thm list -> window -> window)

Synopsis

Rewrite the focus with the context, a list of theorems and basic rewritings.

Failure

once_asm_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

gen_rewrite_win, pure_rewrite_win, rewrite_win, pure_once_rewrite_win,
once_rewrite_win, pure_asm_rewrite_win, asm_rewrite_win,
pure_once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 ONCE_REWRITE_WIN

ONCE_REWRITE_WIN :  (thm list -> void)

66 Chapter 3. ML Functions in the window Library

Synopsis

Rewrite the top focus with a list of theorems and basic rewritings.

Failure

ONCE_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN,
PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN
 once_rewrite_win
once_rewrite_win :  (thm list -> window -> window)

Synopsis

Rewrite the focus of a window with a list of theorems and basic rewritings.

Failure

once_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

gen_rewrite_win, pure_rewrite_win, rewrite_win, pure_once_rewrite_win,
pure_asm_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win
 OPEN_CONTEXT
OPEN_CONTEXT : (term -> path -> void)

Synopsis

Open a subwindow for deriving new lemmas.

Description

OPEN_CONTEXT tm path opens a subwindow on the assumption, lemma or conjecture tm at the position described by path. The subwindow is pushed onto the window stack. The relationship preserved by the subwindow will be chosen so that transforming the subwindow will transform tm to tm' generating the theorem (..|- tm' <== tm). When the subwindow is closed tm' becomes a new lemma in the parent window.

Failure

OPEN_CONTEXT tm path will fail if the window stack is empty.

OPEN_CONTEXT tm path will fail if tm is not an assumption, lemma or conjecture of the top window. This function will also fail if path describes a position which is not present in

tm.

Example

#BEGIN_STACK `example` "(==>) (B /\ C)" ["A ==> B"; "A /\ C"] [];;
    ! A ==> B
    ! A /\ C
==> * B /\ C
() : void
#OPEN_CONTEXT A /\ C [RATOR; RAND];;
    ! A ==> B
    ! A /\ C
    ! C
<== * A
() : void
#RULE_WIN (MP (ASSUME "A ==> B"));;
    ! A ==> B
    ! A /\ C
    ! C
<== * B
() : void
#CLOSE_WIN ();;
    ! A ==> B
    ! A /\ C
    | B /\ C
==> * B /\ C
() : void
#REWRITE_WIN [ASSUME "B /\ C"];;
    ! A ==> B
    ! A /\ C
    | B /\ C
==> * T
() : void

See also

GEN_OPEN_WIN, gen_open_win, open_win, OPEN_WIN, CLOSE_WIN, open_context,
establish, ESTABLISH

 open_context

open_context : (term -> path -> (window -> window) -> window -> window)

\underline{open TAC 69}

Synopsis

Derive a new lemma by applying a transformation to a subwindow on one of the assumptions, lemmas or conjectures.

Description

open_context tm path fn win opens a subwindow on the assumption, lemma or conjecture tm at the position described by path. The window transforming function fn is then applied to the resulting subwindow. The relationship preserved by the subwindow will be chosen so that transforming the subwindow will transform tm to tm' generating the theorem .|- tm' <== tm. The subwindow is then closed thereby making tm' an additional lemma of the parent window. The parent window with its new lemma is returned as the result.

Failure

open_context tm path fn win will fail if tm is not an assumption, lemma or conjecture of win. open_context tm path fn win will fail if path describes a position which is not present in tm.

See also

open_win, OPEN_WIN, CLOSE_WIN, OPEN_CONTEXT, establish, ESTABLISH,
gen_open_win, GEN_OPEN_WIN

 open_TAC

open_TAC : (path -> thm list -> (window -> window) -> tactic)

Synopsis

Do some window inference on the current goal of the subgoals package.

Description

open_TAC path thms fn is a tactic will allows the window inference system to be called from within the subgoals package. A subwindow is opened on that subterm of the goal, goal, selected by path. The window will have the assumptions of the goal as it’s assumptions, as well as any assumptions which follow from it’s context. The window will have thms as it’s set of relevant theorems. The relation preserved by the subwindow is chosen so that transforming the subwindow, with fn, transforms goal to goal', generating the theorem (H |- goal' ==> goal'). The subwindow is then closed and the goal is transformed from goal to goal'.

Failure

open_TAC path thms fn will fail if the goal stack is empty or if path denotes a position which is not present in the current goal.

Example

   #set_goal ([], "A \/ (B \/ F)");;
   "A \/ B \/ F"
   () : void
   #e (open_TAC [RAND] [] (rewrite_win []));;
   OK..
   "A \/ B"
   () : void

See also

BEGIN_STACK_TAC, END_STACK_TAC

 OPEN_WIN

OPEN_WIN : (path -> void)

Synopsis

Open a subwindow on the focus of the top window.

Description

OPEN_WIN path opens a subwindow in the focus of the top window at the position described by path. The subwindow is then pushed onto the top of the window stack.

Failure

OPEN_WIN path will fail if the window stack is empty. OPEN_WIN path will fail if path describes a position which is not present in the focus of the top window.

\underline{open win 71}

Example

#BEGIN_STACK `example` "(==>) (A /\ (B /\ F))" [] [];;
==> * A /\ B /\ F
() : void
#OPEN_WIN [RAND];;
    ! A
==> * B /\ F
() : void
#REWRITE_WIN [];;
    ! A
==> * F
() : void
#CLOSE_WIN [];;
==> * A /\ F
() : void

See also

GEN_OPEN_WIN, gen_open_win, open_win, CLOSE_WIN, open_context, OPEN_CONTEXT,
establish, ESTABLISH

 open_win

open_win : (path -> (window -> window) -> window -> window)

Synopsis

Apply some transformation to a subwindow of a window.

Description

open_win path fn win opens a subwindow in the focus of win at the position described by path. The window transforming function fn is then applied to the resulting subwindow. The subwindow is then closed and the transformed parent window returned as the result.

Failure

open_win path fn win will fail if path describes a position which is not present in the focus of win.

Example

# transform "(==>) (A /\ (B /\ F))" [] []
# (
#       open_win [RAND]
#       (
#               rewrite_win []
#       )
# );;
|- A /\ F ==> A /\ B /\ F

See also

OPEN_WIN, CLOSE_WIN, open_context, OPEN_CONTEXT, establish, ESTABLISH,
gen_open_win, GEN_OPEN_WIN

origin

origin : (window -> term)

Synopsis

The original focus of a window.

Failure

Never fails.

PMI_IMP

PMI_IMP : (thm -> thm)

Synopsis

Changes a backward implication into a forward implication.

Description

H |- u <== t
--------------  PMI_IMP
H |- t ==> u

Failure

PMI_IMP will fail if its argument is not a backward implication.

See also

IMP_PMI, PMI_DEF
 PMI_IMP_CONV
PMI_IMP_CONV : (term -> thm)

Synopsis

Changes a backward implication into a forward implication.

Example

#PMI_IMP_CONV "A ==> B";;
|- (A ==> B) = (B <== A)

Failure

IMP_PMI_CONV will fail if its argument is not a backward implication.

See also

PMI_IMP, IMP_PMI, IMP_PMI_CONV, PMI_DEF
 PMI_REFL
PMI_REFL : conv

Synopsis

Returns a theorem expressing the reflexivity of backward implication.

Description

------------ PMI_REFL "t"
 |- t <== t

See also

REFL, IMP_REFL, PMI_DEF

 pmi_tm
pmi_tm : term

Synopsis

The boolean constant ”¡==”.

See also

equiv_tm, imp_tm.
 PMI_TRANS
PMI_TRANS : (thm -> thm -> thm)

Synopsis

Implements the transitivity of backward implication.

Description

 A1 |- t1 <== t2  A2 |- t2 <== t3
---------------------------------- PMI_TRANS
       A1 u A2 |- t1 <== t3

See also

TRANS, IMP_TRANS, PMI_DEF
 PRINT_STACK
PRINT_WIN : (void -> void)

Synopsis

Print out the top window of the current window stack.

Description

PRINT_STACK will print out the top window on the stack according to the following format.

     ! "a"
     | "l"
     ? "c"
     $ "u"
     @ "b"
   R * "f"

That is, PRINT_STACK prints the context of the window followed by R * "f" where R is the relation that the window is supposed to preserve, and "f" is the focus of the window. Each element in the context is preceded by some prefix. The prefix ! denotes an assumption. The prefix | denotes a lemma. The prefix ? denotes a conjecture. The prefix $ denotes a used conjecture. The prefix @ denotes a bad conjecture.

Failure

PRINT_STACK () will fail if there is no current window stack.

 PURE_ASM_REWRITE_WIN
PURE_ASM_REWRITE_WIN :  (thm list -> void)

Synopsis

Repeatedly rewrite the top focus with the context and a list of theorems.

Failure

PURE_ASM_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may also fail to terminate if the theorems result in a circular rewriting.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN,
ONCE_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 pure_asm_rewrite_win

pure_asm_rewrite_win :  (thm list -> window -> window)

Synopsis

Repeatedly rewrite the focus with the context and a list of theorems.

Failure

pure_asm_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may also fail to terminate if the theorems result in a circular rewriting.

See also

gen_rewrite_win, rewrite_win, pure_rewrite_win, pure_once_rewrite_win,
once_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 PURE_ONCE_ASM_REWRITE_WIN

PURE_ONCE_ASM_REWRITE_WIN :  (thm list -> void)

Synopsis

Rewrite the top focus once with the context and a list of theorems.

Failure

PURE_ONCE_ASM_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN,
ONCE_REWRITE_WIN, PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, ONCE_ASM_REWRITE_WIN,
FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 pure_once_asm_rewrite_win

pure_once_asm_rewrite_win :  (thm list -> window -> window)

Synopsis

Rewrite the focus of a window once with the context and a list of theorems.

Failure

pure_once_asm_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

gen_rewrite_win, pure_rewrite_win, rewrite_win, once_rewrite_win,
pure_once_rewrite_win, pure_asm_rewrite_win, asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 PURE_ONCE_REWRITE_WIN

PURE_ONCE_REWRITE_WIN :  (thm list -> void)

Synopsis

Rewrite the top focus once with a list of theorems.

Failure

PURE_ONCE_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, REWRITE_WIN, ONCE_REWRITE_WIN,
PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 pure_once_rewrite_win

pure_once_rewrite_win :  (thm list -> window -> window)

Synopsis

Rewrite the focus of a window once with a list of theorems.

Failure

pure_once_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window.

See also

gen_rewrite_win, pure_rewrite_win, rewrite_win, once_rewrite_win,
pure_asm_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 PURE_REWRITE_WIN

PURE_REWRITE_WIN :  (thm list -> void)

Synopsis

Repeatedly rewrite the focus of the window on top of the window stack with a list of theorems.

Failure

PURE_REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may also fail to terminate if the theorems result in a circular rewriting.

See also

GEN_REWRITE_WIN, REWRITE_WIN, PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN,
PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN

 pure_rewrite_win

pure_rewrite_win :  (thm list -> window -> window)

Synopsis

Repeatedly rewrite the focus of a window with a list of theorems.

Failure

pure_rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may also fail to terminate if the theorems result in a circular rewriting.

\underline{REDO 79}

See also

gen_rewrite_win, rewrite_win, pure_once_rewrite_win, once_rewrite_win,
pure_asm_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

 REDO

REDO: (void -> void)

Synopsis

Redoes the last change that was undone.

Description

Redoes the last change that was undone from the current stack. Several REDOs can undo the effect of several UNDOs. It is not possible to REDO more UNDOs than are stored in the stacks history. To find out how many states can be stored in a stack, use the GET_MAX_HIST command.

Failure

REDO () will fail if nothing has been undone, or if some other change has been made to the stack since the last UNDO.

See also

UNDO, SET_MAX_HIST, GET_MAX_HIST

 relation

relation : (window -> term)

Synopsis

The relation preserved by a window.

Description

Returns the relation which the window is supposed to preserve between successive focusses.

Failure

Never fails.

 REWRITE_WIN
REWRITE_WIN :  (thm list -> void)

Synopsis

Repeatedly rewrite the focus of the top window of the window stack with a list of theorems and basic rewritings.

Failure

REWRITE_WIN thms will fail if the hypotheses of any of the theorems in thms are not a subset of the context of the window. This function may fail to terminate if thms describe a circular rewriting.

See also

GEN_REWRITE_WIN, PURE_REWRITE_WIN, PURE_ONCE_REWRITE_WIN, ONCE_REWRITE_WIN,
PURE_ASM_REWRITE_WIN, ASM_REWRITE_WIN, PURE_ONCE_ASM_REWRITE_WIN,
ONCE_ASM_REWRITE_WIN, FILTER_PURE_ASM_REWRITE_WIN, FILTER_ASM_REWRITE_WIN,
FILTER_PURE_ONCE_ASM_REWRITE_WIN, FILTER_ONCE_ASM_REWRITE_WIN
 rewrite_win
rewrite_win :  (thm list -> window -> window)

Synopsis

Repeatedly rewrite the focus with a list of theorems and basic rewritings.

Failure

rewrite_win thms will fail if the hypotheses of any of the theorems in thms are not a subset of the conjectures of the window. This function may fail to terminate if thms describe a circular rewriting.

See also

gen_rewrite_win, pure_rewrite_win, pure_once_rewrite_win, once_rewrite_win,
pure_asm_rewrite_win, asm_rewrite_win, pure_once_asm_rewrite_win,
once_asm_rewrite_win, filter_pure_asm_rewrite_win, filter_asm_rewrite_win,
filter_pure_once_asm_rewrite_win, filter_once_asm_rewrite_win

\underline{RULE WIN 81}

 RULE_WIN
RULE_WIN :  ((thm -> thm) -> void)

Synopsis

Apply an inference rule to the focus of the top window.

Description

Assuming RULE is an inference rule of the following form:

    H |- c
   -------- RULE
    H |- c'

RULE_WIN RULE can be used to transform the focus of the top window from c to c', providing the window is supposed to preserve "<==" or some weaker relation.

Failure

RULE_WIN r will fail if the window stack is empty. RULE_WIN r will fail if the top window is not supposed to preserve some relation which is equal to or weaker than "<==".

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, thm_rule_win,
THM_RULE_WIN, rule_win, foc_rule_win, FOC_RULE_WIN, tactic_win, TACTIC_WIN,
rewrite_win, REWRITE_WIN
 rule_win
rule_win :  ((thm -> thm) -> window -> window)

Synopsis

Apply an inference rule to the focus of a window.

82 Chapter 3. ML Functions in the window Library

Description

Assuming RULE is an inference rule of the following form:

    H |- c
   -------- RULE
    H |- c'

rule_win RULE can be used to transform the focus of a window from c to c', providing the window is supposed to preserve "<==" or some weaker relation.

Failure

rule_win r will fail if the window is not supposed to preserve some relation which is equal to or weaker than "<==".

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, RULE_WIN, thm_rule_win,
THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN, tactic_win, TACTIC_WIN, rewrite_win,
REWRITE_WIN.
 SAVE_WIN_THM
SAVE_WIN_THM : (void -> thm)

Synopsis

Stores the theorem held by the top window of the current stack.

Description

The call SAVE_WIN_THM () add the theorem held by the top window of the current window stack to the current theory segment under the name of the current window stack.

Failure

Fails if there is no current window stack. Fails if there the name of the current window stack is already present in the current theory segment. Also fails if the current theory file is read-only.

See also

WIN_THM, save_thm

 SET_MAX_HIST
SET_MAX_HIST: (int -> void)

Synopsis

Sets the maximum history size of all the window stacks.

Failure

Fails if given a history size less than 1.

See also

UNDO, REDO, GET_MAX_HIST
 SET_STACK
SET_STACK : (string -> void)

Synopsis

Sets the current stack.

Description

SET_STACK `name` sets the current stack to the one called `name`.

Failure

SET_STACK `name` fails if there is no stack called `name`.

See also

create_win, BEGIN_STACK, END_STACK, ALL_STACKS, CURRENT_NAME
 SMASH
SMASH : (thm -> thm list)

Synopsis

Recursively splits a compound theorem into a list of simpler one.

Description

The operation of SMASH is similar to that of CONJUNCTS except that it does not just break apart conjunctions. SMASH recursively applies the following inference rules to a theorem to smash it into a list of smaller theorems.

       H |- A /\ B         H |- ~(A \/ B)      H |- ~(A ==> B)
    -----------------    -------------------  ------------------
     H |- A   H |- B      H |- ~A   H |- ~B    H |- A   H |- ~B
     H |- ~(A <== B)      H |- A => B | F
    ------------------   -----------------
     H |- ~A   H |- B     H |- A   H |- B

Failure

Never Fails.

Uses

Used in the assumption generating field of a window rule to smash a single assumption into a list of assumptions.

See also

CONJUNCTS.

 store_rule

store_rule : (window_rule -> void)

Synopsis

Adds a window rule to the window system’s tables.

Description

The system maintains a table of window rules for opening subwindows. This command takes such a rule and adds it to the table maintained by the system.

Failure

Never fails.

See also

empty_rules

 suppositions

suppositions : (window -> goal list)

Synopsis

The suppositions of a window.

Description

The set of goals associated with a window which the user believes to be theorems.

Failure

Never fails.

See also

conjectures

 TACTIC_WIN

TACTIC_WIN :  (tactic -> void)

Synopsis

Apply a tactic to the focus of the top window.

Description

Assuming TAC is a tactic of the following form:

    H |- c
   ======== TAC
    H |- c'

TACTIC_WIN TAC can be used to transform the focus of the top window from c to c', providing the window is supposed to preserve "==>" or some weaker relation.

Failure

TACTIC_WIN t will fail if there is no current stack. TACTIC_WIN t will fail if the top window is not supposed to preserve some relation which is equal to or weaker than "<==". RULE_WIN t will fail if the application ot t generates more then one subgoal.

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, result_rule_win,
RESULT_RULE_WIN, rule_win, RULE_WIN, tactic_win, rewrite_win, REWRITE_WIN

 tactic_win

tactic_win :  (tactic -> window -> window)

Synopsis

Apply a tactic to the focus of a window.

Description

Assuming TAC is an inference rule of the following form:

    P |- c
   ======== TAC
    P |- c'

tactic_win TAC can be used to transform the focus of a window from c to c', providing the window is supposed to preserve "==>" or some weaker relation.

Failure

tactic_win t will fail if the window is not supposed to preserve some relation which is equal to or weaker than "==>" or if the tactic produces multiple subgoals.

See also

transform_win, TRANSFORM_WIN, convert_win, CONVERT_WIN, rule_win, RULE_WIN,
thm_rule_win, THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN, TACTIC_WIN,
rewrite_win, REWRITE_WIN

 THM_RULE_WIN

THM_RULE_WIN :  ((thm -> thm) -> void)

Synopsis

Apply an inference rule to the result of the window on top of the stack.

Description

Assuming RULE is an inference rule of the following form:

      H |- fn R f
    ---------------- RULE
     H' |- fn' R' f

If the top window of the current stack holds the theorem H |- fn R f, it will transform the window to one which holds the theorem H' |- fn' R' f; provided that H' is a subset of the context of the window and R' is as strong as R. This will transform the focus of the top window of the stack from fn to fn'.

Failure

THM_RULE_WIN r if r (WIN_THM ()) is not of the form H' |- fn' R' f (note that this re-

quires that r does not change f); or if H' is not a subset of the context of the window, or R' is not as strong as R.

See also

thm_rule_win, rule_win, RULE_WIN, foc_rule_win, FOC_RULE_WIN, WIN_THM

 thm_rule_win

thm_rule_win :  ((thm -> thm) -> window -> window)

Synopsis

Apply an inference rule to the result of a window.

Description

Assuming RULE is an inference rule of the following form:

      H |- fn R f
    ---------------- RULE
     H' |- fn' R' f

Then if (thm_rule_win RULE) is applied to a window holding the theorem H |- fn R f, it will transform the window to one which holds the theorem H' |- fn' R' f, provided that H' is a subset of the context of the window and R' is as strong as R. This will effectively transform the focus from fn to fn'.

88 Chapter 3. ML Functions in the window Library

Failure

thm_rule_win r w if r (win_thm w) is not of the form H' |- fn' R' f (note that this

requires that r does not change f); or if H' is not a subset of the context of the window, or R' is not as strong as R.

See also

THM_RULE_WIN, rule_win, RULE_WIN, foc_rule_win, FOC_RULE_WIN, win_thm
 TOP_WIN
TOP_WIN :  (void -> window)

Synopsis

Return the window on top of the window stack.

Failure

 transform
transform : (term -> term list -> thm list -> (window -> window) -> thm)

Synopsis

Create and transform a window and return the theorem generated.

Description

transform "r f" hyps thms fn creates a window with: focus "f", relation "r", hypotheses hyps, relevant theorems thms. The function fn is then applied to that window and the theorem held by the resulting window returned.

Uses

The basic command for rerunning noninteractive proofs.

Failure

Never fails.

Example

#transform "(==>) (A /\ T)" [] [] (rewrite_win []);;
|- A ==> A /\ T

See also

create_win

 TRANSFORM_WIN

TRANSFORM_WIN : (thm -> void)

Synopsis

Transform the focus of the top window.

Description

TRANSFORM_WIN (H |- F' R F) is used to transform the focus of the window on top of the window stack from F to F'.

Failure

If f is not the focus of the top window, then TRANSFORM_WIN (H |- F' R F) will fail. TRANSFORM_WIN (H |- F' R F) will fail if H is not a subset of the context of the top window. TRANSFORM_WIN (H |- F' R F) will fail if R is not equal to or stronger than the relation that the top window is supposed to maintain.

See also

transform_win, match_transform_win, MATCH_TRANSFORM_WIN, convert_win,
CONVERT_WIN, rule_win, RULE_WIN, thm_rule_win, THM_RULE_WIN, foc_rule_win,
FOC_RULE_WIN, tactic_win, TACTIC_WIN, rewrite_win, REWRITE_WIN

 transform_win

transform_win : (thm -> window -> window)

Synopsis

Transform the focus of a window.

Description

transform_win (H |- f' R f) transforms the focus of a window from f to f'.

Failure

transform_win (H |- f' R f) w will fail if f is not the focus of the window w. If H is not a subset of the context of the window w, then transform_win (H |- f' R f) w will fail. transform_win (H |- f' R f) will fail if R is not equal to or stronger than the relation that the window is supposed to maintain.

See also

TRANSFORM_WIN, match_transform_win, MATCH_TRANSFORM_WIN, convert_win,
CONVERT_WIN, rule_win, RULE_WIN, thm_rule_win, THM_RULE_WIN, foc_rule_win,
FOC_RULE_WIN, tactic_win, TACTIC_WIN, rewrite_win, REWRITE_WIN

 traverse

traverse : (path -> term -> term)

Synopsis

Use a path to select a subterm from a term.

Example

   #traverse [RATOR; RAND] "A /\ B";;
   "A" : term

Failure

Fails if the path selects a subterm which is not in the term.

 UNDO

UNDO: (void -> void)

Synopsis

Undoes the last transformation made to the current window stack.

\underline{UNDO WIN 91}

Description

Every change made to the current window stack is stored in a history. The most recent n states of the stack can be retrieved by sucessive calls to the UNDO command (n is the number returned by GET_MAX_HIST). Undoing a window with the UNDO_WIN command counts as a change to the stack, and can therefore be undone with UNDO. An UNDO, or seqence of UNDOs, can be undone by a REDO, or sequence of REDOs.

Failure

UNDO () will fail if no transformations have been made to the stack.

See also

UNDO_WIN, REDO, SET_MAX_HIST, GET_MAX_HIST

 UNDO_WIN

UNDO_WIN : (void -> void)

Synopsis

Pops the window stack.

Description

UNDO_WIN () is used to undo the opening of a subwindow and every transformation performed on the subwindow. UNDO_WIN () will return the user to the unchanged parent window.

Failure

UNDO_WIN () will fail no windows have been opened on the window stack.

See also

UNDO

 used_conjectures

used_conjectures : (window -> term list)

Synopsis

The conjectures used by a window.

Description

A list of those conjectures that have actually been used in the transformation of the current window and will therefore need to be proven at some stage. Conjectures which have been used in the current window, and which are not available as hypotheses, lemmas, or conjectures in the parent window must be proven before the current window can be closed.

Failure

Never fails.

See also

used_hypotheses, conjectures, BAD_CONJECTURES

 used_hypotheses

used_hypotheses : (window -> term list)

Synopsis

The used hypotheses of a window.

Description

Those hypotheses of a window that have actually been used in the transformation of the window.

Failure

Never fails.

Comments

The set returned by used_hypotheses for a given window need not be a subset of the set returned by hypotheses for the same window. This is because used_hypotheses will also contain any conjectures which have been used in the transformation of the window.

 window_version

window_version : num

\underline{WIN THM 93}

Synopsis

The version number of the window infernce system you are now using.

Comments

Be sure to quote this number when filing a bug report.

Failure

Never fails.

See also

 WIN_THM

WIN_THM : (void -> thm)

Synopsis

The theorem stored in the top window of the current stack.

Description

Returns the theorem stored in the window on the top of the current window stack. The theorem will have the form that assuming some subset of the hypotheses and conjectures of the window, the current focus is related to the original focus by the relationship the window is supposed to preserve.

Failure

Fails if there is no current window stack.

See also

result

 win_thm

win_thm : (window -> thm)

Synopsis

The theorem stored in a window.

Description

Returns the theorem stored in a window. The theorem will have the form that assuming some subset of the hypotheses and conjectures of the window, the current focus is related to the original focus by the relationship the window is supposed to preserve.

Failure

Never fails.

See also

WIN_THM, SAVE_WIN_THM

Pre-proved Theorems

The section that follows lists some the definitions and theorems in the window library. The name of the theory in which each theorem is stored is given in parentheses after the name of the theorem. Theorems which are not described in this chapter are considered internal to the window library.

4.1 Definitions

PMI_DEF (win)
  |- !a b. a <== b = b ==> a

4.2 Theorems

IMP_REFL_THM (win)
  |- !x. x ==> x
IMP_TRANS_THM (win)
  |- !x y z. (x ==> y) /\ (y ==> z) ==> x ==> z
PMI_DEF (win)
  |- !a b. a <== b = b ==> a
PMI_REFL_THM (win)
  |- !x. x <== x
PMI_TRANS_THM (win)
  |- !x y z. (x <== y) /\ (y <== z) ==> x <== z

Index

! (assumption prefix), 6 <== (backward implication), see PMI_DEF ? (conjecture prefix), 12 @ (bad conjecture prefix), 12 $ (used conjecture prefix), 12 | (lemma prefix), 10

add_relation, 20–21, 25
ADD_SUPPOSE, 12, 26
add_suppose, 26
ADD_THEOREM, 10, 27
add_theorem, 27
add_weak, 21, 28
all_hypotheses, 40
ALL_STACKS, 14, 30

applicable, 12

APPLY_TRANSFORM, 16, 30
ASM_REWRITE_WIN, 30
asm_rewrite_win, 31

assumptions, 6

BAD_CONJECTURES, 13, 31
BEGIN_STACK, 6–7, 14, 32
BEGIN_STACK_TAC, 16, 33
bound, 34

CB, 16

CLOSE_STACK_TAC, 16
CLOSE_WIN, 9, 35
CONJECTURE, 12, 36
conjecture, 37

conjectures, 12 bad, 12 used, 12

conjectures, 37
context, 38
CONVERT_WIN, 8, 38
convert_win, 39
create_win, 39

                                           CURRENT_NAME, 14, 40
                                           dest_pmi, 40
                                           disp_hypotheses, 29
                                           empty_rules, 41
                                           END_STACK, 14, 42
                                           END_STACK_TAC, 42
                                           equiv_tm, 44
                                           ESTABLISH, 13, 44
                                           establish, 45
                                           EXISTS_PMI, 46
                                           FILTER_ASM_REWRITE_WIN, 46
                                           filter_asm_rewrite_win, 47
                                           FILTER_ONCE_ASM_REWRITE_WIN, 47
                                           filter_once_asm_rewrite_win, 48
                                           FILTER_PURE_ASM_REWRITE_WIN, 49
                                           filter_pure_asm_rewrite_win, 49
                                           FILTER_PURE_ONCE_ASM_REWRITE_WIN, 50
                                           filter_pure_once_asm_rewrite_win, 50
                                           FOC_RULE_WIN, 8, 52
                                           foc_rule_win, 52
                                           FOCUS, 51

focus, 6

                                           focus, 51
                                           GEN_OPEN_WIN, 53
                                           gen_open_win, 54
                                           GEN_REWRITE_WIN, 54
                                           gen_rewrite_win, 55
                                           GET_MAX_HIST, 57
                                           hyp_thms, 58
                                           hypotheses, 57
                                           IMP_PMI, 59
                                           IMP_PMI_CONV, 60
                                           IMP_REFL, 60
                                           IMP_REFL_THM, 21, 95

\underline{Index 97}

imp_tm, 60
IMP_TRANS_THM, 21, 95
is_pmi, 61
is_trueimp, 61

lemma, 10–11

LEMMA_THMS, 11, 62
lemma_thms, 63
lemmas, 62
load_window, 6, 63
MATCH_TRANSFORM_WIN, 8, 63
match_transform_win, 64
ONCE_ASM_REWRITE_WIN, 65
once_asm_rewrite_win, 65
ONCE_REWRITE_WIN, 65
once_rewrite_win, 66
OPEN_CONTEXT, 11, 66
open_context, 68
open_TAC, 16, 69
OPEN_WIN, 8–9, 70
open_win, 71
origin, 72
path, 8
PMI_DEF, 6n, 95
PMI_IMP, 72
PMI_IMP_CONV, 73
PMI_REFL, 73
PMI_REFL_THM, 95
pmi_tm, 74
PMI_TRANS, 74
PMI_TRANS_THM, 95
PRINT_STACK, 7, 74
PURE_ASM_REWRITE_WIN, 75
pure_asm_rewrite_win, 75
PURE_ONCE_ASM_REWRITE_WIN, 76
pure_once_asm_rewrite_win, 76
PURE_ONCE_REWRITE_WIN, 77
pure_once_rewrite_win, 77
PURE_REWRITE_WIN, 8, 78
pure_rewrite_win, 78
REDO, 79

relation, 6

relation, 79
REWRITE_WIN, 8, 80

                                           rewrite_win, 80
                                           RULE_WIN, 8, 81
                                           rule_win, 81
                                           SAVE_WIN_THM, 82
                                           SET_MAX_HIST, 83
                                           SET_STACK, 14, 83
                                           SMASH, 83
                                           store_rule, 19, 84

stronger, 21 supposition, 12

                                           suppositions, 85
                                           TACTIC_WIN, 8, 85
                                           tactic_win, 86
                                           THM_RULE_WIN, 8, 86
                                           thm_rule_win, 87
                                           TOP_WIN, 16, 88
                                           transform, 16, 88
                                           TRANSFORM_WIN, 8, 89
                                           transform_win, 89
                                           traverse, 90

UNDO, 8, 9, 90

                                           UNDO_WIN, 9, 91
                                           used_conjectures, 91
                                           used_hypotheses, 92
                                           WIN_THM, 7, 93
                                           win_thm, 93
                                           window_rule, 19
                                           window_version, 92