(* Deep embedding of proofs, etc *) GSub1 = GDC + dtseq + instance sequent :: (strsub) seqsub (seq_ident_seq_sub, seq_seq_subs_closed) types ('s, 't) pSubstp = "'s => 't" ('s, 't) fSubstp = "'s => 't pformula" ('s, 't) sSubstp = "'s => 't pstructr" ('s, 't) pfSubstp = "('s, 't) pSubstp * ('s, 't) fSubstp" ('s, 't) pfsSubstp = "('s, 't) pfSubstp * ('s, 't) sSubstp" pSubst = "string => string" fSubst = "string => string pformula" sSubst = "string => string pstructr" pfSubst = "pSubst * fSubst" pfsSubst = "pfSubst * sSubst" consts I_pf :: "('s, 's) pfSubstp" I_pfs :: "('s, 's) pfsSubstp" (* formerly had PCSubst, equal to ruleSubst *) seqSubst :: "('s, 't) pfsSubstp => 's pstructr sequent => 't pstructr sequent" ruleSubst :: "('s, 't) pfsSubstp => 's pstructr rule => 't pstructr rule" strSubst :: "('s, 't) pfsSubstp => 's pstructr => 't pstructr" strsSubst :: "('s, 't) pfsSubstp => 's pstructr list => 't pstructr list" fmlSubst :: "('s, 't) pfSubstp => 's pformula => 't pformula" fmlsSubst :: "('s, 't) pfSubstp => 's pformula list => 't pformula list" compsubs :: "('s, 't) pfsSubstp => ('t, 'u) pfsSubstp => ('s, 'u) pfsSubstp" defs I_pf_def "I_pf == (%x. x, FV)" I_pfs_def "I_pfs == (I_pf, SV)" primrec "fmlSubst fs (P && Q) = fmlSubst fs P && fmlSubst fs Q" "fmlSubst fs (P v Q) = fmlSubst fs P v fmlSubst fs Q" "fmlSubst fs ( -- Q) = -- fmlSubst fs Q" "fmlSubst fs T = T" "fmlSubst fs F = F" fmlSubst_FV "fmlSubst fs (FV str) = (snd fs) str" "fmlSubst fs (PP str) = PP ((fst fs) str)" primrec "strSubst fs (Comma X Y) = Comma (strSubst fs X) (strSubst fs Y)" "strSubst fs (Star Y) = Star (strSubst fs Y)" "strSubst fs I = I" strSubst_SV "strSubst fss (SV str) = (snd fss) str" "strSubst fss (Structform fml) = Structform (fmlSubst (fst fss) fml)" primrec seqSubst_def "seqSubst fs (Sequent ant suc) = Sequent (strSubst fs ant) (strSubst fs suc)" primrec ruleSubst_Pair "ruleSubst fs (Pair prems concl) = Pair (map (seqSubst fs) prems) (seqSubst fs concl)" constdefs compsubfml :: "('s, 't) pfSubstp => ('t, 'u) pfSubstp => ('s, 'u) pfSubstp" (* don't use this, proof not so easy "compsubfml fs1 fs2 == map (% (str, rep). (str, fmlSubst fs2 rep)) fs1 @ fs2" *) (* "compsubfml fs1 fs2 == (compsubpp (fst fs1) (fst fs2), map (% fsub. (fst fsub, fmlSubst fs2 (snd fsub))) (snd fs1) @ (snd fs2))" *) "compsubfml fs1 fs2 == ((fst fs2) o (fst fs1), fmlSubst fs2 o snd fs1)" primrec (* "compsubs (fs1, ss1) subs2 = (compsubfml fs1 (fst subs2), map (% ssub. (fst ssub, strSubst subs2 (snd ssub))) ss1 @ snd subs2)" *) "compsubs (fs1, ss1) subs2 = (compsubfml fs1 (fst subs2), strSubst subs2 o ss1)" defs all_str_subs_def "all_str_subs == range strSubst" end