22 val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) |
22 val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) |
23 val trans_thms : thm list |
23 val trans_thms : thm list |
24 end; |
24 end; |
25 |
25 |
26 |
26 |
27 infix 4 addrews addcongs delrews delcongs setauto; |
27 infix 4 addcongs delrews delcongs setauto; |
28 |
28 |
29 signature SIMP = |
29 signature SIMP = |
30 sig |
30 sig |
31 type simpset |
31 type simpset |
32 val empty_ss : simpset |
32 val empty_ss : simpset |
33 val addcongs : simpset * thm list -> simpset |
33 val addcongs : simpset * thm list -> simpset |
34 val addrews : simpset * thm list -> simpset |
34 val addrew : Proof.context -> thm -> simpset -> simpset |
35 val delcongs : simpset * thm list -> simpset |
35 val delcongs : simpset * thm list -> simpset |
36 val delrews : simpset * thm list -> simpset |
36 val delrews : simpset * thm list -> simpset |
37 val dest_ss : simpset -> thm list * thm list |
37 val dest_ss : simpset -> thm list * thm list |
38 val print_ss : simpset -> unit |
38 val print_ss : simpset -> unit |
39 val setauto : simpset * (int -> tactic) -> simpset |
39 val setauto : simpset * (int -> tactic) -> simpset |
218 val new_asms = filter (exists not o #2) |
218 val new_asms = filter (exists not o #2) |
219 (ccs ~~ (map (map atomic o Thm.prems_of) congs)); |
219 (ccs ~~ (map (map atomic o Thm.prems_of) congs)); |
220 in add_norms(congs,ccs,new_asms) end; |
220 in add_norms(congs,ccs,new_asms) end; |
221 |
221 |
222 fun normed_rews congs = |
222 fun normed_rews congs = |
223 let val add_norms = add_norm_tags congs in |
223 let |
224 fn thm => |
224 val add_norms = add_norm_tags congs |
|
225 fun normed ctxt thm = |
225 let |
226 let |
226 val ctxt = |
227 val ctxt' = Variable.declare_thm thm ctxt; |
227 Thm.theory_of_thm thm |
|
228 |> Proof_Context.init_global |
|
229 |> Variable.declare_thm thm; |
|
230 in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end |
228 in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end |
231 end; |
229 in normed end; |
232 |
230 |
233 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
231 fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
234 |
232 |
235 val trans_norms = map mk_trans normE_thms; |
233 val trans_norms = map mk_trans normE_thms; |
236 |
234 |
239 |
237 |
240 datatype simpset = |
238 datatype simpset = |
241 SS of {auto_tac: int -> tactic, |
239 SS of {auto_tac: int -> tactic, |
242 congs: thm list, |
240 congs: thm list, |
243 cong_net: thm Net.net, |
241 cong_net: thm Net.net, |
244 mk_simps: thm -> thm list, |
242 mk_simps: Proof.context -> thm -> thm list, |
245 simps: (thm * thm list) list, |
243 simps: (thm * thm list) list, |
246 simp_net: thm Net.net} |
244 simp_net: thm Net.net} |
247 |
245 |
248 val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, |
246 val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, |
249 mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; |
247 mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; |
257 (writeln ("Duplicate rewrite or congruence rule:\n" ^ |
255 (writeln ("Duplicate rewrite or congruence rule:\n" ^ |
258 Display.string_of_thm_without_context th); net); |
256 Display.string_of_thm_without_context th); net); |
259 |
257 |
260 val insert_thms = fold_rev insert_thm_warn; |
258 val insert_thms = fold_rev insert_thm_warn; |
261 |
259 |
262 fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = |
260 fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = |
263 let val thms = mk_simps thm |
261 let val thms = mk_simps ctxt thm |
264 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
262 in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
265 simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} |
263 simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} |
266 end; |
264 end; |
267 |
|
268 fun ss addrews thms = fold addrew thms ss; |
|
269 |
265 |
270 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
266 fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
271 let val congs' = thms @ congs; |
267 let val congs' = thms @ congs; |
272 in SS{auto_tac=auto_tac, congs= congs', |
268 in SS{auto_tac=auto_tac, congs= congs', |
273 cong_net= insert_thms (map mk_trans thms) cong_net, |
269 cong_net= insert_thms (map mk_trans thms) cong_net, |