(* Deep embedding of proofs, etc *) GSub1 = GDC + dtseq + instance sequent :: (strsub) seqsub (seq_ident_seq_sub, seq_seq_subs_closed) types pSubst = "(string => string) " fSubst = "(string => formula) " sSubst = "(string => structr) " pfSubst = "(pSubst * fSubst)" pfsSubst = "(pSubst * fSubst) * sSubst" consts I_pf :: "pfSubst" I_pfs :: "pfsSubst" (* formerly had PCSubst, equal to ruleSubst *) seqSubst :: "pfsSubst => structr sequent trf" ruleSubst :: "pfsSubst => structr rule trf" strSubst :: "pfsSubst => structr trf" strsSubst :: "pfsSubst => structr list trf" fmlSubst :: "(pSubst * fSubst) => formula trf" fmlsSubst :: "(pSubst * fSubst) => formula list trf" compsubs :: "pfsSubst => pfsSubst => pfsSubst" 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 (P oo Q) = fmlSubst fs P oo fmlSubst fs Q" "fmlSubst fs (P +++ Q) = fmlSubst fs P +++ fmlSubst fs Q" "fmlSubst fs ( -- Q) = -- fmlSubst fs Q" "fmlSubst fs ( Q ^) = fmlSubst fs Q ^" "fmlSubst fs T = T" "fmlSubst fs F = F" "fmlSubst fs r1 = r1" "fmlSubst fs r0 = r0" 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 (SemiC X Y) = SemiC (strSubst fs X) (strSubst fs Y)" "strSubst fs (Blob Y) = Blob (strSubst fs Y)" "strSubst fs (Star Y) = Star (strSubst fs Y)" "strSubst fs I = I" "strSubst fs E = E" 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 :: "pfSubst => pfSubst => pfSubst" (* 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