
\newpage
\appendix

\section{Isabelle text of selected definitions and theorems}

\subsection{More details of our General Derivability Predicates} \label{a-gdp}

We now describe more fully the functions we used to describe derivability. 
This framework is general in that a rule merely consists of ``premises''
and a ``conclusion'', and is independent of whether the things derived
are formulae, sequents, or other constructs, but we will refer to them
as sequents.

\begin{verbatim}
types 'a psc = "'a list * 'a"       (* single step inference *)
consts
  derl, adm :: "'a psc set => 'a psc set"
  dersl     :: "'a psc set => ('a list * 'a list) set"
  dercsl    :: "'a psc set => ('a list list * 'a list) set"
  derrec    :: "'a psc set => 'a set => 'a set"
  dersrec   :: "'a psc set => 'a set => 'a list set"
\end{verbatim}

An inference rule (of type \texttt{'a psc}) is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then, \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls}, and \texttt{derrec rls
  prems} is the set of sequents derivable using rules \texttt{rls}
from the set \texttt{prems} of premises.  These were defined separately 
using Isabelle's package for inductively defined sets,
using also the functions \texttt{dersl} and
\texttt{dersrec}. So $\mathtt{(ps, c) \in \derl~\rls}$ reflects the
shape of a derivation tree: \texttt{ps} is a list of exactly the
premises used, in the correct order, whereas $\mathtt{c \in \derrec\
  \rls\ prems}$ holds even if the set of premises \texttt{prems}
contains superfluous sequents.

The auxiliary function \texttt{dersrec} represents several sequents,
all derivable from the premises.  The auxiliary function
\texttt{dersl} represents several derivation trees side by side;
$\mathtt{(ps, cs) \in dersl~rls}$ when \texttt{ps} is the
concatenation of their lists of premises, and \texttt{cs} is the list
of their conclusions.  The function \texttt{dercsl} is similar, but it
shows which premises are part of which tree.  That is, $\mathtt{(pss, cs) \in
\texttt{dercsl}\ rls}$ implies $\mathtt{(concat\ pss, cs) \in \texttt{dersl}\
rls}$.  Curiously, we have used this framework for several years, and
only recently we found the need to redefine \derl\ using
\texttt{dercsl} rather than \texttt{dersl} as the auxiliary function.

The key clauses for defining \texttt{derl} and \texttt{derrec} are shown below
(the full definitions are in the source file \texttt{gen/dtrel.\{thy,ML\})}:
\begin{verbatim}
  dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |] 
              ==> (pss, concl) : derl pscrel"
  derI   : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |] 
              ==>  concl : derrec pscrel prems"
\end{verbatim}

We obtained the expected results linking \texttt{derl} and \texttt{derrec},
and a number of results expressing transitivity of derivation and the
results of derivation using derived rules, for example:
\begin{description}
\item[\texttt{derrec\_trans\_eq}]
derivability from derivable sequents is derivability from the original premises
\item[\texttt{derl\_deriv\_eq}]
derivability (in terms of \texttt{derrec})
using derived rules is derivability using the original rules
\item[\texttt{derrec\_derl\_deriv\_eq}]
derivability (in terms of \texttt{derl}) 
using derived rules is derivability using the original rules
\item[\texttt{derl\_trans}]
composition of derivation trees (joining conclusions to premises)
gives a derivation tree
\end{description}

\begin{verbatim}
derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"
derl_deriv_eq : "derl (derl ?rls) = derl ?rls" 
derrec_derl_deriv_eq : "derrec (derl ?rls) ?prems = derrec ?rls ?prems"
derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
                 ==> (?x, ?c) : derl ?rls" 
\end{verbatim}

The expected link between \texttt{derl} and \texttt{derrec}
was proved in the following form, 
by defining \texttt{derrc} from \texttt{derl},
and proving \texttt{derl\_rr}.

\begin{verbatim}
inductive "derrc pr prems"
  intros
    rcI : "[| (ps, c) : derl pr ; set ps <= prems |] ==>
          c : derrc pr prems" 

derl_rr : "derrec == derrc" 
\end{verbatim}

\subsection{Definitions of the \GLS\ formulae, sequents and rules}
\label{a-gls}

We define a language of formula connectives, formula variables and
primitive (atomic) propositions:
\begin{verbatim}
datatype formula = FC string (formula list) (* formula connective *)
                 | FV string                (* formula variable *)
                 | PP string             (* primitive proposition *)
\end{verbatim}

Although the formula connectives are fixed for each logic, 
we made the datatype as general as possible, 
and then defined (for example) 
$P \land Q$ as \texttt{FC ''Btimes'' [P, Q]}.

\begin{verbatim}
consts Btimes :: "formula => formula => formula" ("_ && _" [67,68] 67)
       Bplus  :: "formula => formula => formula" ("_ v _" [63,64] 63)
defs   Btimes "Btimes f g == FC ''Btimes'' [f, g]"
       Bplus  "Bplus f g == FC ''Bplus'' [f, g]"
\end{verbatim}

This permits a single definition of the immediate (proper) subformula
relation, \texttt{ipsubfml}, which will not need to be changed when new
connectives are added:
\begin{verbatim}
consts ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
  intros  ipsI : "P : set Ps ==> (P, FC conn Ps) : ipsubfml"
\end{verbatim}

If we call $\MC_e$ (in the main text) an \emph{extension} of $\MC_s$,
\texttt{extrs} $S$ means the set of all extensions of all rules 
in the set $S$.

\begin{verbatim}
consts
  extend :: "'a sequent => 'a sequent => 'a sequent"
  extrs  :: "'a sequent psc set => 'a sequent psc set"

defs
  extend_def : "extend fmls seq == seq + fmls"
  pscmap_def : "pscmap f (ps, c) = (map f ps, f c)" 

inductive "extrs rules"
  intros
    I : "psc : rules ==> pscmap (extend flr) psc = epsc ==> 
        epsc : extrs rules"
\end{verbatim}

Then we define \texttt{glss}, the set of rules of \GLS.
Sets \texttt{wkrls} and \texttt{ctrrls} $A$ refer to weakening and contraction
(on $A$) rules (before extension). 
\begin{verbatim}
inductive "wkrls"
  intros
    L : "([0], {#A#} |- {#}) : wkrls"
    R : "([0], {#} |- {#A#}) : wkrls"

inductive "ctrrls A"
  intros
    L : "([{#A#} + {#A#} |- {#}], {#A#} |- {#}) : ctrrls A"
    R : "([{#} |- {#A#} + {#A#}], {#} |- {#A#}) : ctrrls A"

inductive "glir" (* right introduction rules *)
  intros
    andr : "([{#} |- {#A#}, {#} |- {#B#}], {#} |- {#Btimes A B#}) : glir"
    orr1 : "([{#} |- {#A#}], {#} |- {#A v B#}) : glir"
    orr2 : "([{#} |- {#B#}], {#} |- {#A v B#}) : glir"
    negr : "([{#A#} |- {#}], {#} |- {#--A#}) : glir"
    (* single premise right implication rule *)
    impr : "([{#A#} |- {#B#}], {#} |- {#A -> B#}) : glir"

inductive "glil" (* left introduction rules *)
  intros
    andl1 : "([{#A#} |- {#}], {#Btimes A B#} |- {#}) : glil"
    andl2 : "([{#B#} |- {#}], {#Btimes A B#} |- {#}) : glil"
    orl : "([{#A#} |- {#}, {#B#} |- {#}], {#A v B#} |- {#}) : glil"
    negl : "([{#} |- {#A#}], {#--A#} |- {#}) : glil"
    impl : "([{#B#} |- {#}, {#} |- {#A#}], {#A -> B#} |- {#}) : glil"

inductive "glne" (* rules before being extended *)
  intros
    wkI : "(ps, c) : wkrls ==> (ps, c) : glne"
    ctrI : "(ps, c) : ctrrls A ==> (ps, c) : glne"
    ilI : "(ps, c) : glil ==> (ps, c) : glne"
    irI : "(ps, c) : glir ==> (ps, c) : glne"

inductive "glr B"
intros I : "([mset_map Box X + X + {#Box B#} |- {#B#}],
              mset_map Box X |- {#Box B#}) : glr B"

inductive "glss"
intros axiom : "([], {#A#} |- {#A#}) : glss"
        extI : "psc : glne ==> pscmap (extend flr) psc : glss"
        glrI : "psc : glr B ==> psc : glss"
\end{verbatim}

\subsection{Multisets form a monad} \label{a-ms}
These results use the characterisation of a monad which uses three axioms
and the functions \textit{unit} (here \texttt{single})
and \textit{ext} (here \texttt{mset\_ext}). 
(These axioms are often expressed with \textit{bind} in place of \textit{ext}). 
We also show the definition of 
\textit{map} (here \texttt{mset\_map}). 
\begin{verbatim}
  single :: "'a => 'a multiset"    ("{#_#}")
  mset_ext :: "('a => 'b multiset) => 'a multiset => 'b multiset"
  mset_map :: "('a => 'b) => 'a multiset => 'b multiset"

mset_map_def : "mset_map ?f == mset_ext (single o ?f)" 

mset_ext_of_single : "mset_ext ?f {#?x#} = ?f ?x" 
mset_ext_o_single : "mset_ext ?f o single = ?f" 
multiset_E3 : "mset_ext (mset_ext ?f o ?g) = mset_ext ?f o mset_ext ?g" 
\end{verbatim}

\subsection{Definitions of an atom in a lattice}
We produced a number of equivalent definitions characterising atoms of the
lattice, and properties of atomic elements 
(our definition of \texttt{atomic} includes $0$).
Thus we showed that ``$x$ is atomic'' is equivalent to each of the following: 
\\[0.5em] 
\begin{tabular}[c]{l@{\extracolsep{1cm}}l}
\multicolumn{2}{c}{$\forall y  < x.\ y = 0$}
\\ 
 $\forall z.\ x \leq z \lor (\mathit{pg\_meet}\ x\ z = 0)$ 
& $\forall a b.\ x \leq a + b \Rightarrow x \leq a \lor x \leq b$
\\
 $\forall a b.\  0 < a \land 0 < b \Rightarrow a + b \not= x$
& $\forall a b.\  a < x \land b < x \Rightarrow a + b \not= x$
\end{tabular}
\\[0.5em]

\subsection{Definition~\ref{d-gen-step2ssr}}
\begin{verbatim}
gen_step2ssr_simp :
"gen_step2ssr ?P ?A ?sub ?rls ((?psl, ?cl), (?psr, ?cr)) =
( (ALL A'. (A', ?A) : ?sub -->
   (ALL da:derrec ?rls {}. ALL db:derrec ?rls {}. ?P A' (da, db))) -->
  (ALL pa:set ?psl. ?P ?A (pa, ?cr)) -->
  (ALL pb:set ?psr. ?P ?A (?cl, pb)) --> ?P ?A (?cl, ?cr) )"
\end{verbatim}

\subsection{Theorem~\ref{t-gen-step2ssr-lem}}
\begin{verbatim}
gen_step2ssr_lem : 
 "[| ?A : wfp ?sub ; 
     ?seql : derrec ?rls {} ; ?seqr : derrec ?rls {} ;
     ALL A. ALL (psl, cl):?rls. ALL (psr, cr):?rls.
         gen_step2ssr ?P A ?sub rls ((psl, cl), (psr, cr)) |] 
     ==> ?P ?A (?seql, ?seqr)" 
\end{verbatim}

\subsection{Definitions of \texttt{mar}, \texttt{mas} and \texttt{masdt}}
\texttt{mar rls} $A\ (X_l \vdash Y_l, X_r \vdash Y_r)$ means that 
the result of doing multicut elimination of $A$ for these two sequents,
ie $(X_l + X_r \setminus A \vdash Y_l \setminus A + Y_r)$,
is derivable.

\texttt{mas rls} $A\ (X_l \vdash Y_l, X_r \vdash Y_r)$ means the same, 
conditional upon the given sequents,
 $X_l \vdash Y_l$ and $X_r \vdash Y_r$, being derivable.

\texttt{masdt} is similar, except that its arguments are derivation trees
rather than sequents, and uses the condition that they are valid.

A derivation tree is valid according to a set of rules if each ``rule''
contained in the tree is in fact a rule in the given set.

\begin{verbatim}
consts
  mar :: "'a sequent psc set => 'a => ('a sequent * 'a sequent) set"
  mas :: "'a sequent psc set => 'a => ('a sequent * 'a sequent) set"
  masdt ::  "'a sequent psc set => 'a =>
    ('a sequent dertree * 'a sequent dertree) set"

inductive "mar pscrel A"
  intros
    I : "(Xl + ms_delete {A} Xr |- ms_delete {A} Yl + Yr) : derrec pscrel {}
            ==> (Xl |- Yl, Xr |- Yr) : mar pscrel A"

inductive "mas pscrel A"
  intros
    I : "seql : derrec pscrel {} & seqr : derrec pscrel {} -->
              (seql, seqr) : mar pscrel A ==> 
        (seql, seqr) : mas pscrel A"

consts
  masdt ::  "'a sequent psc set => 'a =>
    ('a sequent dertree * 'a sequent dertree) set"

inductive "masdt pscrel A"
  intros
    I : "valid pscrel dtl & valid pscrel dtr -->
            (conclDT dtl, conclDT dtr) : mar pscrel A ==>
          (dtl, dtr) : masdt pscrel A"
\end{verbatim}

\subsection{Theorem~\ref{t-gs2ssr}}
\begin{verbatim}
lmg_gen_steps :
  "[| wk_adm ?erls; extrs {(?ps, ?c)} <= ?erls; ~ ?A :# succ ?c;
        ?pscl = pscmap (extend ?flr) (?ps, ?c) |]
    ==> gen_step2ssr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)"
\end{verbatim}

\subsection{Definition~\ref{d-del0}}
Here \texttt{glra} is the
set of \emph{all} \GLR{}-rule instances, \texttt{antec} is a function to return
the antecedent of a sequent, and \texttt{:\#} is multiset membership.

\begin{verbatim}
primrec Der  : "del0 B (Der seq dtl) =
               (if (map conclDT dtl, seq) : glra then
                   if Box B :# antec seq then 1 else 0
                else del0s B dtl)"
        Unf  : "del0 B (Unf dt) = 0"

        Nil  : "del0s B [] = 0"
        Cons : "del0s B (dt # dts) = del0 B dt + del0s B dts"
\end{verbatim}

\subsection{Definition~\ref{d-muxbn}}
\begin{verbatim} 
defs muxbn_def : "muxbn B n ==
     ALL mu dtb seq. ([conclDT mu], seq) : glr B -->
      del0 B mu <= n --> (Der seq [mu], dtb) : masdt glss (Box B)"
\end{verbatim}

\subsection{Lemma~\ref{l-gr19e}}
\begin{verbatim}
"[| valid glss ?mu ; del0 ?B ?mu = 0 ; (conclDT ?mu) = 
      (mset_map Box ?X + ?X + {# Box ?B#} |- {#?B#}) |] 
  ==> (mset_map Box ?X + ?X |- {#?B#}) : derrec glss {}" 
\end{verbatim}

\subsection{Lemma~\ref{l-gr19bc}\ref{l-gr19b} and \ref{l-gr19c}}
\begin{verbatim}
gr19b : "[| ((conclDT ?mu) = 
             (mset_map Box ?X + ?X + {# Box ?B#} |- {#?B#})) ; 
            valid glss ?mu ; del0 ?B ?mu = Suc ?n ; 
            mas glss ?B = UNIV; muxbn ?B ?n |]
      ==> EX mupr. valid glss mupr & 
                  conclDT mupr = conclDT ?mu & del0 ?B mupr <= ?n"

gr19c' : "[| muxbn ?B ?n; mas glss ?B = UNIV |] ==> muxbn ?B (Suc ?n)" 
\end{verbatim}

\subsection{Lemma~\ref{l-cut-glr}}
\begin{verbatim}
cut_glr : 
  "[| mas glss ?B = UNIV; ([conclDT ?mu], ?seq) : glr ?B |] ==>
  (Der ?seq [?mu], ?dtb) : masdt glss (Box ?B)" 

cw0_mas : "mas glss ?B = UNIV ==> muxbn ?B ?n" 
\end{verbatim}

\subsection{Theorem~\ref{t-glss-ca}}
\begin{verbatim}
mar_glss : 
  "[| ?seqa : derrec glss {}; ?seqb : derrec glss {} |] ==>
  (?seqa, ?seqb) : mar glss ?A" 

glss_ca :
"[| (?Xl |- ?Yl) : derrec glss {}; (?Xr |- ?Yr) : derrec glss {} |] ==> 
(?Xl + ms_delete {?A} ?Xr |- ms_delete {?A} ?Yl + ?Yr) : derrec glss {}" 
\end{verbatim}
