1 (* test for sml/ME/rewtools.sml
2 authors: Walther Neuper 2000, 2006
3 (c) due to copyright terms
5 use"../smltest/ME/rewtools.sml";
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "----------- fun collect_isab_thys -------------------------------";
13 "----------- fun thy_containing_thm ------------------------------";
14 "----------- fun thy_containing_rls ------------------------------";
15 "----------- fun thy_containing_cal ------------------------------";
16 "----------- initContext Thy_ Integration-demo -------------------";
17 "----------- initContext..Thy_, fun context_thm ------------------";
18 "----------- initContext..Thy_, fun context_rls ------------------";
19 "----------- checkContext..Thy_, fun context_thy -----------------";
20 "----------- checkContext..Thy_, fun context_rls -----------------";
21 "----------- checkContext..Thy_ on last formula ------------------";
22 "----------- fun guh2theID ---------------------------------------";
23 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
24 "-----------------------------------------------------------------";
25 "----------- fun string_of_thmI for_[.]_) ------------------------";
26 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
27 "-----------------------------------------------------------------";
28 "----------- fun filter_appl_rews --------------------------------";
29 "----------- fun is_contained_in ---------------------------------";
30 "-----------------------------------------------------------------";
31 "-----------------------------------------------------------------";
35 "----------- fun collect_isab_thys -------------------------------";
36 "----------- fun collect_isab_thys -------------------------------";
37 "----------- fun collect_isab_thys -------------------------------";
38 val thy = first_isac_thy (*def. in Script/ListG.ML*);
39 val {ancestors,...} = rep_theory thy;
40 print_depth 99; map string_of_thy ancestors; print_depth 3;
42 val ancestors = (#ancestors o rep_theory) first_isac_thy;
44 print_depth 99; map theory2theory' ancestors; print_depth 3;
45 val isabthms = (flat o (map PureThy.all_thms_of)) ancestors;
48 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');
49 (*thms from rulesets*)
50 val isacrlsthms = ((map rep_thm_G') o flat o
51 (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
53 (*takes a few seconds...
54 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
56 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
57 print_depth 99; map #1 isacrlsthms; print_depth 3;
58 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
63 map (PureThy.all_thms_of o #2) (!theory');
64 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
65 (*takes a few seconds...
66 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
67 length rlsthmsNOTisac;
68 "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
69 print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
70 "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
73 "----- for 'fun make_isab_thm_thy'";
74 inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
77 (inter eq_thmI) isacrlsthms;
78 (*takes a few seconds...
79 curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
81 val thy = (nth 52 ancestors);
82 val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
83 length (PureThy.all_thms_of (nth 9 ancestors));
89 map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
93 (*takes some seconds...
94 val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
95 ((#ancestors o rep_theory) first_isac_thy);
96 print_depth 99; isab_thm_thy; print_depth 3;
100 "----------- fun thy_containing_thm ------------------------------";
101 "----------- fun thy_containing_thm ------------------------------";
102 "----------- fun thy_containing_thm ------------------------------";
103 val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));
104 if thy_contains_thm str ("XXX",thy) then ()
105 else raise error "rewtools.sml: NOT thy_contains_thm \
106 \(real_diff_minus,(Root.thy,.";
108 dropuntil (curry op= thy');
109 dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));
110 val startsearch = dropuntil ((curry op= thy') o
111 (#1:theory' * theory -> theory'))
113 if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()
114 else raise error "rewtools.sml: NOT thy_containin_thm \
115 \(real_diff_minus,(Root.thy,.";
117 "----- search the same theorem somewhere further below in the list";
118 if thy_contains_thm str ("XXX",Poly.thy) then ()
119 else raise error "rewtools.sml: NOT thy_contains_thm \
120 \(real_diff_minus,(Poly.thy,.";
121 if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()
122 else raise error "rewtools.sml: NOT thy_containing_thm \
123 \(real_diff_minus,(Poly.thy,.";
125 "----- second test -------------------------------";
127 (*args vor thy_containing_thm...*)
128 val (thy',str) = ("Test.thy", "radd_commute");
129 val startsearch = dropuntil ((curry op= thy') o
130 (#1:theory' * theory -> theory'))
134 if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()
135 else raise error "rewtools.sml: diff.behav. in \
136 \thy_containing_thm Test radd_commute";
139 "----------- fun thy_containing_rls ------------------------------";
140 "----------- fun thy_containing_rls ------------------------------";
141 "----------- fun thy_containing_rls ------------------------------";
142 val thy' = "Biegelinie.thy";
143 val dropthys = takewhile [] (not o (curry op= thy') o
144 (#1:theory' * theory -> theory'))
146 if length (!theory') <> length dropthys then ()
147 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 1";
148 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
150 print_depth 99; dropthy's; print_depth 3;
152 (*WN100819========================================================
153 "Isac" mem dropthy's;
154 op mem ("Isac", dropthy's);
156 ((op mem) o swap) (dropthy's, "Isac");
157 curry ((op mem) o swap);
158 curry ((op mem) o swap) dropthy's "Isac";
159 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
160 ((#1 o #2) : rls' * (theory' * rls) -> theory'))
162 print_depth 99; map (#1 o #2) startsearch; print_depth 3;
163 if length (!ruleset') <> length startsearch then ()
164 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 2";
166 val rls' = "norm_Poly";
167 case assoc (startsearch, rls') of
168 SOME (thy', _) => thyID2theory' thy'
169 | _ => raise error ("thy_containing_rls : rls '"^str^
170 "' not in !rulset' und thy '"^thy'^"'");
172 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()
173 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 3";
176 "----------- fun thy_containing_cal ------------------------------";
177 "----------- fun thy_containing_cal ------------------------------";
178 "----------- fun thy_containing_cal ------------------------------";
179 val thy' = "Atools.thy";
180 val dropthys = takewhile [] (not o (curry op= thy') o
181 (#1:theory' * theory -> theory'))
183 length dropthys <> length (!theory');
184 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
188 map #1 (rev (!calclist'));
189 map (#1 : calc -> string) (rev (!calclist'));
190 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
191 (#1 : calc -> string)) (rev (!calclist'));
192 ========================================================WN100819*)
194 "----------- initContext Thy_ Integration-demo -------------------";
195 "----------- initContext Thy_ Integration-demo -------------------";
196 "----------- initContext Thy_ Integration-demo -------------------";
199 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
200 ("Integrate.thy",["integrate","function"],
201 ["diff","integration"]))];
204 (*TODO.new_c: cvs before 071227, 11:50------------------
205 autoCalculate 1 CompleteCalc;
206 interSteps 1 ([1],Res);
207 interSteps 1 ([1,1],Res);
208 val ((pt,p),_) = get_calc 1; show_pt pt;
209 if existpt' ([1,1,1], Frm) pt then ()
210 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
212 initContext 1 Thy_ ([1,1,1], Frm);
213 --------------------TODO.new_c: cvs before 071227, 11:50*)
215 "----------- initContext..Thy_, fun context_thm ------------------";
216 "----------- initContext..Thy_, fun context_thm ------------------";
217 "----------- initContext..Thy_, fun context_thm ------------------";
219 CalcTree (*start of calculation, return No.1*)
220 [(["equality (x+1=2)", "solveFor x","solutions L"],
222 ["sqroot-test","univariate","equation","test"],
223 ["Test","squ-equ-test-subpbl1"]))];
224 Iterator 1; moveActiveRoot 1;
225 autoCalculate 1 CompleteCalc;
227 "----- no thy-context at result -----";
229 initContext 1 Thy_ p;
232 interSteps 1 ([2], Res);
233 interSteps 1 ([3,1], Res);
234 val ((pt,_),_) = get_calc 1; show_pt pt;
236 val p = ([2,4], Res);
237 val tac = Rewrite ("radd_left_commute","");
238 initContext 1 Thy_ p;
239 (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
240 --- in initContext..Thy_ ---*)
241 val ContThm {thm,result,...} = context_thy (pt,p) tac;
242 if thm = "thy_isac_Test-thm-radd_left_commute"
243 andalso term2str result = "-2 + (1 + x) = 0" then ()
244 else raise error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
246 val p = ([3,1,1], Frm);
247 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
248 initContext 1 Thy_ p;
249 (*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1
250 --- in initContext..Thy_ ---*)
251 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
252 if thm = "thy_isac_Test-thm-risolate_bdv_add"
253 andalso term2str result = "x = 0 + -1 * -1" then ()
254 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
256 initContext 1 Thy_ ([2,5], Res);
257 (*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
258 --- in initContext..Thy_ ---*)
261 "----------- initContext..Thy_, fun context_rls ------------------";
262 "----------- initContext..Thy_, fun context_rls ------------------";
263 "----------- initContext..Thy_, fun context_rls ------------------";
264 (*using pt from above*)
266 val tac = Rewrite_Set "Test_simplify";
267 initContext 1 Thy_ p;
268 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
269 --- in initContext..Thy_ ---*)
270 val ContRls {rls,result,...} = context_thy (pt,p) tac;
271 if rls = "thy_isac_Test-rls-Test_simplify"
272 andalso term2str result = "-1 + x = 0" then ()
273 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
275 val p = ([3,1], Frm);
276 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
277 initContext 1 Thy_ p;
278 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
279 --- in initContext..Thy_ ---*)
280 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
281 if rls = "thy_isac_Test-rls-isolate_bdv"
282 andalso term2str result = "x = 0 + -1 * -1" then ()
283 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
287 "----------- checkContext..Thy_, fun context_thy -----------------";
288 "----------- checkContext..Thy_, fun context_thy -----------------";
289 "----------- checkContext..Thy_, fun context_thy -----------------";
290 (*using pt from above*)
292 val p = ([2,4], Res);
293 val tac = Rewrite ("radd_left_commute","");
294 checkContext 1 p "thy_Test-thm-radd_left_commute";
295 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
296 --- in checkContext..Thy_ ---*)
297 val ContThm {thm,result,...} = context_thy (pt,p) tac;
298 if thm = "thy_isac_Test-thm-radd_left_commute"
299 andalso term2str result = "-2 + (1 + x) = 0" then ()
300 else raise error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
302 val p = ([3,1,1], Frm);
303 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
304 checkContext 1 p "thy_Test-thm-risolate_bdv_add";
305 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
306 --- in checkContext..Thy_ ---*)
307 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
308 if thm = "thy_isac_Test-thm-risolate_bdv_add"
309 andalso term2str result = "x = 0 + -1 * -1" then ()
310 else raise error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
312 val p = ([2,5], Res);
313 val tac = Calculate "plus";
314 (*checkContext..Thy_ 1 ([2,5], Res);*)
315 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
317 (* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
318 --- in checkContext..Thy_ ---*)
321 "----------- checkContext..Thy_, fun context_rls -----------------";
322 "----------- checkContext..Thy_, fun context_rls -----------------";
323 "----------- checkContext..Thy_, fun context_rls -----------------";
324 (*using pt from above*)
328 val tac = Rewrite_Set "Test_simplify";
329 checkContext 1 p "thy_isac_Test-rls-Test_simplify";
330 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
331 --- in checkContext..Thy_ ---*)
332 val ContRls {rls,result,...} = context_thy (pt,p) tac;
333 if rls = "thy_isac_Test-rls-Test_simplify"
334 andalso term2str result = "-1 + x = 0" then ()
335 else raise error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
337 val p = ([3,1], Frm);
338 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
339 checkContext 1 p "thy_Test-rls-isolate_bdv";
340 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
341 if rls = "thy_isac_Test-rls-isolate_bdv"
342 andalso term2str result = "x = 0 + -1 * -1" then ()
343 else raise error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
346 "----------- checkContext..Thy_ on last formula ------------------";
347 "----------- checkContext..Thy_ on last formula ------------------";
348 "----------- checkContext..Thy_ on last formula ------------------";
350 CalcTree (*start of calculation, return No.1*)
351 [(["equality (x+1=2)", "solveFor x","solutions L"],
353 ["sqroot-test","univariate","equation","test"],
354 ["Test","squ-equ-test-subpbl1"]))];
355 Iterator 1; moveActiveRoot 1;
357 autoCalculate 1 CompleteCalcHead;
358 autoCalculate 1 (Step 1);
359 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
360 initContext 1 Thy_ ([1], Frm);
361 checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
363 autoCalculate 1 (Step 1);
364 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
365 initContext 1 Thy_ ([1], Res);
366 checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
370 "----------- fun guh2theID ---------------------------------------";
371 "----------- fun guh2theID ---------------------------------------";
372 "----------- fun guh2theID ---------------------------------------";
373 val guh = "thy_scri_ListG-thm-zip_Nil";
375 take_fromto 1 4 (explode guh);
376 take_fromto 5 9 (explode guh);
377 val rest = takerest (9,(explode guh));
380 space_implode "-" rest;
384 val thyID = takewhile [] (not o (curry op= delim)) rest;
385 val rest' = dropuntil (curry op= delim) rest;
386 val setc = take_fromto 1 5 rest';
387 val xstr = takerest (5, rest');
389 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
390 else raise error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
393 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
394 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
395 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
396 "----- initContext -----";
399 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
401 ["linear","univariate","equation","test"],
402 ["Test","solve_linear"]))];
403 Iterator 1; moveActiveRoot 1;
404 autoCalculate 1 CompleteCalcHead;
406 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
407 if is_curr_endof_calc pt ([1],Frm) then ()
408 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm)";
410 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
411 if not (is_curr_endof_calc pt ([1],Frm)) then ()
412 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
413 if is_curr_endof_calc pt ([1],Res) then ()
414 else raise error "rewtools.sml is_curr_endof_calc ([1],Res)";
416 initContext 1 Thy_ ([1],Res);
418 "----- checkContext -----";
421 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
423 ["linear","univariate","equation","test"],
424 ["Test","solve_linear"]))];
425 Iterator 1; moveActiveRoot 1;
426 autoCalculate 1 CompleteCalc;
427 interSteps 1 ([1],Res);
428 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
430 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
432 interSteps 1 ([2],Res);
433 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
435 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
436 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
439 "----------- fun string_of_thmI for_[.]_) ------------------------";
440 "----------- fun string_of_thmI for_[.]_) ------------------------";
441 "----------- fun string_of_thmI for_[.]_) ------------------------";
442 "----- these work ?!?";
443 val th = sym_thm real_minus_eq_cancel;
444 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
445 val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
446 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
448 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
449 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
450 val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
451 applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
452 "- compose stac as done in | appy (*leaf*) by handle_leaf";
453 val (th, sr, E, a, v, t) =
455 (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
456 [(str2term "q__::bool", str2term "q x = q_0")],
457 SOME (str2term "q x = q_0"),
458 str2term "q__::bool",
459 str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
460 val (a', STac stac) = handle_leaf "next " th sr E a v t;
462 "--- but this \"m\" is already corrupted";
463 val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
464 "- because in assoc_thm'...";
465 val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
466 val "s"::"y"::"m"::"_"::id = explode thmid;
467 ((num_str o (get_thm thy)) (implode id)) RS sym;
468 ((get_thm thy) (implode id)) RS sym;
469 "... this creates [.]";
470 ((get_thm thy) (implode id));
471 "... while this has _NO_ [.]";
473 "----- thus we repair the [.] in string_of_thmI...";
474 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
475 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
476 else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
477 " = " ^ string_of_thmI thm);
480 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
481 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
482 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
484 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
485 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
486 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
487 "FunktionsVariable x"],
489 ["MomentBestimmte","Biegelinien"],
490 ["IntegrierenUndKonstanteBestimmen"]))];
492 autoCalculate 1 CompleteCalcHead;
493 autoCalculate 1 (Step 1) (*Apply_Method*);
494 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
495 "--- this was corrupted before 'fun string_of_thmI'";
496 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
497 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
498 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
499 else raise error "rewtools.sml: string_of_thmI ?!?";
501 getTactic 1 ([1],Frm);
503 "----------- fun filter_appl_rews --------------------------------";
504 "----------- fun filter_appl_rews --------------------------------";
505 "----------- fun filter_appl_rews --------------------------------";
506 val f = str2term "a + z + 2*a + 3*z + 5 + 6";
507 val thy = assoc_thy "Isac.thy";
508 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
509 val rls = Test_simplify;
510 (* val rls = rls_p_33; filter_appl_rews ---> length 2
511 val rls = norm_Poly; filter_appl_rews ---> length 1
513 if filter_appl_rews thy subst f rls =
514 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
515 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
516 Calculate "plus"] then ()
517 else raise error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
520 "----------- fun is_contained_in ---------------------------------";
521 "----------- fun is_contained_in ---------------------------------";
522 "----------- fun is_contained_in ---------------------------------";
523 val r1 = Thm ("real_diff_minus",num_str real_diff_minus);
524 if contains_rule r1 Test_simplify then ()
525 else raise error "rewtools.sml contains_rule Thm";
527 val r1 = Calc ("op +", eval_binop "#add_");
528 if contains_rule r1 Test_simplify then ()
529 else raise error "rewtools.sml contains_rule Calc";
531 val r1 = Calc ("op -", eval_binop "#add_");
532 if not (contains_rule r1 Test_simplify) then ()
533 else raise error "rewtools.sml contains_rule Calc";