(* some equivalents of theory ctr, but for
left weakening and contraction only,
for a logic with singletons on the right *)
theory lctr imports ctr begin
consts
lctr_adm :: "'a sequent psc set => 'a => bool"
lctr_admd :: "'a sequent set => 'a => bool"
lid_adm :: "'a sequent psc set => bool"
lext_concl :: "'a sequent psc set => bool"
lext_concl_rl :: "'a sequent psc set => 'a sequent psc => bool"
defs
(* left contraction admissibility for formula A ;
if A,A,X |- Y is derivable, then so is A,X |- Y *)
lctr_admd_def : "lctr_admd derivs A ==
ALL XY. ctr_adm_seq derivs XY ({#A#} |- 0)"
lctr_adm_def' : "lctr_adm rls A == lctr_admd (derrec rls {}) A"
(* can extend conclusions : suffices for admissibility of weakening *)
primrec
"lext_concl_rl rls (ps, c) =
(ALL A. EX ps'. (ps', c + (A |- 0)) : rls &
(ps, ps') : allrel {(X |- Y, X' |- Y) | X X' Y. X' >= X})"
defs
lext_concl_def' :
"lext_concl rls == ALL (ps, c) : rls. lext_concl_rl rls (ps, c)"
(* admissibility of weakened axiom *)
lid_adm_def :
"lid_adm rls == ALL A X. A :# X --> (X |- {#A#}) : derrec rls {}"
end