1

1 
(* Title: Provers/simplifier


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1993 TU Munich


5 


6 
Generic simplifier, suitable for most logics.


7 


8 
*)

88

9 
infix addsimps addeqcongs delsimps

0

10 
setsolver setloop setmksimps setsubgoaler;


11 


12 
signature SIMPLIFIER =


13 
sig


14 
type simpset

1

15 
val addeqcongs: simpset * thm list > simpset

0

16 
val addsimps: simpset * thm list > simpset

88

17 
val delsimps: simpset * thm list > simpset

0

18 
val asm_full_simp_tac: simpset > int > tactic


19 
val asm_simp_tac: simpset > int > tactic


20 
val empty_ss: simpset


21 
val merge_ss: simpset * simpset > simpset


22 
val prems_of_ss: simpset > thm list


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


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


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


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


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


28 
val simp_tac: simpset > int > tactic


29 
end;


30 


31 
structure Simplifier:SIMPLIFIER =


32 
struct


33 


34 
datatype simpset =


35 
SS of {mss: meta_simpset,


36 
simps: thm list,


37 
congs: thm list,


38 
subgoal_tac: simpset > int > tactic,


39 
finish_tac: thm list > int > tactic,


40 
loop_tac: int > tactic};


41 


42 
val empty_ss =


43 
SS{mss=empty_mss,


44 
simps= [],


45 
congs= [],


46 
subgoal_tac= K(K no_tac),


47 
finish_tac= K(K no_tac),


48 
loop_tac= K no_tac};


49 


50 


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


52 
SS{mss=mss,


53 
simps= simps,


54 
congs= congs,


55 
subgoal_tac= subgoal_tac,


56 
finish_tac=finish_tac,


57 
loop_tac=loop_tac};


58 


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


60 
SS{mss=mss,


61 
simps= simps,


62 
congs= congs,


63 
subgoal_tac= subgoal_tac,


64 
finish_tac=finish_tac,


65 
loop_tac=loop_tac};


66 


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


68 
SS{mss=mss,


69 
simps= simps,


70 
congs= congs,


71 
subgoal_tac= subgoal_tac,


72 
finish_tac=finish_tac,


73 
loop_tac=loop_tac};


74 


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


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


77 
simps= simps,


78 
congs= congs,


79 
subgoal_tac= subgoal_tac,


80 
finish_tac=finish_tac,


81 
loop_tac=loop_tac};


82 


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

88

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

0

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


86 
simps= rews' @ simps,


87 
congs= congs,


88 
subgoal_tac= subgoal_tac,


89 
finish_tac=finish_tac,


90 
loop_tac=loop_tac}


91 
end;


92 

88

93 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =


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


95 
SS{mss= Thm.del_simps(mss,rews'),


96 
simps= foldl (gen_rem eq_thm) (simps,rews'),


97 
congs= congs,


98 
subgoal_tac= subgoal_tac,


99 
finish_tac=finish_tac,


100 
loop_tac=loop_tac}


101 
end;


102 

1

103 
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =

0

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


105 
simps= simps,


106 
congs= newcongs @ congs,


107 
subgoal_tac= subgoal_tac,


108 
finish_tac=finish_tac,


109 
loop_tac=loop_tac};


110 


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


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


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


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


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


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


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


118 
in SS{mss= mss',


119 
simps= simps,


120 
congs= congs',


121 
subgoal_tac= subgoal_tac,


122 
finish_tac= finish_tac,


123 
loop_tac= loop_tac}


124 
end;


125 


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


127 


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


129 


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


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


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


133 
subgoal_tac=subgoal_tac,finish_tac=finish_tac,


134 
loop_tac=loop_tac}


135 
end;


136 

1

137 
fun NEWSUBGOALS tac tacf =


138 
STATE(fn state0 =>


139 
tac THEN STATE(fn state1 => tacf(nprems_of state1  nprems_of state0)));


140 

0

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


142 
let fun solve_all_tac mss =


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


144 
subgoal_tac=subgoal_tac,


145 
finish_tac=finish_tac, loop_tac=loop_tac}

1

146 
val solve1_tac =


147 
NEWSUBGOALS (subgoal_tac ss 1)


148 
(fn n => if n<0 then all_tac else no_tac)


149 
in DEPTH_SOLVE(solve1_tac) end

0

150 


151 
fun simp_loop i thm =


152 
tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN

1

153 
(finish_tac (prems_of_mss mss) i ORELSE looper i),

0

154 
thm)

1

155 
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))


156 
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))

0

157 
and simp_loop_tac i = Tactic(simp_loop i)


158 

146

159 
in fn i => COND (has_fewer_prems 1) no_tac (simp_loop_tac i) end;

0

160 


161 
fun asm_simp_tac ss =


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


163 


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


165 


166 
end;
