A set $rls$ of rules satisfies the weakening admissibility property if,
whenever a sequent $X \vdash Y$ is derivable, any larger sequent
$(X \vdash Y) + As$ is derivable.
\begin{verbatim}
wk_adm :: "'a sequent psc set => bool"
wk_adm_def : "wk_adm rls ==
ALL XY. XY : derrec rls {} --> (ALL As. XY + As : derrec rls {})"
\end{verbatim}
A set \texttt{rls} of rules satisfies the contraction admissibility property
for the formula $A$ if,
whenever a sequent $X \vdash Y$ such that
$(A \vdash 0) + (A \vdash 0) \leq (X \vdash Y)$ is derivable,
the sequent $(X \vdash Y) - (A \vdash 0)$ is derivable,
and likewise for $0 \vdash A$.
The first condition (\verb|ms_of_seq As = {#?A#}|)
says that the multiset of formulae on both sides of the sequent $As$
is the singleton multiset \verb|{#?A#}|
\begin{verbatim}
ctr_adm_def :
"ctr_adm ?rls ?A == ALL As. ms_of_seq As = {#?A#} -->
(ALL XY. XY : derrec ?rls {} --> As + As <= XY -->
XY - As : derrec ?rls {})"
\end{verbatim}
A rule $(ps, c)$ is \emph{invertible} with respect to a set $rls$ of rules
used for derivations if, whenever $c$ is derivable, then $ps$ is derivable.
\begin{verbatim}
inv_rl.simps:
"inv_rl ?rls (?ps, ?c) = (?c : derrec ?rls {} --> ?ps : dersrec ?rls {})"
\end{verbatim}
A pair of sequents satisfies the properties \texttt{cas} and \texttt{car} if
cut-admissibility is available (in different senses)
for that pair of sequents.
NOTE - the definition of cas in the printed document you showed me must be very
out of date.
Precisely, $(X_l \vdash Y_l, X_r \vdash Y_r) \in \texttt{car}\ rls\ A$ iff
$(X_l, (X_r - A) \vdash (Y_l - A), Y_r)$ is derivable using $rls$,
whereas \texttt{cas} means that this holds, conditionally on
$X_l \vdash Y_l$ and $X_r \vdash Y_r$ being themselves derivable.
\begin{verbatim}
car.caI : "(Xl + (Xr - {#A#}) |- (Yl - {#A#}) + Yr) : derrec rls {} ==>
(Xl |- Yl, Xr |- Yr) : car rls A"
cas.caI : "seql : derrec rls {} & seqr : derrec rls {} -->
(seql, seqr) : car rls A ==> (seql, seqr) : cas rls A"
\end{verbatim}
When wwe are talking about proving these by induction on the derivation of the
two sequents, that is, we are talking about two sequents which are derivable,
then these two concepts become equivalent.
\begin{verbatim}
gs2_cas_eq_car: "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls =
gen_step2sr (prop2 car ?rls) ?A ?sub ?rls"
\end{verbatim}
Sometimes we need to proceed by induction on (for example) the length of a
derivation by which a sequent can be ontained, rather than by the fact of a
sequent having been obtained earlier in the same derivation.
So to compare (say) the heights of derivations, we must be able to define them
and for this we need to look at explicit derivation trees.
Firstly we define \texttt{casdt}:
two derivation trees satisfy \texttt{casdt} $rls$ $A$ if:
if the two trees are \emph{valid}
(ie, no unproved leaves, and all steps are rules of the system),
then their conclusions satisfy \texttt{car}
\begin{verbatim}
casdt.I: "valid rls dtl & valid rls dtr -->
(conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"
\end{verbatim}
The step of in induction proof based on explicit derivation trees is expressed
using the following lemmas:
\begin{verbatim}
gen_step_tr_lem:
"[| ?A : wfp ?sub; ALL A. All (gen_step_tr ?P A ?sub) |] ==> ?P ?A ?x"
gen_step2_tr_lem:
"[| ?A : wfp ?sub; ALL A dta dtb. gen_step2_tr ?P A ?sub (dta, dtb) |] ==>
?P ?A (?dta, ?dtb)"
\end{verbatim}
where these properties expressing steps of the inductive proofs are defined as
\begin{verbatim}
gen_step_tr_def: "gen_step_tr ?P ?A ?sub ?dt ==
(ALL A'. (A', ?A) : ?sub --> All (?P A')) -->
(ALL dtp:set (nextUp ?dt). ?P ?A dtp) --> ?P ?A ?dt"
gen_step2_tr.simps: "gen_step2_tr ?P ?A ?sub (?dta, ?dtb) =
((ALL A'. (A', ?A) : ?sub --> All (?P A')) -->
(ALL dtp:set (nextUp ?dta). ?P ?A (dtp, ?dtb)) -->
(ALL dtq:set (nextUp ?dtb). ?P ?A (?dta, dtq)) --> ?P ?A (?dta, ?dtb))"
\end{verbatim}
These properties are exact analogues, for explicit derivation trees,
of the properties
\texttt{gen\_step} and \texttt{gen\_step2sr}
and lemmas \texttt{gen\_step\_lem} and \texttt{gen\_step2sr\_lem},
with the following theorem linking them.
\begin{verbatim}
gs2_tr_casdt_sr:
"gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls (botRule ?dta, botRule ?dtb)
==> gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (?dta, ?dtb)"
\end{verbatim}
However, the purpose of using explicit derivation trees is to define different
induction patters.
For example, we defined an induction pattern which depends on the inductive
assumption that the property $P$ holds for the given tree on one side, and any
smaller tree on the other side.
\begin{verbatim}
"height_step2_tr P A sub (dta, dtb) =
((ALL A'. (A', A) : sub --> (ALL a b. a : wfp (measure heightDT) -->
b : wfp (measure heightDT) --> P A' (a, b))) -->
(ALL dtp. (dtp, dta) : measure heightDT --> P A (dtp, dtb)) -->
(ALL dtq. (dtq, dtb) : measure heightDT --> P A (dta, dtq)) -->
P A (dta, dtb))"
\end{verbatim}
In some cases we found that this wasn't enough, and defined a more general
pattern, where the inductive assumption applies where the sum of heights of the
two trees is smaller.
\begin{verbatim}
sumh_step2_tr_eq: "sumh_step2_tr ?P ?A ?sub (?dta, ?dtb) =
((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
(ALL dta' dtb'.
heightDT dta' + heightDT dtb' < heightDT ?dta + heightDT ?dtb -->
?P ?A (dta', dtb')) -->
?P ?A (?dta, ?dtb))"
\end{verbatim}
Each of these properties is successively weaker (inductive assumption is
stronger, ie that $P$ applies to a wider class of trees).
\begin{verbatim}
gs2_tr_height: "gen_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
height_step2_tr ?P ?A ?sub (?dta, ?dtb)"
hs2_sumh: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
sumh_step2_tr ?P ?A ?sub (?dta, ?dtb)"
\end{verbatim}
Accordingly we need the lemma that proving these step results is sufficient
for only the weakest of them.
\begin{verbatim}
sumh_step2_tr_lem: "[| ?A : wfp ?sub;
ALL A dta dtb. sumh_step2_tr ?P A ?sub (dta, dtb) |] ==>
?P ?A (?dta, ?dtb)"
\end{verbatim}