val [vw1, vw2] = [valid_def RS def_imp_eq RS iffD1 RS conjunct1] RL [allDTD1, allDTD2] ; (* ; val prems = it ; *) val () = qed_goal_spec_mp "cutExRed" SNCE.thy "C345 rules --> c8sn rules --> \ \ isCut dt --> valid rules dt --> allNextDTs (cutOnFmls {}) dt --> \ \ (EX dtn. cutReduces dt dtn & valid rules dtn )" (fn _ => [Safe_tac, (case_tac "dt" 1), Asm_full_simp_tac 2, (case_tac "seq" 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 ([asm_rl, refl, refl] MRS pRedLP3) 3 2), etac exI 2, (case_tac "rootIsAntP pr" 1), (datac ([asm_rl, refl, refl] MRS pRedRP3) 3 2), etac exI 2, (datac cutIsLP_I 1 1), (datac cutIsRP_I 1 1), (etac (refl RSN (2, vformCR)) 1), atac 2, rewtac cutIsLRP_def, Fast_tac 1]) ; val () = qed_goalw_spec_mp "validRedUp" SNCE.thy [valid_def, validRed_def] "valid rules (Der sequent rule list) --> d:set list --> \ \ (dn, d) : validRed rules --> (Der sequent rule (repfst list d dn), \ \ Der sequent rule list) : validRed rules" (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 mem_same 1), Simp_tac 1, (induct_tac "list" 1), Simp_tac 1, (dtac reduction_sim' 1), Asm_simp_tac 1]) ; val ther = prove_goalw SNCE.thy [validRed_def] "C345 rules --> c8sn rules --> \ \ ((~ allDT (Not o isCut) dt & valid rules dt --> \ \ (EX dtn. (dtn, dt) : validRed rules)) & \ \ (~ allDTs (Not o isCut) dts & (ALL d: set dts. valid rules d) --> \ \ (EX d: set dts. EX dn. (dn, d) : validRed rules)))" (fn _ => [ strip_tac 1, (induct_tac "dt dts" 1), Force_tac 4, (ALLGOALS Simp_tac), (Clarify_tac 1), (subgoal_tac "Ball (set list) (valid rules)" 1), (Clarify_tac 2), (etac validUp 2), Asm_simp_tac 2, (case_tac "allDTs (%u. ~ isCut u) list" 1), (ftac (thin_rl RS cutExRed) 1), (REPEAT (atac 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]) ; val [ExRed, _] = store_thms ("ExReds", meta_std_conj ther) ; 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 rules)" (fn _ => [Safe_tac, (rtac (wfRed RS spec RS mp) 1), Fast_tac 1]) ; val validRed_min = zero_var_indexes (wf_validRed RS wf_min) ; val () = qed_goalw_spec_mp "tcsc" SNCE.thy [validRed_def] "(dtn, dt) : (validRed rules)^* --> 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 "C345 rules --> c8sn rules --> valid rules dt --> \ \ (EX dtn. allDT (Not o isCut) dtn & conclDT dtn = conclDT dt & \ \ valid rules dtn & (dtn, dt) : (validRed rules)^*)" (fn _ => [(cut_facts_tac [validRed_min] 1), Safe_tac, (subgoal_tac "valid rules dtn" 1), (datac (tacthm (etac (rotate_prems 2 ExRed) 2) swap) 3 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] "C345 rules --> c8sn rules --> \ \ IsDerivableR rules {} concl --> IsDerivableR (rules - {cutr}) {} concl" (fn _ => [Safe_tac, (fatac (thin_rl RS redNoCut) 2 1), (REPEAT (force_tac (claset () addSEs [cfpt'], esimps [valid_def]) 1))]) ;