drtsub = drtree + dtrule +
(* stuff involving derivation trees and sets of substitutions,
but not dependent on specific definition of structures *)
consts
rulefsg_1 :: "'seq trf set => 'seq psc => 'seq psc set"
rulefsg :: "'seq trf set => 'seq psc set trf"
inductive "rulefsg subs rls"
intrs
iisubI "r : rls ==> sub : subs ==> (pscmap sub r) : rulefsg subs rls"
defs
rulefsg_1_def "rulefsg_1 subs r == rulefsg subs {r}"
(* version of above involving type class,
since we only ever use one set of substitutions *)
consts
all_seq_subs :: "'seq trf set"
axclass seqsub < type
ident_seq_sub "id : all_seq_subs"
seq_subs_closed
"f : all_seq_subs ==> g : all_seq_subs ==> g o f : all_seq_subs"
consts
rulefsc_1 :: "'seq psc => 'seq psc set"
rulefsc :: "'seq psc set trf"
inductive "rulefsc rls"
intrs
iisubI "r : rls ==> sub : all_seq_subs ==> (pscmap sub r) : rulefsc rls"
defs
rulefsc_1_def "rulefsc_1 r == rulefsc {r}"
(* now try the above with the same name as before *)
consts
rulefs_1 :: "'seq psc => 'seq psc set"
rulefs :: "'seq psc set trf"
inductive "rulefs rls"
intrs
iisubIa "r : rls ==> sub : all_seq_subs ==> (pscmap sub r) : rulefs rls"
defs
rulefs_1_def "rulefs_1 r == rulefs {r}"
consts
wfb :: "'seq :: seqsub dertree => bool"
valid :: "'seq :: seqsub psc set => 'seq dertree => bool"
primrec (* changed from previous work *)
wfb_Unf "wfb (Unf seq) = True"
wfb_Der "wfb (Der seq rule dtl) = ((map conclDT dtl, seq) : rulefs {rule})"
(*
wfb_Der "wfb (Der seq rule dtl) =
(? inst : rulefs {rule}. premsRule inst = map conclDT dtl &
conclRule inst = seq)"
*)
defs
valid_def "valid rules dt ==
allDT wfb dt & allDT (frb rules) dt & premsDT dt = []"
consts
(* a particular derived rule (set of premises and conclusion)
is derivable from a rule set *)
IsDerivable :: "'seq :: seqsub psc set => 'seq psc => bool"
IsDerivableR :: "'seq :: seqsub psc set => ['seq set, 'seq] => bool"
IsDerivableRs :: "'seq :: seqsub psc set => ['seq set, 'seq list] => bool"
derivableR :: "'seq :: seqsub psc set => 'seq set => 'seq set"
derivableRs :: "'seq :: seqsub psc set => 'seq set => 'seq list set"
(* a particular derived bidirectional rule is derivable from a rule set *)
IsDerivableB :: "'seq :: seqsub psc set => ['seq, 'seq] => bool"
defs
IsDerivableR_def "IsDerivableR rules prems concl == (? dtr.
allDT (frb rules) dtr & allDT wfb dtr &
conclDT dtr = concl & set (premsDT dtr) <= prems)"
IsDerivableRs_def "IsDerivableRs rules prems concls == (? dtrs.
allDTs (frb rules) dtrs & allDTs wfb dtrs &
map conclDT dtrs = concls & set (premsDTs dtrs) <= prems)"
IsDerivableB_def "IsDerivableB rules prem concl ==
IsDerivableR rules {prem} concl"
defs (* these definitions use rulefs *)
derivableR_def "derivableR rules == derrec (rulefs rules)"
derivableRs_def "derivableRs rules == dersrec (rulefs rules)"
primrec
(* a derived rule is derivable from a set of rules,
note - this is in a more general sense where the derived rule may
contain extra and reordered premises *)
IsDerivable_def "IsDerivable rules (Pair prems concl) =
IsDerivableR rules (set prems) concl"
consts
inv_rules :: "'seq :: seqsub psc set => bool"
inv_rules2 :: "'seq :: seqsub psc set => 'seq :: seqsub psc set => bool"
bi_inv_rules :: "'seq :: seqsub psc set => 'seq :: seqsub psc set => bool"
defs
inv_rules_def "inv_rules rules ==
(ALL r : rules. EX p. premsRule r = [p] &
([conclRule r], p) : derl (rulefs rules))"
inv_rules2_def "inv_rules2 rules rrules ==
(ALL r : rules. EX p c. r = ([p], c) & ([c], p) : derl (rulefs rrules))"
bi_inv_rules_def "bi_inv_rules rules rrules ==
inv_rules2 rules rrules & inv_rules2 rrules rules"
end