(* C8.ML for dKt *) uses "autoC8.ML" ; 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 c8tt = [ ((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)), ((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))] val c8tab = map thmnames c8tt fun rr names = case assoc (c8tab, names) of Some tlb => tlb | None => (raise NoC8case names) (* | None => (writeln (#1 names) ; writeln (#2 names) ; 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 ; (* check of entry in c8tt *) fun chk ((ths, tha), (tsl,b)) = let val pt = tsl2pt tsl val thp = ptpthm pt val thc = [ths, tha] MRS cut in (thp, thc, eq_rule (thp, thc)) end ; (* ac8t : ((string * string) * (rtpt list * rtpt list -> rtpt)) list table of entries for pairs of rules *) val ac8t = map mkc8te [ (* (tA, tS), (fS, fA), check spuriously fails *) (ors, ora), (impS, impa), (anda, ands), (wbxS, wbxa), (bbxs, bbxa), (wdma, wdms), (bdmA, bdms), (wbxs, wbxa), (bdma, bdms), (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 ;