\subsection{Automating these proofs in Isabelle}

Note the form of the theorem \texttt{p\_rp\_anda} in \S\ref{??},
which requires finding values for unknowns $p', q, q', d$ such that
(among other requirements) $(p,p'), (q,q')$ and $(d, d')$ are all in
\texttt{ms\_deep\_equiv}.

We mostly used a recursive compund tactic for this, initially defined thus

\begin{verbatim}
fun perm_msde_tac' sg = FIRST' [ atac,
  (resolve_tac [msde.seqs, msde_commas, msde_commas_rev]
    THEN_ALL_NEW perm_msde_tac'),
  rtac refl_msde', etac refl_ms_of_ns_eq, 
  eresolve_tac msde_commas_empty, resolve_tac msde_assocs,
  resolve_tac msde_comm_assocs] sg ;
\end{verbatim}

For the above, \texttt{msde.seqs} and \texttt{msde\_commas} are shown;
the last three lines represent various ways to solve the goal, and samples of
the theorems used are shown.

\begin{verbatim}
msde.seqs : "[| (?aa, ?ba) : ms_deep_equiv; (?as, ?bs) : ms_deep_equiv |]
      ==> ($?aa => $?as, $?ba => $?bs) : ms_deep_equiv"
msde_commas : "[| (?aa, ?ba) : ms_deep_equiv; (?as, ?bs) : ms_deep_equiv |]
      ==> ($?aa,,, $?as, $?ba,,, $?bs) : ms_deep_equiv"
msde_commas_empty (one of them) :
   ["ms_of_ns ?Y = {#} ==> ($?X,,, $?Y, ?X) : ms_deep_equiv"
msde_comm_assocs (one of them) ;
   ["(($?aa1,,, $?C2),,, $?B2, ($?C2,,, $?B2),,, $?aa1) : ms_deep_equiv"
\end{verbatim}

The tactic works generally when there are some, but not too many, unknowns in
the goal to be instantiated.  Generally, of the three occurrences of
$(\_, \_) \in \texttt{ms\_deep\_equiv}$, it was best to attempt the first and
last before the middle one.
However, this led to a problem.
If a premise of each subgoal was $(A, B) \in \texttt{ms\_deep\_equiv}$,
then the first and last subgoals of the form 
$(\_, \_) \in \texttt{ms\_deep\_equiv}$ 
could both get solved by instantiating in a way
which used that premise, and then the final (second of the three)
subgoal would look like
$(\ldots B \ldots, \ldots A \ldots) \in \texttt{ms\_deep\_equiv}$,
which wouldn't get solved.
Thus we devised a general technique to ensure that a premise which appeared in
multiple subgoals could only get used in one of them.

\begin{verbatim}
keep :: bool => 'a => 'a"
keep_def : "keep ?b ?f == ?f"
keep_msdeI : "?nsp : ms_deep_equiv ==> keep ?b (?nsp : ms_deep_equiv)"
keepF_thin : "[| keep False ?P; PROP ?W |] ==> PROP ?W"
keepFD : "keep False ?P ==> ?P"
\end{verbatim}

First (\emph{before} the premise which is to be used once only is propagated to
multiple subgoals), change each such premise $P$ to 
\texttt{keep ?b } $P$ ---
in this case, by the tactic \texttt{REPEAT o dtac keep\_msdeI}.
Then, in \texttt{perm\_msde\_tac'} above, we changed
\texttt{atac} to \texttt{etac keepFD}.
This ensures that when such a premise is used, the variable \texttt{?b} is
changed to \texttt{False}.
Finally, we use the tactic \texttt{REPEAT o ematch\_tac [keepF\_thin]}
to remove occurrences of \texttt{keep False} \ldots where and when required.
In our case the problem was to avoid reuse of a premise in \emph{separate} 
uses of \texttt{perm\_msde\_tac'}, so we defined \texttt{perm\_msde\_tac} as shown.
(This would not have prevented the same premise being used twice within the
same invocation of \texttt{perm\_msde\_tac}).

\begin{verbatim}
val perm_msde_tac = 
  (REPEAT o ematch_tac [keepF_thin]) THEN' perm_msde_tac' ;
\end{verbatim}

The proofs of the permutation lemma involved a large number of cases,
because a sequent expression such as $X [\mathcal S \seq \mathcal T]$
can match a given sequent $Z$ in numerous ways, for two reasons:
\begin{itemize}
\item when $\mathcal S$ and $\mathcal T$ are multisets (that is, in our
formulation, there are many ways that
$(\mathcal S, \ldots) \in \texttt{msde\_deep\_equiv}$ can be achieved)
\item the context $X [~]$ may be of any size (which means that 
$\mathcal S \seq \mathcal T$ can match any part of $Z$
\end{itemize}

The attempted proof encounters plenty of obviously impossible cases
such as a formula matching $\mathcal S \seq \mathcal T$.
After these are detected and eliminated, we counted the cases where 
a goal (such as the conclusion of \texttt{p\_rp\_anda}) is actually solved.
These cases numbered 616, which shows the value of automating the process as
much as possible.  

