(* Deep embedding of proofs, etc *) (* note, at present derivation trees require rule of the same type as the sequents, so doesn't allow for a substitution of the rule which changes type *) GDT = drtree + GSub + consts ruleSubOf :: "'s pstructr sequent dertree => ('s, 's) pfsSubstp" subDT :: "('s, 's) pfsSubstp => 's pstructr sequent dertree => 's pstructr sequent dertree" subDTs :: "('s, 's) pfsSubstp => 's pstructr sequent dertree list => 's pstructr sequent dertree list" primrec ruleSubOf_Der "ruleSubOf (Der seq rule dtl) = (@ fs. (premsRule (ruleSubst fs rule) = map conclDT dtl) & conclRule (ruleSubst fs rule) = seq)" defs subDT_def "subDT sub == subfDT (seqSubst sub)" subDTs_def "subDTs sub == subfDTs (seqSubst sub)" end