theory gl imports glgen
begin
(* listing of rules, logic with two separate or-right and and-left rules,
ie |- A |- B A |- B |-
---------- ---------- --------- ---------
|- A v B |- A v B A & B |- A & B |-
*)
consts
(* some admissible rules *)
bbbcf :: "formula multiset => formula multiset =>
formula sequent => formula sequent"
bbirsf :: "formula => formula sequent => formula sequent"
bbelsf :: "formula => formula sequent => formula sequent"
bblblf :: "formula multiset => formula multiset =>
formula sequent => formula sequent"
primrec
defn : "bbirsf D (X |- Y) = (X |- mins (Box (Box D)) (ms_delete {Box D} Y))"
primrec
defn : "bbelsf D (X |- Y) = (mins (Box D) (ms_delete {Box (Box D)} X) |- Y)"
defs
bblblf_def : "bblblf Bs Cs ==
etr (mset_map Box Cs |- 0) (mset_map Box Bs |- 0)"
defs
bbbcf_def : "bbbcf Bs Cs == etr (Cs |- 0) (Bs |- 0)"
end