(* keep.tac *)
(* tactics for replacing parts of term by I,
and them removing them if possible,
requires rules VerI and EfqI, and pr_id *)
signature I_THMS = sig
val VerI : thm ; (* "$I |- $?X ==> $?Y |- $?X" *)
val EfqI : thm ; (* "$?X |- $I ==> $?X |- $?Y" *)
val pr_id : patrules ; (* expressing that $I is identity *)
end ;
signature KEEP = sig
val redstrs : ''a list list -> ''a -> ''a list list ;
val keep_tac : string list -> int -> tactic ;
val keep_tac_sol : (side * oppos list) list -> int ->tactic ;
end ;
functor Keep (I_Thms : I_THMS) : KEEP = struct
(* redstrs : ''a list list -> ''a -> ''a list list
tests a list of lists against a value tch;
where tch is the first element in a list it is deleted;
otherwise that list is deleted *)
fun redstrs ((ch::str)::strs) tch =
if ch = tch then str::(redstrs strs tch)
else redstrs strs tch
| redstrs [] tch = [] ;
fun redstrs_as side = map snd o filter (fn (s, _) => s = side) ;
(* ktes : oppos list -> side -> int -> tactic
in ktes loc side, replaces subterm tm by I
loc is reversed list of operand positions, which indicates location of tm
in the sequent *)
fun ktes loc side =
d_b_tac_sol_p (side, (rev loc)) (rtac I_Thms.VerI, rtac I_Thms.EfqI);
(* ktaux : oppos list list -> oppos list -> term -> side -> int -> tactic
in ktaux strs loc tm asp,
strs is list of operand positions indicating locations of subterms
of tm which are to be kept (ie not replaced by I)
tm is current subterm, loc and side as for ktes above;
the tactic returned will replace the subterms not to be kept by I *)
fun ktaux [[]] loc tm side = (fn i => all_tac) (* whole subterm to be kept *)
| ktaux [] loc tm side = ktes loc side (* no subterm to be kept *)
| ktaux strs loc tm side = (* some subterms to be kept *)
if Library.mem ([], strs) then (fn i => all_tac)
else
let
fun doch lch tm side =
let val rstrs = redstrs strs lch
in ktaux rstrs (lch::loc) tm side end
in
case tm of
(Const (_, _) $ L $ R) => doch Left L side THEN' doch Right R side
| (Const (_, _) $ U) => doch Un U side
end ;
(* ktseq : (side * oppos list) list -> term -> int -> tactic
given a term and a list of positions, returns the tactic which
keeps subterms in the indicated positions and weakens away the rest *)
fun ktseq sols (Const ("DL.Sequent", _) $ L $ R) =
ktaux (redstrs_as Ant sols) [] L Ant THEN'
ktaux (redstrs_as Suc sols) [] R Suc ;
(* keep_tac_sol : (side * oppos list) list -> int -> tactic
keep_tac : string list -> int -> tactic
replaces all but indicated subterms by I, then eliminates I where possible;
in keep_tac_sol sols or keep_tac strs,
sols or strs indicates which subterms are to be kept *)
fun keep_tac_sol sols sg state = (ktseq sols
(nth (prems_of state, sg-1)) THEN' glob_tac (tfpr I_Thms.pr_id)) sg state ;
fun keep_tac strs sg state = keep_tac_sol (map str2apl strs) sg state ;
end ; (* functor Keep *)
(* test
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@l*", "-r*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@l*", "-l*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@r*", "-r*"] 1) ;
goal thy "*@( **A, **B) |- *@**C, **@ D" ;
by (keep_tac ["|*@r*", "-l*"] 1) ;
*)