(* seq.thy
Sequent Calculi under Isabelle/HOL, deep embedding of sequents
using multisets
*)
theory seqgen imports MS pmgl begin
datatype 'a sequent = Sequent "'a multiset" "'a multiset"
("((_)/ |- (_))" [6,6] 5)
instance sequent :: (type) zero
by intro_classes ;
instance sequent :: (type) plus
by intro_classes ;
instance sequent :: (type) minus
by intro_classes ;
instance sequent :: (type) ord
by intro_classes ;
instance sequent :: (type) leq
by intro_classes ;
consts
(* map both sides of s sequent *)
seqmap :: "('a => 'b) => 'a sequent => 'b sequent"
(* extend a sequent by adding context to conclusion and premises *)
extend :: "'a sequent => 'a sequent => 'a sequent"
(* extend a set of rules *)
extrs :: "'a sequent psc set => 'a sequent psc set"
iextrs :: "'a sequent psc set => 'a sequent psc set"
extrsl :: "'a sequent psc set => 'a sequent psc set"
extcs :: "'a sequent psc set => 'a sequent psc set"
iextcs :: "'a sequent psc set => 'a sequent psc set"
antec :: "'a sequent => 'a multiset"
succ :: "'a sequent => 'a multiset"
ms_of_seq :: "'a sequent => 'a multiset"
seq_size :: "'a sequent => nat"
seq_filter :: "('a => bool) => 'a sequent => 'a sequent"
seq_delete :: "'a sequent => 'a sequent => 'a sequent"
ms_mem :: "'a => 'a sequent => bool"
seqid :: "'a sequent set"
iscrls :: "'a sequent psc set"
scrls :: "'a sequent psc set" (* single-conclusion rules *)
idrls :: "'a sequent psc set" (* axiom, or identity, rules *)
wkrls :: "'a sequent psc set" (* weakening rules *)
ctrrls :: "'a => 'a sequent psc set" (* contraction rules *)
seq_singles :: "'a sequent => 'a sequent"
unique_concl :: "'a psc set => bool"
primrec
seqmap_def : "seqmap f (a |- s) = (mset_map f a |- mset_map f s)"
primrec antec_def : "antec (Sequent ant suc) = ant"
primrec succ_def : "succ (Sequent ant suc) = suc"
primrec ms_of_seq_def : "ms_of_seq (Sequent ant suc) = ant + suc"
primrec
"seq_filter p (Sequent ant suc) = (ms_filter p ant |- ms_filter p suc)"
(* note - seq_delete deletes occurrences of formulae on each side separately *)
primrec
"seq_delete dseq (ant |- suc) =
(ms_delete (set_of (antec dseq)) ant |- ms_delete (set_of (succ dseq)) suc)"
primrec
"seq_singles (X |- Y) = (singles (set_of X) |- singles (set_of Y))"
defs
seq_leq_def : "z [= y == (z :: 'a sequent) <= y"
ms_mem_def : "ms_mem a seq == a :# ms_of_seq seq"
primrec (* uses multiset size *)
seq_size_def : "seq_size (Sequent ant suc) = size ant + size suc"
defs
seq_plus_def : "seq + fmls ==
Sequent (antec seq + antec fmls) (succ seq + succ fmls)"
seq_minus_def : "seq - fmls ==
Sequent (antec seq - antec fmls) (succ seq - succ fmls)"
seq_zero_def : "0 == Sequent 0 0"
seq_le_def : "seq <= fmls ==
(antec seq <= antec fmls) & (succ seq <= succ fmls)"
seq_less_def : "seq < fmls == seq <= fmls & seq ~= (fmls::'a sequent)"
constdefs
seq_join :: "'a sequent => 'a sequent => 'a sequent"
"seq_join seq (fmls::'a sequent) ==
ms_join (antec seq) (antec fmls) |- ms_join (succ seq) (succ fmls)"
seq_meet :: "'a sequent => 'a sequent => 'a sequent"
"seq_meet seq (fmls::'a sequent) ==
ms_meet (antec seq) (antec fmls) |- ms_meet (succ seq) (succ fmls)"
defs
extend_def : "extend fmls seq == seq + fmls"
(* common rules *)
inductive "seqid"
intros
I : "({#A#} |- {#A#}) : seqid"
inductive "wkrls"
intros
L : "([0], {#A#} |- {#}) : wkrls"
R : "([0], {#} |- {#A#}) : wkrls"
inductive "ctrrls A"
intros
L : "([{#A#} + {#A#} |- {#}], {#A#} |- {#}) : ctrrls A"
R : "([{#} |- {#A#} + {#A#}], {#} |- {#A#}) : ctrrls A"
(* set of rules : axiom (A |- A) or rules with a single (principal) formula
in conclusion (can be extended using extrs) *)
inductive "iscrls" (* single conclusion rules, and identity *)
intros
idI : "rl : idrls ==> rl : iscrls"
s1I : "rl : scrls ==> rl : iscrls"
inductive "scrls" (* single conclusion rules *)
intros
I : "seq_size c = 1 ==> (ps, c) : scrls"
(* single conclusion rules, and identity, former definition
inductive "iscrls"
intros
idI : "([], {#A#} |- {#A#}) : scrls"
s1I : "seq_size c = 1 ==> (ps, c) : scrls"
*)
inductive "idrls" (* identity rules *)
intros
I : "([], {#A#} |- {#A#}) : idrls"
(* pscmap (extend (fl, fr)) : extend a sequent rule by adding formulae
(fl, fr) to the (left, right) of the conclusion and each premise ;
extcs : extend conclusion of each rule only
iextcs : extend conclusion of each rule on left only
extrs : extend each rule thus (for any (fl, fr))
iextrs : extend each rule (premises and conclusion) on left only
extrsl : extend premises on the left only, conclusion both sides *)
inductive "extcs rules"
intros
I : "(ps, c) : rules ==> (ps, extend flr c) = epsc ==> epsc : extcs rules"
inductive "iextcs rules"
intros
I : "(ps, c) : rules ==> (ps, extend (fl |- 0) c) = epsc ==>
epsc : iextcs rules"
inductive "extrs rules"
intros
I : "psc : rules ==> pscmap (extend flr) psc = epsc ==> epsc : extrs rules"
inductive "iextrs rules"
intros
I : "psc : rules ==> pscmap (extend (fl |- 0)) psc = epsc ==>
epsc : iextrs rules"
inductive "extrsl rules"
intros
I : "(ps, c) : rules ==> (map (extend (Sequent fl 0)) ps,
extend (Sequent fl fr) c) = epsc ==> epsc : extrsl rules"
defs
(* unique conclusion property :
two different rules have different conclusions *)
unique_concl_def : "unique_concl rls ==
(ALL qs qs' d. (qs, d): rls & (qs', d): rls --> qs = qs')"
end