val [vw1, vw2] = [valid_def RS def_imp_eq RS iffD1 RS conjunct1] RL [allDTD1, allDTD2] ; val () = bind_thm ("cutExRed", meta_std (prove_goal SNCE.thy "isCut dt & valid rls dt & allNextDTs (cutOnFmls {}) dt --> \ \ (EX dtn. cutReduces dt dtn & valid rls dtn )" (fn _ => [Safe_tac, (case_tac "dt" 1), Asm_full_simp_tac 2, (case_tac "sequent" 1), (asm_full_simp_tac (HOL_ss addsimps [isCut_Der]) 1), (ftac vw1 1), (dtac (cut_wfb' RS iffD1) 1), Safe_tac, (full_simp_tac (init_ss addsimps [allNextDTs_Der, allDTs]) 1), (etac conjE 1), (dtac (reop rev noCutncLP) 1), (dtac vw2 1), atac 2, Simp_tac 1, (dtac (reop rev noCutncRP) 1), (dtac vw2 1), atac 2, Simp_tac 1, (case_tac "rootIsSucP pl" 1), (datac ([refl, refl] MRS pRedLP3) 2 2), etac exI 2, (case_tac "rootIsAntP pr" 1), (datac ([refl, refl] MRS pRedRP3) 2 2), etac exI 2, (datac cutIsLP_I 1 1), (datac cutIsRP_I 1 1), (rtac (refl RS vformC8W') 1), atac 2, rewtac cutIsLRP_def, Fast_tac 1]))) ; val () = qed_goalw_spec_mp "validRedUp" SNCE.thy [valid_def, validRed_def] "valid rls (Der sequent rule list) --> d:set list --> (dn, d) : validRed --> \ \ (Der sequent rule (repfst list d dn), Der sequent rule list) : validRed" (fn _ => [ Safe_tac, (datac onered_repfst 1 4), Fast_tac 4, (ALLGOALS (asm_full_simp_tac (esimps [allDTs, noPrems]))), (rtac conjI 1), (ALLGOALS (REPEAT o etac conjE)), (TRYALL (eatac all_repfst 1)), (etac ex_match 1), (dtac reduction_sim' 1), (asm_full_simp_tac (esimps [matches_map]) 1), (induct_tac "list" 1), Simp_tac 1, Asm_simp_tac 1]) ; val [ExRed, _] = store_thms ("ExReds", map meta_std ([prove_goalw SNCE.thy [validRed_def] "(~ allDT (Not o isCut) dt & valid rls dt --> \ \ (EX dtn. (dtn, dt) : validRed)) & \ \ (~ allDTs (Not o isCut) dts & (ALL d: set dts. valid rls d) --> \ \ (EX d: set dts. EX dn. (dn, d) : validRed))" (fn _ => [ (induct_tac "dt dts" 1), Force_tac 4, (ALLGOALS Simp_tac), (Clarify_tac 1), (subgoal_tac "Ball (set list) (valid rls)" 1), (Clarify_tac 2), (etac validUp 2), Asm_simp_tac 2, (case_tac "allDTs (%u. ~ isCut u) list" 1), (dtac (thin_rl RS cutExRed) 1), atac 2, Force_tac 1, (rtac (allNDT_isCut_COF RS iffD1) 1), (asm_full_simp_tac (HOL_ss addsimps [valid_def]) 1), (asm_simp_tac (esimps [o_def]) 1), (etac ex_match 1), Fast_tac 1, (asm_full_simp_tac (esimps [o_def]) 1), (TRY (mp_tac 1)), (Clarify_tac 1), (datac (full_simplify (esimps [validRed_def]) validRedUp) 1 1), Auto_tac])] RL conjuncts)) ; val wfRed = rewrite_rule [strongNorm_def, mk_meta_eq snwf] all_sn ; val wf_validRed = prove_goalw SNCE.thy [wf_def, validRed_def] "wf validRed" (fn _ => [Safe_tac, (rtac (wfRed RS spec RS mp) 1), Fast_tac 1]) ; val validRed_min = wf_validRed RS wf_min ; val () = qed_goalw_spec_mp "tcsc" SNCE.thy [validRed_def] "(dtn, dt) : (validRed)^* --> conclDT dtn = conclDT dt" (fn _ => [rtac impI 1, (etac rtrancl_induct 1), (ALLGOALS Asm_full_simp_tac), (rtac (reduction_sim' RS sym) 1), Safe_tac]) ; val () = qed_goal_spec_mp "redNoCut" SNCE.thy "valid rls dt --> \ \ (EX dtn. allDT (Not o isCut) dtn & conclDT dtn = conclDT dt & \ \ valid rls dtn & (dtn, dt) : validRed^*)" (fn _ => [(cut_facts_tac [validRed_min] 1), Safe_tac, (subgoal_tac "valid rls dtn" 1), (datac (tacthm (etac ExRed 2) swap) 1 1), (ftac tcsc 1), Fast_tac 1, (dtac converseI 1), (full_simp_tac (esimps [rtrancl_converse RS sym]) 1), (eatac rtrancl_induct 1 1), (asm_full_simp_tac (esimps [validRed_def]) 1)]) ; val () = qed_goalw_spec_mp "cutElim_SN" SNCE.thy [IsDerivableR_def] "IsDerivableR rls {} concl --> IsDerivableR (rls - {cutr}) {} concl" (fn _ => [Safe_tac, (ftac (thin_rl RS redNoCut) 1), (REPEAT (force_tac (claset () addSEs [cfpt'], esimps [valid_def]) 1))]) ;