(* C8.ML for dRA *) uses "autoC8.ML" ; (* following two duplicated *) val cutname = name_of_thm cut ; val idfname = name_of_thm idf ; exception NoC8case of (string * string) ; (* C8 : (rtpt, rtpt) -> rtpt where args are proof trees ending in introduction rules on right and left for some formula operator, with say X |- A and A |- Y at the bottom, produces a proof tree with cuts higher up, with X |- Y at the bottom *) local val rtac = pair (* simpler than using tsltac *) fun thmnames ((ths, tha), tlb) = ((name_of_thm ths, name_of_thm tha), tlb) val c8tab = map thmnames [ (* ((ors, ora), ([rtac (md2 cs1) 1, rtac cut 1, rtac (md1 cs1) 1, rtac (md2 cs2) 1, rtac cut 1, rtac (md1 cs2) 1], false)), ((ands, anda), ([rtac (md2 ca1) 1, rtac cut 1, rtac (md1 ca1) 2, rtac (md2 ca2) 2, rtac cut 2, rtac (md1 ca2) 3], false)), ((rss, rsa), ([rtac (md2 ss1) 1, rtac cut 1, rtac (md1 ss1) 1, rtac (md2 ss2) 1, rtac cut 1, rtac (md1 ss2) 1], false)), ((comps, compa), ([rtac (md2 sa1) 1, rtac cut 1, rtac (md1 sa1) 2, rtac (md2 sa2) 2, rtac cut 2, rtac (md1 sa2) 3], false)), *) ((ors, orA), ([rtac cS 1, rtac (md2 cs1) 1, rtac cut 1, rtac (md1 cs1) 1, rtac (md2 cs2) 1, rtac cut 1, rtac (md1 cs2) 1], false)), ((andS, anda), ([rtac cA 1, rtac (md2 ca1) 1, rtac cut 1, rtac (md1 ca1) 2, rtac (md2 ca2) 2, rtac cut 2, rtac (md1 ca2) 3], false)), ((convs, conva), ([rtac (md2 blbl) 1, rtac cut 1, rtac (md2 blob) 2, rtac (md1 blob) 1], false)), ((nots, nota), ([rtac (md2 dcp) 1, rtac cut 1, rtac (md2 sS) 2, rtac (md1 sA) 1], true)), ((fS, fA), ([], false)), ((tS, tA), ([], false)), ((fS, (fA RS exa)), ([rtac exa 1], false)), (((tS RS exs), tA), ([rtac exs 1], false)), ((r1S, r1A), ([], false)), ((r0S, r0A), ([], false)) ] fun rr names = case assoc (c8tab, names) of Some tlb => tlb | None => raise NoC8case names in fun C8 (left as Pr (botl, restl), right as Pr (botr, restr)) = let val names as (lname, rname) = (name_of_thm botl, name_of_thm botr) in if lname = idfname then right else if rname = idfname then left else let val (rtl, rev) = rr names val [ptl] = addl2ptl rtl (if rev then restr @ restl else restl @ restr) (* val _ = pairself print names *) in ptl end end end ; (* ac8t : ((string * string) * (rtpt list * rtpt list -> rtpt)) list table of entries for pairs of rules *) val ac8t = map mkc8te [ (ors, ora), (rss, rsa), (anda, ands), (compa, comps), (conva, md1 blbl RS convs), (convs, md1 blbl RS conva), (nots, md1 dcp RS nota), (nota, md1 dcp RS nots)] ; fun ac8 (left as Pr (botl, restl), right as Pr (botr, restr)) = let val names as (lname, rname) = (name_of_thm botl, name_of_thm botr) in if lname = idfname then right else if rname = idfname then left else case assoc (ac8t, names) of Some ptf => ptf (restl, restr) | None => C8 (left, right) end ;