(* the replacement relation *) HOL_Cut = HOL_DT + (* note - putting HOL_Rls first seems to get the right version of cut, otherwise you get the constant cut from WF.thy *) consts (* note - these predicates are false on (Unf sequent) *) isCut :: "dertree => bool" notCut :: "dertree => bool" cutIsLP :: "formula => dertree => bool" cutIsRP :: "formula => dertree => bool" cutIsLRP :: "formula => dertree => bool" cutLPcf :: "dertree => bool" cutRPcf :: "dertree => bool" cutLRPcf :: "dertree => bool" cutOnFmls :: "formula set => dertree => bool" cutOnFmls_r :: "formula set => dertree set" cutOnFmls_l :: "formula set => dertree => bool" rootIsAntP :: "dertree => bool" rootIsSucP :: "dertree => bool" cutForm :: "dertree => formula" (* the cut-formula of a well-formed tree rooted in cut *) primrec cutForm_Der "cutForm (Der seq rule dtl) = form_of (succ (conclDT (hd dtl)))" inductive "cutOnFmls_r fmls" intrs cutOnFmls_r_nc "rule ~= cutr ==> Der seq rule dtl : cutOnFmls_r fmls" cutOnFmls_r_cut "[| conclDT pr = (fml |- $suc) ; fml : fmls |] ==> Der seq cutr [pl, pr] : cutOnFmls_r fmls" primrec cutOnFmls_Unf "cutOnFmls fmls (Unf sequent) = False" cutOnFmls_Der "cutOnFmls fmls (Der seq rule dtl) = (rule ~= cutr | (EX pl pr suc fml . fml : fmls & dtl = [pl, pr] & conclDT pr = (Sequent (Structform fml) suc)))" primrec "cutOnFmls_l fmls (Unf sequent) = False" "cutOnFmls_l fmls (Der seq rule dtl) = (rule ~= cutr | (EX pl pr ant fml . fml : fmls & dtl = [pl, pr] & conclDT pl = (Sequent ant (Structform fml))))" primrec cutIsLP_Unf "cutIsLP fml (Unf sequent) = False" cutIsLP_Der "cutIsLP fml (Der seq rule dtl) = (rule ~= cutr | (EX pr ant rule' dtl' fml' rant. dtl = [Der (Sequent ant (Structform fml)) rule' dtl', pr] & conclRule rule' = Sequent rant (Structform fml')))" primrec cutIsRP_Unf "cutIsRP fml (Unf sequent) = False" cutIsRP_Der "cutIsRP fml (Der seq rule dtl) = (rule ~= cutr | (EX pl suc rule' dtl' fml' rsuc. dtl = [pl, Der (Sequent (Structform fml) suc) rule' dtl'] & conclRule rule' = Sequent (Structform fml') rsuc))" primrec rootIsAntP_Unf "rootIsAntP (Unf sequent) = False" rootIsAntP_Der "rootIsAntP (Der seq rule dtl) = strIsFml (antec (conclRule rule))" primrec rootIsSucP_Unf "rootIsSucP (Unf sequent) = False" rootIsSucP_Der "rootIsSucP (Der seq rule dtl) = strIsFml (succ (conclRule rule))" defs cutIsLRP_def "cutIsLRP fml dt == (cutIsLP fml dt & cutIsRP fml dt)" primrec cutLPcf_Der "cutLPcf (Der seq rule dtl) = rootIsSucP (hd dtl)" primrec cutRPcf_Der "cutRPcf (Der seq rule dtl) = rootIsAntP (hd (tl dtl))" defs cutLRPcf_def "cutLRPcf dt == cutLPcf dt & cutRPcf dt" primrec isCut_Unf "isCut (Unf sequent) = False" isCut_Der "isCut (Der seq rule dtl) = (rule = cutr)" primrec "notCut (Unf sequent) = False" "notCut (Der seq rule dtl) = (rule ~= cutr)" end