theory xrls imports lksyn seq (* for the syntax *) begin consts K :: "formula sequent psc set" K4 :: "formula sequent psc set" S4 :: "formula sequent psc set" S4c :: "formula sequent psc set" GTD :: "formula sequent psc set" s4g :: "(formula => formula set) => formula sequent psc set" Tnc :: "formula sequent psc set" Tsnc :: "formula sequent psc set" lkrefl :: "formula sequent psc set" circ :: "formula sequent psc set" s4cbox :: "formula sequent psc set" inductive "K" intros I : "([X |- {#B#}], mset_map Box X |- {#Box B#}) : K" inductive "K4" intros I : "([mset_map Box X + X |- {#B#}], mset_map Box X |- {#Box B#}) : K4" inductive "GTD" intros I : "A = B | A = Box B ==> ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : GTD" (* generalised S4 rule - encompasses GTD *) inductive "s4g prs" intros I : "A : prs B ==> ([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : s4g prs" inductive "Tnc" (* T rule with no context - note, X is a multiset *) intros I : "([mset_map Box X + X |- {#}], mset_map Box X |- {#}) : Tnc" inductive "Tsnc" (* simpler T rule with no context *) intros I : "([{#A#} |- {#}], {#Box A#} |- {#}) : Tsnc" (* The T/refl rule *) inductive "lkrefl" intros I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl" inductive "S4" intros T : "etrl : extrs Tnc ==> etrl : S4" R4 : "([mset_map Box X |- {#B#}], mset_map Box X |- {#Box B#}) : S4" (* for S4c - has Circ and Box as operators *) consts nkmap :: "nat => formula sequent psc => formula sequent psc" nkmaps :: "formula sequent psc set => formula sequent psc set" boxfmls :: "formula set" msboxfmls :: "formula multiset set" circrel :: "formula relation => formula relation" defs nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))" inductive "nkmaps rls" intros I : "rl : rls ==> nkmap k rl : nkmaps rls" inductive "circrel r" intros I : "(sf, f) : r ==> (funpow Circ k sf, funpow Circ k f) : circrel r" inductive "boxfmls" intros I : "funpow Circ k (Box B) : boxfmls" inductive "msboxfmls" intros I : "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls" inductive "circ" intros I : "([seq], seqmap Circ seq) : circ" inductive "s4cbox" intros boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cbox" inductive "S4c" intros T : "etrl : extrs Tsnc ==> etrl : S4c" circI : "([seq], seqmap Circ seq) : S4c" boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : S4c" end