infix addsimps addcongs
setsolver setloop setmksimps setsubgoaler;
signature SIMPLIFIER =
sig
type simpset
val addcongs: simpset * thm list -> simpset
val addsimps: simpset * thm list -> simpset
val asm_full_simp_tac: simpset -> int -> tactic
val asm_simp_tac: simpset -> int -> tactic
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val prems_of_ss: simpset -> thm list
val rep_ss: simpset -> {simps: thm list, congs: thm list}
val setsolver: simpset * (thm list -> int -> tactic) -> simpset
val setloop: simpset * (int -> tactic) -> simpset
val setmksimps: simpset * (thm -> thm list) -> simpset
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
val simp_tac: simpset -> int -> tactic
end;
structure Simplifier:SIMPLIFIER =
struct
datatype simpset =
SS of {mss: meta_simpset,
simps: thm list,
congs: thm list,
subgoal_tac: simpset -> int -> tactic,
finish_tac: thm list -> int -> tactic,
loop_tac: int -> tactic};
val empty_ss =
SS{mss=empty_mss,
simps= [],
congs= [],
subgoal_tac= K(K no_tac),
finish_tac= K(K no_tac),
loop_tac= K no_tac};
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
SS{mss=mss,
simps= simps,
congs= congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac};
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
SS{mss=mss,
simps= simps,
congs= congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac};
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =
SS{mss=mss,
simps= simps,
congs= congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac};
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
SS{mss=Thm.set_mk_rews(mss,mk_simps),
simps= simps,
congs= congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac};
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
in
SS{mss= Thm.add_simps(mss,rews'),
simps= rews' @ simps,
congs= congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac}
end;
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
SS{mss= Thm.add_congs(mss,newcongs),
simps= simps,
congs= newcongs @ congs,
subgoal_tac= subgoal_tac,
finish_tac=finish_tac,
loop_tac=loop_tac};
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
SS{simps=simps2,congs=congs2,...}) =
let val simps' = gen_union eq_thm (simps,simps2)
val congs' = gen_union eq_thm (congs,congs2)
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
val mss' = Thm.add_simps(mss',simps')
val mss' = Thm.add_congs(mss',congs')
in SS{mss= mss',
simps= simps,
congs= congs',
subgoal_tac= subgoal_tac,
finish_tac= finish_tac,
loop_tac= loop_tac}
end;
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
let val rews = flat(map (mk_rews_of_mss mss) prems)
in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
subgoal_tac=subgoal_tac,finish_tac=finish_tac,
loop_tac=loop_tac}
end;
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
let fun solve_all_tac mss =
let val ss = SS{mss=mss,simps=simps,congs=congs,
subgoal_tac=subgoal_tac,
finish_tac=finish_tac, loop_tac=loop_tac}
fun solve1 thm = tapply(
STATE(fn state => let val n = nprems_of state
in if n=0 then all_tac
else subgoal_tac ss 1 THEN
COND (has_fewer_prems n) (Tactic solve1) no_tac
end),
thm)
in DEPTH_SOLVE(Tactic solve1) end
fun simp_loop i thm =
tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
(finish_tac (prems_of_mss mss) i ORELSE STATE(looper i)),
thm)
and allsimp i m state =
let val n = nprems_of state
in EVERY(map (fn j => simp_loop_tac (i+j)) ((n-m) downto 0)) end
and looper i state =
TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))
and simp_loop_tac i = Tactic(simp_loop i)
in simp_loop_tac end;
fun asm_simp_tac ss =
METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
end;