270 val subst = subs'2subst thy subs'; |
270 val subst = subs'2subst thy subs'; |
271 val subrls = instantiate_rls subs' rls |
271 val subrls = instantiate_rls subs' rls |
272 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct |
272 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct |
273 (*end*); |
273 (*end*); |
274 |
274 |
275 (* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t); |
275 (* given a list of equalities (lhs = rhs) and a term, |
276 *) |
276 replace all occurrences of lhs in the term with rhs; |
277 (*.rewrite using a list of terms.*) |
277 thus the order or equalities matters: put variables in lhs first. *) |
278 fun rewrite_terms_ thy ord erls subte t = |
278 fun rewrite_terms_ thy ord erls equs t = |
279 let (*val _=tracing("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^ |
279 let (*val _=tracing("### rewrite_terms_ equs= '"^terms2str equs^"' ..."^ |
280 term_detail2str (hd subte)^ |
280 term_detail2str (hd equs)^ |
281 "### rewrite_terms_ t= '"^term2str t^"' ..."^ |
281 "### rewrite_terms_ t= '"^term2str t^"' ..."^ |
282 term_detail2str t);*) |
282 term_detail2str t);*) |
283 fun rew_ (t', asm') [] _ = (t', asm') |
283 fun rew_ (t', asm') [] _ = (t', asm') |
284 (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t); |
284 (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], equs, t); |
285 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t''); |
285 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t''); |
286 rew_ (t', asm') (r::rs) t; |
286 rew_ (t', asm') (r::rs) t; |
287 *) |
287 *) |
288 | rew_ (t', asm') (rules as r::rs) t = |
288 | rew_ (t', asm') (rules as r::rs) t = |
289 let val _ = tracing("rew_ "^term2str t); |
289 let val _ = tracing("rew_ "^term2str t); |
290 val (t'', asm'', lrd, rew) = |
290 val (t'', asm'', lrd, rew) = |
291 rew_sub thy 1 [] ord erls false [] r t |
291 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t |
292 in if rew |
292 in if rew |
293 then (tracing("true rew_ "^term2str t''); |
293 then (tracing ("true rew_ " ^ term2str t''); |
294 rew_ (t'', asm' @ asm'') rules t'') |
294 rew_ (t'', asm' @ asm'') rules t'') |
295 else (tracing("false rew_ "^term2str t''); |
295 else (tracing ("false rew_ " ^ term2str t''); |
296 rew_ (t', asm') rs t') |
296 rew_ (t', asm') rs t') |
297 end |
297 end |
298 val (t'', asm'') = rew_ (e_term, []) subte t |
298 val (t'', asm'') = rew_ (e_term, []) equs t |
299 in if t'' = e_term |
299 in if t'' = e_term |
300 then NONE else SOME (t'', asm'') |
300 then NONE else SOME (t'', asm'') |
301 end; |
301 end; |
302 |
302 |
303 |
303 |