open CutRed ; val cutReduces_same_conc = prove_goal CutRed.thy "cutReduces dt1 dt2 --> conclDT dt1 = conclDT dt2" (fn _ => [exhaust_tac "dt1" 1, Auto_tac]) RS mp ; val cutReduces_Unf_2 = prove_goal CutRed.thy " ~ (cutReduces dt (Unf seq))" (fn _ => [exhaust_tac "dt" 1, Auto_tac]) ; val cutReduces_Unf_1 = prove_goal CutRed.thy " ~ (cutReduces (Unf seq) dt)" (fn _ => [Auto_tac]) ; val cutReduces_Nil = prove_goal CutRed.thy " ~ (cutReduces (Der seq cutr []) dt)" (fn _ => [Auto_tac]) ; val cutReduces_IsCut = prove_goal CutRed.thy "(cutReduces (Der seq rule dtl) dt --> rule = cutr)" (fn _ => [Auto_tac]) RS mp ; val c8redsfP_reflNC = store_thm ("c8redsfP_reflNC", prove_goalw CutRed.thy [c8redsfP] "(botRule dt ~= cutr) = c8redsfP dt dt" (fn _ => [ (fast_tac (claset () addSIs [isSubt_refl] addSDs [rewrite_rule [not_def] ipsubfml_irrefl RS mp]) 1)])) ; val c8redP_reflNC = store_thm ("c8redP_reflNC", prove_goalw CutRed.thy [c8redP] "(botRule dt ~= cutr) = c8redP dt dt" (fn _ => [ (fast_tac (claset () addSIs [isSubt_refl]) 1)])) ; val () = qed_goalw_spec_mp "c8redsfP_c8redP" CutRed.thy [c8redsfP, c8redP] "c8redsfP dt dtn --> c8redP dt dtn" (fn _ => [(fast_tac (claset () addSIs [ipsubfml_size]) 1)]) ; val trivC8sf = store_thm ("trivC8sf", meta_std (prove_goalw CutRed.thy [c8redsfP] "dts : set dtl & conclDT dts = seq --> c8redsfP (Der seq cutr dtl) dts" (fn _ => [Safe_tac, (etac subtASym' 2), (Simp_tac 2), (eatac (isSubtI RS isSubt_trans) 1 1)]))) ; val trivC8 = trivC8sf RS c8redsfP_c8redP ; val () = qed_goal "wf_LRPorder" CutRed.thy "wf LRPorder" (fn _ => [ rtac (wf_iff_no_infinite_down_chain RS iffD2) 1, Safe_tac, (forw_inst_tac [("x", "0")] spec 1), (forw_inst_tac [("x", "Suc 0")] spec 1), (REPEXP (etac LRPorder.elim) 1), (ALLGOALS (asm_full_simp_tac (init_ss addsimps [cutLRPcf_def]))), (ALLGOALS (dres_inst_tac [("x", "Suc (Suc 0)")] spec)), (ALLGOALS (etac LRPorder.elim)), (ALLGOALS (asm_full_simp_tac (init_ss addsimps [cutLRPcf_def]))) ]) ; fun tacsNE _ = [ (case_tac "dt" 1), Asm_simp_tac 2, (asm_simp_tac (esimps [c8redP]) 1), Safe_tac, (eres_inst_tac [("x", "Der sequent cutr list")] allE 1), Full_simp_tac 1, (TRY (etac (wf_LRPorder RS wf_not_refl RS notE) 1))] ; val () = bind_thm ("c8redNE", meta_std (prove_goal CutRed.thy "c8redP dt dtn & isCut dt --> dtn ~= dt" tacsNE)) ; val () = bind_thm ("nparRedNE", meta_std (prove_goal CutRed.thy "nparRedP dt dtn & isCut dt --> dtn ~= dt" tacsNE)) ; val [c8red] = [c8red_def] RL [meta_eq_to_obj_eq RS iffD1 RS conjunct2 RS conjunct2 RS conjunct2] ; (* val nparRed = read_instantiate [("dt5", "(Der ?seq cutr ?dtl)")] nparRed' ; *) val () = qed_goalw_spec_mp "vformCR" CutRed.thy [c8sn_def] "c8sn rules --> dt = Der seq cutr dtl --> \ \ cutIsLRP form dt --> valid rules dt \ \ --> (EX dtn. cutReduces dt dtn & valid rules dtn)" (fn _ => [ Safe_tac, (REPEAT (etac allE 1)), (etac impE 1), Fast_tac 1, etac ex_match 1, (asm_full_simp_tac (simpset () delsimps [wfb_Der]) 1), (safe_tac (claset () addSDs [c8redsfP_c8redP])), (force_tac (claset () addSDs [lrwfc], esimps [valid_def] delsimps [wfb_Der]) 1), (dtac c8redNE 2), Simp_tac 2, (case_tac "dtn" 1), (ALLGOALS Asm_full_simp_tac)]) ; ~