\chapter{ML Functions in the window Library}
\input{entries-intro}
\DOC{add\_relation}

\TYPE {\small\verb%add_relation : ((thm # thm) -> void)%}\egroup

\SYNOPSIS
Declares a new relation for use with the window system.

\DESCRIBE
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, {\small\verb%NEW%}, the user should
first prove to new theorems {\small\verb%NEW_REFL_THM%} and {\small\verb%NEW_TRANS_THM%}.  These
theorems should have a form analogous to that of {\small\verb%IMP_REFL_THM%} and
{\small\verb%IMP_TRANS_THM%} respectively.  The user should then execute the following
command:

\noindent{\small\verb%
	add_relation (NEW_REFL_THM,NEW_TRANS_THM)
%}.

\FAILURE
Never fails.

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

\ENDDOC
\DOC{ADD\_SUPPOSE}

\TYPE {\small\verb%ADD_SUPPOSE : (goal -> void)%}\egroup

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

\DESCRIBE
{\small\verb%ADD_SUPPOSE (p ?- c)%} adds the supposition {\small\verb%(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 {\small\verb%(q ?- p)%} were already a supposition 
and the supposition {\small\verb%(p ?- c)%} was added, then the supposition {\small\verb%(q ?- c)%}
would be inferred.

\FAILURE
Fails if there is no current window stack.

\SEEALSO
add_suppose, CONJECTURE, ADD_THEOREM, ESTABLISH

\ENDDOC
\DOC{add\_suppose}

\TYPE {\small\verb%add_suppose : (goal -> window -> window)%}\egroup

\SYNOPSIS
Add a supposition to the set associated with a window.

\DESCRIBE
{\small\verb%add_suppose (p ?- c)%} adds the supposition {\small\verb%(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 {\small\verb%(q ?- p)%} were already a supposition 
and the supposition {\small\verb%(p ?- c)%} was added, then the supposition {\small\verb%(q ?- c)%}
would be inferred.

\FAILURE
Never fails.

\SEEALSO
ADD_SUPPOSE, conjecture, add_theorem, establish

\ENDDOC
\DOC{ADD\_THEOREM}

\TYPE {\small\verb%ADD_THEOREM : (thm -> void)%}\egroup

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

\DESCRIBE
{\small\verb%ADD_THEOREM (a |- c)%} adds the theorem {\small\verb%(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 {\small\verb%(b |- a)%} is already held by the system,
and the theorem {\small\verb%(a |- c)%} was added, then the theorem {\small\verb%(b |- c)%}
would be inferred.

\FAILURE
Fails if there is no currrent window stack.

\SEEALSO
add_theorem

\ENDDOC
\DOC{add\_theorem}

\TYPE {\small\verb%add_theorem : (thm -> window -> window)%}\egroup

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

\DESCRIBE
{\small\verb%add_theorem (a |- c)%} adds the theorem {\small\verb%(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 {\small\verb%(b |- a)%} is already held by the system,
and the theorem {\small\verb%(a |- c)%} was added, then the theorem {\small\verb%(b |- c)%}
would be inferred.

\FAILURE
Never fails.

\SEEALSO
ADD_THEOREM

\ENDDOC
\DOC{add\_weak}

\TYPE {\small\verb%add_weak : (thm -> void)%}\egroup

\SYNOPSIS
Adds a weakening rule to the window system tables.

\DESCRIBE
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 {\small\verb%"S"%} is 
stronger than the relation {\small\verb%"R"%}.
First you should define the following theorem:
{\par\samepage\setseps\small
\begin{verbatim}
   WEAK_SR |- !x y. (x S y) ==> (x R y)
\end{verbatim}
}
\noindent Next you add this theorem with the command
{\small\verb%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 {\small\verb%"S"%} to {\small\verb%"R"%} and {\small\verb%"R"%}
to {\small\verb%"Q"%}, the system can infer that both {\small\verb%"R"%} and {\small\verb%"S"%} can be used as
substitutes for {\small\verb%"Q"%}, but {\small\verb%"R"%} is preferable since it is the weaker of the
two relations.

\FAILURE
{\small\verb%add_weak%} will fail if you try to add a rule which duplicates information
already stored or inferred by the system.
{\small\verb%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.
{\small\verb%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.

\SEEALSO
add_relation.

\ENDDOC
\DOC{disp\_hypotheses}

\TYPE {\small\verb%disp_hypotheses : (window -> term list)%}\egroup

\SYNOPSIS
The hypotheses of a window - as displayed interactively.

\DESCRIBE
This is the list of things that may be assumed in the context of a window.
{\small\verb%disp_hypotheses%} returns the hypotheses in the form that they will
be printed when the window library is used interactively.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #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

\end{verbatim}
}

\FAILURE
Never fails.

\SEEALSO
hyp_thms, hypotheses, all_hypotheses, context

\ENDDOC
\DOC{ALL\_STACKS}

\TYPE {\small\verb%ALL_STACKS : (void -> string list)%}\egroup

\SYNOPSIS
Lists all the available stacks.

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

\FAILURE
Never fails.

\SEEALSO
create_win, BEGIN_STACK, END_STACK, SET_STACK, CURRENT_NAME

\ENDDOC
\DOC{APPLY\_TRANSFORM}

\TYPE {\small\verb%APPLY_TRANSFORM : ((window -> window) -> void)%}\egroup

\SYNOPSIS
Apply a window transforming function to the top window.

\DESCRIBE
{\small\verb%APPLY_TRANSFORM fn%} transforms the window on top of the window stack by
applying {\small\verb%fn%} to it.

\FAILURE
Fails if the window stack is empty.

\ENDDOC
\DOC{ASM\_REWRITE\_WIN}

\TYPE {\small\verb%ASM_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%ASM_REWRITE_WIN thms%} will fail if the hypotheses of any of the theorems
in {\small\verb%thms%} are not a subset of the context of the window.
This function may fail to terminate if {\small\verb%thms%} describe a circular rewriting.

\SEEALSO
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

\ENDDOC
\DOC{asm\_rewrite\_win}

\TYPE {\small\verb%asm_rewrite_win :  (thm list -> window -> window)%}\egroup

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

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

\SEEALSO
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

\ENDDOC
\DOC{BAD\_CONJECTURES}

\TYPE {\small\verb%BAD_CONJECTURES : (void -> term list)%}\egroup

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

\DESCRIBE
{\small\verb%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.

\SEEALSO
used_conjectures, ESTABLISH, establish, PRINT_WIN

\ENDDOC
\DOC{BEGIN\_STACK}

\TYPE {\small\verb%BEGIN_STACK : (string -> term -> term list -> thm list -> void)%}\egroup

\SYNOPSIS
Create a window stack.

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

\FAILURE
{\small\verb%BEGIN_STACK `name` "r f" hyps thms%} fails if there already exists
a window stack called {\small\verb%`name`%}.

\USES
Use this command to start an interactive reasoning session.

\SEEALSO
create_win, END_STACK, SET_STACK, ALL_STACKS, CURRENT_NAME

\ENDDOC
\DOC{BEGIN\_STACK\_TAC}

\TYPE {\small\verb%BEGIN_STACK_TAC : (string -> path -> thm list -> tactic)%}\egroup

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

\DESCRIBE
The tactic {\small\verb%BEGIN_STACK_TAC name path thms%} leaves the current goal unchanged,
but as a side-effect it creates a new window stack called {\small\verb%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 {\small\verb%thms%} as it's set of relevant theorems.
The relation preserved by the window will be such that if {\small\verb%goal%} is
the current goal, the window can be used to transform {\small\verb%goal%} to {\small\verb%goal'%},
generating the theorem {\small\verb%(H |- goal' ==> goal)%}.
When the stack is ended with {\small\verb%END_STACK_TAC name%} the goal will be
transformed from {\small\verb%goal%} to {\small\verb%goal'%}.

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

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
	#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
\end{verbatim}
}

\COMMENTS
{\small\verb%BEGIN_STACK_TAC%} is for interactive use only.
For noninteractive applications use {\small\verb%open_TAC%}.

\SEEALSO
open_TAC, END_STACK_TAC

\ENDDOC
\DOC{bound}

\TYPE {\small\verb%bound : (window -> term list)%}\egroup

\SYNOPSIS
The list of variables bound by a window.

\DESCRIBE
{\small\verb%bound w%} returns the list of variables which are said to be bound by
the window {\small\verb%w%}.   This is list list of variables which appear to be
free in {\small\verb%w%}, but are bound in the its parent window.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
    #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
\end{verbatim}
}


\FAILURE
Never fails.

\SEEALSO

\ENDDOC
\DOC{CLOSE\_WIN}

\TYPE {\small\verb%CLOSE_WIN : (void -> void)%}\egroup

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

\DESCRIBE
{\small\verb%CLOSE_WIN ()%} removes the top window from the window stack and
uses the theorem in that window to transform the parent window.
{\small\verb%CLOSE_WIN%} is used to close subwindows opened by the
{\small\verb%GEN_OPEN_WIN%}, {\small\verb%OPEN_WIN%}, {\small\verb%OPEN_CONTEXT%} and {\small\verb%ESTABLISH%} commands.

\FAILURE
{\small\verb%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.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#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
\end{verbatim}
}

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

\ENDDOC
\DOC{CONJECTURE}

\TYPE {\small\verb%CONJECTURE : (term -> void)%}\egroup

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

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

\FAILURE
Fails if there is no current window stack.

\SEEALSO
conjecture, ADD_SUPPOSE, ADD_THEOREM, ESTABLISH

\ENDDOC
\DOC{conjecture}

\TYPE {\small\verb%conjecture : (term -> window -> window)%}\egroup

\SYNOPSIS
Add a conjecture to a window.

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

\FAILURE
Never fails.

\SEEALSO
add_suppose, ADD_SUPPOSE, add_theorem, ADD_THEOREM, establish

\ENDDOC
\DOC{conjectures}

\TYPE {\small\verb%conjectures : (window -> term list)%}\egroup

\SYNOPSIS
The conjectures of a window.

\DESCRIBE
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.

\SEEALSO
used_conjectures, BAD_CONJECTURES

\ENDDOC
\DOC{context}

\TYPE {\small\verb%context : (window -> term list)%}\egroup

\SYNOPSIS
The context of a window.

\DESCRIBE
{\small\verb%context w%} retuns all the hypotheses, lemmas, and conjectures that
may be assumed in the context of the window {\small\verb%w%}.

\FAILURE
Never fails.

\SEEALSO
all_hypotheses, lemmas, conjectures

\ENDDOC
\DOC{CONVERT\_WIN}

\TYPE {\small\verb%CONVERT_WIN :  (conv -> void)%}\egroup

\SYNOPSIS
Apply a conversion to the focus of the top window.

\DESCRIBE
If the focus of the top window is {\small\verb%"f"%}, and applying a conversion {\small\verb%c%} to
{\small\verb%"f"%} yields the theorem {\small\verb%(|- f = f')%}, then {\small\verb%CONVERT_WIN c%} transforms the
focus of the top window from {\small\verb%"f"%} to {\small\verb%"f'"%}.

\FAILURE
{\small\verb%CONVERT_WIN c%} if the window stack is empty.

\noindent {\small\verb%CONVERT_WIN c%} will fail if the hypotheses of the theorem
returned when {\small\verb%c%} is applied to the focus of the top window are not a subset
of the context of the window.

\SEEALSO
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

\ENDDOC
\DOC{convert\_win}

\TYPE {\small\verb%convert_win :  (conv -> window -> window)%}\egroup

\SYNOPSIS
Apply a conversion to the focus of a window.

\DESCRIBE
If the focus of the window, {\small\verb%win%}, is {\small\verb%"f"%}, and applying a conversion {\small\verb%c%} to
{\small\verb%"f"%} yields {\small\verb%(|- f = f')%}, then {\small\verb%CONVERT_WIN c win%} transforms the
focus of {\small\verb%win%} from {\small\verb%"f"%} to {\small\verb%"f'"%}.

\FAILURE
{\small\verb%convert_win c win%} will fail if the hypotheses of the theorem returned when
{\small\verb%c%} is applied to the focus of the window are not a subset of the
context of {\small\verb%win%}.

\SEEALSO
transform_win, TRANSFORM_WIN, CONVERT_WIN, 
rewrite_win, REWRITE_WIN

\ENDDOC
\DOC{create\_win}

\TYPE {\small\verb%create_win : (term -> term list -> thm list -> window)%}\egroup

\SYNOPSIS
Create a window.

\DESCRIBE
{\small\verb%create_win "r f" hyps thms%} creates a window with:
focus {\small\verb%"f"%}, relation {\small\verb%"r"%}, hypotheses {\small\verb%hyps%} and relevant theorems {\small\verb%thms%}.

\FAILURE
Never fails.

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

\SEEALSO
transform, BEGIN_STACK

\ENDDOC
\DOC{CURRENT\_NAME}

\TYPE {\small\verb%CURRENT_NAME : (void -> string)%}\egroup

\SYNOPSIS
Returns the name of the current window stack.

\FAILURE
Fails if there is no current window stack.

\SEEALSO
create_win, BEGIN_STACK, END_STACK, SET_STACK, ALL_STACKS

\ENDDOC
\DOC{dest\_pmi}

\TYPE {\small\verb%dest_pmi : (term -> (term # term))%}\egroup

\SYNOPSIS
Breaks apart a backward implication into antecedent and consequent.

\DESCRIBE
{\small\verb%dest_pmi%} is a term destructor for backward negations.
{\small\verb%dest_pmi "t1 <== t2"%} returns {\small\verb%("t1","t2")%}.

\COMMENTS
Unlike {\small\verb%dest_imp%}, {\small\verb%dest_pmi%} does not consider negation to be a special case
of implication.

\FAILURE
Fails if the term is not a backward implication.

\SEEALSO
dest_imp, PMI_DEF.

\ENDDOC
\DOC{all\_hypotheses}

\TYPE {\small\verb%all_hypotheses : (window -> term list)%}\egroup

\SYNOPSIS
The hypotheses of a window - in all their forms.

\DESCRIBE
This is the list of things that may be assumed in the context of a window.
{\small\verb%all_hypotheses%} returns the hypotheses in both the noninteractive and
interactive forms.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #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

\end{verbatim}
}

\FAILURE
Never fails.

\SEEALSO
hyp_thms, hypotheses, disp_hypotheses, context

\ENDDOC
\DOC{empty\_rules}

\TYPE {\small\verb%empty_rules : (void -> void)%}\egroup

\SYNOPSIS
Deletes all window rules from the system's tables.

\DESCRIBE
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 {\small\verb%store_rule%} command.
To reload the default entries in the table you should reload the following
segments of the window library: {\small\verb%basic_close%}, {\small\verb%eq_close%}, {\small\verb%imp_close%} and
{\small\verb%pmi_close%}.

\FAILURE
Never fails.

\SEEALSO
store_rule

\ENDDOC
\DOC{END\_STACK}

\TYPE {\small\verb%END_STACK : (string -> void)%}\egroup

\SYNOPSIS
Destroys a window stack.

\DESCRIBE
{\small\verb%END_STACK `name`%} destroyes the window stack with name {\small\verb%`name`%}.
If {\small\verb%`name`%} is the name of the current stack, then 
{\small\verb%END_STACK `name`%} leaves you with no current stack.

\FAILURE
{\small\verb%END_STACK `name`%} fails if there is no stack called {\small\verb%`name`%}.

\SEEALSO
create_win, BEGIN_STACK, SET_STACK, ALL_STACKS, CURRENT_NAME

\ENDDOC
\DOC{END\_STACK\_TAC}

\TYPE {\small\verb%END_STACK_TAC : (string -> tactic)%}\egroup

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

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

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

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #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
\end{verbatim}
}

\COMMENTS
{\small\verb%END_STACK_TAC%} is for interactive use only.
For noninteractive applications use {\small\verb%open_TAC%}.

\SEEALSO
BEGIN_STACK_TAC, open_TAC

\ENDDOC
\DOC{equiv\_tm}

\TYPE {\small\verb%equiv_tm : term%}\egroup

\SYNOPSIS
The boolean constant "=:bool -> (bool -> bool)".

\SEEALSO
imp_tm, pmi_tm.

\ENDDOC
\DOC{ESTABLISH}

\TYPE {\small\verb%ESTABLISH : (term -> void)%}\egroup

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

\DESCRIBE
{\small\verb%ESTABLISH tm%} pushes a subwindow with focus {\small\verb%tm%} onto the window stack.
If {\small\verb%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 {\small\verb%"==>"%}.
The user should then transform the focus of the subwindow from {\small\verb%tm%} to 
{\small\verb%"T"%}(true).
The subwindow should then be closed making {\small\verb%tm%} a lemma of the parent window.

\FAILURE
{\small\verb%ESTABLISH%} will fail if the window stack is empty.

\noindent Attempts to use {\small\verb%CLOSE_WIN%} on a window
opened by {\small\verb%ESTABLISH%} and whose focus has not been transformed to {\small\verb%"T"%} will
fail.
If the focus can not be proven you can abandon the proof attempt with
{\small\verb%UNDO_WIN%}.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PRINT_WIN ();;
= * f
() : void

#ESTABLISH A \/ ~A;;
==> * A \/ ~A
() : void

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

#CLOSE_WIN ();;
  | A \/ ~A
= * f
() : void
\end{verbatim}
}

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

\ENDDOC
\DOC{establish}

\TYPE {\small\verb%establish : (term -> (window -> window) -> window -> window)%}\egroup

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

\DESCRIBE
{\small\verb%establish tm fn win%} opens a subwindow with focus {\small\verb%tm%}.
If {\small\verb%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 {\small\verb%"==>"%}.
{\small\verb%fn%} is then used to transform the focus of the subwindow from {\small\verb%tm%} to
{\small\verb%"T"%}(true).
The subwindow is then closed and {\small\verb%tm%} becomes a lemma in the parent window.
The parent window with the new lemma is returned as the result.

\FAILURE
{\small\verb%establish tm fn win%} will fail if {\small\verb%fn%} does not transform {\small\verb%tm%} to {\small\verb%"T"%} in
the subwindow.

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

\ENDDOC
\DOC{EXISTS\_PMI}

\TYPE {\small\verb%EXISTS_PMI : (term -> thm -> thm)%}\egroup

\SYNOPSIS
Existentially quantifies the antecedent and consequent of backward implication.

\DESCRIBE
When applied to a variable {\small\verb%x%} and a theorem {\small\verb%A |- t1 <== t2%}, the
inference rule {\small\verb%EXISTS_PMI%} returns the theorem {\small\verb%A |- (?x. t1) <== (?x. t2)%},
provided {\small\verb%x%} is not free in the assumptions.
{\par\samepage\setseps\small
\begin{verbatim}
         A |- t1 <== t2
   --------------------------  EXISTS_IMP "x"   [where x is not free in A]
    A |- (?x.t1) <== (?x.t2)
\end{verbatim}
}
\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.

\SEEALSO
EXISTS_EQ, EXISTS_IMP, PMI_DEF.

\ENDDOC
\DOC{FILTER\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%FILTER_ASM_REWRITE_WIN :  ((term -> bool) -> thm list -> void)%}\egroup

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

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

\FAILURE
Fails if there is no current stack.


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

\SEEALSO
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

\ENDDOC
\DOC{filter\_asm\_rewrite\_win}

\TYPE {\small\verb%filter_asm_rewrite_win : ((term- bool)->thm list->window->window)%}\egroup

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

\DESCRIBE
{\small\verb%filter_asm_rewrite_win p thms%} repeatedly rewrites the focus of a
window with {\small\verb%thms%}, a list of basic rewritings and those theorems in
the context of the window, the conclusions of which satisfy the predicate
{\small\verb%p%}.

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

\SEEALSO
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

\ENDDOC
\DOC{FILTER\_ONCE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%FILTER_ONCE_ASM_REWRITE_WIN :  ((term -> bool) -> thm list -> void)%}\egroup

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

\DESCRIBE
{\small\verb%FILTER_ONCE_ASM_REWRITE_WIN p thms%} rewrites the focus of a
window with {\small\verb%thms%}, those theorems in the context of the window, the
conclusions of which satisfy the predicate {\small\verb%p%}, and a list of basic rewrites.

\FAILURE
{\small\verb%FILTER_ONCE_ASM_REWRITE_WIN p thms%} will fail if the hypotheses of any of
the theorems in {\small\verb%thms%} are not a subset of the conjectures of the window.

\SEEALSO
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

\ENDDOC
\DOC{filter\_once\_asm\_rewrite\_win}

\TYPE {\small\verb%filter_once_asm_rewrite_win:((term->bool)->thm list->window->window)%}\egroup

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

\DESCRIBE
{\small\verb%filter_once_asm_rewrite_win p thms%} rewrites the focus of a
window with {\small\verb%thms%}, those theorems in the context of the window, the
conclusions of which satisfy the predicate {\small\verb%p%}, and a list of basic rewrites.

\FAILURE
{\small\verb%filter_once_asm_rewrite_win p thms%} will fail if the hypotheses of any of
the theorems in {\small\verb%thms%} are not a subset of the conjectures of the window.

\SEEALSO
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

\ENDDOC
\DOC{FILTER\_PURE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%FILTER_PURE_ASM_REWRITE_WIN : ((term -> bool) -> thm list -> void)%}\egroup

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

\DESCRIBE
{\small\verb%FILTER_PURE_ASM_REWRITE_WIN p thms%} repeatedly rewrites the focus of 
of the top window on the current stack with {\small\verb%thms%} and those theorems in the
context of the window, the conclusions of which satisfy the predicate {\small\verb%p%}.

\FAILURE
Fails if there is not current stack.

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

\SEEALSO
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

\ENDDOC
\DOC{filter\_pure\_asm\_rewrite\_win}

\TYPE {\small\verb%filter_pure_asm_rewrite_win:((term->bool)->thm list->window->window)%}\egroup

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

\DESCRIBE
{\small\verb%filter_pure_asm_rewrite_win p thms%} repeatedly rewrites the focus of a
window with {\small\verb%thms%} and those theorems in the context of the window, the
conclusions of which satisfy the predicate {\small\verb%p%}.

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

\SEEALSO
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

\ENDDOC
\DOC{FILTER\_PURE\_ONCE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%FILTER_PURE_ONCE_ASM_REWRITE_WIN : ((term -> bool) -> thm list -> void)%}\egroup

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

\DESCRIBE
{\small\verb%FILTER_PURE_ONCE_ASM_REWRITE_WIN p thms%} rewrites the focus of the top
window of the current stack with {\small\verb%thms%} and those theorems in the context of
the window, the conclusions of which satisfy the predicate {\small\verb%p%}.

\FAILURE
Fails if there is no current stack.

{\small\verb%FILTER_PURE_ONCE_ASM_REWRITE_WIN p thms%} will fail if the hypotheses of
any of the theorems in {\small\verb%thms%} are not a subset of the conjectures of the window.

\SEEALSO
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

\ENDDOC
\DOC{filter\_pure\_once\_asm\_rewrite\_win}

\TYPE {\small\verb%filter_pure_once_asm_rewrite_win:(term->bool)->thm list->window->window%}\egroup

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

\DESCRIBE
{\small\verb%filter_pure_once_asm_rewrite_win p thms%} rewrites the focus of a
window with {\small\verb%thms%} and those theorems in the context of the window, the
conclusions of which satisfy the predicate {\small\verb%p%}.

\FAILURE
{\small\verb%filter_pure_once_asm_rewrite_win p thms%} will fail if the hypotheses of
any of the theorems in {\small\verb%thms%} are not a subset of the conjectures of the window.

\SEEALSO
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

\ENDDOC
\DOC{FOCUS}

\TYPE {\small\verb%FOCUS : (void -> term)%}\egroup

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

\FAILURE
Fails if there is no current window stack.

\SEEALSO
focus

\ENDDOC
\DOC{focus}

\TYPE {\small\verb%focus : (window -> term)%}\egroup

\SYNOPSIS
The focus of a window.

\FAILURE

\SEEALSO
FOCUS

\ENDDOC
\DOC{FOC\_RULE\_WIN}

\TYPE {\small\verb%FOC_RULE_WIN :  ((term -> thm) -> void)%}\egroup

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

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
   ------------- RULE "f"
    H |- f' R f
\end{verbatim}
}
\noindent {\small\verb%FOC_RULE_WIN RULE%} can be used to transform the focus of the top
window from {\small\verb%f%} to {\small\verb%f'%}, providing the window is supposed to preserve {\small\verb%"R"%} or
some weaker relation.

\FAILURE
{\small\verb%RULE_WIN r%} will fail if there is no current window stack or if
the assumpitions of the theorem generated by {\small\verb%r%} are not ab subset of the
context of the top window.

\noindent {\small\verb%RULE_WIN r%} will fail if the top window is not supposed to
preserve some relation which is equal to or weaker than {\small\verb%"R%}.

\SEEALSO
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

\ENDDOC
\DOC{foc\_rule\_win}

\TYPE {\small\verb%foc_rule_win :  ((term -> thm) -> window -> window)%}\egroup

\SYNOPSIS
Apply an inference rule to the focus of a window.

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
   ------------- RULE "f"
    H |- f' R f
\end{verbatim}
}
\noindent {\small\verb%foc_rule_win RULE%} can be used to transform the focus of a window
from {\small\verb%f%} to {\small\verb%f'%}, providing the window is supposed to preserve {\small\verb%"R"%} or
some weaker relation.

\COMMENTS
The actual type displayed by the system is ":(conv -> window -> window)".

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

\SEEALSO
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.

\ENDDOC
\DOC{GEN\_OPEN\_WIN}

\TYPE {\small\verb%GEN_OPEN_WIN : (win_path -> void)%}\egroup

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

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

\SEEALSO
GEN_OPEN_WIN, open_win, open_context, OPEN_WIN, OPEN_CONTEXT,
CLOSE_WIN

\ENDDOC
\DOC{gen\_open\_win}

\TYPE {\small\verb%gen_open_win : (win_path -> (window -> window) -> window -> window)%}\egroup

\SYNOPSIS
Apply some transformation to a subwindow of a window.

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

\SEEALSO
GEN_OPEN_WIN, open_win, open_context, OPEN_WIN, OPEN_CONTEXT,
CLOSE_WIN

\ENDDOC
\DOC{GEN\_REWRITE\_WIN}

\TYPE {\small\verb%gen_rewrite_win : ((conv -> conv) -> thm list -> thm list -> void)%}\egroup

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

\DESCRIBE
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 {\small\verb%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 {\small\verb%"~t"%} are transformed into the corresponding
equations {\small\verb%"t = F"%}. Theorems {\small\verb%"t"%} which are not equations are cast as
equations of form {\small\verb%"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
{\small\verb%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, {\small\verb%rewrite_win%} could be implemented as
{\par\samepage\setseps\small
\begin{verbatim}
    gen_rewrite_win TOP_DEPTH_CONV basic_rewrites
\end{verbatim}
}
\noindent which specifies that matches should be searched recursively
starting from the whole term of the theorem, and {\small\verb%basic_rewrites%} must
be added to the user defined set of theorems employed in rewriting.

\SEEALSO
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

\ENDDOC
\DOC{gen\_rewrite\_win}

\TYPE {\small\verb%gen_rewrite_win:((conv->conv)->thm list->thmlist->window->window)%}\egroup

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

\DESCRIBE
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 {\small\verb%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 {\small\verb%"~t"%} are transformed into the corresponding
equations {\small\verb%"t = F"%}. Theorems {\small\verb%"t"%} which are not equations are cast as
equations of form {\small\verb%"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
{\small\verb%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, {\small\verb%rewrite_win%} could be implemented as
{\par\samepage\setseps\small
\begin{verbatim}
    gen_rewrite_win TOP_DEPTH_CONV basic_rewrites
\end{verbatim}
}
\noindent which specifies that matches should be searched recursively
starting from the whole term of the theorem, and {\small\verb%basic_rewrites%} must
be added to the user defined set of theorems employed in rewriting.

\SEEALSO
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 

\ENDDOC
\DOC{GET\_MAX\_HIST}

\TYPE {\small\verb%GET_MAX_HIST: (void -> int)%}\egroup

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

\FAILURE

\SEEALSO
UNDO, REDO, SET_MAX_HIST

\ENDDOC
\DOC{hypotheses}

\TYPE {\small\verb%hypotheses : (window -> term list)%}\egroup

\SYNOPSIS
The set of hypotheses of a window.

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

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #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
\end{verbatim}
}

\FAILURE
Never fails.

\SEEALSO
hyp_thms, disp_hypotheses, all_hypotheses, context

\ENDDOC
\DOC{hyp\_thms}

\TYPE {\small\verb%hyp_thms : (window -> thm list)%}\egroup

\SYNOPSIS
The theorems infered from the context of a window.

\DESCRIBE
{\small\verb%hyp_thms w%} is the list of theorems which are infered from the context
of {\small\verb%w%}.  The conclusions of these theorems are the hypotheses of the window.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #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
\end{verbatim}
}

\FAILURE
Never fails.

\SEEALSO
hypotheses, disp_hypotheses, all_hypothese

\ENDDOC
\DOC{IMP\_PMI}

\TYPE {\small\verb%IMP_PMI : (thm -> thm)%}\egroup

\SYNOPSIS
Changes a forward implication into a backward implication.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
 H |- t ==> u
--------------  IMP_PMI
 H |- u <== t
\end{verbatim}
}
\FAILURE
{\small\verb%IMP_PMI%} will fail if its argument is not an implication.


\SEEALSO
PMI_IMP, PMI_DEF

\ENDDOC
\DOC{IMP\_PMI\_CONV}

\TYPE {\small\verb%IMP_PMI_CONV : (term -> thm)%}\egroup

\SYNOPSIS
Changes a forward implication into a backward implication.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#IMP_PMI_CONV "A ==> B";;
|- (A ==> B) = (B <== A)
\end{verbatim}
}
\FAILURE
{\small\verb%IMP_PMI_CONV%} will fail if its argument is not an implication.


\SEEALSO
PMI_IMP, IMP_PMI, PMI_IMP_CONV, PMI_DEF

\ENDDOC
\DOC{IMP\_REFL}

\TYPE {\small\verb%IMP_REFL : conv%}\egroup

\SYNOPSIS
Returns a theorem expressing the reflexivity of implication.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
------------ IMP_REFL "t"
 |- t ==> t
\end{verbatim}
}

\SEEALSO
REFL, PMI_REFL

\ENDDOC
\DOC{imp\_tm}

\TYPE {\small\verb%imp_tm : term%}\egroup

\SYNOPSIS
The boolean constant "==>".

\SEEALSO
equiv_tm, pmi_tm.

\ENDDOC
\DOC{is\_pmi}

\TYPE {\small\verb%is_pmi : (term -> bool)%}\egroup

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

\DESCRIBE
{\small\verb%is_pmi "t1 <== t2"%} returns {\small\verb%true%}.
If the argument is not a backward implication it returns {\small\verb%false%}.

\COMMENTS
Unlike {\small\verb%is_imp%}, {\small\verb%is_pmi%} does not consider negation to be a special case
of implication.

\FAILURE
Never fails.

\SEEALSO
is_imp, PMI_DEF

\ENDDOC
\DOC{is\_trueimp}

\TYPE {\small\verb%is_trueimp : (term -> bool)%}\egroup

\SYNOPSIS
Tests a term to see if it is an implication.

\DESCRIBE
{\small\verb%is_trueimp "t1 ==> t2"%} returns {\small\verb%true%}.
If the argument is not an implication it returns {\small\verb%false%}.

\FAILURE
Never fails.

\SEEALSO
is_imp, is_pmi

\ENDDOC
\DOC{lemmas}

\TYPE {\small\verb%lemmas : (window -> term list)%}\egroup

\SYNOPSIS
The lemmas of a window.

\DESCRIBE
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.

\SEEALSO
theorems

\ENDDOC
\DOC{LEMMA\_THMS}

\TYPE {\small\verb%LEMMA_THMS : (void -> thm list)%}\egroup

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

\FAILURE
Fails if there is not current window stack.

\SEEALSO
lemma_thms

\ENDDOC
\DOC{lemma\_thms}

\TYPE {\small\verb%lemma_thms : (window -> thm list)%}\egroup

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

\FAILURE
Never fails.

\SEEALSO
LEMMA_THMS, lemmas

\ENDDOC
\DOC{load\_window}

\TYPE {\small\verb%load_window : (void -> void)%}\egroup

\SYNOPSIS
Finishes loading the window library.

\DESCRIBE

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

\COMMENTS
The function {\small\verb%load_window%} is only defined if the initial attempt to load
the window library did not succeed.

\FAILURE
Fails if the theory {\small\verb%win%} is not the parent theory
and the system is not in draft mode.

\SEEALSO

\ENDDOC
\DOC{MATCH\_TRANSFORM\_WIN}

\TYPE {\small\verb%MATCH_TRANSFORM_WIN : (thm -> void)%}\egroup

\SYNOPSIS
Transform the focus of the current window.

\DESCRIBE
{\small\verb%MATCH_TRANSFORM_WIN (H |- !x1...xn. g R f)%} specialises the quantified
variables {\small\verb%x1%} ... {\small\verb%xn%} and then instantiates the free variables so that
{\small\verb%f%} matches the focus of the current window.   The focus is then transformed to
{\small\verb%g%} (with the same substitutions applied).

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

\SEEALSO
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

\ENDDOC
\DOC{match\_transform\_win}

\TYPE {\small\verb%match_transform_win : (thm -> window -> window)%}\egroup

\SYNOPSIS
Transform the focus of a window.

\DESCRIBE
{\small\verb%match_transform_win (H |- !x1...xn. g R f)%} specialises the quantified
variables {\small\verb%x1%} ... {\small\verb%xn%} and then instantiates the free variables so that
{\small\verb%f%} matches the focus of window.   The focus is then transformed to
{\small\verb%g%} (with the same substitutions applied).

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

\SEEALSO
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

\ENDDOC
\DOC{ONCE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%ONCE_ASM_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%ONCE_ASM_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{once\_asm\_rewrite\_win}

\TYPE {\small\verb%once_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%once_asm_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{ONCE\_REWRITE\_WIN}

\TYPE {\small\verb%ONCE_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%ONCE_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{once\_rewrite\_win}

\TYPE {\small\verb%once_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%once_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{OPEN\_CONTEXT}

\TYPE {\small\verb%OPEN_CONTEXT : (term -> path -> void)%}\egroup

\SYNOPSIS
Open a subwindow for deriving new lemmas.

\DESCRIBE
{\small\verb%OPEN_CONTEXT tm path%} opens a subwindow on the
assumption, lemma or conjecture {\small\verb%tm%} at the position described by {\small\verb%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 {\small\verb%tm%} to {\small\verb%tm'%} generating the
theorem {\small\verb%(..|- tm' <== tm)%}.
When the subwindow is closed {\small\verb%tm'%} becomes a new lemma in the parent window.

\FAILURE
{\small\verb%OPEN_CONTEXT tm path%} will fail if the window stack is empty.

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

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#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
\end{verbatim}
}

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

\ENDDOC
\DOC{open\_context}

\TYPE {\small\verb%open_context : (term -> path -> (window -> window) -> window -> window)%}\egroup

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

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

\FAILURE
{\small\verb%open_context tm path fn win%} will fail if {\small\verb%tm%} is not an assumption, lemma
or conjecture of {\small\verb%win%}.
{\small\verb%open_context tm path fn win%} will fail if {\small\verb%path%} describes a position which
is not present in {\small\verb%tm%}.

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

\ENDDOC
\DOC{open\_TAC}

\TYPE {\small\verb%open_TAC : (path -> thm list -> (window -> window) -> tactic)%}\egroup

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

\DESCRIBE
{\small\verb%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, {\small\verb%goal%}, selected by {\small\verb%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 {\small\verb%thms%} as it's set of relevant theorems.
The relation preserved by the subwindow is chosen so that transforming the
subwindow, with {\small\verb%fn%}, transforms {\small\verb%goal%} to {\small\verb%goal'%}, generating the theorem
{\small\verb%(H |- goal' ==> goal')%}.
The subwindow is then closed and the goal is transformed from {\small\verb%goal%} to
{\small\verb%goal'%}.

\FAILURE
{\small\verb%open_TAC path thms fn%} will fail if the goal stack is empty or if
{\small\verb%path%} denotes a position which is not present in the current goal.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #set_goal ([], "A \/ (B \/ F)");;
   "A \/ B \/ F"
   
   () : void
   
   #e (open_TAC [RAND] [] (rewrite_win []));;
   OK..
   "A \/ B"
   
   () : void
\end{verbatim}
}

\SEEALSO
BEGIN_STACK_TAC, END_STACK_TAC

\ENDDOC
\DOC{OPEN\_WIN}

\TYPE {\small\verb%OPEN_WIN : (path -> void)%}\egroup

\SYNOPSIS
Open a subwindow on the focus of the top window.

\DESCRIBE
{\small\verb%OPEN_WIN path%} opens a subwindow in the focus of the top window at the
position described by {\small\verb%path%}.
The subwindow is then pushed onto the top of the window stack.

\FAILURE
{\small\verb%OPEN_WIN path%} will fail if the window stack is empty.

\noindent {\small\verb%OPEN_WIN path%} will fail if {\small\verb%path%} describes a position which
is not present in the focus of the top window.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#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
\end{verbatim}
}

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

\ENDDOC
\DOC{open\_win}

\TYPE {\small\verb%open_win : (path -> (window -> window) -> window -> window)%}\egroup

\SYNOPSIS
Apply some transformation to a subwindow of a window.

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

\FAILURE
{\small\verb%open_win path fn win%} will fail if {\small\verb%path%} describes a position which
is not present in the focus of {\small\verb%win%}.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   # transform "(==>) (A /\ (B /\ F))" [] []
   # (
   #       open_win [RAND]
   #       (
   #               rewrite_win []
   #       )
   # );;
   |- A /\ F ==> A /\ B /\ F
\end{verbatim}
}

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

\ENDDOC
\DOC{origin}

\TYPE {\small\verb%origin : (window -> term)%}\egroup

\SYNOPSIS
The original focus of a window.

\FAILURE
Never fails.

\ENDDOC
\DOC{PMI\_IMP}

\TYPE {\small\verb%PMI_IMP : (thm -> thm)%}\egroup

\SYNOPSIS
Changes a backward implication into a forward implication.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
 H |- u <== t
--------------  PMI_IMP
 H |- t ==> u
\end{verbatim}
}
\FAILURE
{\small\verb%PMI_IMP%} will fail if its argument is not a backward implication.

\SEEALSO
IMP_PMI, PMI_DEF

\ENDDOC
\DOC{PMI\_IMP\_CONV}

\TYPE {\small\verb%PMI_IMP_CONV : (term -> thm)%}\egroup

\SYNOPSIS
Changes a backward implication into a forward implication.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
#PMI_IMP_CONV "A ==> B";;
|- (A ==> B) = (B <== A)
\end{verbatim}
}
\FAILURE
{\small\verb%IMP_PMI_CONV%} will fail if its argument is not a backward implication.


\SEEALSO
PMI_IMP, IMP_PMI, IMP_PMI_CONV, PMI_DEF

\ENDDOC
\DOC{PMI\_REFL}

\TYPE {\small\verb%PMI_REFL : conv%}\egroup

\SYNOPSIS
Returns a theorem expressing the reflexivity of backward implication.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
------------ PMI_REFL "t"
 |- t <== t
\end{verbatim}
}

\SEEALSO
REFL, IMP_REFL, PMI_DEF

\ENDDOC
\DOC{pmi\_tm}

\TYPE {\small\verb%pmi_tm : term%}\egroup

\SYNOPSIS
The boolean constant "<==".

\SEEALSO
equiv_tm, imp_tm.

\ENDDOC
\DOC{PMI\_TRANS}

\TYPE {\small\verb%PMI_TRANS : (thm -> thm -> thm)%}\egroup

\SYNOPSIS
Implements the transitivity of backward implication.

\DESCRIBE
{\par\samepage\setseps\small
\begin{verbatim}
 A1 |- t1 <== t2  A2 |- t2 <== t3
---------------------------------- PMI_TRANS
       A1 u A2 |- t1 <== t3
\end{verbatim}
}
\SEEALSO
TRANS, IMP_TRANS, PMI_DEF

\ENDDOC
\DOC{PRINT\_STACK}

\TYPE {\small\verb%PRINT_WIN : (void -> void)%}\egroup

\SYNOPSIS
Print out the top window of the current window stack.

\DESCRIBE
{\small\verb%PRINT_STACK%} will print out the top window on the stack according to the
following format.
{\par\samepage\setseps\small
\begin{verbatim}
     ! "a"
     | "l"
     ? "c"
     $ "u"
     @ "b"
   R * "f"
\end{verbatim}
}
That is, {\small\verb%PRINT_STACK%} prints the context of the window followed by
{\small\verb%R * "f"%} where {\small\verb%R%} is the relation that the window is supposed to
preserve, and {\small\verb%"f"%} is the focus of the window.
Each element in the context is preceded by some prefix.
The prefix {\small\verb%!%} denotes an assumption.
The prefix {\small\verb%|%} denotes a lemma.
The prefix {\small\verb%?%} denotes a conjecture.
The prefix {\small\verb%$%} denotes a used conjecture.
The prefix {\small\verb%@%} denotes a bad conjecture.

\FAILURE
{\small\verb%PRINT_STACK ()%} will fail if there is no current window stack.

\ENDDOC
\DOC{PURE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%PURE_ASM_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%PURE_ASM_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%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.

\SEEALSO
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

\ENDDOC
\DOC{pure\_asm\_rewrite\_win}

\TYPE {\small\verb%pure_asm_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%pure_asm_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%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.

\SEEALSO
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

\ENDDOC
\DOC{PURE\_ONCE\_ASM\_REWRITE\_WIN}

\TYPE {\small\verb%PURE_ONCE_ASM_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%PURE_ONCE_ASM_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{pure\_once\_asm\_rewrite\_win}

\TYPE {\small\verb%pure_once_asm_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%pure_once_asm_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{PURE\_ONCE\_REWRITE\_WIN}

\TYPE {\small\verb%PURE_ONCE_REWRITE_WIN :  (thm list -> void)%}\egroup

\SYNOPSIS
Rewrite the top focus once with a list of theorems.

\FAILURE
{\small\verb%PURE_ONCE_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{pure\_once\_rewrite\_win}

\TYPE {\small\verb%pure_once_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%pure_once_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.

\SEEALSO
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

\ENDDOC
\DOC{PURE\_REWRITE\_WIN}

\TYPE {\small\verb%PURE_REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%PURE_REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%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.

\SEEALSO
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

\ENDDOC
\DOC{pure\_rewrite\_win}

\TYPE {\small\verb%pure_rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%pure_rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%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.

\SEEALSO
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

\ENDDOC
\DOC{REDO}

\TYPE {\small\verb%REDO: (void -> void)%}\egroup

\SYNOPSIS
Redoes the last change that was undone.

\DESCRIBE
Redoes the last change that was undone from the current stack.
Several {\small\verb%REDO%}s can undo the effect of several {\small\verb%UNDO%}s.
It is not possible to {\small\verb%REDO%} more {\small\verb%UNDO%}s than are stored in the stacks
history.   To find out how many states can be stored in a stack, use the
{\small\verb%GET_MAX_HIST%} command.

\FAILURE
{\small\verb%REDO ()%} will fail if nothing has been undone, or if some other
change has been made to the stack since the last {\small\verb%UNDO%}.

\SEEALSO
UNDO, SET_MAX_HIST, GET_MAX_HIST

\ENDDOC
\DOC{relation}

\TYPE {\small\verb%relation : (window -> term)%}\egroup

\SYNOPSIS
The relation preserved by a window.

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

\FAILURE
Never fails.

\ENDDOC
\DOC{REWRITE\_WIN}

\TYPE {\small\verb%REWRITE_WIN :  (thm list -> void)%}\egroup

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

\FAILURE
{\small\verb%REWRITE_WIN thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
context of the window.
This function may fail to terminate if {\small\verb%thms%} describe a circular rewriting.

\SEEALSO
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

\ENDDOC
\DOC{rewrite\_win}

\TYPE {\small\verb%rewrite_win :  (thm list -> window -> window)%}\egroup

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

\FAILURE
{\small\verb%rewrite_win thms%} will fail if the
hypotheses of any of the theorems in {\small\verb%thms%} are not a subset of the
conjectures of the window.
This function may fail to terminate if {\small\verb%thms%} describe a circular rewriting.

\SEEALSO
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

\ENDDOC
\DOC{RULE\_WIN}

\TYPE {\small\verb%RULE_WIN :  ((thm -> thm) -> void)%}\egroup

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

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
    H |- c
   -------- RULE
    H |- c'
\end{verbatim}
}
\noindent {\small\verb%RULE_WIN RULE%} can be used to transform the focus of the top
window from {\small\verb%c%} to {\small\verb%c'%}, providing the window is supposed to preserve {\small\verb%"<=="%} or
some weaker relation.

\FAILURE
{\small\verb%RULE_WIN r%} will fail if the window stack is empty.

\noindent {\small\verb%RULE_WIN r%} will fail if the top window is not supposed to
preserve some relation which is equal to or weaker than {\small\verb%"<=="%}.

\SEEALSO
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

\ENDDOC
\DOC{rule\_win}

\TYPE {\small\verb%rule_win :  ((thm -> thm) -> window -> window)%}\egroup

\SYNOPSIS
Apply an inference rule to the focus of a window.

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
    H |- c
   -------- RULE
    H |- c'
\end{verbatim}
}
\noindent {\small\verb%rule_win RULE%} can be used to transform the focus of a window
from {\small\verb%c%} to {\small\verb%c'%}, providing the window is supposed to preserve {\small\verb%"<=="%} or
some weaker relation.

\FAILURE
{\small\verb%rule_win r%} will fail if the window is not supposed to preserve some
relation which is equal to or weaker than {\small\verb%"<=="%}.

\SEEALSO
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.

\ENDDOC
\DOC{SAVE\_WIN\_THM}

\TYPE {\small\verb%SAVE_WIN_THM : (void -> thm)%}\egroup

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

\DESCRIBE

The call {\small\verb%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.

\SEEALSO
WIN_THM, save_thm

\ENDDOC
\DOC{SET\_MAX\_HIST}

\TYPE {\small\verb%SET_MAX_HIST: (int -> void)%}\egroup

\SYNOPSIS
Sets the maximum history size of all the window stacks.

\FAILURE
Fails if given a history size less than 1.

\SEEALSO
UNDO, REDO, GET_MAX_HIST

\ENDDOC
\DOC{SET\_STACK}

\TYPE {\small\verb%SET_STACK : (string -> void)%}\egroup

\SYNOPSIS
Sets the current stack.

\DESCRIBE
{\small\verb%SET_STACK `name`%} sets the current stack to the one called {\small\verb%`name`%}.

\FAILURE
{\small\verb%SET_STACK `name`%} fails if there is no stack called {\small\verb%`name`%}.

\SEEALSO
create_win, BEGIN_STACK, END_STACK, ALL_STACKS, CURRENT_NAME

\ENDDOC
\DOC{SMASH}

\TYPE {\small\verb%SMASH : (thm -> thm list)%}\egroup

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

\DESCRIBE
The operation of {\small\verb%SMASH%} is similar to that of {\small\verb%CONJUNCTS%} except that
it does not just break apart conjunctions.
{\small\verb%SMASH%} recursively applies the following inference rules to a theorem
to smash it into a list of smaller theorems.
{\par\samepage\setseps\small
\begin{verbatim}
       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
\end{verbatim}
}

\FAILURE
Never Fails.

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

\SEEALSO
CONJUNCTS.

\ENDDOC
\DOC{store\_rule}

\TYPE {\small\verb%store_rule : (window_rule -> void)%}\egroup

\SYNOPSIS
Adds a window rule to the window system's tables.

\DESCRIBE
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.

\SEEALSO
empty_rules

\ENDDOC
\DOC{suppositions}

\TYPE {\small\verb%suppositions : (window -> goal list)%}\egroup

\SYNOPSIS
The suppositions of a window.

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

\FAILURE
Never fails.

\SEEALSO
conjectures

\ENDDOC
\DOC{TACTIC\_WIN}

\TYPE {\small\verb%TACTIC_WIN :  (tactic -> void)%}\egroup

\SYNOPSIS
Apply a tactic to the focus of the top window.

\DESCRIBE
Assuming {\small\verb%TAC%} is a tactic of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
    H |- c
   ======== TAC
    H |- c'
\end{verbatim}
}
\noindent {\small\verb%TACTIC_WIN TAC%} can be used to transform the focus of the top
window from {\small\verb%c%} to {\small\verb%c'%}, providing the window is supposed to preserve {\small\verb%"==>"%} or
some weaker relation.

\FAILURE
{\small\verb%TACTIC_WIN t%} will fail if there is no current stack.

\noindent {\small\verb%TACTIC_WIN t%} will fail if the top window is not supposed to
preserve some relation which is equal to or weaker than {\small\verb%"<=="%}.

\noindent {\small\verb%RULE_WIN t%} will fail if the application ot {\small\verb%t%} generates more
then one subgoal.

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

\ENDDOC
\DOC{tactic\_win}

\TYPE {\small\verb%tactic_win :  (tactic -> window -> window)%}\egroup

\SYNOPSIS
Apply a tactic to the focus of a window.

\DESCRIBE
Assuming {\small\verb%TAC%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
    P |- c
   ======== TAC
    P |- c'
\end{verbatim}
}
\noindent {\small\verb%tactic_win TAC%} can be used to transform the focus of a window
from {\small\verb%c%} to {\small\verb%c'%}, providing the window is supposed to preserve {\small\verb%"==>"%} or
some weaker relation.

\FAILURE
{\small\verb%tactic_win t%} will fail if the window is not supposed to preserve some
relation which is equal to or weaker than {\small\verb%"==>"%} or if the
tactic produces multiple subgoals.

\SEEALSO
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

\ENDDOC
\DOC{THM\_RULE\_WIN}

\TYPE {\small\verb%THM_RULE_WIN :  ((thm -> thm) -> void)%}\egroup

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

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
      H |- fn R f
    ---------------- RULE
     H' |- fn' R' f
\end{verbatim}
}
If the top window of the current stack holds the theorem {\small\verb%H |- fn R f%},
it will transform the window to one which holds the theorem {\small\verb%H' |- fn' R' f%};
provided that {\small\verb%H'%} is a subset of the context of the window and {\small\verb%R'%} is as
strong as {\small\verb%R%}.
This will transform the focus of the top window of the stack from {\small\verb%fn%} to {\small\verb%fn'%}.

\FAILURE
{\small\verb%THM_RULE_WIN r%} if {\small\verb%r (WIN_THM ())%} is not of the form {\small\verb%H' |- fn' R' f%}
(note that this requires that {\small\verb%r%} does not change {\small\verb%f%});
or if {\small\verb%H'%} is not a subset of the context of the window, or {\small\verb%R'%} is not as
strong as {\small\verb%R%}.

\SEEALSO
thm_rule_win, rule_win, RULE_WIN, foc_rule_win, FOC_RULE_WIN, WIN_THM

\ENDDOC
\DOC{thm\_rule\_win}

\TYPE {\small\verb%thm_rule_win :  ((thm -> thm) -> window -> window)%}\egroup

\SYNOPSIS
Apply an inference rule to the result of a window.

\DESCRIBE
Assuming {\small\verb%RULE%} is an inference rule of the following form:
{\par\samepage\setseps\small
\begin{verbatim}
      H |- fn R f
    ---------------- RULE
     H' |- fn' R' f
\end{verbatim}
}
Then if {\small\verb%(thm_rule_win RULE)%} is applied to a window holding the 
theorem {\small\verb%H |- fn R f%}, it will transform the window to one which holds the
theorem {\small\verb%H' |- fn' R' f%}, provided that {\small\verb%H'%} is a subset of the context
of the window and {\small\verb%R'%} is as strong as {\small\verb%R%}.
This will effectively transform the focus from {\small\verb%fn%} to {\small\verb%fn'%}.

\FAILURE
{\small\verb%thm_rule_win r w%} if {\small\verb%r (win_thm w)%} is not of the form {\small\verb%H' |- fn' R' f%}
(note that this requires that {\small\verb%r%} does not change {\small\verb%f%});
or if {\small\verb%H'%} is not a subset of the context of the window, or {\small\verb%R'%} is not as
strong as {\small\verb%R%}.

\SEEALSO
THM_RULE_WIN, rule_win, RULE_WIN, foc_rule_win, FOC_RULE_WIN, win_thm

\ENDDOC
\DOC{TOP\_WIN}

\TYPE {\small\verb%TOP_WIN :  (void -> window)%}\egroup

\SYNOPSIS
Return the window on top of the window stack.

\FAILURE

\ENDDOC
\DOC{transform}

\TYPE {\small\verb%transform : (term -> term list -> thm list -> (window -> window) -> thm)%}\egroup

\SYNOPSIS
Create and transform a window and return the theorem generated.

\DESCRIBE
{\small\verb%transform "r f" hyps thms fn%} creates a window with:
focus {\small\verb%"f"%}, relation {\small\verb%"r"%}, hypotheses {\small\verb%hyps%}, relevant theorems {\small\verb%thms%}.
The function {\small\verb%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
{\par\samepage\setseps\small
\begin{verbatim}
#transform "(==>) (A /\ T)" [] [] (rewrite_win []);;
|- A ==> A /\ T
\end{verbatim}
}

\SEEALSO
create_win

\ENDDOC
\DOC{TRANSFORM\_WIN}

\TYPE {\small\verb%TRANSFORM_WIN : (thm -> void)%}\egroup

\SYNOPSIS
Transform the focus of the top window.

\DESCRIBE
{\small\verb%TRANSFORM_WIN (H |- F' R F)%} is used to transform the focus of the
window on top of the window stack from {\small\verb%F%} to {\small\verb%F'%}.

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

\SEEALSO
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

\ENDDOC
\DOC{transform\_win}

\TYPE {\small\verb%transform_win : (thm -> window -> window)%}\egroup

\SYNOPSIS
Transform the focus of a window.

\DESCRIBE
{\small\verb%transform_win (H |- f' R f)%} transforms the focus of a window
from {\small\verb%f%} to {\small\verb%f'%}.

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

\SEEALSO
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

\ENDDOC
\DOC{traverse}

\TYPE {\small\verb%traverse : (path -> term -> term)%}\egroup

\SYNOPSIS
Use a path to select a subterm from a term.

\EXAMPLE
{\par\samepage\setseps\small
\begin{verbatim}
   #traverse [RATOR; RAND] "A /\ B";;
   "A" : term
\end{verbatim}
}

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

\ENDDOC
\DOC{UNDO}

\TYPE {\small\verb%UNDO: (void -> void)%}\egroup

\SYNOPSIS
Undoes the last transformation made to the current window stack.

\DESCRIBE

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

\FAILURE
{\small\verb%UNDO ()%} will fail if no transformations have been made to the stack.

\SEEALSO
UNDO_WIN, REDO, SET_MAX_HIST, GET_MAX_HIST

\ENDDOC
\DOC{UNDO\_WIN}

\TYPE {\small\verb%UNDO_WIN : (void -> void)%}\egroup

\SYNOPSIS
Pops the window stack.

\DESCRIBE
{\small\verb%UNDO_WIN ()%} is used to undo the opening of a subwindow and every
transformation performed on the subwindow.
{\small\verb%UNDO_WIN ()%} will return the user to the unchanged parent window.

\FAILURE
{\small\verb%UNDO_WIN ()%} will fail no windows have been opened on the window stack.

\SEEALSO
UNDO

\ENDDOC
\DOC{used\_conjectures}

\TYPE {\small\verb%used_conjectures : (window -> term list)%}\egroup

\SYNOPSIS
The conjectures used by a window.

\DESCRIBE
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.

\SEEALSO
used_hypotheses, conjectures, BAD_CONJECTURES

\ENDDOC
\DOC{used\_hypotheses}

\TYPE {\small\verb%used_hypotheses : (window -> term list)%}\egroup

\SYNOPSIS
The used hypotheses of a window.

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

\FAILURE
Never fails.

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

\ENDDOC
\DOC{window\_version}

\TYPE {\small\verb%window_version : num%}\egroup

\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.

\SEEALSO

\ENDDOC
\DOC{WIN\_THM}

\TYPE {\small\verb%WIN_THM : (void -> thm)%}\egroup

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

\DESCRIBE
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.

\SEEALSO
result

\ENDDOC
\DOC{win\_thm}

\TYPE {\small\verb%win_thm : (window -> thm)%}\egroup

\SYNOPSIS
The theorem stored in a window.

\DESCRIBE
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.

\SEEALSO
WIN_THM, SAVE_WIN_THM

\ENDDOC