(* stuff for Wansing proof of strong normalization / cut elimination *) Wansing2 = Wansing + SN2 + consts cut_subt :: "(dertree => bool) => dertree => dertree => bool" cut_sub1t :: "(dertree => bool) => dertree list => dertree => bool" cut_Subt :: "(dertree => bool) => (dertree * dertree) set" cut_Sub1t :: "(dertree => bool) => (dertree * dertree list) set" subt, isubt, psubt :: "(dertree * dertree) set" sub1t :: "(dertree * dertree list) set" parRed, parRedP, parRedP' :: "dertree => dertree => bool" (* the well-founded relation used for the inductive proof of Lemma 4.10 *) rel410 :: "(dertree * dertree) set" primrec (* relation between proof trees, the second is a subtree of the first, where the rules added below the second to get the first do not include cuts which do not satisfy f *) "cut_subt f (Der seq rule dtl) dt = (dt = Der seq rule dtl | (rule = cutr --> f (Der seq rule dtl)) & cut_sub1t f dtl dt)" "cut_subt f (Unf seq) dt = (dt = Unf seq)" "cut_sub1t f [] dt = False" "cut_sub1t f (h # t) dt = (cut_subt f h dt | cut_sub1t f t dt)" inductive "cut_Subt f" "cut_Sub1t f" intrs cut_Subt_any "(dt, dt) : cut_Subt f" cut_Subt_cutr "[| rule = cutr --> f (Der seq rule dtl) ; (dt, dtl) : cut_Sub1t f |] ==> (dt, Der seq rule dtl) : cut_Subt f" cut_Sub1t_hd "(dt, h) : cut_Subt f ==> (dt, h # t) : cut_Sub1t f" cut_Sub1t_tl "(dt, t) : cut_Sub1t f ==> (dt, h # t) : cut_Sub1t f" inductive "isubt" intrs isubtI "dt : set dtl ==> (dt, Der seq rule dtl) : isubt" defs psubt_def "psubt == isubt^+" subt_def "subt == psubt^=" inductive "sub1t" intrs sub1tI "[| dt : set dtl ; (dts, dt) : subt |] ==> (dts, dtl) : sub1t" (* for a parametric reduction, any cut-subtree dts of the result is either a proper subtree of the original, or has the same cut-formula as the original, but its two premise trees are subtrees* of the premise trees of the original; note *: (1) at least one is a proper subtree (2) this subtree relation disallows instances of cut in between *) (* note - parRedP is wrongly defined, because a new cut may have premise trees one of which is a subtree of the original, with further modifications (changes from A to Y, and further new cuts) *) primrec parRedP_Der "parRedP (Der seq rule dtl) dtn = (rule = cutr & (ALL dts. isSubt dtn dts & botRule dts = cutr --> (isSubt (Der seq cutr dtl) dts & (Der seq cutr dtl) ~= dts) | ((nextUp dts, dtl) : allrel (cut_Subt (%x. False))) & cutForm (Der seq cutr dtl) = cutForm dts & dtl ~= nextUp dts))" "parRedP (Unf seq) dtn = False" primrec parRedP'_Der "parRedP' (Der seq rule dtl) dtn = (rule = cutr & (ALL dts. (dts, dtn) : subt & botRule dts = cutr --> ((dts, Der seq cutr dtl) : psubt) | ((nextUp dts, dtl) : allrel (cut_Subt (%x. False))) & cutForm (Der seq cutr dtl) = cutForm dts & dtl ~= nextUp dts))" "parRedP' (Unf seq) dtn = False" defs rel410_def "rel410 == inv_image (less_than <*lex*> less_than) (%dt. (size (cutForm dt), suml (map ind_size (nextUp dt))))" (* call a cut-(sub)tree a tree with a cut at the bottom; for a C8 reduction, any cut-subtree dts of the result is either a proper subtree of the original, or has a smaller cut-formula *) parRed_def "parRed dt dtn == conclDT dtn = conclDT dt & allDT wfb dtn & allDT (frb rls) dtn & parRedP dt dtn" rules (* the cut formula does not change when you reduce a premise proof tree *) cutForm_nc "(dtl', dtl) : onered ==> cutForm (Der seq cutr dtl) = cutForm (Der seq cutr dtl')" cutReduces_cases "cutReduces dt dtn == (c8red rls dt dtn & dt ~= dtn | parRed dt dtn)" end