(* results to do with (left) consecution calculi *)
bdlcons = bdseq +
consts
(* multicut, single cut admissibilty property *)
mclca, mclcd :: "('f structr, 'f) sequent psc set => 'f =>
('f structr, 'f) sequent pair => bool"
strrep :: "'f structr pair set => 'f structr pair set"
primrec
mclca "mclca rls A (cl, cr) =
(cl : derrec rls {} --> cr : derrec rls {} --> mclcd rls A (cl, cr))"
(* the (multi-)cut admissibility property we want needs to be that
we can replace each of multiple instances of the cut-formula in the
antecedent of the rh premise by a copy of the structure which is
the antecedent of the lh premise *)
(* note - this doesn't mean replacing all copies *)
inductive "strrep S"
intrs
same "(s, s) : strrep S"
repl "p : S ==> p : strrep S"
sc "(u, v) : strrep S ==> (x, y) : strrep S ==> (u; x, v; y) : strrep S"
primrec
mclcd "mclcd rls A (cl, cr) = (ALL Xl Xr Y B.
cl = (Xl |- A) --> cr = (Xr |- B) -->
(Xr, Y) : strrep {(Sf A, Xl)} --> (Y |- B) : derrec rls {})"
(* evaluation of structure *)
consts
(* evaluation of a structure, not a function because only partial *)
astr_eval :: "((formula * formula) structr * formula) set"
(* annotation of structure with formulae from set (eg, theorems) *)
str_ann :: "formula set =>
(formula structr * (formula * formula) structr) set"
(* we will try using T -> (A -> A) as the annotation for T *)
inductive "astr_eval"
intrs
evmp "(lstr, A -> B) : astr_eval ==> (rstr, A) : astr_eval ==>
(lstr; rstr, B) : astr_eval"
evmpp "(Sf (A -> B, A), B) : astr_eval"
inductive "str_ann combs"
intrs
sc "(sl, sla) : str_ann combs ==> (sr, sra) : str_ann combs ==>
(sl; sr, sla; sra) : str_ann combs"
comb "c : combs ==> (Sf s, Sf (c, s)) : str_ann combs"
end