(* pftr.ML *)
(* procedures to process a proof tree and apply cut-elimination procedure *)
(* name_of_thm : thm -> string, gives name of a theorem - in name.ML *)
uses "name.ML" ;
exception NoSubgoal of thm ;
exception NotFinished ;
(* ht : 'a -> 'a list -> 'a * 'a list
td : 'a -> int -> 'a list -> 'a list * 'a list
ht empty gives notional head and tail of rttb list,
td empty n gives notional take and drop n items of rttb list;
`notional' means null list [] is extended with empty
items (proof trees) as necessary *)
fun ht empty [] = (empty, [])
| ht empty (ptb::ptbl) = (ptb, ptbl) ;
fun td empty 0 rttbl = ([], rttbl)
| td empty n rttbl =
let val (head, tail) = ht empty rttbl
val (take, drop) = td empty (n-1) tail
in (head::take, drop) end ;
(* represents a proof tree, where each step is resolution (or similar)
of a subgoal; root of the structure is bottom of the proof *)
datatype rtpt = Unf (* proof unfinished at this point *)
| Pr of (thm * rtpt list) ; (* list of proof trees of premises *)
(* ptpthm : rtpt -> thm, get theorem from proof tree *)
fun ptpthm Unf = seq_asm_rl
| ptpthm (Pr (th, pts)) = map ptpthm pts MRS th ;
(* iterate, reviter : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
where f x is a function, gives composition of {f x | x in list};
iterate applies head of list first, reviter applies head last *)
fun iterate f (ti::til) = iterate f til o f ti
| iterate f [] = I ;
fun reviter f (ti::til) = f ti o reviter f til
| reviter f [] = I ;
(* add2ptl : thm * int -> rtpt list -> rtpt list
adds theorem and subgoal number to bottom of list of proof trees *)
fun add2ptl (th,1) rtptl =
let val (take, drop) = td Unf (nprems_of th) rtptl
in Pr (th, take) :: drop end
| add2ptl (th,n) rtptl =
let val (take, drop) = td Unf (n-1) rtptl
in take @ add2ptl (th,1) drop end ;
(* addl2ptl : (thm * int) list -> rtpt list -> rtpt list
adds list of (theorem, subgoal number) pairs
to bottom of list of proof trees *)
val addl2ptl = reviter add2ptl ;
(* tsl2pt : (thm * int) list -> rtpt
creates proof tree out of list of (theorem, subgoal number) pairs *)
fun tsl2pt tsl = case reviter add2ptl tsl [] of [pt] => pt | [] => Unf ;
(* pt2sga : rtpt -> (thm * int) list * int -> (thm * int) list * int
tsl is list, in reverse order, of (thm, subgoal) pairs,
(in effect, we are just building a list starting from the front)
fsg is the number of the first subgoal on which the proof tree(s) operate
input arguments (tsl, fsg) represent the part of the proof tree already
processed, in terms of the initial part of the (thm, subgoal) list,
and number of proof tree branches not closed
the output is (tsl, fsg) as updated by processing the part of the proof
tree given by the first argument *)
fun pt2sga Unf (tsl, fsg) = (tsl, fsg+1)
| pt2sga (Pr (th, ptl)) (tsl, fsg) =
iterate pt2sga ptl ((th, fsg) :: tsl, fsg) ;
fun pt2tsl pt = rev (fst (pt2sga pt ([], 1))) ;
(* build a proof tree differently, each node is a pair of an rtpt
with an integer, the integer showing the number of subgoals in that
part of the tree *)
(* represents a proof tree, where each step is resolution (or similar)
of a subgoal; root of the structure is bottom of the proof;
each tree also has an integer, number of unfinished branches *)
datatype rtnt = Unfn (* proof unfinished at this point *)
| Prn of (thm * (rtnt * int) list) ; (* list of proof trees of premises *)
fun sum (i::il) = i + sum il | sum [] = 0 ;
fun p2n Unf = (Unfn, 1)
| p2n (Pr (th, ptl)) =
let val ntl = map p2n ptl
in (Prn (th, ntl), sum (map snd ntl)) end ;
fun n2p (Unfn, 1) = Unf
| n2p (Prn (th, ntl), n) =
let val true = n = sum (map snd ntl) (* with check *)
in Pr (th, map n2p ntl) end ;
(* following for trees of type rtnt * int *)
(* add2nt : thm * int -> int -> rtnt * int -> rtnt * int
add2ntl : thm * int -> int -> (rtnt * int) list -> (rtnt * int) list
addl2nt : (thm * int) list -> rtnt * int -> rtnt * int
finds location of indicated subgoal number in proof tree and adds
the new entry; if subgoal number not found, number in remaining
part of tree returned *)
fun add2nt (th, np) 1 (Unfn, 1) = (Prn (th, replicate np (Unfn, 1)), np)
| add2nt (th, np) i (Prn (thp, ntl), m) =
(Prn (thp, add2ntl (th, np) i ntl), m+np-1)
and add2ntl (th, np) i ((nt,k)::ntsl) =
if i > k then (nt,k) :: add2ntl (th, np) (i-k) ntsl
else add2nt (th, np) i (nt, k) :: ntsl ;
(* addl2nt : (thm * int) list -> rtnt * int -> rtnt * int
adds a list of new steps to top of a proof tree *)
fun addl2nt ((th,sg)::tsl) nt =
addl2nt tsl (add2nt (th, nprems_of th) sg nt)
| addl2nt [] nt = nt ;
(* addb2pt : rtpt list * rtpt -> rtpt list * rtpt
addb2ptl : rtpt list * rtpt list -> rtpt list * rtpt list
pt : a proof tree, with some open branches
ptl : a list of such proof trees
btl : a list of proof trees
addb2pt (btl, pt), addb2ptl (btl, ptl) puts the trees in the
list btl onto the open branches of pt or of the trees in ptl
returns (unused part of btl, modified pt/ptl) *)
fun addb2pt (btl, Pr (th, brl)) =
let val (btlr, nbrl) = addb2ptl (btl, brl)
in (btlr, Pr (th, nbrl)) end
| addb2pt (bt::btl, Unf) = (btl, bt)
and addb2ptl (btl, pt::ptl) =
let val (btlr, npt) = addb2pt (btl, pt)
val (btlrr, nptl) = addb2ptl (btlr, ptl)
in (btlrr, npt::nptl) end
| addb2ptl (btl, []) = (btl, []) ;
(* addbr2pt : rtpt list -> rtpt -> rtpt
as for addb2pt, but checks that all of btl used up, and
doesn't return the rest *)
fun addbr2pt btl pt = let val (nil, npt) = addb2pt (btl, pt) in npt end ;
(* replace_th : (string * rtpt) list -> rtpt -> rtpt
replaces a theorem in a proof tree by an associated proof tree,
first argument is an association list of theorem names and their
replacement proof trees *)
fun replace_th nal (Pr (th, btl)) =
(case assoc_string (nal, name_of_thm th) of
None => Pr (th, map (replace_th nal) btl)
| Some bt => addbr2pt (map (replace_th nal) btl) bt)
| replace_th _ Unf = Unf ;
(* andl : bool list -> bool, conjunction of elements of list *)
fun andl [] = true | andl (x :: xs) = x andalso andl xs;
(* pteq : rtpt * rtpt -> bool,
test equality of proof trees, using theorem names *)
fun pteq (Unf, Unf) = true
| pteq (Pr (th1, ptl1), Pr (th2, ptl2)) =
name_of_thm th1 = name_of_thm th2 andalso andl (map2 pteq (ptl1, ptl2))
| pteq _ = false ;
(* simppt : thm -> rtpt, make simple proof tree, handy for testing *)
fun simppt th = Pr (th, replicate (nprems_of th) Unf) ;
(* findcuts : rtpt -> rtpt list -> rtpt list
finds trees rooted in "cut", adds to list *)
local val cutname = name_of_thm cut in
fun findcuts (tr as Pr (th, rtl)) =
if name_of_thm th = cutname then cons tr
else reviter findcuts rtl
| findcuts Unf = I
end ;
(* npftr : rtpt -> int, gives no of nodes (including Unf) *)
fun npftr Unf = 1
| npftr (Pr (_, rtl)) = 1 + sum (map npftr rtl) ;