\section{Conclusions; Further Work}

Methods of imitating the capability to rewrite subterms have been presented
for LPF and Display Logic.
Since Display Logic does not have equality of subterms, and 
LPF does not have equality of the possibly undefined terms used,
in neither case does the logic explicitly support such rewrites.
However, in each case, certain features of the logic enable the
effect of a general rewrite capability to be achieved;
tactics have been written to exploit these features of the logics,
to make the ``rewriting'' fairly straightforward for the user.

Of the methods described in this paper, that for Display Logic has
been used extensively, and proved very valuable in facilitating a number
of long proofs.
Examples of these are given in \cite{thesis}.
This was no surprise;
given the prevalence of term rewriting as a proof method, it is 
to be expected that a method achieving the same effect would be valuable.
The method has been adapted to several different display logics.
Recent re-implementation work has made it much easier to implement 
a new display logic in Isabelle, and then the tactics descibed in
\S\ref{dl} will apply automatically.
The tactics are fairly straightforward to use.

In the case of the method for LPF, 
so far as the user is concerned, the tactics are reasonably easy to apply.
However, they have been implemented so far only for classical first-order logic,
and have not yet been used significantly.
Extension to other theories would require further work;
in particular, it would be necessary to derive rules of the form of 
(\ref{rep-cong}) for every monotone operator in the system.
Some other programming (eg adapting the function which  
selects the appropriate rule of the form (\ref{rep-cong}) at every step,
and adapting some functions to handle multiple Isabelle types)
would also be necessary.

Both methods have been implemented so as to permit the user to 
specify the strategy for traversing a term looking for subterms which can be
rewritten, as can be done with HOL conversionals.
So far the ``ordered'' rewriting which Isabelle's rewrite tactics 
use for ``permutative'' rewrite rules (see \cite{Ref}, \S10.4)
has not been implemented;
this potential further work would not be difficult.

Reade (\cite{Reade}, Ch. 10) describes various constructions for domains.
Briefly, a \emph{flat} domain has only the usual elements of the type,
plus an undefined element $\bot$.
Alternatively, a domain can have ``partly undefined'' elements,
such as a tuple $(3,\bot)$.
This means that there would be a choice of ways of extending LPF 
to handle compound types.
Possible further work in this area would include analysing the implications
of such choices on the use of the methods described in \S\ref{lpf}.