1 (* test for rewtools.sml
2 authors: Walther Neuper 2000, 2006
5 "--------------------------------------------------------";
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- fun make_isac ------------------------------";
10 "----------- fun collect_isab_thys ----------------------";
11 "----------- fun thy_containing_thm ---------------------";
12 "----------- fun thy_containing_rls ---------------------";
13 "----------- fun thy_containing_cal ---------------------";
14 "----------- initContext Thy_ Integration-demo ----------";
15 "----------- initContext..Thy_, fun context_thm ---------";
16 "----------- initContext..Thy_, fun context_rls ---------";
17 "----------- checkContext..Thy_, fun context_thy --------";
18 "----------- checkContext..Thy_, fun context_rls --------";
19 "----------- checkContext..Thy_ on last formula ---------";
20 "----------- fun guh2theID ------------------------------";
21 "----------- debugging on Tests/solve_linear_as_rootpbl -";
22 "--------------------------------------------------------";
23 "----------- fun string_of_thmI for_[.]_) ---------------";
24 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
25 "--------------------------------------------------------";
26 "----------- fun filter_appl_rews -----------------------";
27 "----------- fun is_contained_in ------------------------";
28 "--------------------------------------------------------";
29 "--------------------------------------------------------";
32 "----------- fun make_isac ------------------------------";
33 "----------- fun make_isac ------------------------------";
34 "----------- fun make_isac ------------------------------";
35 "----- rlsthmsNOTisac: in rls requested from Isabelle ---";
36 map #1 (rlsthmsNOTisac : (string * thm) list) = (*WN101011, Isabelle2009-2*)
37 ["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",
38 "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",
39 "sym_real_mult_minus1", "left_distrib", "right_distrib",
40 "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
41 "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
42 "add_0_left", "add_0_right", "divide_zero_left", "sym_real_mult_assoc",
43 "real_le_refl", "minus_minus", "real_mult_commute", "real_mult_assoc",
44 "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",
45 "right_minus", "sym_add_assoc", "left_diff_distrib",
46 "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",
47 "times_divide_eq_left", "divide_divide_eq_left",
48 "divide_divide_eq_right", "divide_1", "add_divide_distrib",
50 if length rlsthmsNOTisac > 40 then ()
51 else error "rewtools.sml: some rlsthmsNOTisac dropped";
53 "----- FIXME: rlsthmsNOTisac DOES contain thms from isac ---";
54 map (Thm.derivation_name o #2) rlsthmsNOTisac;
55 "----- FIXME: sym_* in rlsthmsNOTisac DOES contain thms from isac ---";
56 val symthms = [("real_mult_minus1", @{thm real_mult_minus1}),
57 ("realpow_twoI", @{thm realpow_twoI}),
58 ("realpow_addI", @{thm realpow_addI}),
59 ("real_mult_2", @{thm real_mult_2}),
60 ("real_mult_assoc", @{thm real_mult_assoc}),
61 ("add_assoc", @{thm add_assoc}),
62 ("rmult_assoc", @{thm rmult_assoc})];
63 map (Thm.derivation_name o #2) symthms;
66 (*=== inhibit exn ?=============================================================
67 "----------- fun collect_isab_thys ----------------------";
68 "----------- fun collect_isab_thys ----------------------";
69 "----------- fun collect_isab_thys ----------------------";
70 val ancestors = Theory.ancestors_of (theory "Complex_Main");
71 val isabthms = (flat o (map Theory.axioms_of)) ancestors;
73 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');
74 (*thms from rulesets*)
75 val isacrlsthms = ((map rep_thm_G') o flat o
76 (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
78 (*takes a few seconds...
79 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
81 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
82 print_depth 99; map #1 isacrlsthms; print_depth 3;
83 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
88 map (PureThy.all_thms_of o #2) (!theory');
89 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
90 (*takes a few seconds...
91 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
92 length rlsthmsNOTisac;
93 "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
94 print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
95 "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
98 "----- for 'fun make_isab_thm_thy'";
99 inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
102 (inter eq_thmI) isacrlsthms;
103 (*takes a few seconds...
104 curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
106 val thy = (nth 52 ancestors);
107 val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
108 length (PureThy.all_thms_of (nth 9 ancestors));
114 map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
118 (*takes some seconds...
119 val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
120 ((#ancestors o rep_theory) first_isac_thy);
121 print_depth 99; isab_thm_thy; print_depth 3;
125 "----------- fun thy_containing_thm ---------------------";
126 "----------- fun thy_containing_thm ---------------------";
127 "----------- fun thy_containing_thm ---------------------";
128 val (str, (thy', thy)) = ("real_diff_minus",("Root", Root.thy));
129 if thy_contains_thm str ("XXX",thy) then ()
130 else error "rewtools.sml: NOT thy_contains_thm \
131 \(real_diff_minus,(Root.thy,.";
133 dropuntil (curry op= thy');
134 dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));
135 val startsearch = dropuntil ((curry op= thy') o
136 (#1:theory' * theory -> theory'))
138 if thy_containing_thm thy' str = ("IsacKnowledge", "Root") then ()
139 else error "rewtools.sml: NOT thy_containin_thm \
140 \(real_diff_minus,(Root.thy,.";
142 "----- search the same theorem somewhere further below in the list";
143 if thy_contains_thm str ("XXX",Poly.thy) then ()
144 else error "rewtools.sml: NOT thy_contains_thm \
145 \(real_diff_minus,(Poly.thy,.";
146 if thy_containing_thm "LinEq" str = ("IsacKnowledge", "Poly") then ()
147 else error "rewtools.sml: NOT thy_containing_thm \
148 \(real_diff_minus,(Poly.thy,.";
150 "----- second test -------------------------------";
152 (*args vor thy_containing_thm...*)
153 val (thy',str) = ("Test", "radd_commute");
154 val startsearch = dropuntil ((curry op= thy') o
155 (#1:theory' * theory -> theory'))
159 if thy_containing_thm thy' str = ("IsacKnowledge", "Test") then ()
160 else error "rewtools.sml: diff.behav. in \
161 \thy_containing_thm Test radd_commute";
164 "----------- fun thy_containing_rls ---------------------";
165 "----------- fun thy_containing_rls ---------------------";
166 "----------- fun thy_containing_rls ---------------------";
167 val thy' = "Biegelinie";
168 val dropthys = takewhile [] (not o (curry op= thy') o
169 (#1:theory' * theory -> theory'))
171 if length (!theory') <> length dropthys then ()
172 else error "rewtools.sml: diff.behav. in thy_containing_rls 1";
173 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
175 print_depth 99; dropthy's; print_depth 3;
177 (*WN100819=======================================================
178 WN100819 THIS DATE MUST BE WRONG: at this date changeset 37934:56f10b13005e
179 finished update ME/calchead.sml + pushed updates over all sml+test
181 "Isac" mem dropthy's;
182 op mem ("Isac", dropthy's);
184 ((op mem) o swap) (dropthy's, "Isac");
185 curry ((op mem) o swap);
186 curry ((op mem) o swap) dropthy's "Isac";
187 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
188 ((#1 o #2) : rls' * (theory' * rls) -> theory'))
190 print_depth 99; map (#1 o #2) startsearch; print_depth 3;
191 if length (!ruleset') <> length startsearch then ()
192 else error "rewtools.sml: diff.behav. in thy_containing_rls 2";
194 val rls' = "norm_Poly";
195 case assoc (startsearch, rls') of
196 SOME (thy', _) => thyID2theory' thy'
197 | _ => error ("thy_containing_rls : rls '"^str^
198 "' not in !rulset' und thy '"^thy'^"'");
200 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()
201 else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
204 "----------- fun thy_containing_cal ---------------------";
205 "----------- fun thy_containing_cal ---------------------";
206 "----------- fun thy_containing_cal ---------------------";
208 val dropthys = takewhile [] (not o (curry op= thy') o
209 (#1:theory' * theory -> theory'))
211 length dropthys <> length (!theory');
212 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
216 map #1 (rev (!calclist'));
217 map (#1 : calc -> string) (rev (!calclist'));
218 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
219 (#1 : calc -> string)) (rev (!calclist'));
220 WN100819 =====================================================*)
222 "----------- initContext Thy_ Integration-demo ----------";
223 "----------- initContext Thy_ Integration-demo ----------";
224 "----------- initContext Thy_ Integration-demo ----------";
227 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
228 ("Integrate",["integrate","function"],
229 ["diff","integration"]))];
232 (*TODO.new_c: cvs before 071227, 11:50------------------
233 autoCalculate 1 CompleteCalc;
234 interSteps 1 ([1],Res);
235 interSteps 1 ([1,1],Res);
236 val ((pt,p),_) = get_calc 1; show_pt pt;
237 if existpt' ([1,1,1], Frm) pt then ()
238 else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
240 initContext 1 Thy_ ([1,1,1], Frm);
241 --------------------TODO.new_c: cvs before 071227, 11:50*)
243 "----------- initContext..Thy_, fun context_thm ---------";
244 "----------- initContext..Thy_, fun context_thm ---------";
245 "----------- initContext..Thy_, fun context_thm ---------";
246 states:=[]; (*start of calculation, return No.1*)
247 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
248 ("Test", ["sqroot-test","univariate","equation","test"],
249 ["Test","squ-equ-test-subpbl1"]))];
250 Iterator 1; moveActiveRoot 1;
251 autoCalculate 1 CompleteCalc;
253 "----- no thy-context at result -----";
255 initContext 1 Thy_ p;
258 interSteps 1 ([2], Res);
259 interSteps 1 ([3,1], Res);
260 val ((pt,_),_) = get_calc 1; show_pt pt;
262 val p = ([2,4], Res);
263 val tac = Rewrite ("radd_left_commute","");
264 initContext 1 Thy_ p;
265 (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
266 --- in initContext..Thy_ ---*)
267 val ContThm {thm,result,...} = context_thy (pt,p) tac;
268 if thm = "thy_isac_Test-thm-radd_left_commute"
269 andalso term2str result = "-2 + (1 + x) = 0" then ()
270 else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
272 val p = ([3,1,1], Frm);
273 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
274 initContext 1 Thy_ p;
275 (*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1
276 --- in initContext..Thy_ ---*)
277 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
278 if thm = "thy_isac_Test-thm-risolate_bdv_add"
279 andalso term2str result = "x = 0 + -1 * -1" then ()
280 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
282 initContext 1 Thy_ ([2,5], Res);
283 (*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
284 --- in initContext..Thy_ ---*)
287 "----------- initContext..Thy_, fun context_rls ---------";
288 "----------- initContext..Thy_, fun context_rls ---------";
289 "----------- initContext..Thy_, fun context_rls ---------";
290 (*using pt from above*)
292 val tac = Rewrite_Set "Test_simplify";
293 initContext 1 Thy_ p;
294 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
295 --- in initContext..Thy_ ---*)
296 val ContRls {rls,result,...} = context_thy (pt,p) tac;
297 if rls = "thy_isac_Test-rls-Test_simplify"
298 andalso term2str result = "-1 + x = 0" then ()
299 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
301 val p = ([3,1], Frm);
302 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
303 initContext 1 Thy_ p;
304 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
305 --- in initContext..Thy_ ---*)
306 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
307 if rls = "thy_isac_Test-rls-isolate_bdv"
308 andalso term2str result = "x = 0 + -1 * -1" then ()
309 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
312 "----------- checkContext..Thy_, fun context_thy --------";
313 "----------- checkContext..Thy_, fun context_thy --------";
314 "----------- checkContext..Thy_, fun context_thy --------";
315 (*using pt from above*)
317 val p = ([2,4], Res);
318 val tac = Rewrite ("radd_left_commute","");
319 checkContext 1 p "thy_Test-thm-radd_left_commute";
320 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
321 --- in checkContext..Thy_ ---*)
322 val ContThm {thm,result,...} = context_thy (pt,p) tac;
323 if thm = "thy_isac_Test-thm-radd_left_commute"
324 andalso term2str result = "-2 + (1 + x) = 0" then ()
325 else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
327 val p = ([3,1,1], Frm);
328 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
329 checkContext 1 p "thy_Test-thm-risolate_bdv_add";
330 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
331 --- in checkContext..Thy_ ---*)
332 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
333 if thm = "thy_isac_Test-thm-risolate_bdv_add"
334 andalso term2str result = "x = 0 + -1 * -1" then ()
335 else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
337 val p = ([2,5], Res);
338 val tac = Calculate "plus";
339 (*checkContext..Thy_ 1 ([2,5], Res);*)
340 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
342 (* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
343 --- in checkContext..Thy_ ---*)
346 "----------- checkContext..Thy_, fun context_rls --------";
347 "----------- checkContext..Thy_, fun context_rls --------";
348 "----------- checkContext..Thy_, fun context_rls --------";
349 (*using pt from above*)
353 val tac = Rewrite_Set "Test_simplify";
354 checkContext 1 p "thy_isac_Test-rls-Test_simplify";
355 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
356 --- in checkContext..Thy_ ---*)
357 val ContRls {rls,result,...} = context_thy (pt,p) tac;
358 if rls = "thy_isac_Test-rls-Test_simplify"
359 andalso term2str result = "-1 + x = 0" then ()
360 else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
362 val p = ([3,1], Frm);
363 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
364 checkContext 1 p "thy_Test-rls-isolate_bdv";
365 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
366 if rls = "thy_isac_Test-rls-isolate_bdv"
367 andalso term2str result = "x = 0 + -1 * -1" then ()
368 else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
371 "----------- checkContext..Thy_ on last formula ---------";
372 "----------- checkContext..Thy_ on last formula ---------";
373 "----------- checkContext..Thy_ on last formula ---------";
374 states:=[]; (*start of calculation, return No.1*)
375 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
376 ("Test", ["sqroot-test","univariate","equation","test"],
377 ["Test","squ-equ-test-subpbl1"]))];
378 Iterator 1; moveActiveRoot 1;
380 autoCalculate 1 CompleteCalcHead;
381 autoCalculate 1 (Step 1);
382 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
383 initContext 1 Thy_ ([1], Frm);
384 checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
386 autoCalculate 1 (Step 1);
387 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
388 initContext 1 Thy_ ([1], Res);
389 checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
392 "----------- fun guh2theID ------------------------------";
393 "----------- fun guh2theID ------------------------------";
394 "----------- fun guh2theID ------------------------------";
395 val guh = "thy_scri_ListG-thm-zip_Nil";
397 take_fromto 1 4 (explode guh);
398 take_fromto 5 9 (explode guh);
399 val rest = takerest (9,(explode guh));
402 space_implode "-" rest;
406 val thyID = takewhile [] (not o (curry op= delim)) rest;
407 val rest' = dropuntil (curry op= delim) rest;
408 val setc = take_fromto 1 5 rest';
409 val xstr = takerest (5, rest');
411 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
412 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
415 "----------- debugging on Tests/solve_linear_as_rootpbl -";
416 "----------- debugging on Tests/solve_linear_as_rootpbl -";
417 "----------- debugging on Tests/solve_linear_as_rootpbl -";
418 ----- initContext -----";
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 CompleteCalcHead;
428 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
429 if is_curr_endof_calc pt ([1],Frm) then ()
430 else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
432 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
433 if not (is_curr_endof_calc pt ([1],Frm)) then ()
434 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
435 if is_curr_endof_calc pt ([1],Res) then ()
436 else error "rewtools.sml is_curr_endof_calc ([1],Res)";
438 initContext 1 Thy_ ([1],Res);
440 "----- checkContext -----";
443 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
445 ["linear","univariate","equation","test"],
446 ["Test","solve_linear"]))];
447 Iterator 1; moveActiveRoot 1;
448 autoCalculate 1 CompleteCalc;
449 interSteps 1 ([1],Res);
450 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
452 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
454 interSteps 1 ([2],Res);
455 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
457 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
458 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
461 "----------- fun string_of_thmI for_[.]_) ---------------";
462 "----------- fun string_of_thmI for_[.]_) ---------------";
463 "----------- fun string_of_thmI for_[.]_) ---------------";
464 "----- these work ?!?";
465 val th = sym_thm real_minus_eq_cancel;
466 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
467 val th'= mk_thm (theory "Isac") ((de_quote o string_of_thm) real_minus_eq_cancel);
468 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
470 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
471 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
472 val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
473 applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
474 "- compose stac as done in | appy (*leaf*) by handle_leaf";
475 val (th, sr, E, a, v, t) =
477 (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
478 [(str2term "q__::bool", str2term "q x = q_0")],
479 SOME (str2term "q x = q_0"),
480 str2term "q__::bool",
481 str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
482 val (a', STac stac) = handle_leaf "next " th sr E a v t;
484 "--- but this \"m\" is already corrupted";
485 val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
486 "- because in assoc_thm'...";
487 val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
488 val "s"::"y"::"m"::"_"::id = explode thmid;
489 ((num_str o (get_thm thy)) (implode id)) RS sym;
490 ((get_thm thy) (implode id)) RS sym;
491 "... this creates [.]";
492 ((get_thm thy) (implode id));
493 "... while this has _NO_ [.]";
495 "----- thus we repair the [.] in string_of_thmI...";
496 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
497 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
498 else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
499 " = " ^ string_of_thmI thm);
502 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
503 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
504 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
506 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
507 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
508 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
509 "FunktionsVariable x"],
511 ["MomentBestimmte","Biegelinien"],
512 ["IntegrierenUndKonstanteBestimmen"]))];
514 autoCalculate 1 CompleteCalcHead;
515 autoCalculate 1 (Step 1) (*Apply_Method*);
516 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
517 "--- this was corrupted before 'fun string_of_thmI'";
518 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
519 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
520 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
521 else error "rewtools.sml: string_of_thmI ?!?";
523 getTactic 1 ([1],Frm);
525 "----------- fun filter_appl_rews -----------------------";
526 "----------- fun filter_appl_rews -----------------------";
527 "----------- fun filter_appl_rews -----------------------";
528 val f = str2term "a + z + 2*a + 3*z + 5 + 6";
529 val thy = assoc_thy "Isac";
530 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
531 val rls = Test_simplify;
532 (* val rls = rls_p_33; filter_appl_rews ---> length 2
533 val rls = norm_Poly; filter_appl_rews ---> length 1
535 if filter_appl_rews thy subst f rls =
536 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
537 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
538 Calculate "plus"] then ()
539 else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
542 "----------- fun is_contained_in ------------------------";
543 "----------- fun is_contained_in ------------------------";
544 "----------- fun is_contained_in ------------------------";
545 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
546 if contains_rule r1 Test_simplify then ()
547 else error "rewtools.sml contains_rule Thm";
549 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
550 if contains_rule r1 Test_simplify then ()
551 else error "rewtools.sml contains_rule Calc";
553 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
554 if not (contains_rule r1 Test_simplify) then ()
555 else error "rewtools.sml contains_rule Calc";
556 ===== inhibit exn ?===========================================================*)