val WC8_thy = theory "WC8" ; (* sttac : tactic to handle cases of dts being a subtree of itself *) val sttac = [ (* next two lines just to get rid of extraneous assumptions *) (eres_inst_tac [("P", "isSubt ?t dts")] rev_mp), (REPEAT o (etac thin_rl)), (rtac impI), (asm_simp_tac HOL_ss), Clarify_tac, (dtac subtASym''), Simp_tac, Simp_tac] ; (* scftac : tactic to handle cases relying on size of cutformula of dts *) val thcf = meta_std (prove_goal HOL_Cut.thy "cutForm dts = B --> (B, A) : r --> (cutForm dts, A) : r" (fn _ => [Auto_tac])) ; val scftac = EVERY' [rtac disjI2, (subgoal_tac "wfb dts"), (datac cutFormD 1), (resolve_tac [disjI1, disjI2]), (* may need to backtrack *) Simp_tac, Fast_tac, etac thcf, MSSG Simp_tac, (asm_full_simp_tac (simpset () delsimps thms "wfb.simps"))] ; val bl = meta_std (prove_goal HOL_Cut.thy "botRule dts = cutr & dts = spt --> botRule spt = cutr" (fn _ => [Auto_tac ])) ; (* bctac : handle contradiction in premises, between botRule dts = cut and specific value of dts given *) val bctac = let val t3 = conjI RS thin_rl in DETERM o EVERY' [datac bl 1, REPEAT_DETERM o eatac t3 1, rtac FalseE, asm_full_simp_tac (esimps (cut :: dp_defs))] end ; val lem'' = meta_std (prove_goal WC8_thy "cutOnFmls {f} dt & dt = Der seq cutr dtl & allDT wfb dt --> cutForm dt = f" (fn _ => [Safe_tac, (rtac (singleton_iff RS iffD1) 1), (rtac cutOnFmls_cutForm 1), (Asm_simp_tac 2), (rtac (cof_eqv RS iffD2) 1), (etac allDTD1 1), atac 1])) ; val tacC8Ws = [ (Force_tac 2), (* subgoal c8redP dt dtn *) (rewrite_goals_tac [c8redsfP, c8redP]), (strip_tac 1), (etac conjE 1), (datac lem'' 2 1), (REPEAT (thin_tac "allDT ?f dt" 1)), (asm_full_simp_tac (simpset () delsimps [allDT_Der]) 1), (REPEXP (etac disjE) 1), (TRYALL (MSSG bctac)), (TRYALL (EVERY' sttac)), ALLGOALS scftac ] ; fun tacC8W'' thC8_23 prems = tacC8''A thC8_23 prems @ tacC8Ws ; fun tacC8W thC8_1 thC8W''opt prems = [ (cut_facts_tac prems 1), (* deal with cases other than dt = Der sequent rule list, rule = cut *) (exhaust_tac "dt" 1), (hyp_subst_tac 2), (full_simp_tac (esimps [cutIsLRP_def]) 2), (case_tac "rule = cutr" 1), rtac exI 2, (REPEXP (rtac conjI) 2), rtac refl 2, atac 2, atac 2, (resolve_tac ([c8redsfP_reflNC, c8redP_reflNC] RL [iffD1]) 2), (REPEAT (Force_tac 2)), (fatac (reop rev thC8_1) 2 1), (hyp_subst_tac 1), rtac refl 1, ((TRY o etac disjE THEN_ALL_NEW REPEAT o (eresolve_tac [bexE, exE, conjE])) 1), (* using C8 proof tree *) case thC8W''opt of SOME thC8W'' => EVERY [ etac thC8W'' 2, etac LRP_Fmls 2, (REPEAT (atac 2))] | NONE => all_tac, (* case where thC8_1 gives subtree of original tree *) (res_inst_tac [("x", "dt'")] exI 1), (safe_asm_full_simp_tac (esimps [allDTs]) 1), (REPEXP (rtac conjI) 1), (TRYALL Fast_tac), (eresolve_tac [trivC8sf, trivC8] 1), atac 1, (force_tac (claset (), esimps [premsDTs]) 1)] ; fun tacC8W''con thC8_2 prems = [(cut_facts_tac prems 1), (fatac thC8_2 2 1), (res_inst_tac [("x", "dtiy")] exI 1), (Asm_simp_tac 1), rtac conjI 1, (Asm_full_simp_tac 1), (rewrite_goals_tac [c8redsfP, c8redP]), (strip_tac 1), (REPEAT (etac conjE 1)), (thin_tac "dt = ?dt" 1), (asm_full_simp_tac (simpset () delsimps [allDT_Der]) 1), (EVERY' sttac 1)] ; (* ; val prems = it ; *)