(* Deep embedding of proofs, etc *) GSub = GSub2 + types ssdertree = structr sequent dertree consts pFind :: "(string * string) list => string => string" fFind :: "(string * formula) list => string => formula" sFind :: "(string * structr) list => string => structr" defSubs :: "string list => sSubst => sSubst => sSubst" strCtnsFml :: "structr => bool" strsCtnsFml :: "structr list => bool" seqCtnsFml :: "structr sequent => bool" fmlCtnsFV :: "formula => bool" fmlsCtnsFV :: "formula list => bool" strIsFml :: "structr => bool" seqNoSSF :: "structr sequent => bool" seqFmls :: "structr sequent => formula list" strFmls :: "structr => formula list" strsFmls :: "structr list => formula list" fmlFVPPs :: "formula => formula set" strFVPPs :: "structr => formula set" seqFVPPs :: "structr sequent => formula set" seqSVs :: "structr sequent => string list" strSVs :: "structr => string list" strsSVs :: "structr list => string list" seqSVs' :: "bool => structr sequent => string list" strSVs' :: "bool => structr => string list" strsSVs' :: "bool => [structr list, bool list] => string list" seqSVs'' :: "structr sequent => string list" strSVs'' :: "structr => string list" bprops, C3, C4, C5 :: "structr rule => bool" C345 :: "structr rule set => bool" cprops :: "structr sequent => bool" (* all occurrences of SV s are in antecedent (succedent) position in sequent or positive or negative position in structure *) allSA :: "bool => string => structr sequent => bool" allPN :: "bool => string => structr => bool" allsPN :: "bool => string => [structr list, bool list] => bool" primrec pFind_Nil "pFind [] str = str" pFind_Cons "pFind (sf # sfs) str = (if fst sf = str then snd sf else pFind sfs str)" primrec fFind_Nil "fFind [] str = FV str" fFind_Cons "fFind (sf # sfs) str = (if fst sf = str then snd sf else fFind sfs str)" primrec sFind_Nil "sFind [] str = SV str" sFind_Cons "sFind (sf # sfs) str = (if fst sf = str then snd sf else sFind sfs str)" primrec "fmlFVPPs (P && Q) = fmlFVPPs P Un fmlFVPPs Q" "fmlFVPPs (P v Q) = fmlFVPPs P Un fmlFVPPs Q" "fmlFVPPs (P oo Q) = fmlFVPPs P Un fmlFVPPs Q" "fmlFVPPs (P +++ Q) = fmlFVPPs P Un fmlFVPPs Q" "fmlFVPPs ( -- Q) = fmlFVPPs Q" "fmlFVPPs ( Q ^) = fmlFVPPs Q" "fmlFVPPs T = {}" "fmlFVPPs F = {}" "fmlFVPPs r1 = {}" "fmlFVPPs r0 = {}" fml "fmlFVPPs (FV str) = {FV str}" "fmlFVPPs (PP str) = {PP str}" defs (* defSubs_def "defSubs strl sub1 sub2 == [ss:sub1. fst ss mem strl] @ [ss':sub2. ~ fst ss' mem strl]" *) defSubs_def "defSubs strl sub1 sub2 ss == if ss : set strl then sub1 ss else sub2 ss" primrec "strCtnsFml (Comma X Y) = ((strCtnsFml X) | (strCtnsFml Y))" "strCtnsFml (SemiC X Y) = ((strCtnsFml X) | (strCtnsFml Y))" "strCtnsFml (Blob Y) = (strCtnsFml Y)" "strCtnsFml (Star Y) = (strCtnsFml Y)" "strCtnsFml I = False" "strCtnsFml E = False" "strCtnsFml (SV str) = False" "strCtnsFml (Structform fml) = True" primrec "seqCtnsFml (Sequent X Y) = ((strCtnsFml X) | (strCtnsFml Y))" primrec "strIsFml (Comma X Y) = False" "strIsFml (SemiC X Y) = False" "strIsFml (Blob Y) = False" "strIsFml (Star Y) = False" "strIsFml I = False" "strIsFml E = False" "strIsFml (SV str) = False" "strIsFml (Structform fml) = True" primrec "fmlCtnsFV (P && Q) = (fmlCtnsFV P | fmlCtnsFV Q)" "fmlCtnsFV (P v Q) = (fmlCtnsFV P | fmlCtnsFV Q)" "fmlCtnsFV (P oo Q) = (fmlCtnsFV P | fmlCtnsFV Q)" "fmlCtnsFV (P +++ Q) = (fmlCtnsFV P | fmlCtnsFV Q)" "fmlCtnsFV ( -- Q) = fmlCtnsFV Q" "fmlCtnsFV ( Q ^) = fmlCtnsFV Q" "fmlCtnsFV T = False" "fmlCtnsFV F = False" "fmlCtnsFV r1 = False" "fmlCtnsFV r0 = False" "fmlCtnsFV (FV str) = True" "fmlCtnsFV (PP str) = False" (* seqNoSSF : indicates whether a sequent has no substructure which is a formula, ie, true if, whenever one side of the turnstile contains a formula, then the whole of that side is a formula ; *) primrec seqNoSSF_def "seqNoSSF (Sequent ant suc) = ((strIsFml ant | ~ strCtnsFml ant) & (strIsFml suc | ~ strCtnsFml suc))" (* strFmls, seqFmls : get list of formulae in structure or sequent *) primrec "strFmls (Comma X Y) = ((strFmls X) @ (strFmls Y))" "strFmls (SemiC X Y) = ((strFmls X) @ (strFmls Y))" "strFmls (Blob Y) = (strFmls Y)" "strFmls (Star Y) = (strFmls Y)" "strFmls I = []" "strFmls E = []" "strFmls (SV str) = []" "strFmls (Structform fml) = [fml]" primrec seqFmls_def "seqFmls (Sequent ant suc) = (strFmls ant @ strFmls suc)" defs strFVPPs_def "strFVPPs str == UNION (set (strFmls str)) fmlFVPPs" primrec seqFVPPs_def "seqFVPPs ($X |- $Y) = (strFVPPs X Un strFVPPs Y)" (* strSVs, seqSVs : get list of structure variables in structure or sequent strSVs', seqSVs' : ditto, in succedent or antecedent positions *) primrec "strSVs (Comma X Y) = ((strSVs X) @ (strSVs Y))" "strSVs (SemiC X Y) = ((strSVs X) @ (strSVs Y))" "strSVs (Blob Y) = (strSVs Y)" "strSVs (Star Y) = (strSVs Y)" "strSVs I = []" "strSVs E = []" "strSVs (SV str) = [str]" "strSVs (Structform fml) = []" primrec seqSVs_def "seqSVs (Sequent ant suc) = (strSVs ant @ strSVs suc)" primrec "strSVs' pn (Comma X Y) = ((strSVs' pn X) @ (strSVs' pn Y))" "strSVs' pn (SemiC X Y) = ((strSVs' pn X) @ (strSVs' pn Y))" "strSVs' pn (Blob Y) = (strSVs' pn Y)" "strSVs' pn (Star Y) = (strSVs' (~pn) Y)" "strSVs' pn I = []" "strSVs' pn E = []" "strSVs' pn (SV str) = (if pn then [str] else [])" "strSVs' pn (Structform fml) = []" primrec seqSVs'_def "seqSVs' sa (Sequent ant suc) = (strSVs' (~sa) ant @ strSVs' sa suc)" defs seqSVs''_def "seqSVs'' seq == seqSVs' True seq @ seqSVs' False seq" strSVs''_def "strSVs'' str == strSVs' True str @ strSVs' False str" bprops_def "bprops rule == C3 rule & C4 rule & C5 rule" C3_def "C3 rule == distinct (seqSVs (conclRule rule))" C4_def "C4 rule == (ALL prem:set (premsRule rule). ALL b. ALL s:set (seqSVs' b (conclRule rule)). s ~: set (seqSVs' (~ b) prem))" C5_def "C5 rule == seqNoSSF (conclRule rule)" C345_def "C345 rules == ALL rule. rule : rules --> bprops rule" (* properties of the conclusion of a rule *) cprops_def "cprops seq == distinct (seqSVs seq) & seqNoSSF seq" primrec (* allPN True/False s st means all occurrences of SV s are in a positive/negative position within structure st *) "allPN b s (Comma X Y) = (allPN b s X & allPN b s Y)" "allPN b s (SemiC X Y) = (allPN b s X & allPN b s Y)" "allPN b s (Blob Y) = (allPN b s Y)" "allPN b s (Star Y) = (allPN (~b) s Y)" "allPN b s I = True" "allPN b s E = True" "allPN b s (SV str) = (if str = s then b else True)" "allPN b s (Structform fml) = True" primrec (* allSA True/False s seq means all occurrences of SV s are in a succedent/antecedent position within sequent seq *) allSA_def "allSA b s (Sequent ant suc) = (allPN (~b) s ant & allPN b s suc)" end