open WC8cases ; (* ; val prems = it ; *) (* we obtain variants of the C8 theorems, eg, orC8W in place of orC8; both give a reduction of an LRP cut on A v B, but whereas orC8 assumes all other cuts are on A or B, and gives a result where all cuts are on A or B, orC8W gives a reduction satisfying c8redP (which implies c8redP, but gives exactly what we'd like to write in the paper) *) val restC8W'' = " allDT wfb dt; allDT (frb rls) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & allDT wfb dtn & allDT (frb rls) dtn & \ \ c8redP dt dtn & set (premsDT dtn) <= set (premsDT dt)" ; val orC8W'' = prove_goal WC8_thy ("[| dt = Der ($Z |- $X,, $Y) cutr \ \ [Der zab ors [dtzab], Der abxy ora [dtax, dtby]] ; \ \ cutOnFmls {A v B} dt; " ^ restC8W'') (tacC8W'' (orC8_2 RS orC8_3)) ; (* val thC8_23 = (orC8_2 RS orC8_3) ; val thC8' = orC8' ; val thC8_2 = orC8_2 ; val thC8_1 = orC8_1 ; val thC8W'' = orC8W'' ; ; val prems = it ; val ts = (tacC8W'' (orC8_2 RS orC8_3)) prems ; *) val andC8W'' = prove_goal WC8_thy ("[| dt = Der ($Y,, $X |- $Z) cutr \ \ [Der abxy ands [dtby, dtax], Der zab anda [dtzab]] ; \ \ cutOnFmls {B && A} dt ; " ^ restC8W'') (tacC8W'' (andC8_2 RS andC8_3)) ; val thC8_23 = (andC8_2 RS andC8_3) ; val ts = (tacC8W'' (andC8_2 RS andC8_3)) prems ; val rsC8W'' = prove_goal WC8_thy ("[| dt = Der ($Z |- $X ;; $Y) cutr \ \ [Der zab rss [dtzab], Der abxy rsa [dtax, dtby]] ; \ \ cutOnFmls {A +++ B} dt ; " ^ restC8W'') (tacC8W'' (rsC8_2 RS rsC8_3)) ; val compC8W'' = prove_goal WC8_thy ("[| dt = Der ($Y ;; $X |- $Z) cutr \ \ [Der abxy comps [dtby, dtax], Der zab compa [dtzab]] ; \ \ cutOnFmls {B oo A} dt ; " ^ restC8W'') (tacC8W'' (compC8_2 RS compC8_3)) ; val convC8W'' = prove_goal WC8_thy ("[| dt = Der ($Z |- $Y) cutr [Der za convs [dtza], Der ay conva [dtay]] ; \ \ cutOnFmls {A^} dt ; " ^ restC8W'') (tacC8W'' (convC8_2 RS convC8_3)) ; val thC8_23 = (convC8_2 RS convC8_3) ; val ts = (tacC8W'' (convC8_2 RS convC8_3)) prems ; val notC8W'' = prove_goal WC8_thy ("[| dt = Der ($Z |- $Y) cutr [Der za nots [dtza], Der ay nota [dtay]] ; \ \ cutOnFmls {--A} dt ; " ^ restC8W'') (tacC8W'' (notC8_2 RS notC8_3)) ; val thC8_2 = convC8_2 ; val thC8' = convC8' ; val tC8W'' = prove_goal WC8_thy ("[| dt = Der ($I |- $Y) cutr [Der IT tS [], Der TY tA [dtiy]] ; \ \ cutOnFmls {T} dt ; " ^ restC8W'') (tacC8W''con tC8_2) ; val fC8W'' = prove_goal WC8_thy ("[| dt = Der ($Y |- $I) cutr [Der IT fS [dtiy], Der TY fA []] ; \ \ cutOnFmls {F} dt ; " ^ restC8W'') (tacC8W''con fC8_2) ; val r1C8W'' = prove_goal WC8_thy ("[| dt = Der ($E |- $Y) cutr [Der IT r1S [], Der TY r1A [dtiy]] ; \ \ cutOnFmls {r1} dt ; " ^ restC8W'') (tacC8W''con r1C8_2) ; val r0C8W'' = prove_goal WC8_thy ("[| dt = Der ($Y |- $E) cutr [Der IT r0S [dtiy], Der TY r0A []] ; \ \ cutOnFmls {r0} dt ; " ^ restC8W'') (tacC8W''con r0C8_2) ; val formsts = [("A v B", (orC8_1, SOME orC8W'')), ("A +++ B", (rsC8_1, SOME rsC8W'')), ("A && B", (andC8_1, SOME andC8W'')), ("A oo B", (compC8_1, SOME compC8W'')), ("--A", (notC8_1, SOME notC8W'')), ("A^", (convC8_1, SOME convC8W'')), ("T", (tC8_1, SOME tC8W'')), ("F", (fC8_1, SOME fC8W'')), ("r0", (r0C8_1, SOME r0C8W'')), ("r1", (r1C8_1, SOME r1C8W'')), ("FV str", (FVC8_1, NONE)), ("PP str", (PPC8_1, NONE))] ; val formstrs = map #1 formsts ; (* mkc8W gives the result showing the existence of the replacement proof tree *) fun mkC8W (str, (thC8_1, thC8W''opt)) = let val thstr = "[| cutIsLRP (" ^ str ^ ") dt ; allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & allDT wfb dtn & allDT (frb rls) dtn & \ \ c8redP dt dtn & set (premsDT dtn) <= set (premsDT dt)" in prove_goal WC8_thy thstr (tacC8W thC8_1 thC8W''opt) end ; (* val (str, (thC8_1, thC8W''opt)) = hd formsts ; val prems = it ; *) val thsC8W as [orC8W, rsC8W, andC8W, compC8W, notC8W, convC8W, tC8W, fC8W, r0C8W, r1C8W, FVC8W, PPC8W] = map mkC8W formsts ; val formsC8Ws = ListPair.zip (formstrs, thsC8W) ; fun mkvC8W (str, thC8W) = let val thstr = "[| cutIsLRP (" ^ str ^ ") dt ; valid rls dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & c8redP dt dtn & valid rls dtn" in prove_goalw WC8_thy [valid_def] thstr (fn prems => [(cut_facts_tac prems 1), dtac thC8W 1, Auto_tac]) end ; (* val (str, thC8W) = hd formsC8Ws ; *) val thsvC8W as orvC8W :: _ = map mkvC8W formsC8Ws ; val thsvcC8W = map (rewrite_rule conn_defs) thsvC8W ; (* could prove this, using formsC8Ws, similarly to proof of vformC8W, but do we want to? val formC8W = prove_goal WC8_thy "[| cutIsLRP form dt ; allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & allDT wfb dtn & allDT (frb rls) dtn & \ \ c8redP dt dtn & set (premsDT dtn) <= set (premsDT dt)" *) val () = qed_goalw "c8sn_rls" WC8cases.thy [c8sn_def] "c8sn rls" (fn _ => if general_connectives then [ (safe_tac set_cs), (ftac LRP_LP 1), (case_tac "dt" 1), Clarsimp_tac 2, (case_tac "x = cutr" 1), (res_inst_tac [("x", "dt")] exI 2), (clarsimp_tac (cesimps [c8redP_reflNC RS sym]) 2), (eatac (rotate_prems 1 cut_conns_exh) 1 1), (safe_tac set_cs), (TRYALL (dresolve_tac thsvC8W THEN' atac THEN' atac)), (TRYALL (rtac refl)), (ftac (thin_rl RS lrwfc) 1), (force_tac (claset (), HOL_ss addsimps [valid_def, allDT_Der]) 1), Safe_tac, (rtac exI 1), Safe_tac, atac 1, (etac validUp 2), Simp_tac 2, (rtac trivC8 1), (ALLGOALS Full_simp_tac) ] else [ Safe_tac, (case_tac "form" 1), Safe_tac, (TRYALL (dresolve_tac thsvcC8W THEN' atac THEN' atac)) ]) ;