open RP ; context RP.thy ; val g = goal RP.thy ; val gw = goalw RP.thy ; val oss = [mLP'_Der, mRP'_Der, mLP_Der, mRP_Der] ; Delsimps oss ; val () = qed_goal "mLP_Der'" RP.thy "mLP dtAY seqY (Der seqA rule dtlA) = \ \ (if strIsFml (succ (conclRule rule)) & succ seqA ~= succ seqY then \ \ let seqYA = Sequent (antec seqY) (succ seqA) \ \ in Der seqY cutr [mLP' dtAY seqYA (Der seqA rule dtlA), dtAY] \ \ else mLP' dtAY seqY (Der seqA rule dtlA))" (fn _ => [ (simp_tac (esimps (Let_def :: oss)) 1)]) ; val () = qed_goal "mRP_Der'" RP.thy "mRP dtAY seqY (Der seqA rule dtlA) = \ \ (if strIsFml (antec (conclRule rule)) & antec seqA ~= antec seqY then \ \ let seqYA = Sequent (antec seqA) (succ seqY) \ \ in Der seqY cutr [dtAY, mRP' dtAY seqYA (Der seqA rule dtlA)] \ \ else mRP' dtAY seqY (Der seqA rule dtlA))" (fn _ => [ (simp_tac (esimps (Let_def :: oss)) 1)]) ; (* converting mXP rules to mLP or mRP *) val mXPsimps = (thms "mXP.simps" @ thms "mXP'.simps" @ thms "mXPs.simps") ; local val ss = map mk_meta_eq mXPsimps ; fun X2L_R pn thm = rewrite_rule ss (read_instantiate [("pn", pn)] thm) ; in val X2L = X2L_R "True" ; val X2R = X2L_R "False" ; fun X2LR thm = [X2L thm, X2R thm] ; end ; (* simplifications of mXP', mXPs, as though defined like mLP', mLPs etc *) val () = qed_goal "mXP'_Der" RP.thy "mXP' pn dtAY seqY (Der seqA rule dtlA) = \ \ (let sub = newSub (Der seqA rule dtlA) seqY ; \ \ premsinst = premsRule (ruleSubst sub rule) \ \ in Der seqY rule (mXPs pn dtAY premsinst dtlA))" (fn _ => [(case_tac "pn" 1), (ALLGOALS (asm_simp_tac (esimps [mLP'_Der, mRP'_Der])))]) ; val () = qed_goal "mXP_Unf" RP.thy "mXP pn dtAY seqY (Unf seqA) = Unf seqY" (fn _ => [(case_tac "pn" 1), (ALLGOALS Asm_simp_tac)]) ; val () = qed_goal "mXP'_Unf" RP.thy "mXP' pn dtAY seqY (Unf seqA) = Unf seqY" (fn _ => [(case_tac "pn" 1), (ALLGOALS Asm_simp_tac)]) ; val () = qed_goal "mXPs_Nil" RP.thy "mXPs pn dtAY prems [] = []" (fn _ => [(case_tac "pn" 1), (ALLGOALS Asm_simp_tac)]) ; val () = qed_goal "mXPs_Cons" RP.thy "mXPs pn dtAY prems (h # t) = \ \ mXP pn dtAY (hd prems) h # mXPs pn dtAY (tl prems) t" (fn _ => [(case_tac "pn" 1), (ALLGOALS Asm_simp_tac)]) ; (** conclusion of modified tree is sequent given as argument **) (* note - following is to ensure we do not use actual defn of newSub, just certain properties *) val nss = [Let_def, mLP'_Der, mRP'_Der, mLP_Der', mRP_Der'] ; Delsimps [newSub_Der] ; Addsimps [mXP'_Unf, mXP_Unf, mXPs_Nil, mXPs_Cons] ; val () = qed_goal "concl_mXP'" RP.thy "conclDT (mXP' pn dtAY seqY dt) = seqY" (fn _ => [(case_tac "dt" 1), (ALLGOALS (asm_simp_tac (esimps [mXP'_Der, Let_def])))]) ; val () = qed_goal "concl_mXP" RP.thy "conclDT (mXP pn dtAY seqY dt) = seqY" (fn _ => [((case_tac "pn" THEN_ALL_NEW case_tac "dt") 1), (ALLGOALS (asm_simp_tac (esimps nss)))]) ; val concl_mXPs = store_thm ("concl_mXPs", meta_std (prove_goal RP.thy "ALL seqYs. length seqYs = length dts --> \ \ map conclDT (mXPs pn dtAY seqYs dts) = seqYs" (fn _ => [(induct_tac "dts" 1), ALLGOALS Simp_tac, Auto_tac, (case_tac "seqYs" 1), ALLGOALS Asm_full_simp_tac, (rtac concl_mXP 1)]))) ; (** if tree has no premises then so does modified tree **) val () = qed_goal_spec_mp "prems_mXPs" RP.thy "ALL seqYs. (ALL dt:set dtl. ALL seqY. premsDT (mXP pn dtAY seqY dt) = []) \ \ --> premsDTs (mXPs pn dtAY seqYs dtl) = []" (fn _ => [ (induct_tac "dtl" 1), Simp_tac 1, Asm_simp_tac 1]) ; val [concl_mLPs, concl_mRPs] = X2LR concl_mXPs ; val [concl_mLP', concl_mRP'] = X2LR concl_mXP' ; val [concl_mLP, concl_mRP] = X2LR concl_mXP ; val [prems_mLPs, prems_mRPs] = X2LR prems_mXPs ; val noPrems_mXP = store_thm ("noPrems_mXP", (standard o meta_std) (prove_goal RP.thy "(ALL seqY. premsDT dt = [] & premsDT dtAY = [] --> \ \ premsDT (mXP pn dtAY seqY dt) = []) & \ \ (ALL seqYs. premsDTs dts = [] & premsDT dtAY = [] --> \ \ premsDTs (mXPs pn dtAY seqYs dts) = [])" (fn _ => [ (induct_tac "dt dts" 1), (REPEAT ((Simp_tac THEN_ALL_NEW Fast_tac) 2)), (case_tac "pn" 1), (ALLGOALS (asm_full_simp_tac (esimps nss)))]) RS conjunct1)) ; val [noPrems_mLP, noPrems_mRP] = X2LR noPrems_mXP ; (** characterization of mLPs and mRPs **) val mXPs = store_thm ("mXPs", meta_std (prove_goal RP.thy "(ALL ms xs. length ys <= length xs --> \ \ (ms = mXPs pn dtAY xs ys) = (length ms = length ys & \ \ (ALL n. n < length ys --> ms!n = mXP pn dtAY (xs!n) (ys!n))))" (fn _ => [ (induct_tac "ys" 1), Simp_tac 1, rtac allI 1, rtac allI 1, (case_tac "xs" 1), Asm_full_simp_tac 1, (case_tac "ms" 1), Asm_full_simp_tac 1, (eres_inst_tac [("x", "tl ms")] allE 1), (eres_inst_tac [("x", "tl xs")] allE 1), Asm_full_simp_tac 1, Safe_tac, (eres_inst_tac [("x", "Suc na")] allE 5), (eres_inst_tac [("x", "0")] allE 4), (REPEAT (Force_tac 2)), (case_tac "n" 1), Asm_simp_tac 1, Asm_full_simp_tac 1]))) ; val mXPs' = store_thm ("mXPs'", meta_std (prove_goal RP.thy "m : set (mXPs pn dtAY xs ys) & length ys <= length xs --> \ \ (EX n. n < length ys & m = mXP pn dtAY (xs!n) (ys!n))" (fn _ => [ (safe_tac (HOL_cs addSDs [ex_nth RS iffD1])), dtac (mXPs RS iffD1) 1, rtac refl 1, etac conjE 1, (datac (eq_imp_le RSN (2, less_le_trans)) 1 1), Auto_tac]))) ; val [mLPs, mRPs] = X2LR mXPs ; val [mLPs', mRPs'] = X2LR mXPs' ; (** if tree already has desired conclusion **) val sameConcXP = store_thm ("sameConcXP", meta_std (prove_goal RP.thy "(allDT wfb dtA --> mXP pn dtAY (conclDT dtA) dtA = dtA) & \ \ (allDTs wfb dtAs --> mXPs pn dtAY (map conclDT dtAs) dtAs = dtAs)" (fn _ => [ (induct_tac "dtA dtAs" 1), (REPEAT (Asm_simp_tac 2)), let val th = refl RS newSub_same RS conjunct2 ; val ss = simpset () addsimps (premsSub :: nss) delsimps [wfb_Der] ; in ((case_tac "pn" THEN_ALL_NEW EVERY' [ (asm_full_simp_tac ss), Clarify_tac, mp_tac, (asm_full_simp_tac (esimps [th]))]) 1) end]) RS conjunct1)) ; val () = qed_goal "sameXP'" RP.thy "mXP' pn dtAY (conclDT dtA) dtA = mXP pn dtAY (conclDT dtA) dtA" (fn _ => [(case_tac "dtA" 1), Asm_simp_tac 2, (case_tac "pn" 1), (ALLGOALS (asm_simp_tac (esimps [mLP_Der', mRP_Der'])))]) ; val () = bind_thm ("sameConcXP'", [sameXP', sameConcXP] MRS trans) ; val [sameConcLP', sameConcRP'] = X2LR sameConcXP' ; val [sameLP', sameRP'] = X2LR sameXP' ; val [sameConcLP, sameConcRP] = X2LR sameConcXP ; val lem2' = wfbLen RS sym ; val lem2 = refl RSN (3, meta_std (exI RS (wfb_Der RS iffD2) RS lem2')) ; val lem2'' = exI RS rewrite_rule [ruleMatches_def] lem2 ; (* ; val prems = it ; *) val () = qed_goal_spec_mp "allrel_mapf" HOL_Ths.thy "ALL B. ((map f A, map g B) : allrel r) = \ \ ((A, B) : allrel {(a, b). (f a, g b) : r})" (fn _ => [(induct_tac "A" 1), (safe_tac (claset () delrules [iffCE])), (ALLGOALS (etac allrel.elim)), (case_tac "B" 6), (ALLGOALS Asm_full_simp_tac), Fast_tac 1]) ; val allrel_mapf' = simplify (simpset ()) (read_instantiate [("g", "(%x. x)")] allrel_mapf) ; val () = bind_thm ("lem2XP'", meta_std (prove_goal RP.thy "ALL seqYs. dtY : set (mXPs pn dtAY seqYs dtAs) & \ \ (dtAs, seqYs) : allrel (Collect (split f)) --> \ \ (EX dtA : set dtAs. (EX seqY : set seqYs. \ \ dtY = mXP pn dtAY seqY dtA & f dtA seqY))" (fn _ => [(induct_tac "dtAs" 1), (Simp_tac 1), (Simp_tac 1), (clarify_tac (claset () delrules [disjCI]) 1), (etac allrel.elim 1), Full_simp_tac 1, (eres_inst_tac [("x", "tb")] allE 1), Auto_tac]))) ; val [lem2LP', lem2RP'] = X2LR lem2XP' ; (* fold_rule in the following fails - TO FIX *) fun mk_lem2XP'_seqRep lem2XP' = fold_rule [mk_meta_eq allrel_mapf'] (read_instantiate [("f", "%dtA. seqRep ?pn ?X ?Y (?g dtA)")] lem2XP') ; (* "%dtA dtB. (?g dtA, dtB) : seqrep ?pn ?X ?Y" *) fun mk_lem2XP'_seqRep lem2XP' = fold_rule [mk_meta_eq allrel_mapf', seqreps_def] (read_instantiate [("f", "%dtA dtB. (?g dtA, dtB) : seqrep ?pn ?X ?Y")] lem2XP') ; val [lem2XP'_seqRep, lem2LP'_seqRep, lem2RP'_seqRep] = map mk_lem2XP'_seqRep [lem2XP', lem2LP', lem2RP'] ; val [lem2XP_seqRep, lem2LP_seqRep, lem2RP_seqRep] = map mksR [lem2XP'_seqRep, lem2LP'_seqRep, lem2RP'_seqRep] ; val () = bind_thm ("lem1XP'", (prove_goal RP.thy "(ALL dt:set dtl. ALL seqY. seqRep pn (Structform A) Y (conclDT dt) seqY --> \ \ allDT f (mXP pn dtAY seqY dt)) = \ \ (ALL seqYs. seqReps pn (Structform A) Y (map conclDT dtl) seqYs --> \ \ allDTs f (mXPs pn dtAY seqYs dtl))" (fn _ => [(induct_tac "dtl" 1), Simp_tac 1, rtac iffI 1, Force_tac 1, (Asm_full_simp_tac 1), (rtac conjI 1), ALLGOALS strip_tac, (eres_inst_tac [("x", "seqY # map conclDT list")] allE 1), (eres_inst_tac [("x", "conclDT a # seqYs")] allE 2), ALLGOALS (etac impE), (auto_tac (claset (), esimps [seqRep_refl, seqReps_refl]))]))) ; val [lem1LP', lem1RP'] = X2LR lem1XP' ; val lem1XP'' = meta_std (lem1XP' RS iffD1) ; (* trivially implied by lem1XP'' *) val () = bind_thm ("lem1XP", meta_std (prove_goal RP.thy "(ALL dt:set dtl. ALL seqY. seqRep pn (Structform A) Y (conclDT dt) seqY --> \ \ allDT f (mXP pn dtAY seqY dt)) --> \ \ (ALL seqYs. length dtl <= length seqYs & \ \ seqReps pn (Structform A) Y (map conclDT dtl) seqYs --> \ \ allDTs f (mXPs pn dtAY seqYs dtl))" (fn _ => [(induct_tac "dtl" 1), Auto_tac]))) ; val [lem1LP, lem1RP] = X2LR lem1XP ; val wfmXP' = prove_goal RP.thy "[| allDT wfb dtAY; ALL dt:set dtl. ALL seqY. \ \ seqRep pn (Structform A) Y (conclDT dt) seqY --> \ \ allDT wfb (mXP pn dtAY seqY dt); \ \ allDT wfb (Der seqA rule dtl) ; \ \ seqRep pn (Structform A) Y seqA seqY ; bprops rule ; \ \ strIsFml (side pn (conclRule rule)) --> side pn seqA = side pn seqY |] \ \ ==> allDT wfb (mXP' pn dtAY seqY (Der seqA rule dtl))" (fn prems => [(cut_facts_tac prems 1), (simp_tac (simpset() addsimps [Let_def, matches_map, mXP'_Der]) 1), rtac conjI 1, rtac exI 1, (REPEXP (rtac conjI) 1), rtac (ruleMatches_refl RS ruleMatches_sub) 1, rtac (concl_mXPs RS trans RS sym) 1, (simp_tac (esimps [premsSub]) 1), rtac refl 2, rtac wfbLen 1, (etac allDTD1 1), (simp_tac (HOL_ss addsimps [conclSub]) 1), (rtac nslem1' 1), (etac allDTD1 1), (REPEAT (atac 1)), (ftac allDTD1 1 THEN dtac (wfb_Der' RS iffD1) 1), (REPEAT (eresolve_tac [conjE, exE] 1)), (ftac (rotate_prems ~2 nslem5) 1), (TRYALL (hyp_subst_tac THEN' atac)), rtac refl 1, (asm_full_simp_tac (HOL_ss addsimps [matches_map, premsSub]) 1), (etac lem1XP 1), (dtac (allDTD1wfb RS wfbLen) 1), Auto_tac]) ; val [wfmLP', wfmRP'] = X2LR wfmXP' ; val () = qed_goal_spec_mp "bpr'" RP.thy "(frb rls) (Der sequent rule list) --> bprops rule" (fn _ => [rtac impI 1, (rtac bprops_rls 1), (etac (frb_Der RS iffD1) 1)]) ; val () = qed_goal_spec_mp "bpr" RP.thy "allDT (frb rls) (Der sequent rule list) --> bprops rule" (fn _ => [rtac impI 1, (rtac bpr' 1), (etac allDTD1 1)]) ; fun wfm_tac wfmXP' tf prems = [(cut_facts_tac prems 1), (res_inst_tac [("dertree1", "dtA")] dertree_induct 1), (Simp_tac 2), Safe_tac, (simp_tac (HOL_ss addsimps [mLP_Der', mRP_Der']) 1), (rtac conjI 1), (ALLGOALS (rtac impI)), (etac wfmXP' 2), atac 3, (Asm_full_simp_tac 3), (etac bpr 3), (asm_simp_tac (HOL_ss addsimps [sideTrue, sideFalse]) 3), (force_tac (claset (), esimps [allDTs, premsDT_Nil]) 2), (simp_tac (init_ss addsimps [allDT_Der, Let_def, allDTs]) 1), (REPEXP (ares_tac [conjI]) 1), (eres_inst_tac [] wfmXP' 2), atac 3, etac bpr 4, (simp_tac (esimps [sideTrue, sideFalse]) 4), (case_tac "sequent" 3), (case_tac "seqY" 3), (Asm_full_simp_tac 3), (fast_tac (claset () addSIs [strRep_refl]) 3), (force_tac (claset (), esimps [allDTs, premsDT_Nil]) 2), (case_tac "sequent" 1), (case_tac "seqY" 1), hyp_subst_tac 1, (rtac (cut_wfb RS iffD2) 1), (rtac exI 1), (asm_simp_tac (HOL_ss addsimps [concl_mLP', concl_mRP']) 1), (dtac (allDTD1wfb RS wfbCF) 1), (fast_tac (claset () addSss esimps ([sideTrue, sideFalse] RL [sym])) 1), (dtac (strIsFml RS iffD1) 1), (etac exE 1), Asm_full_simp_tac 1] ; val wfmLP = store_thm ("wfmLP", meta_std (prove_goal RP.thy "[| allDT wfb dtAY; conclDT dtAY = (A |- $Y) |] ==> \ \ ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ seqRep True (Structform A) Y (conclDT dtA) seqY --> \ \ allDT wfb (mLP dtAY seqY dtA)" (wfm_tac wfmLP' "True"))) ; (* ; val prems = it ; *) val wfmRP = store_thm ("wfmRP", meta_std (prove_goal RP.thy "[| allDT wfb dtAY; conclDT dtAY = ($Y |- A) |] ==> \ \ ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ seqRep False (Structform A) Y (conclDT dtA) seqY --> \ \ allDT wfb (mRP dtAY seqY dtA)" (wfm_tac wfmRP' "False"))) ; (** alternative proof of wfmLP, wfmRP **) fun wfm_tac2 wfbCFSA prems = [(induct_tac "dtA dtAs" 1), (REPEAT (Force_tac 2)), Safe_tac, (ftac bpr 1), (cut_facts_tac prems 1), (dtac (allDT_Der RS iffD1) 1), (ftac (allDT_Der RS iffD1) 1), (simp_tac (HOL_ss addsimps ([Let_def, mLP_Der', mRP_Der'] @ thms "allDT_allDTs.simps")) 1), (asm_full_simp_tac (HOL_ss addsimps [conclDT_Der]) 1), Safe_tac, (TRYALL (resolve_tac [wfmLP', wfmRP'])), (TRYALL (atac ORELSE' (asm_simp_tac (HOL_ss addsimps [antec_def, succ_def, sideTrue, sideFalse, lem1LP', lem1RP'])))), (case_tac "sequent" 2), (case_tac "seqY" 2), Asm_full_simp_tac 2, (case_tac "sequent" 1), (case_tac "seqY" 1), hyp_subst_tac 1, (rtac (cut_wfb RS iffD2) 1), rtac exI 1, (asm_full_simp_tac (simpset () delsimps [wfb_Der]) 1), Safe_tac, rtac refl 2, ALLGOALS (EVERY' [ (simp_tac (HOL_ss addsimps [concl_mLP', concl_mRP'])), (datac strRepFmlEq' 1), (datac wfbCFSA 1)]), Auto_tac] ; val wfmLP = store_thm ("wfmLP", (standard o meta_std) (prove_goal RP.thy "[| allDT wfb dtAY; conclDT dtAY = (A |- $Y) |] ==> \ \ (ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ seqRep True (Structform A) Y (conclDT dtA) seqY --> \ \ allDT wfb (mLP dtAY seqY dtA)) & \ \ (ALL seqYs. allDTs (frb rls) dtAs & allDTs wfb dtAs & \ \ seqReps True (Structform A) Y (map conclDT dtAs) seqYs --> \ \ allDTs wfb (mLPs dtAY seqYs dtAs))" (wfm_tac2 wfbCFSuc) RS conjunct1)) ; val wfmRP = store_thm ("wfmRP", (standard o meta_std) (prove_goal RP.thy "[| allDT wfb dtAY; conclDT dtAY = ($Y |- A) |] ==> \ \ (ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ seqRep False (Structform A) Y (conclDT dtA) seqY --> \ \ allDT wfb (mRP dtAY seqY dtA)) & \ \ (ALL seqYs. allDTs (frb rls) dtAs & allDTs wfb dtAs & \ \ seqReps False (Structform A) Y (map conclDT dtAs) seqYs --> \ \ allDTs wfb (mRPs dtAY seqYs dtAs))" (wfm_tac2 wfbCFAnt) RS conjunct1)) ; (* shorter available fun frm_tac mXP' prems = [ rtac impI 1, (res_inst_tac [("dertree1", "dtA")] dertree_induct 1), (Simp_tac 2), Safe_tac, (subgoal_tac ("ALL seqY'. allDT (frb rls) (" ^ mXP' ^ " dtAY seqY' (Der sequent rule list))") 1), (asm_simp_tac (HOL_ss addsimps [frb_Der, mLP_Der', mRP_Der', Let_def] @ rii_thms' @ thms "allDT_allDTs.simps") 1), (rtac allI 1), (asm_full_simp_tac (HOL_ss addsimps [mLP'_Der, mRP'_Der, Let_def, allDT_Der, allDTs, frb_Der]) 1), (rtac ballI 1), (dresolve_tac [mLPs', mRPs'] 1), (Clarify_tac 1), (dtac wfbLen 1), (asm_simp_tac (esimps [premsSub]) 1), (Clarify_tac 1), (dtac nth_mem 1), (REPEAT (datac bspec 1 1)), (REPEAT (eatac impE 1 1)), (Asm_simp_tac 1)] ; val () = qed_goal_spec_mp "frmLP" RP.thy "allDT (frb rls) dtAY --> \ \ (ALL seqY. allDT (frb rls) dtA --> allDT wfb dtA --> \ \ allDT (frb rls) (mLP dtAY seqY dtA))" (frm_tac "mLP'") ; val () = qed_goal_spec_mp "frmRP" RP.thy "allDT (frb rls) dtAY --> \ \ (ALL seqY. allDT (frb rls) dtA --> allDT wfb dtA --> \ \ allDT (frb rls) (mRP dtAY seqY dtA))" (frm_tac "mRP'") ; *) val frm_tac2 = (fn prems => [(induct_tac "dtA dtAs" 1), (REPEAT (Force_tac 2)), Safe_tac, (asm_full_simp_tac (esimps (prems @ nss @ rii_thms) delsimps [wfb_Der]) 1)]) ; val () = bind_thm ("frmLP", (standard o meta_std) (prove_goal RP.thy "allDT (frb rls) dtAY ==> \ \ (ALL seqY. allDT (frb rls) dtA --> allDT wfb dtA --> \ \ allDT (frb rls) (mLP dtAY seqY dtA)) & \ \ (ALL seqYs. allDTs (frb rls) dtAs --> allDTs wfb dtAs --> \ \ allDTs (frb rls) (mLPs dtAY seqYs dtAs))" frm_tac2 RS conjunct1)) ; val () = bind_thm ("frmRP", (standard o meta_std) (prove_goal RP.thy "allDT (frb rls) dtAY ==> \ \ (ALL seqY. allDT (frb rls) dtA --> allDT wfb dtA --> \ \ allDT (frb rls) (mRP dtAY seqY dtA)) & \ \ (ALL seqYs. allDTs (frb rls) dtAs --> allDTs wfb dtAs --> \ \ allDTs (frb rls) (mRPs dtAY seqYs dtAs))" frm_tac2 RS conjunct1)) ; fun mXP_XP'_tac prems = [Safe_tac, (asm_simp_tac (HOL_ss addsimps [Let_def, mLP_Der', mRP_Der']) 1), Safe_tac, (simp_tac (HOL_ss addsimps [Let_def, mLP'_Der, cutIsLP_Der, mRP'_Der, cutIsRP_Der]) 1), (case_tac "conclRule rule" 1), (asm_full_simp_tac (HOL_ss addsimps strIsFml :: thms "succ.simps") 1), (etac exE 1), (REPEXP (resolve_tac [exI, conjI]) 1), (simp_tac (init_ss addsimps dertree.simps @ sequent.simps) 1), (REPEXP (resolve_tac [refl, conjI]) 1), (fast_tac (claset () addSss (esimps [])) 2), (case_tac "seqA" 1), (fast_tac (claset () addSss (esimps [ruleMatches_def, conclSub])) 1)] ; val mLP_LP' = meta_std (prove_goal RP.thy "dtA = (Der seqA rule dtlA) --> \ \ wfb dtA --> seqRep True (Structform A) Y seqA seqY --> \ \ (ALL seqY'. seqRep True (Structform A) Y seqA seqY' --> \ \ (strIsFml (succ (conclRule rule)) --> succ seqA = succ seqY') --> \ \ (cutIsLP A) (mLP' dtAY seqY' dtA)) --> \ \ (cutIsLP A) (mLP dtAY seqY dtA)" mXP_XP'_tac) ; val mRP_RP' = meta_std (prove_goal RP.thy "dtA = (Der seqA rule dtlA) --> \ \ wfb dtA --> seqRep False (Structform A) Y seqA seqY --> \ \ (ALL seqY'. seqRep False (Structform A) Y seqA seqY' --> \ \ (strIsFml (antec (conclRule rule)) --> antec seqA = antec seqY') --> \ \ (cutIsRP A) (mRP' dtAY seqY' dtA)) --> \ \ (cutIsRP A) (mRP dtAY seqY dtA)" mXP_XP'_tac) ; val mXP_XP''_tacs = [ (fast_tac (claset () addSEs allDTD1 :: ([refl] RL [mLP_LP', mRP_RP'])) 2), (simp_tac (HOL_ss addsimps [mLP_Der', mRP_Der']) 1), (rtac conjI 1), Fast_tac 2, (simp_tac (HOL_ss addsimps [allDT_Next]) 1), Safe_tac, (asm_full_simp_tac (HOL_ss addsimps [mLP_Der', mRP_Der']) 1), (asm_simp_tac (init_ss addsimps [Let_def, allDTs] @ thms "allNextDTs.simps") 1), (etac allE 1), (dtac mp 1), (etac mp 2), (Simp_tac 2), (case_tac "seqY" 1), (case_tac "seqA" 1), (Asm_full_simp_tac 1)] ; val mLP_LP'' = meta_std (prove_goal RP.thy "dtA = (Der seqA rule dtlA) --> allDT (cutIsLP A) dtAY --> wfb dtA --> \ \ seqRep True (Structform A) Y seqA seqY --> \ \ (ALL seqY'. seqRep True (Structform A) Y seqA seqY' --> \ \ (strIsFml (succ (conclRule rule)) --> succ seqA = succ seqY') --> \ \ allDT (cutIsLP A) (mLP' dtAY seqY' dtA)) --> \ \ allDT (cutIsLP A) (mLP dtAY seqY dtA)" (fn _ => (Safe_tac :: (subgoal_tac "(cutIsLP A) (mLP dtAY seqY (Der seqA rule dtlA))" 1) :: mXP_XP''_tacs))) ; val mRP_RP'' = meta_std (prove_goal RP.thy "dtA = (Der seqA rule dtlA) --> allDT (cutIsRP A) dtAY --> wfb dtA --> \ \ seqRep False (Structform A) Y seqA seqY --> \ \ (ALL seqY'. seqRep False (Structform A) Y seqA seqY' --> \ \ (strIsFml (antec (conclRule rule)) --> antec seqA = antec seqY') --> \ \ allDT (cutIsRP A) (mRP' dtAY seqY' dtA)) --> \ \ allDT (cutIsRP A) (mRP dtAY seqY dtA)" (fn _ => (Safe_tac :: (subgoal_tac "(cutIsRP A) (mRP dtAY seqY (Der seqA rule dtlA))" 1) :: mXP_XP''_tacs))) ; (* ; val prems = it ; *) fun mXP_XPtac prems = [(cut_facts_tac prems 1), (res_inst_tac [("dertree1", "dtA")] dertree_induct 1), (Simp_tac 2), (Clarify_tac 1), (forward_tac ([refl] RL [mLP_LP'', mRP_RP'']) 1), atac 2, (simp_tac (HOL_ss addsimps [conclDT_Der]) 1), etac allDTD1 1, (full_simp_tac (HOL_ss addsimps [conclDT_Der]) 2), (rtac allI 1), (simp_tac (HOL_ss addsimps [allDT_Der, mLP'_Der, mRP'_Der, Let_def]) 1), (REPEAT (rtac impI 1)), (rtac conjI 1), (Asm_full_simp_tac 1), (simp_tac (HOL_ss addsimps [allDTs]) 1), (rtac ballI 1), (dresolve_tac [mLPs', mRPs'] 1), (simp_tac (esimps [premsSub]) 1), (ftac (thin_rl RS wfbLen) 1), (etac allDTD1 1), (arith_tac 1), (Clarify_tac 1), (dtac bspec 1), (etac nth_mem 1), etac allE 1, etac mp 1, (REPEXP (rtac conjI) 1), (REPEAT (eatac (nth_mem RSN (2, allDTD2)) 1 1)), (dtac (allDTD1wfb RS (wfb_Der' RS iffD1)) 1), (REPEAT (eresolve_tac [conjE, exE] 1)), (asm_full_simp_tac (HOL_ss addsimps [conclDT_Der, premsSub]) 1), (dtac (rotate_prems ~2 nslem5) 1), atac 5, (asm_full_simp_tac (HOL_ss addsimps ([sideFalse, sideTrue] RL [sym])) 4), (Asm_simp_tac 2), rtac refl 1, (etac bpr 1), (dtac (reop rev seqReps_nth) 1), (REPEAT (asm_full_simp_tac (init_ss addsimps [matches_map]) 1))] ; val mLP_LP = store_thm ("mLP_LP", meta_std (prove_goal RP.thy "[| allDT (cutIsLP A) dtAY |] ==> \ \ ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ allDT (cutOnFmls {}) dtA & \ \ seqRep True (Structform A) Y (conclDT dtA) seqY --> \ \ allDT (cutIsLP A) (mLP dtAY seqY dtA)" mXP_XPtac)) ; val mRP_RP = store_thm ("mRP_RP", meta_std (prove_goal RP.thy "[| allDT (cutIsRP A) dtAY |] ==> \ \ ALL seqY. allDT (frb rls) dtA & allDT wfb dtA & \ \ allDT (cutOnFmls {}) dtA & \ \ seqRep False (Structform A) Y (conclDT dtA) seqY --> \ \ allDT (cutIsRP A) (mRP dtAY seqY dtA)" mXP_XPtac)) ; val makeCutmLP = prove_goal RP.thy "[| allDT (cutOnFmls {}) dtAY; allDT (frb rls) dtAY; allDT wfb dtAY; \ \ conclDT dtAY = (A |- $Y); allDT (frb rls) dtA; allDT wfb dtA; \ \ allDT (cutOnFmls {}) dtA; \ \ seqRep True (Structform A) Y (conclDT dtA) seqY ; \ \ dtY = mLP dtAY seqY dtA |] ==> \ \ conclDT dtY = seqY & \ \ allDT (cutIsLP A) dtY & allDT (frb rls) dtY & allDT wfb dtY" (fn prems => [(cut_facts_tac prems 1), Safe_tac, (simp_tac (esimps [concl_mLP]) 1), (eatac frmLP 2 2), ((etac wfmLP THEN_ALL_NEW TRY o atac) 2), ((rtac mLP_LP THEN_ALL_NEW TRY o atac) 1), (etac allDT_mono 1 THEN etac noCutLP 1)]) ; (* ; val prems = it ; *) fun tacs mXPs = [ (rtac allI 1), (REPEAT (etac conjE 1)), (simp_tac (HOL_ss addsimps [allDT_Der, allDTs, mLP_Der', mRP_Der', Let_def]) 1), (REPEXP (resolve_tac [impI, conjI]) 1), (case_tac "seqY" 1), (force_tac (claset () addSEs [cutIsLP_I, cutIsRP_I], HOL_ss addsimps [cut_wfb]) 1), (simp_tac init_ss 1), (rtac conjI 1), ((etac allDT_mono THEN' eresolve_tac [noCutLP, noCutRP]) 1 ORELSE (etac allDT_mono THEN' eresolve_tac [noCutLP, noCutRP]) 2), (etac allE 1), (dtac mp 1), (etac mp 2), (force_tac (HOL_cs, init_ss) 2), (simp_tac (esimps [mLP_Der', mRP_Der']) 1), (etac allE 1), (dtac mp 1 THEN eatac mp 1 2), (force_tac (HOL_cs, esimps [mLP_Der', mRP_Der']) 1), Safe_tac, (simp_tac (HOL_ss addsimps [mLP'_Der, mRP'_Der, Let_def, allDT_Der, allDTs]) 1), Safe_tac, Asm_full_simp_tac 1, (dresolve_tac [mLPs', mRPs'] 1), Safe_tac, (dtac bspec 2), (dtac mp 3), (etac nth_mem 2), (fast_tac (claset () addSEs [allDTD2, nth_mem]) 2), ((dtac allDTD1 THEN' dtac wfbLen') 1), (etac (sym RS eq_imp_le) 1), (etac allE 1), (etac mp 1), (full_simp_tac (HOL_ss addsimps [mLP'_Der, mRP'_Der, Let_def]) 1), ((dtac allDTD1 THEN' dtac wfbLen') 1), (EVERY (map (etac thin_rl) [1,1,1,1,1])), (etac allDTD2 1), (rtac (ex_nth RS iffD2) 1), rtac exI 1, (ftac ([thin_rl, refl] MRS (mXPs RS iffD1)) 1), etac conjE 2, etac allE 2, etac impE 2, rtac conjI 3, etac sym 4, Auto_tac, (etac (sym RS eq_imp_le) 1)] ; val LP_mRP = store_thm ("LP_mRP", meta_std (prove_goal RP.thy "allDT (cutOnFmls {}) dtAY & rootIsSucP dtAY & conclDT dtAY = ($Y |- A) --> \ \ allDT (cutOnFmls {}) dtA & allDT wfb dtA --> \ \ (ALL seqY. allDT wfb (mRP dtAY seqY dtA) --> \ \ allDT (cutIsLP A) (mRP dtAY seqY dtA))" (fn _ => [rtac impI 1, (res_inst_tac [("dertree1", "dtA")] dertree_induct 1), (Simp_tac 2), rtac impI 1, (subgoal_tac "ALL seqY'. mRP' dtAY seqY' (Der sequent rule list) = \ \ mRP dtAY seqY' (Der sequent rule list) --> \ \ allDT wfb (mRP' dtAY seqY' (Der sequent rule list)) --> \ \ allDT (cutIsLP A) (mRP' dtAY seqY' (Der sequent rule list))" 1)] @ tacs mRPs))) ; (* ; val prems = it ; *) val makeCutmRP = prove_goal RP.thy "[| allDT (cutOnFmls {}) dtAY; rootIsSucP dtAY; allDT (frb rls) dtAY; \ \ allDT wfb dtAY; conclDT dtAY = ($Y |- A); allDT (frb rls) dtA; \ \ allDT wfb dtA; allDT (cutOnFmls {}) dtA; \ \ seqRep False (Structform A) Y (conclDT dtA) seqY ; \ \ dtY = mRP dtAY seqY dtA |] ==> \ \ conclDT dtY = seqY & \ \ allDT (cutIsLRP A) dtY & allDT (frb rls) dtY & allDT wfb dtY" (fn prems => [(cut_facts_tac prems 1), Safe_tac, (simp_tac (esimps [concl_mRP]) 1), (eatac frmRP 2 2), ((etac wfmRP THEN_ALL_NEW TRY o atac) 2), let val th1 = cutIsLRP_def RS meta_eq_to_obj_eq ; val th2 = tacthm (rtac allI 1 THEN rtac th1 1) allDT_and ; in (rtac (th2 RS iffD2) 1) end, rtac conjI 1, ((etac LP_mRP THEN_ALL_NEW TRY o atac) 1), ((etac wfmRP THEN_ALL_NEW TRY o atac) 1), ((rtac mRP_RP THEN_ALL_NEW TRY o atac) 1), (etac allDT_mono 1 THEN etac noCutRP 1)]) ; (* results makeCutmLP and makeCutmRP are the same as makeCutLP and makeCutRP except that they specify the new (reduced) tree rather than just asserting its existence; therefore they show that the cut-reduction procedure can be done using the reductions involving the functions mLP and mRP *) (* ; val prems = it ; *) val RP_mLP = store_thm ("RP_mLP", meta_std (prove_goal RP.thy "allDT (cutOnFmls {}) dtAY & rootIsAntP dtAY & conclDT dtAY = (A |- $Y) --> \ \ allDT (cutOnFmls {}) dtA & allDT wfb dtA --> \ \ (ALL seqY. allDT wfb (mLP dtAY seqY dtA) --> \ \ allDT (cutIsRP A) (mLP dtAY seqY dtA))" (fn _ => [rtac impI 1, (res_inst_tac [("dertree1", "dtA")] dertree_induct 1), (Simp_tac 2), rtac impI 1, (subgoal_tac "ALL seqY'. mLP' dtAY seqY' (Der sequent rule list) = \ \ mLP dtAY seqY' (Der sequent rule list) --> \ \ allDT wfb (mLP' dtAY seqY' (Der sequent rule list)) --> \ \ allDT (cutIsRP A) (mLP' dtAY seqY' (Der sequent rule list))" 1)] @ tacs mLPs))) ; (* ; val prems = it ; *)