(* autoC8.ML, automatic generation of proof of C8 *) uses "pftr.ML" ; fun delsf (Const ("DL.Structform", _) $ F) = F | delsf tm = raise TERM ("delsf : ", [tm]) ; fun ixn_of (Var (ixn, _)) = ixn | ixn_of tm = raise TERM ("ixn_of : ", [tm]) ; (* fun C8 (left as Pr (botl, restl), right as Pr (botr, restr)) = let val cutsl = concl_of botl val cutsr = concl_of botr val cutfl = seqside Suc cutsl val cutfr = seqside Ant cutsr fun ops (b $ l $ r) = (b, [l, r]) | ops (b $ u) = (b, [u]) | ops (b) = (b, []) val (bl, ndsl) = ops cutfl val (br, ndsr) = ops cutfr val true = bl = br (* simpfs : term -> side option, tests whether term is simply A |- X or X |- A, if so, indicates which side formula is on *) fun simpfs (Const ("DL.Sequent", _) $ Var (ixns, _) $ (Const ("DL.Structform", _) $ Var (ixnf, _)) ) = Some Suc | simpfs (Const ("DL.Sequent", _) $ (Const ("DL.Structform", _) $ Var (ixnf, _)) $ Var (ixns, _) ) = Some Ant | simpfs _ = None (* allsame : ('a -> ''b option) -> 'a list -> ''b option tests whether all elements of list give same result when f applied *) fun allsame f [e] = f e | allsame f [] = None | allsame f (e::el) = case allsame f el of None => None | Some r => if f e = Some r then Some r else None *) (* natir is introduction rule like X |- A s B ==> X |- A f B vpir is introduction rule like [| A |- Y ; B |- Z |] ==> A f B |- Y s Z ; this routine gives proof tree of X |- Y s Z by cuts on A and B, not on A f B *) (* notes - assumes each formula variable in introduction rule appears exactly once in premises and in conclusion; assumes one introduction rule has one premise, the other has one premise for each formula variable *) val natside = Suc ; val vpside = Ant ; val natir = ors ; val vpir = ora ; val tr = Unf ; val vptrs = [Unf, Unf] ; val vptr = hd vptrs ; (* val ops = fn : term -> term * term list separates term into operator and operands *) fun ops (b $ l $ r) = (b, [l, r]) | ops (b $ u) = (b, [u]) | ops (b) = (b, []) ; (* patsfvi : indexname -> term -> bool tests a term to see if it is a structure which is a given formula variable *) fun patsfvi indnam (Const ("DL.Structform", _) $ Var (indnamv, _)) = indnam = indnamv | patsfvi _ _ = false ; (* findsfvi : term -> indexname -> side * (term * oppos) list finds a structure which is a given formula variable in a sequent *) fun findsfvi tm indnam = findseq (patsfvi indnam) tm ; (* patsfv : term -> bool tests a term to see if it is a structure which is any formula variable *) fun patsfv (Const ("DL.Structform", _) $ Var _) = true | patsfv _ = false ; (* patsv : term -> bool tests a term to see if it is a structure variable *) fun patsv (Var (_, Type ("DL.structure", []))) = true | patsv _ = false ; (* patsf : term -> bool tests a term to see if it is a structure which is a formula term *) fun patsf (Const ("DL.Structform", _) $ _) = true | patsf _ = false ; (* patsft : term -> term -> bool tests a term to see if it is a structure which is a given formula term *) fun patsft ftm (Const ("DL.Structform", _) $ tm) = tm = ftm | patsft _ _ = false ; fun pos (e :: es) x = if x = e then 0 else 1 + pos es x ; (* val natp = natprem ; val vpp = hd vpprems ; val natlocs = map (findsfvi natprem) (map ixn_of natfv) ; (* cutvpp : term -> term -> rtpt -> rtpt -> rtpt cuts a premise of the vp side into the nat side premise *) fun cutvpp natp vpprem vptr tr = let val (fvside, []) = findseq patsfv vpprem val fv = delsf (seqside fvside vpprem) val fvpos = pos vpfv fv val nfv = nth (natfv, fvpos) val nfvloc = findseq (patsft nfv) natp val dp = tn (getdpl dptab nfvloc) in case fvside of Ant => Pr (md2 dp, [Pr (cut, [Pr (md1 dp, [tr]), vptr])]) | Suc => Pr (md2 dp, [Pr (cut, [vptr, Pr (md1 dp, [tr])])]) end ; (* cutvpp : term -> term -> rtpt -> rtpt -> rtpt cuts a premise of the vp side into the nat side premise ; written to do as much of the calculation as possible once only *) fun cutvpp natp vpprem = let val (fvside, []) = findseq patsfv vpprem val fv = delsf (seqside fvside vpprem) val fvpos = pos vpfv fv val nfv = nth (natfv, fvpos) val nfvloc = findseq (patsft nfv) natp val dp = tn (getdpl dptab nfvloc) fun fant vptr tr = Pr (md2 dp, [Pr (cut, [Pr (md1 dp, [tr]), vptr])]) fun fsuc vptr tr = Pr (md2 dp, [Pr (cut, [vptr, Pr (md1 dp, [tr])])]) val f = case fvside of Ant => fant | Suc => fsuc in f end ; (* val cutall = fn : term -> term list -> rtpt list -> rtpt -> rtpt performs cutvpp for all fvs and premises on the vp side *) fun cutall natp (vpprem :: vpprems) (vptr :: vptrs) = cutvpp natp vpprem vptr o cutall natp vpprems vptrs | cutall _ [] [] = I ; (* alternative *) fun cutall natp (vpprem :: vpprems) (vptr :: vptrs) = cutall natp vpprems vptrs o cutvpp natp vpprem vptr | cutall _ [] [] = I ; fun c8r (rules, rulea) = let val prs = prems_of rules val pra = prems_of rulea val concls = concl_of rules val concla = concl_of rulea val (natir, vpir, natside, vpside) = case (length prs, length pra) of (2,1) => (rulea, rules, Ant, Suc) | (1,2) => (rules, rulea, Suc, Ant) val (natop, natfv) = (ops o delsf o seqside natside o concl_of) natir val (vpop, vpfv) = (ops o delsf o seqside vpside o concl_of) vpir val true = natop = vpop val [natprem] = prems_of natir val vpprems = prems_of vpir in cutall natprem vpprems (replicate 2 Unf) Unf end ; fun c8t (rules, rulea) = eq_rule (ptpthm (c8r (rules, rulea)), [rules, rulea] MRS cut) ; fun c8nv (natir, vpir) = let val (natside, []) = findseq patsf (concl_of natir) val (vpside, []) = findseq patsf (concl_of vpir) val false = natside = vpside val (natop, natfv) = (ops o delsf o seqside natside o concl_of) natir val (vpop, vpfv) = (ops o delsf o seqside vpside o concl_of) vpir val true = natop = vpop val [natprem] = prems_of natir val vpprems = prems_of vpir val npr = length vpprems val cutth = case natside of Suc => [natir, vpir] MRS cut | Ant => [vpir, natir] MRS cut val pt = cutall natprem vpprems (replicate npr Unf) Unf val ptth = ptpthm pt in (ptth, cutth, eq_rule (ptth, cutth)) end ; *) uses "eqrule.ML" ; (* c8te : C8-table entry, contains names of introduction rules just above cut, and function to merge the proof trees (above those rules) to give a proof tree whose conclusion is the conclusion of the cut *) type c8te = (string * string) * (rtpt list * rtpt list -> rtpt) ; (* mkc8te : thm * thm -> c8te makes C8-table entry, arguments are introduction rules ; natir is rule which gives a straight translation from structural connective to logical connective (other side of conclusion is simple structural variable) ; vpir is rule which has one premise for each operand of the connective, each premise of the form A |- X *) fun mkc8te (natir, vpir) = let val (natside, []) = findseq patsf (concl_of natir) val (vpside, []) = findseq patsf (concl_of vpir) val false = natside = vpside val (natop, natfv) = (ops o delsf o seqside natside o concl_of) natir val (vpop, vpfv) = (ops o delsf o seqside vpside o concl_of) vpir val true = natop = vpop val [natprem] = prems_of natir val vpprems = prems_of vpir val nsvloc = findseq patsv natprem val dispnsv = case nsvloc of (_, []) => I | loc => (fn tr => Pr (md1 (tn (getdpl dptab loc)), [tr])) (* cutvpp : term -> rtpt -> rtpt -> rtpt cuts a premise of the vp side into the nat side premise ; written to do as much of the calculation as possible once only *) fun cutvpp vpprem = let val (fvside, []) = findseq patsfv vpprem val fv = delsf (seqside fvside vpprem) val fvpos = pos vpfv fv val nfv = nth (natfv, fvpos) val nfvloc = findseq (patsft nfv) natprem val dp = tn (getdpl dptab nfvloc) fun fant vptr tr = Pr (md2 dp, [Pr (cut, [Pr (md1 dp, [tr]), vptr])]) fun fsuc vptr tr = Pr (md2 dp, [Pr (cut, [vptr, Pr (md1 dp, [tr])])]) val f = case fvside of Ant => fant | Suc => fsuc in f end (* cutfs : (rtpt -> rtpt -> rtpt) list list of one cutvpp function for each premise of vpir *) val cutfs = map cutvpp vpprems (* cutall : (rtpt -> rtpt -> rtpt) list -> rtpt list -> rtpt -> rtpt performs cutvpp for all fvs and premises on the vp side *) fun cutall (cutf :: cutfs) (vptr :: vptrs) = cutf vptr o cutall cutfs vptrs | cutall [] [] = I (* alternative *) fun cutall (cutf :: cutfs) (vptr :: vptrs) = cutall cutfs vptrs o cutf vptr | cutall [] [] = I (* ptfant, ptfsuc, ptf : rtpt list * rtpt list -> rtpt as cutall cutfs, but arguments now lists of proof trees on left and right sides, above introduction rules *) fun ptfsuc ([lptr], rptrs) = dispnsv (cutall cutfs rptrs lptr) fun ptfant (lptrs, [rptr]) = dispnsv (cutall cutfs lptrs rptr) val (l, r, ptf) = case natside of Suc => (natir, vpir, ptfsuc) | Ant => (vpir, natir, ptfant) val names = (name_of_thm l, name_of_thm r) (* check that new and original proof trees (without premises) give same theorems *) val chths as (thc, thp) = ([l, r] MRS cut, ptpthm (dispnsv (cutall cutfs (replicate (length vpprems) Unf) Unf))) val _ = if eq_rule chths then () else raise THM ("mkc8te : ", 0, [thc, thp]) in (names, ptf) end ;