\section{Implementation of LPF rewriting in Isabelle} \label{app:LPF-impl}

The implementation of this technique was motivated by the manner in which 
the HOL theorem prover permits the user to specify a strategy for 
navigating through a term and rewriting rewritable subterms where they 
are found.
In HOL, this is done by specifying conversions and conversionals.
A full description of these is in \cite[Chapter~13]{HOLdesc}.
A \emph{conversion} is a function of type \texttt{term -> thm},
which takes a term $t$ to a theorem $t = t'$ (which can be used to  
rewrite $t$ to $t'$).
A \emph{conversional} is a function which acts on or modifies conversions.
For example, if 
$\textit{conv}\ t$ is $t = t'$ (to rewrite $t$ to $t'$), and 
$\textit{conv}'\ t'$ is $t' = t''$ (to rewrite $t'$ to $t''$)
then $(\textit{conv}\ \texttt{THENC}\ \textit{conv}')\ t$ is $t = t''$
(to rewrite $t$ to $t''$).
Another example is the \texttt{REPEATC} conversional, 
which repeatedly applies a conversion until there is no further change
to the term.
These are described in \cite[\S13.1]{HOLdesc}.
The conversional \texttt{SUB\_CONV}
applies a conversion to the immediate subterms of a term.
These conversionals may be used to program various more complex
strategies for rewriting (where possible) subterms of a term,
as described in \cite[\S13.2]{HOLdesc}.
A conversion \textit{conv} that ``fails'', in the sense that 
$\textit{conv}\ t$ finds no $t'$ such that $t = t'$,
can be programmed either to return $t = t$ or to raise an exception,
and there are functions to change one sort of conversion to the other.

Any conversion can be converted to either a forward proof rule or a tactic for
backwards proof by the functions \texttt{CONV\_RULE} and \texttt{CONV\_TAC},
see \cite[\S13.1]{HOLdesc}.
The conversions form the basis of \texttt{REWRITE\_RULE} and 
\texttt{REWRITE\_TAC}, used in forward proof and backward proof respectively.

Implementation of the simulated rewriting technique for LPF relies
heavily on the concepts of the HOL implementation, though the details differ.

In Isabelle, we implemented the axioms and rules of \cite{BCJ}
as a theory.
In addition, we defined a function 
$\texttt{rep} (t,t')$ to mean that $t$ is replaceable by $t'$,
(ie, $ t \sqsubseteq t'$) and we proved,
from the LPF axioms, 
results of the form of
(\ref{rep-cong}) (see \S\ref{LPF-impl})
for each binary propositional operator \textit{op},
and corresponding results for the unary propositional operators.
We also proved the reflexivity and transitivity of \texttt{rep},
and the result (\ref{repD}).

We define a new datatype which provides a way
(other than by using exceptions)
to indicate whether or not a term is unchanged,
$$ \texttt{datatype crep = Unc | Rep of thm ; }$$
A \emph{rep-conversion}, of type \texttt{cterm -> crep},
is given a term \textit{t}
% which is a proposition (without "Trueprop")
and produces a theorem.
In the case of a rep-conversion used for forwards (resp. backwards) proof,
the theorem is $\texttt{rep} (t,t')$ (resp. $\texttt{rep} (t',t)$)
for some $t'$.
This is analogous to a HOL conversion, except
that because \texttt{rep} is a preorder, not an equivalence, 
different rep-conversions are needed for forwards and for backwards proof.
A related function which helps in the implementation 
(in particular, it makes composition straightforward) is
a \emph{rep-transformation}, of type \texttt{thm -> crep};
a {rep-transformation} takes a theorem
$\texttt{rep} (s,t)$ and transforms it to
the theorem $\texttt{rep} (s,t')$ (for forwards proof)
or $\texttt{rep} (s',t)$ (for backwards proof).
It does this by discovering the theorem 
$\texttt{rep} (t,t')$ or $\texttt{rep} (s',s)$
% for forwards or backwards proof
respectively,
and using the transitivity of \texttt{rep}.
In either case the resulting theorem is prefixed by \texttt{Rep};
if the function does not find $t'$ ($s'$) distinct from $t$ ($s$)
then \texttt{Unc} is returned
(in which case we say the function \emph{fails}).
The transitivity and reflexivity of \texttt{rep} 
enables direct translation between rep-conversions and rep-transformations;
the detailed implementation uses both.

We then define operators on these as follows:
\begin{description}

\item[\texttt{THENtt : (thm -> crep) * (thm -> crep) -> thm -> crep}] (infix)
applies two rep-transformations (of which the first need not succeed)
in sequence.

\item[\texttt{SUBcr : (cterm -> crep) -> cterm -> crep}] 
applies a rep-conversion to the immediate subterms of a term.
It uses previously proved rules of the form of (\ref{rep-cong})
to ``join'' the results of applying the rep-conversion 
to the subterms.

\item[\texttt{SUBtt : (thm -> crep) -> thm -> crep}]
corresponds to \texttt{SUBcr}, but is in terms of rep-trans\-formations.

\item[\texttt{REPtt : (thm -> crep) -> thm -> crep}]
repeats a rep-trans\-formation one or more times until it fails.

%\item[\texttt{TDtt, BUtt : (thm -> crep) -> thm -> crep}]
%These (and many others) can be defined easily, using the above operators.
%\texttt{TDtt} \textit{tt} 
%applies the rep-transformation \textit{tt} repeatedly wherever possible,
%proceeding through the term ``top-down'', 
%first dealing with the whole term, then the immediate subterms, and so on 
%down to the smallest subterms.
%\texttt{BU} is similar, but ``bottom-up'';
%it tries to rewrite the smallest subterms first.
%These are defined by 
%\begin{center}
%\texttt{ \noindent
%\mbox{fun TDtt tt th = (REPtt tt THENtt SUBtt (TDtt tt)) th ;} \\
%\mbox{fun BUtt tt th = (SUBtt (BUtt tt) THENtt REPtt tt) th ;}
%}
%\end{center}

\end{description}

These operators are for forward proof;
of them, \texttt{SUBtt} %, \texttt{TDtt} and \texttt{BUtt}
needs to be programmed differently for backwards proof.
%(In fact, \texttt{SUBcr} does not;
%we chose to work in terms of rep-transformations rather than rep-conversions
%because the rep-conversion analogues of
%\texttt{THENtt} and \texttt{REPtt} do require different versions for
%backward proof).

Various search strategies can now be defined easily, using the above operators.
For example, 
\texttt{TDtt} \textit{tt},
given by 
\begin{center}
\texttt{fun TDtt tt th = (REPtt tt THENtt SUBtt (TDtt tt)) th ;} 
\end{center}
applies the rep-transformation \textit{tt} repeatedly wherever possible,
proceeding through the term ``top-down'', 
first dealing with the whole term, then the immediate subterms, and so on 
down to the smallest subterms.

The following functions make rep-transformations:
\begin{description}
\item[\texttt{rep\_tt : thm -> thm -> crep}]
From a theorem $\texttt{rep} (A, B)$, \texttt{rep\_tt}
gives the rep-transformation
which transforms a theorem
$\texttt{rep} (X, A')$ to $\texttt{rep} (X, B')$,
where $A'$ and $B'$ are instantiations of $A$ and $B$.

\item[\texttt{rep\_tt\_rev : thm -> thm -> crep}]
is the corresponding function for backward proof.
%from a theorem $\texttt{rep} (A, B)$, it gives the rep-transformation
%which transforms the theorem
%$\texttt{rep} (B', X)$ to $\texttt{rep} (A', X)$,
%where $A'$ and $B'$ are instantiations of $A$ and $B$.

\end{description}

Finally, these rep-transformations can be applied in forwards or backwards
proof.
There are functions to 
apply a rep-trans\-formation to a theorem, in performing forward proof,
and to 
apply a rep-trans\-form\-ation to a subgoal as a tactic in backwards proof.
\comment{
\begin{description}
\item[\texttt{reprule : (thm -> crep) -> thm -> thm}]
applies a rep-trans\-formation to a theorem, in performing forward proof.
If $t$ is the conclusion of the theorem \textit{th},
and \textit{tt} transforms the theorem $\texttt{rep}(t, t)$ to
$\texttt{rep}(t, t')$,
then \texttt{reprule}~\textit{tt~th} gives
the theorem \textit{th} with the conclusion $t$ replaced by $t'$.
\item[\texttt{rep\_prem\_tac : (thm -> crep) -> int -> int -> tactic}]
In the course of a backwards proof,
\texttt{rep\_prem\_tac} \textit{tt pn sg}
does a similar forward inference on premise number \textit{pn}
in subgoal number \textit{sg}
using rep-trans\-form\-ation \textit{tt}.
\item[\texttt{rep\_rew\_tac : (thm -> crep) -> int -> tactic}]
applies a rep-trans\-form\-ation to a subgoal as a tactic in backwards proof.
If $s$ is the \textit{sg}'th subgoal,
and \textit{tt} transforms the theorem $\texttt{rep}(s, s)$ to
$\texttt{rep}(s', s)$,
then \texttt{rep\_rew\_tac}~\textit{tt~sg} 
gives a new proof state in which subgoal $s$ is replaced by $s'$.

\end{description}
}