0

1 
infix addsimps addcongs


2 
setsolver setloop setmksimps setsubgoaler;


3 


4 
signature SIMPLIFIER =


5 
sig


6 
type simpset


7 
val addcongs: simpset * thm list > simpset


8 
val addsimps: simpset * thm list > simpset


9 
val asm_full_simp_tac: simpset > int > tactic


10 
val asm_simp_tac: simpset > int > tactic


11 
val empty_ss: simpset


12 
val merge_ss: simpset * simpset > simpset


13 
val prems_of_ss: simpset > thm list


14 
val rep_ss: simpset > {simps: thm list, congs: thm list}


15 
val setsolver: simpset * (thm list > int > tactic) > simpset


16 
val setloop: simpset * (int > tactic) > simpset


17 
val setmksimps: simpset * (thm > thm list) > simpset


18 
val setsubgoaler: simpset * (simpset > int > tactic) > simpset


19 
val simp_tac: simpset > int > tactic


20 
end;


21 


22 
structure Simplifier:SIMPLIFIER =


23 
struct


24 


25 
datatype simpset =


26 
SS of {mss: meta_simpset,


27 
simps: thm list,


28 
congs: thm list,


29 
subgoal_tac: simpset > int > tactic,


30 
finish_tac: thm list > int > tactic,


31 
loop_tac: int > tactic};


32 


33 
val empty_ss =


34 
SS{mss=empty_mss,


35 
simps= [],


36 
congs= [],


37 
subgoal_tac= K(K no_tac),


38 
finish_tac= K(K no_tac),


39 
loop_tac= K no_tac};


40 


41 


42 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =


43 
SS{mss=mss,


44 
simps= simps,


45 
congs= congs,


46 
subgoal_tac= subgoal_tac,


47 
finish_tac=finish_tac,


48 
loop_tac=loop_tac};


49 


50 
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =


51 
SS{mss=mss,


52 
simps= simps,


53 
congs= congs,


54 
subgoal_tac= subgoal_tac,


55 
finish_tac=finish_tac,


56 
loop_tac=loop_tac};


57 


58 
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =


59 
SS{mss=mss,


60 
simps= simps,


61 
congs= congs,


62 
subgoal_tac= subgoal_tac,


63 
finish_tac=finish_tac,


64 
loop_tac=loop_tac};


65 


66 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =


67 
SS{mss=Thm.set_mk_rews(mss,mk_simps),


68 
simps= simps,


69 
congs= congs,


70 
subgoal_tac= subgoal_tac,


71 
finish_tac=finish_tac,


72 
loop_tac=loop_tac};


73 


74 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =


75 
let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)


76 
in


77 
SS{mss= Thm.add_simps(mss,rews'),


78 
simps= rews' @ simps,


79 
congs= congs,


80 
subgoal_tac= subgoal_tac,


81 
finish_tac=finish_tac,


82 
loop_tac=loop_tac}


83 
end;


84 


85 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =


86 
SS{mss= Thm.add_congs(mss,newcongs),


87 
simps= simps,


88 
congs= newcongs @ congs,


89 
subgoal_tac= subgoal_tac,


90 
finish_tac=finish_tac,


91 
loop_tac=loop_tac};


92 


93 
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},


94 
SS{simps=simps2,congs=congs2,...}) =


95 
let val simps' = gen_union eq_thm (simps,simps2)


96 
val congs' = gen_union eq_thm (congs,congs2)


97 
val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)


98 
val mss' = Thm.add_simps(mss',simps')


99 
val mss' = Thm.add_congs(mss',congs')


100 
in SS{mss= mss',


101 
simps= simps,


102 
congs= congs',


103 
subgoal_tac= subgoal_tac,


104 
finish_tac= finish_tac,


105 
loop_tac= loop_tac}


106 
end;


107 


108 
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;


109 


110 
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};


111 


112 
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =


113 
let val rews = flat(map (mk_rews_of_mss mss) prems)


114 
in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,


115 
subgoal_tac=subgoal_tac,finish_tac=finish_tac,


116 
loop_tac=loop_tac}


117 
end;


118 


119 
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =


120 
let fun solve_all_tac mss =


121 
let val ss = SS{mss=mss,simps=simps,congs=congs,


122 
subgoal_tac=subgoal_tac,


123 
finish_tac=finish_tac, loop_tac=loop_tac}


124 
fun solve1 thm = tapply(


125 
STATE(fn state => let val n = nprems_of state


126 
in if n=0 then all_tac


127 
else subgoal_tac ss 1 THEN


128 
COND (has_fewer_prems n) (Tactic solve1) no_tac


129 
end),


130 
thm)


131 
in DEPTH_SOLVE(Tactic solve1) end


132 


133 
fun simp_loop i thm =


134 
tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN


135 
(finish_tac (prems_of_mss mss) i ORELSE STATE(looper i)),


136 
thm)


137 
and allsimp i m state =


138 
let val n = nprems_of state


139 
in EVERY(map (fn j => simp_loop_tac (i+j)) ((nm) downto 0)) end


140 
and looper i state =


141 
TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))


142 
and simp_loop_tac i = Tactic(simp_loop i)


143 


144 
in simp_loop_tac end;


145 


146 
fun asm_simp_tac ss =


147 
METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);


148 


149 
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);


150 


151 
end;
