62 val lhs_of = #2 o dest_red; |
62 val lhs_of = #2 o dest_red; |
63 val rhs_of = #3 o dest_red; |
63 val rhs_of = #3 o dest_red; |
64 |
64 |
65 (*** Indexing and filtering of theorems ***) |
65 (*** Indexing and filtering of theorems ***) |
66 |
66 |
67 fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2); |
67 fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); |
68 |
68 |
69 (*insert a thm in a discrimination net by its lhs*) |
69 (*insert a thm in a discrimination net by its lhs*) |
70 fun lhs_insert_thm (th,net) = |
70 fun lhs_insert_thm (th,net) = |
71 Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net |
71 Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net |
72 handle Net.INSERT => net; |
72 handle Net.INSERT => net; |
246 |
246 |
247 (** Insertion of congruences and rewrites **) |
247 (** Insertion of congruences and rewrites **) |
248 |
248 |
249 (*insert a thm in a thm net*) |
249 (*insert a thm in a thm net*) |
250 fun insert_thm_warn th net = |
250 fun insert_thm_warn th net = |
251 Net.insert_term Drule.eq_thm_prop (concl_of th, th) net |
251 Net.insert_term Thm.eq_thm_prop (concl_of th, th) net |
252 handle Net.INSERT => |
252 handle Net.INSERT => |
253 (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; |
253 (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; |
254 net); |
254 net); |
255 |
255 |
256 val insert_thms = fold_rev insert_thm_warn; |
256 val insert_thms = fold_rev insert_thm_warn; |
272 |
272 |
273 (** Deletion of congruences and rewrites **) |
273 (** Deletion of congruences and rewrites **) |
274 |
274 |
275 (*delete a thm from a thm net*) |
275 (*delete a thm from a thm net*) |
276 fun delete_thm_warn th net = |
276 fun delete_thm_warn th net = |
277 Net.delete_term Drule.eq_thm_prop (concl_of th, th) net |
277 Net.delete_term Thm.eq_thm_prop (concl_of th, th) net |
278 handle Net.DELETE => |
278 handle Net.DELETE => |
279 (writeln"\nNo such rewrite or congruence rule:"; print_thm th; |
279 (writeln"\nNo such rewrite or congruence rule:"; print_thm th; |
280 net); |
280 net); |
281 |
281 |
282 val delete_thms = fold_rev delete_thm_warn; |
282 val delete_thms = fold_rev delete_thm_warn; |
283 |
283 |
284 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
284 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
285 let val congs' = fold (remove Drule.eq_thm_prop) thms congs |
285 let val congs' = fold (remove Thm.eq_thm_prop) thms congs |
286 in SS{auto_tac=auto_tac, congs= congs', |
286 in SS{auto_tac=auto_tac, congs= congs', |
287 cong_net= delete_thms (map mk_trans thms) cong_net, |
287 cong_net= delete_thms (map mk_trans thms) cong_net, |
288 mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
288 mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
289 end; |
289 end; |
290 |
290 |
291 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = |
291 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = |
292 let fun find((p as (th,ths))::ps',ps) = |
292 let fun find((p as (th,ths))::ps',ps) = |
293 if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) |
293 if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) |
294 | find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; |
294 | find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; |
295 print_thm thm; |
295 print_thm thm; |
296 ([],simps')) |
296 ([],simps')) |
297 val (thms,simps') = find(simps,[]) |
297 val (thms,simps') = find(simps,[]) |
298 in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
298 in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |