231 rules=rules, rew_ord=rew_ord, preconds=preconds} |
231 rules=rules, rew_ord=rew_ord, preconds=preconds} |
232 | sym_rls (Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = |
232 | sym_rls (Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = |
233 Rrls {id="sym_"^id, scr=scr, calc=calc, errpatts=errpatts, erls=erls, prepat=prepat, |
233 Rrls {id="sym_"^id, scr=scr, calc=calc, errpatts=errpatts, erls=erls, prepat=prepat, |
234 rew_ord=rew_ord}; |
234 rew_ord=rew_ord}; |
235 |
235 |
236 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm) |
236 (* toggles sym_* and keeps "#:" for ad-hoc calculations *) |
237 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls) |
237 fun sym_rule (Thm (thmID, thm)) = |
238 | sym_Thm r = error ("sym_Thm: not for "^(rule2str r)); |
238 let |
|
239 val thm' = sym_thm thm |
|
240 val thmID' = case Symbol.explode thmID of |
|
241 "s"::"y"::"m"::"_"::id => implode id |
|
242 | "#"::":":: _ => "#: " ^ string_of_thmI thm' |
|
243 | _ => "sym_" ^ thmID |
|
244 in Thm (thmID', thm') end |
|
245 | sym_rule (Rls_ rls) = Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *) |
|
246 | sym_rule r = error ("sym_rule: not for " ^ (rule2str r)); |
239 (* |
247 (* |
240 val th = Thm ("real_one_collect",num_str @{thm real_one_collect}); |
248 val th = Thm ("real_one_collect",num_str @{thm real_one_collect}); |
241 sym_Thm th; |
249 sym_rule th; |
242 val th = |
250 val th = |
243 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n") |
251 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n") |
244 : rule |
252 : rule |
245 ML> val it = |
253 ML> val it = |
246 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*) |
254 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*) |
247 |
255 |
248 |
256 |
249 (*version for reverse rewrite used before 040214*) |
257 (*version for reverse rewrite used before 040214*) |
250 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a)); |
258 fun rev_deriv (t, r, (t', a)) = (sym_rule r, (t, a)); |
251 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t'); |
259 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t'); |
252 *) |
260 *) |
253 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t = |
261 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t = |
254 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t); |
262 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t); |
255 (* |
263 (* |