\renewcommand\cfile{raisa.tex} \section{Implementation in Isabelle} \label{impl} The syntax of \dRA\ has been implemented in Isabelle, in the theory files \texttt{RS.thy} and \texttt{dRA.thy}. (See \apsrc{any} regarding any source file mentioned). It uses the Isabelle type \texttt{prop} (for sequents) and defines types \texttt{structure} and \texttt{formula}, so as to distinguish structure and formula variables. Since a formula can also be a structure, there is a coercing operator ``Structform'', which takes a formula argument (of Isabelle type \verb:formula:) and returns the ``same'' term, but with the type \verb:structure:. Externally, at the user level, a structure variable is preceded by `\verb:$:', to distinguish it from a formula variable. Doing this in Isabelle is quite complex, and the method used was copied from the Isabelle sequent calculus theory (\cite{OL}, Ch 6). In the Isabelle implementation, the operators are represented as follows. Note that \verb:^: is postfix, so $\smile A$ becomes \verb:A^:. \begin{center} \begin{tabular}{c@{\quad}cccccccccccccccc} \dRA & $,$ & $*$ & $I$ & $;$ & $\bullet$ & $E$ & $\land$ & $\lor$ & $\neg$ & $\bot$ & $\top$ & $\circ$ & + & $\smile$ & \1 & \0 \\ \texttt{dRA.thy} & \texttt{,} & \texttt{*} & \texttt{I} & \texttt{;} & \texttt{@} & \texttt{E} & \texttt{\&} & \texttt{v} & \texttt{-} & \texttt{F} & \texttt{T} & \texttt{o} & \texttt{+} & \verb:^: & \texttt{1} & \texttt{0} \end{tabular} \end{center} The rules have been implemented in Isabelle; the \dRA\ name of the rule using symbols is given on the left in the figures, and the Isabelle name is given on the right (in a few cases the Isabelle rule is not quite the same). It was noted that some rules of \dRA\ can be derived from others, and the Isabelle implementation reflects this; some of them (indicated by \dag\ in Figures \ref{fig:dps} to \ref{fig:lir}) are derived rather than being specified in the theory file. However, no effort was made to find a minimal set of rules. Some particularly useful derived rules are shown in \fig{sdr}. Most are derived \insrc{RS.ML}. It will be noticed that the two unary structural operators commute, and both distribute over both the binary structural operators. The rules \texttt{andS} and \texttt{orA}, which are derived \insrc{dRA.ML}, are equivalent to \texttt{ands} and \texttt{ora}, since \texttt{ands} and \texttt{ora} can be derived from \texttt{andS} and \texttt{orA} and the monotonicity rules (see \texttt{andsder} and \texttt{orader} in \texttt{dRA.ML}). % SELECTED DERIVED RULES \begin{figure}[htbp] \begin{center} \begin{tabular}{c@{\hspace{15mm}}c} \multicolumn 2 c { \invrule { X \vdash **Y } { X \vdash Y } (\ttdef{rssS}) \quad \invrule { X \vdash Y } { *Y \vdash *X } (\ttdef{dcp}) \quad \invrule { X \vdash \bullet \bullet Y } { X \vdash Y } (\ttdef{rbbS}) \quad \invrule { X \vdash Y } { \bullet X \vdash \bullet Y } (\ttdef{blbl}) } \\ & \\ \invrule {*(X,Y) \vdash Z } { *Y, *X \vdash Z } (\ttdef{stcdista}) & \invrule {X \vdash *(Y,Z) } { X \vdash *Z, *Y } (\ttdef{stcdists}) \\ & \\ \invrule {* (X; Y) \vdash Z} {* X; * Y \vdash Z} (\ttdef{stscdista}) & \invrule {Z \vdash * (X; Y)} {Z \vdash * X; * Y} (\ttdef{stscdists}) \\ & \\ \invrule {\bullet (X; Y) \vdash Z} {\bullet Y; \bullet X \vdash Z} (\ttdef{blscdista}) & \invrule {Z \vdash \bullet (X; Y)} {Z \vdash \bullet Y; \bullet X} (\ttdef{blscdists}) \\ & \\ \invrule {(\bullet X, \bullet Y) \vdash Z} {\bullet (X, Y) \vdash Z} (\ttdef{blcdista}) & \invrule {X \vdash \bullet Y, \bullet Z} {X \vdash \bullet (Y, Z)} (\ttdef{blcdists}) \\ & \\ \slrule {(X; Y), (X; Z) \vdash W} {X; (Y, Z) \vdash W} (\ttdef{sccldista}) & \slrule {W \vdash (X; Y), (X; Z)} {W \vdash X; (Y, Z)} (\ttdef{sccldists}) \\ & \\ \slrule {(X; Z), (Y; Z) \vdash W} {(X, Y); Z \vdash W} (\ttdef{sccrdista}) & \slrule {W \vdash (X; Z), (Y; Z)} {W \vdash (X, Y); Z} (\ttdef{sccrdists}) \\ & \\ \invrule {X ; Y \vdash Z }{\bullet Y ; \bullet X \vdash \bullet Z } (\ttdef{tagae}) & \invrule {Z \vdash X ; Y }{\bullet Z \vdash \bullet Y ; \bullet X } (\ttdef{tagse}) \\ & \\ \invrule {\bullet * X \vdash Y } { * \bullet X \vdash Y} (\ttdef{bsA}) & \invrule {X \vdash \bullet * Y } {X \vdash * \bullet Y } (\ttdef{bsS}) \\ & \\ ($* E \vdash$)\invrule{E \vdash X}{* E \vdash X} (\ttdef{sEa}) & ($\vdash * E $)\invrule{X \vdash E }{X \vdash * E } (\ttdef{sEs})\\ & \\ ($* I \vdash$)\invrule{I \vdash X}{* I \vdash X} (\ttdef{sIa}) & ($\vdash * I $)\invrule{X \vdash I }{X \vdash * I } (\ttdef{sIs})\\ & \\ \invrule { \bullet X, E \vdash Y} {X, E \vdash Y } (\ttdef{blcEa}) & \invrule {Y \vdash \bullet X, E} {Y \vdash X, E} (\ttdef{blcEs}) \\ & \\ \slrule {A \vdash X \quad B \vdash X } {A \lor B \vdash X } (\ttdef{orA}) & \slrule {X \vdash A \quad X \vdash B} {X \vdash A \land B} (\ttdef{andS}) \end{tabular} \end{center} \caption{Selected Derived Rules} \label{fig:sdr} \end{figure} As in classical sequent calculus, the \emph{modus operandi} for proving a sequent is to start the proof from the bottom, ie, from the goal, and work ``backwards''; in terms of the written representation of proofs, that means working upwards. The first step is, where possible, to remove all the formula (logical) operators, using the logical introduction rules. In Display Logic (unlike classical sequent calculus) this requires that the formula which is to be ``broken up'' must first be displayed. As any formula can be displayed, this is not a difficulty, except in that it is tedious to select display postulates one-by-one. The tactics described in the next two subsections were first written to help in this style of proof. Note that many of these functions have arguments and can be considered as having return values of type \verb:int -> tactic:. We define a \bfi{sg-tactic}\label{sg-tactic} as a function of type \verb:int -> tactic: which, where the argument is a subgoal number, returns a tactic which affects only that subgoal. (Thus, for example, \verb:rtac: \textit{th} is an sg-tactic). We can think of an sg-tactic as an operation which transforms subgoals (noting that it can produce any number of subgoals from a given one). Many of the functions we describe can be thought of as transformations of sg-tactics. \subsection{Display Tactics} Tactics were written to help in this process of displaying a chosen substructure. These tactics are found in the file \verb:RS.tac:. \begin{description} \item[\texttt{disp\_tac : string -> int -> tactic}]\tti{disp\_tac} \label{disp_tac} replaces a subgoal by one in which a selected structure is displayed. The structure selected is indicated by a string argument, of which the first character is `\verb:|:' or `\verb:-:', to indicate the left or right side of the turnstile; remaining characters are \begin{itemize} \item[] `\verb:l:' or `\verb:r:', to indicate the left or right operand of the `,' operator \item[] `\verb:L:' or `\verb:R:', to indicate the left or right operand of the `;' operator \item[] `\verb:*:' or `\verb:@:', to indicate the operand of the `$*$' or the `$\bullet$' operator \end{itemize} For example, in the (sub)goal $Q \vdash (Y; * \bullet R), (* S; * \bullet P)$ the string \verb:"-lR*@": denotes the sub-structure $R$. Thus \verb:disp_tac "-lR*@": takes that (sub)goal %$Q \vdash (Y; * \bullet R), (* S; * \bullet P)$ in a backwards proof to the new subgoal \mbox{$R \vdash \bullet * (* \bullet Y; (Q, * (* S; * \bullet P)))$,} which has $R$ displayed, by these steps (read upwards) \vpf \begin{center} \bpf \A "$R \vdash \bullet * (* \bullet Y; (Q, * (* S; * \bullet P)))$" \U "$\bullet R \vdash * (* \bullet Y; (Q, * (* S; * \bullet P)))$" \U "$* \bullet Y; (Q, * (* S; * \bullet P)) \vdash * \bullet R$" \U "$Q, * (* S; * \bullet P) \vdash Y; * \bullet R$" \U "$Q \vdash (Y; * \bullet R), (* S; * \bullet P)$" \epf \end{center} \item[\texttt{fdisp : string -> thm -> thm}]\tti{fdisp} is the corresponding function for forward proof, displaying the selected part of the conclusion of the given theorem. \item[\texttt{d\_b\_tac : string -> (int -> tactic) -> int -> tactic}] \tti{d\_b\_tac} \mbox{}\\ \verb:d_b_tac: \textit{str tacfn sg} takes subgoal \textit{sg}, displays the part selected by \textit{str} (as for \verb:disp_tac:) and applies \textit{tacfn} to the transformed subgoal. It then applies the reverse of the display steps to each resulting subgoal. This requires that the subgoals produced by \textit{tacfn} are in a suitable form to permit the display steps used to be reversed. This will be the case if \textit{tacfn} only affects the displayed sub-structure, and leaves the rest of the sequent alone. This was the purpose of deriving the rules \texttt{andS} and \texttt{orA} (which satisfy this requirement) from \texttt{ands} and \texttt{ora} (which do not). For example, if we start with the subgoal $R \vdash ((* T; \bullet * S), \bullet * Q); Y$ then \verb:d_b_tac "-L" (rtac mrs): applies the monotonicity rule ($\vdash M$) (\texttt{mrs}) to the sub-structure $(* T; \bullet * S), \bullet * Q$ by the following steps (read upwards) \vpf \begin{center} \bpf \A "$R \vdash (* T; \bullet * S); Y$" \U "$R ; * \bullet Y \vdash * T; \bullet * S$" "(reverse of \texttt{disp\_tac "-L"})" \U "$R ; * \bullet Y \vdash (* T; \bullet * S), \bullet * Q$" "(\texttt{mrs})" \U "$R \vdash ((* T; \bullet * S), \bullet * Q); Y$" "(\texttt{disp\_tac "-L"})" \epf \end{center} %displays the sub-structure $(* T; \bullet * S), \bullet * Q$ %to give %$R ; * \bullet Y \vdash (* T; \bullet * S), \bullet * Q$, %applies the monotonicity rule ($\vdash M$) to give %$R ; * \bullet Y \vdash * T; \bullet * S$, %and reverses the display operation to %give the new subgoal %$R \vdash (* T; \bullet * S); Y$. \item[\texttt{THENEXP : (int -> tactic) * (int -> tactic) -> int -> tactic}] \tti{THENEXP} %\mbox{} \\ line above just long enough is a tactical used in \verb:d_b_tac:. \verb:(:\textit{tacf1} \verb:THENEXP: \textit{tacf2}\verb:): \textit{sg} applies \textit{tacf1} to subgoal number \textit{sg}, then applies \textit{tacf2} to each resulting subgoal. This tactical may be generally useful; it corresponds to the HOL tactical \texttt{THEN} (\cite{HOLdesc}, \S14.4.4), and to the tactical \ttdef{THEN\_ALL\_NEW\_SUBGOALS} as described by Easthaughffe et al in \cite{dove}, p.~378. \item[\texttt{fdispfun : string -> (thm -> thm) -> thm -> thm}]\tti{fdispfun} \mbox{} \\ is a corresponding operation for forward proof. \verb:fdispfun: \textit{str thfn th} displays the part of theorem \textit{th} indicated by string \textit{str}, applies transformation \textit{thfn} to the result, then reverses the display steps used. \end{description} \subsection{Search-and-Replace Tactics} \label{srtac} Tactics were written to display all structures in a sequent in turn, and apply any appropriate transformations (selected from a given set) to the structure. These can be used to rewrite all substructures of a particular form, for example, to rewrite all occurrences of $X,(Y,Z)$ to $(X,Y),Z$. These tactics are found in the file \texttt{glob.tac}. \begin{description} \item[\texttt{glob\_tac :}]\tti{glob\_tac}\mbox{} \\ \mbox{\textbf{\texttt{(term -> int -> (int -> tactic) list) -> int -> tactic}}} \\ The first argument of \texttt{glob\_tac} is a function \textit{actfn}\label{actfnbwd}, called as \textit{actfn tm asp}, where \textit{tm} is a subterm, and \textit{asp} has the value 0 or 1 to indicate that \textit{tm} is displayed as the antecedent or succedent part of a sequent. \textit{actfn tm asp} should return either \verb:[]: or \verb:[:\textit{tacf}\verb:]:, where \textit{tacf} is an sg-tactic, ie when \textit{sg} is a subgoal number, \textit{tacf sg} is a tactic. When \textit{tm} is displayed as the antecedent (if $\textit{asp} = 0$) or succedent (if $\textit{asp} = 1$), \textit{tacf} should be a tactic which changes only \textit{tm}. Then \texttt{glob\_tac} \textit{actfn sg} displays in turn every subterm of subgoal \textit{sg}, and applies the tactic, if any, given by \textit{actfn tm asp}, (where \textit{tm} is the subterm displayed, as antecedent if $\textit{asp} = 0$ or succedent if $\textit{asp} = 1$) to the sequent thus produced. All the display steps are eventually reversed, in the same way as for \verb:d_b_tac:. \texttt{glob\_tac} uses a top-down strategy: it first tests the whole structure with the function \textit{actfn}, then, recursively, each sub-structure. (Note that although elsewhere we refer to the ``top'' or ``bottom'' of a proof tree, in this context we are using ``top-down'' and ``bottom-up'' to describe the order in which we examine all sub-terms of a term; ``top-down'' means that we look at a term before its sub-terms, whereas ``bottom-up'' means that we look at the sub-terms of a term before the term). If \textit{actfn} returns an sg-tactic (ie, not the empty list) then the changed structure is tested again (thus \texttt{glob\_tac} will loop infinitely if \textit{actfn} returns \verb:[:\textit{tacf}\verb:]: such that \textit{tacf} leaves the subgoal unchanged). \item[\ttdef{bup\_tac}] is like \texttt{glob\_tac}, but uses a bottom-up strategy, displaying and testing the smallest sub-structures first. Like \texttt{glob\_tac}, it will retest a (possibly) changed sub-structure after \verb:[:\textit{tacf}\verb:]: is applied. \item[\texttt{glob\_s\_tac, bup\_s\_tac}] \tti{glob\_s\_tac}\tti{bup\_s\_tac} are like \texttt{glob\_tac} and \texttt{bup\_tac}, but take an additional first argument, which should be 0 (1) to indicate that only the antecedent (succedent) side of the subgoal should be affected. (The value $-1$ (\verb:~1: in ML) means both sides, so \verb:glob_s_tac ~1: is the same as \texttt{glob\_tac}). \item[\texttt{fgl\_fun, fbl\_fun :}]\tti{fgl\_fun}\tti{fbl\_fun}\mbox{} \\ \mbox{\textbf{\texttt{(term -> int -> (thm -> thm) list) -> thm -> thm}}} \\ These functions are like \texttt{glob\_tac} and \texttt{bup\_tac}, but for doing forward proof. Their first argument is a function \textit{actfn}\label{actfnfwd}, called as \textit{actfn tm asp}, where \textit{tm} is a subterm, and \textit{asp} has the value 0 or 1 to indicate that \textit{tm} is displayed as the antecedent or succedent part of a sequent. \textit{actfn tm asp} should return either \verb:[]: or \verb:[:\textit{thtr}\verb:]:, where \textit{thtr} is a theorem transformation, ie a function of type \verb:thm -> thm:. When \textit{tm} is displayed as the antecedent (if $\textit{asp} = 0$) or succedent (if $\textit{asp} = 1$) of the conclusion of a theorem \textit{th}, \textit{thtr th} should be a theorem which differs from \textit{th} only in that \textit{tm} has been changed. Then \texttt{fgl\_fun} \textit{actfn th} displays every sub-structure of the conclusion of \textit{th} and tests it with \textit{actfn}; if \textit{actfn} returns a theorem transformation then it is applied. The strategy is top-down, as for \texttt{glob\_tac}, with every transformed sub-structure retested. \texttt{fbl\_fun} does the same, but using a bottom-up strategy. Again, a (possibly) changed sub-structure will be retested after \verb:[:\textit{thtr}\verb:]: is applied. \item[\texttt{fgl\_s\_fun, fbl\_s\_fun :}] \tti{fgl\_fun}\tti{fbl\_fun} \mbox{} \\ \mbox{\textbf{\texttt{int -> (term -> int -> (thm -> thm) list) -> thm -> thm}}} \\ These are like \texttt{fgl\_fun} and \texttt{fbl\_fun} but take an extra first argument, which is 0 or 1 to indicate that only the antecedent or succedent should be transformed (and $-1$ for both). \end{description} \subsection{Implementation of the Search-and-Replace Tactics} \label{srimp} We now describe the implementation of the search-and-replace tactics. \noindent\tti{travdown}\mbox{\texttt{\textbf{ travdown : (term -> int -> 'a -> 'b) -> 'b -> }}} \mbox{} \\ \mbox{\textbf{\texttt{('b * 'b -> 'b) -> (thm -> 'b) -> term -> int -> 'a -> 'b}}}\\ \textbf{\texttt{globfns : \textsl{\rmfamily 'b} -> (\textsl{\rmfamily 'b} * \textsl{\rmfamily 'b} -> \textsl{\rmfamily 'b}) -> (thm -> \textsl{\rmfamily 'b}) -> \textsl{\rmfamily 'c} \\ \mbox{}\hspace{4em} -> (int -> (term -> int -> \textsl{\rmfamily 'b} list) -> \textsl{\rmfamily 'b}) \textsl{\rmfamily pair}}} \\ % and \texttt{globfns}\tti{globfns} are functions which are used to specify a strategy for exploring a term, searching for sub-structures to be transformed. %\verb:travdown: They are used in two different contexts. %In both cases, a term is traversed and, where possible, %a part of the term is transformed. Firstly, for backward proof, the term is a subgoal, and the transformation consists of applying a tactic to the term, to produce a number of new subgoals. Secondly, for forward proof, the term is the conclusion of the theorem generated so far, and its transformation results in a new theorem. The type \verb:'a: above is the type of the argument \textit{actfn} as in the description of the various functions in \S\ref{srtac} above. For backward proof, type \verb:'b: is the sg-tactic type described above (\page{sg-tactic}), ie, \verb:int -> tactic:. For forward proof, we would want type \verb:'b: to be the type of a theorem transformation, \verb:thm -> thm:. However, for \texttt{travdown} and \texttt{globfns} to work on both sg-tactics and theorem transformations, both must have the same number of arguments; so we make the type of a theorem transformation \verb:int -> thm -> thm:, with the \verb:int: argument always being ignored. The type of \texttt{globfns} is more complicated than that shown above, but it is used with \textsl{'b} the same as \texttt{'b}, and with \textsl{'c} being \texttt{int -> thm -> term}. %When called as \\ %\texttt{travdown} \textit{do\_below idact actcomb dpact} \\ %\texttt{globfns} \textit{idact actcomb dpact find\_tm} \\ When called as \texttt{travdown}~\textit{do\_below~idact~actcomb~dpact} and \texttt{globfns}~\textit{idact~actcomb~dpact~find\_tm} the arguments are as follows: \begin{description} \shrinklist{0.5} \item[\mdseries\textit{idact}] is the identity action, the action which doesn't make any change \item[\mdseries\textit{actcomb}] is the composition of two actions \item[\mdseries\textit{dpact dp}] is the action to be taken to transform a term given a display postulate \textit{dp} \item[\mdseries\textit{find\_tm}] is the function which finds the term being examined, ie, in backwards proof, the subgoal, or, in forward proof, the conclusion of the theorem. \end{description} The source code defining the values used for these arguments is \begin{center} \begin{tabular}{l} \textbf{\qquad \qquad for backward proof} \\ \\ \texttt{fun idact sg = all\_tac ;} \\ \texttt{val actcomb = op THENEXP ;} \\ \texttt{val dpact = rtac o md2 ;} \\ \texttt{fun find\_tm sg state = nth (prems\_of state, sg-1) ;} % \end{tabular} \end{center} \begin{center} \begin{tabular}{l} \\ \\ \textbf{\qquad \qquad for forward proof} \\ \\ \texttt{fun idact \_ th = th ;} \\ \texttt{fun actcomb (f, g) \_ = (g 0) o (f 0) ;} \\ \texttt{fun dpact theq \_ th = th RS md1 theq ;} \\ \texttt{fun find\_tm \_ = concl\_of ;} \end{tabular} \end{center} If we call the result and the first argument of \texttt{travdown} a ``strategy'', then the first two arguments of a strategy are a displayed term and an integer (0 or 1) indicating whether the term is displayed as antecedent or succedent. Then \texttt{travdown}~\textit{do\_below} displays in turn the top-level sub-structures (ie, the two operands of `,' or `;', or the single operands of $*$ or $\bullet$) of the term, and applies the strategy \textit{do\_below} to them. Clearly \texttt{travdown} can potentially be used to program strategies other than those used in the functions described in \S\ref{srtac}. With the arguments described above, the function \texttt{globfns} returns the pair \texttt{(glob\_s\_tac, bup\_s\_tac)} (described in \S\ref{srtac}) for backward proof, and \texttt{(fgl\_is\_fun, fbl\_is\_fun)} for forward proof. \texttt{fgl\_is\_fun} and \texttt{fbl\_is\_fun} are like \texttt{fgl\_s\_fun} and \texttt{fbl\_s\_fun}, except that, for the former, the type of a theorem transformation is taken as having the extra integer argument (which is ignored), as discussed above. An alternative implementation of the top-down strategies was programmed also \seesrc{nglob.tac}. \ttdef{mglob} is like \texttt{globfns}, except that it returns only a single result, \texttt{glob\_s\_tac} or \texttt{fgl\_is\_fun}, not a pair. It uses \noindent \tti{travdowneqs}\mbox{\textbf{\texttt{ travdowneqs : (term -> thm list -> int -> 'a -> 'b) -> 'b}}} \mbox{\textbf{\texttt{ -> ('b * 'b -> 'b) -> term -> thm list -> int -> 'a -> 'b}}} When called as \verb:travdowneqs: \textit{do\_below idact actcomb}, the arguments are as for \texttt{travdown}, except that the argument \textit{dpact} is not needed, and the type of ``strategy'' (first argument and result) is different, in that it also uses an argument of type \verb:thm list:. In this implementation the term is traversed, but the appropriate display postulates are not applied until it is apparent that it is useful to do so. This contrasts with the first implementation where often a sequence of display postulates would be applied, and then its inverse applied, without anything else happening in between. In this second implementation, a list of display postulates is kept, to be applied when needed. (Such a list is the extra argument of a ``strategy''). These display postulates will then be applied to display a sub-structure when it is seen that that sub-structure, if displayed, could be transformed. (The function \textit{actfn} tells whether a displayed sub-structure could be transformed.) As noted above, two particular search strategies are provided, in \texttt{glob\_tac} and \texttt{fgl\_fun} (top-down), and in \texttt{bup\_tac} and \texttt{fbl\_fun} (bottom-up). Further work in this area might provide a means for the user to program his/her own search strategy, in the manner of the HOL \label{fwconv} conversionals, or conversion functionals, as in \cite{HOLdesc}, \S13.2. \subsection{Application of the Search-and-Replace Tactics} \label{srapp} We now describe some uses of the search-and-replace tactics. These require programming a function \textit{actfn}, as described in \S\ref{srtac}. Recall that \textit{actfn tm asp} tests whether to perform an action on a sequent which has \textit{tm} displayed on the side indicated by \textit{asp}; it returns either \verb:[]: or \verb:[:\textit{action}\verb:]:. In practice, the action performed on the sequent will change only \textit{tm}, leaving the other side of the sequent unchanged; thus these tactics are used to perform local ``rewrites'' on subexpressions. This is implemented \insrc{pat.tac}, using the functions \noindent\textbf{\texttt{ tfpr : ((term -> bool) * thm) list list \\ \indent -> term -> int -> (int -> tactic) list}} \ (for backward proof)\\ \textbf{\texttt{ffpr : ((term -> bool) * thm) list list \\ \indent -> term -> int -> (thm -> thm) list}} \ (for forward proof) The first argument of these functions is of the form \verb:[:\textit{apr}\verb:,:\textit{spr}\verb:]:, where \textit{apr} (\textit{spr}) is used in the case where the displayed term is on the antecedent (succedent) side. \textit{apr} and \textit{spr} are lists of entries of the form \verb:(:\textit{patfn}\verb:,:\textit{rule}\verb:):, where \textit{patfn} tests a term, and returns \verb:true: if the theorem \textit{rule} may be ``used'' on a sequent with that term displayed. In this context, ``using'' a theorem means \begin{itemize} \shrinklist{0.5} \item[--] for backward proof (with \verb:tfpr:), returning the sg-tactic \texttt{rtac} \textit{rule} \item[--] for forward proof (with \verb:ffpr:), returning the theorem transformation \texttt{resfwd} \textit{rule}, where \verb:resfwd: is defined by \texttt{fun resfwd thr th = th RS thr;} \end{itemize} Then \verb:tfpr: \verb:[:\textit{apr}\verb:,:\textit{spr}\verb:]: and \verb:ffpr: \verb:[:\textit{apr}\verb:,:\textit{spr}\verb:]: can be used as the function \textit{actfn} required by the search-and-replace tactics. Note that as \textit{apr} and \textit{spr} are lists, \verb:tfpr: and \verb:ffpr: simply use the first \textit{rule} for which the corresponding \textit{patfn} returns \verb:true:. In the source files arguments for \verb:tfpr: are conventionally called \verb:pr_:\ldots, and arguments for \verb:ffpr: are conventionally called \verb:fpr_:\ldots. Examples of the use of these tactics are {(see source files \texttt{pat.tac} and \texttt{dRA.tac})} \begin{itemize} \shrinklist{0.5} \item[--] to eliminate $**$ and $\bullet \bullet$ (\verb:pr_dbl:, \verb:fpr_dbl:) \item[--] to use the various distributive laws to push $*$ and $\bullet$ down (\verb:pr_dist:, \verb:fpr_dist:) \item[--] to eliminate logical operators, where possible, using those logical introduction rules satisfying the property mentioned in \S\ref{decproc} below (backward proof only, \verb:pr_intr:) \end{itemize} The fact that \texttt{pr\_intr} is available for backward proof only illustrates that these tactics can be used with uni-directional rules, such as the logical introduction rules, as well as with bi-directional rules. This useful aspect of the tactics contrasts with the more usual rewriting tactics, such as \texttt{rewrite\_tac} and \texttt{rewrite\_rule} in Isabelle, and \texttt{REWRITE\_TAC} and \texttt{REWRITE\_RULE} in HOL, where the rules used to rewrite an expression must be equalities. To convert a theorem in structural form to one in logical form, for example, from $B ; \bullet A \vdash \bullet D , * C$ to $B \circ \smile A \vdash \smile D \lor \neg C$, in a forward proof, we use some of the logical introduction rules, in their original form (\fig{lir}). The transformation \ttdef{s2l}, defined as \tti{fpr\_tau}\texttt{fbl\_fun (ffpr fpr\_tau)} does this conversion. Note that it must be done bottom up, ie, on the smallest sub-structures first, because only at the bottom are the sub-structures also formulae; also all the variables must be formula variables, not structure variables. This transformation implements the function $\tau$\index{tau@$\tau$|textbf}, as defined in \cite{dRA}, \S4. \subsection{Other Tactics and Methods} \label{otm} \paragraph{idf, idf\_tac} Recall that in the identity rule (id) $p \vdash p$ (\page{id}), $p$ stands for a primitive proposition, not an arbitrary formula. It is, however, true that $A \vdash A$ for any formula $A$; this is proved by induction (see Gor\'e \cite{dRA}, Lemma 2). The restriction to primitive propositions is not reflected in the Isabelle implementation, which contains the rule $A \vdash A$, called \ttdef{idf}, where $A$ is a formula variable, standing for any formula. However there is a tactic \ttdef{idf\_tac} which will convert an identity subgoal such as $$B \circ (\smile A \lor \neg C) \vdash B \circ (\smile A \lor \neg C)$$ into separate subgoals $$ B \vdash B \qquad A \vdash A \qquad C \vdash C $$ The tactic can therefore provide a demonstration, in any particular instance, of the theorem that $A \vdash A$ for any formula $A$. This tactic uses a set of derived results, proved as \ttdef{congs} \insrc{dRA.ML}. \vspace{-2.0ex} \begin{center} \small \begin{tabular}{c@{\quad}c@{\quad}c} \slrule {A_1 \vdash A \quad B_1 \vdash B} {A_1 \lor B_1 \vdash A \lor B} (\ttdef{cong\_or}) & \slrule {A_1 \vdash A \quad B_1 \vdash B} {A_1 \land B_1 \vdash A \land B} (\ttdef{cong\_and}) & \slrule {A \vdash A_1 } {\lnot A_1 \vdash \lnot A } (\ttdef{cong\_not}) \label{congs} \\ & \\ \slrule {A_1 \vdash A \quad B_1 \vdash B} {A_1 + B_1 \vdash A + B} (\ttdef{cong\_rs}) & \slrule {A_1 \vdash A \quad B_1 \vdash B} {A_1 \circ B_1 \vdash A \circ B} (\ttdef{cong\_comp}) & \slrule {A_1 \vdash A } {\smile A_1 \vdash \smile A } (\ttdef{cong\_conv}) \end{tabular} \end{center} It also uses a tactical \ttdef{REP\_DET\_EXP}, which repeatedly applies a tactic to the given subgoal and to all resulting subgoals. (For simplicity, it works deterministically, in the sense described in the discussion of \texttt{REPEAT\_DETERM} in \cite{Ref}). It is probably similar to the tactical \ttdef{REPEAT\_ALL\_NEW\_SUBGOALS} mentioned by Easthaughffe et al \cite{dove}, p.~378. \paragraph{Structural operators from logical ones} It is also possible to implement the function $\tau$\index{tau@$\tau$} in a backwards proof, to ``create'' logical connectives as we read a proof upwards; this can be helpful on occasions (though it is never \emph{necessary} in proving a sequent which is a tautology since it must use the (cut) rule, and we know (cut) is eliminable -- see Chapter~\ref{ch:cut}). The tactic \ttdef{tau\_tac}, \insrc{dRA.tac}, does this. It uses another different selection of variants of the logical introduction rules, where all the premises are of the form $A \vdash X$ or $X \vdash A$, and operators appear only in the conclusion. These rules are listed in \ttdef{tau\_thms}. The inverse of $\tau$\index{tau@$\tau$} is implemented for forward proof by \ttdef{l2s}, defined as \tti{fpr\_inv\_tau}\texttt{fgl\_fun (ffpr fpr\_inv\_tau)} \seesrc{dRA.tac}. This use of the search-and-replace method can only be done top down, and it also uses the cut rule. Not all formula operators will necessarily be changed to structural ones -- $\circ$ or $\land$ in a succedent position and $+$ or $\lor$ in an antecedent position cannot be converted to structural operators. \paragraph{Flipping theorems}\label{flip} It may be observed in \fig{bsr} that many of the rules in the right-hand column were in fact derived from other rules (as indicated by the \dag). In fact they were generally derived from the corresponding rule in the left-hand column. The procedure for doing this has been formalized in theorem transformations \noindent\textbf{\texttt{flip\_st\_p, flip\_st\_c : thm -> thm}} \noindent These use the theorem \verb:dcp: (see \fig{sdr}) to swap the sides of each sequent (which puts a $*$ in front of each side), use the distributive laws to push the $*$ down as far as possible, and rename variables to absorb the $*$. These transformations require all variables and operators to be structural. Unfortunately they are not very ``robust'', and some forms of theorem causes these transformations to fail, or to produce a result different from that intended; in particular, they don't work when the identities $I$ and $E$ are present. Sometimes \texttt{flip\_st\_p} (which works on the premises first) and \texttt{flip\_st\_c} (which works on the conclusion first) behave differently. Useful further work would include investigating these problems and finding a simple fix. The theorem transformations \noindent\textbf{\texttt{flip\_bl\_p, flip\_bl\_c : thm -> thm}} \noindent do the same thing, but with $\bullet$ instead of $*$. These transform a theorem to a corresponding one in terms of the converse relations. These functions are found \insrc{flip.tac}. \renewcommand\cfile{}