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