neuper@37906: (* test for sml/ME/rewtools.sml
neuper@37906:    authors: Walther Neuper 2000, 2006
neuper@37906:    (c) due to copyright terms
neuper@37906: 
neuper@37906: use"../smltest/ME/rewtools.sml";
neuper@37906: use"rewtools.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- fun collect_isab_thys -------------------------------";
neuper@37906: "----------- fun thy_containing_thm ------------------------------";
neuper@37906: "----------- fun thy_containing_rls ------------------------------";
neuper@37906: "----------- fun thy_containing_cal ------------------------------";
neuper@37906: "----------- initContext Thy_ Integration-demo -------------------";
neuper@37906: "----------- initContext..Thy_, fun context_thm ------------------";
neuper@37906: "----------- initContext..Thy_, fun context_rls ------------------";
neuper@37906: "----------- checkContext..Thy_, fun context_thy -----------------";
neuper@37906: "----------- checkContext..Thy_, fun context_rls -----------------";
neuper@37906: "----------- checkContext..Thy_ on last formula ------------------"; 
neuper@37906: "----------- fun guh2theID ---------------------------------------";
neuper@37906: "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- fun string_of_thmI for_[.]_) ------------------------";
neuper@37906: "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- fun filter_appl_rews --------------------------------";
neuper@37906: "----------- fun is_contained_in ---------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun collect_isab_thys -------------------------------";
neuper@37906: "----------- fun collect_isab_thys -------------------------------";
neuper@37906: "----------- fun collect_isab_thys -------------------------------";
neuper@37906: val thy = first_isac_thy (*def. in Script/ListG.ML*); 
neuper@37906: val {ancestors,...} = rep_theory thy;
neuper@37906: print_depth 99; map string_of_thy ancestors; print_depth 3;
neuper@37906: length ancestors;
neuper@37906: val ancestors = (#ancestors o rep_theory) first_isac_thy;
neuper@37906: length ancestors;
neuper@37906: print_depth 99; map theory2theory' ancestors; print_depth 3;
neuper@37936: val isabthms = (flat o (map PureThy.all_thms_of)) ancestors;
neuper@37906: length isabthms;
neuper@37906: 
neuper@37906: val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');
neuper@37906: (*thms from rulesets*)
neuper@37906: val isacrlsthms = ((map rep_thm_G') o flat o 
neuper@37936: 		(map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
neuper@37906: length isacrlsthms;
neuper@37906: (*takes a few seconds...
neuper@37906: val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
neuper@37906: length isacrlsthms;
neuper@37906: "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
neuper@37906: print_depth 99; map #1 isacrlsthms; print_depth 3;
neuper@37906: "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
neuper@37906: ...*)
neuper@37906: 
neuper@37906: (!theory');
neuper@37906: map #2 (!theory');
neuper@37936: map (PureThy.all_thms_of o #2) (!theory');
neuper@37936: val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');
neuper@37906: (*takes a few seconds...
neuper@37906: val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
neuper@37906: length rlsthmsNOTisac;
neuper@37906: "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
neuper@37906: print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
neuper@37906: "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
neuper@37906: ...*)
neuper@37906: 
neuper@37906: "----- for 'fun make_isab_thm_thy'";
neuper@37936: inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));
neuper@37936: inter eq_thmI;
neuper@37936: (inter eq_thmI);
neuper@37936: (inter eq_thmI) isacrlsthms;
neuper@37906: (*takes a few seconds...
neuper@37936: curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));
neuper@37906: 
neuper@37906: val thy = (nth 52 ancestors);
neuper@37936: val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);
neuper@37936: length (PureThy.all_thms_of (nth 9 ancestors));
neuper@37906: length sec;
neuper@37906: ...*)
neuper@37906: 
neuper@37906: (*takes 1 minute...
neuper@37906: print_depth 99; 
neuper@37936: map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;
neuper@37906: print_depth 3;
neuper@37906: *)
neuper@37906: 
neuper@37906: (*takes some seconds...
neuper@37906: val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
neuper@37906: 		       ((#ancestors o rep_theory) first_isac_thy);
neuper@37906: print_depth 99; isab_thm_thy; print_depth 3;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun thy_containing_thm ------------------------------";
neuper@37906: "----------- fun thy_containing_thm ------------------------------";
neuper@37906: "----------- fun thy_containing_thm ------------------------------";
neuper@37906: val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));
neuper@37906: if thy_contains_thm str ("XXX",thy) then ()
neuper@38031: else error "rewtools.sml: NOT thy_contains_thm \
neuper@37906: 		 \(real_diff_minus,(Root.thy,.";
neuper@37906: (rev (!theory'));
neuper@37906: dropuntil (curry op= thy');
neuper@37906: dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));
neuper@37906: val startsearch = dropuntil ((curry op= thy') o 
neuper@37906: 			     (#1:theory' * theory -> theory')) 
neuper@37906: 			    (rev (!theory'));
neuper@37906: if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()
neuper@38031: else error "rewtools.sml: NOT thy_containin_thm \
neuper@37906: 		 \(real_diff_minus,(Root.thy,.";
neuper@37906: 
neuper@37906: "----- search the same theorem somewhere further below in the list";
neuper@37906: if thy_contains_thm str ("XXX",Poly.thy) then ()
neuper@38031: else error "rewtools.sml: NOT thy_contains_thm \
neuper@37906: 		 \(real_diff_minus,(Poly.thy,.";
neuper@37906: if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()
neuper@38031: else error "rewtools.sml: NOT thy_containing_thm \
neuper@37906: 		 \(real_diff_minus,(Poly.thy,.";
neuper@37906: 
neuper@37906: "----- second test -------------------------------";
neuper@37906: show_thes();
neuper@37906: (*args vor thy_containing_thm...*)
neuper@37906: val (thy',str) = ("Test.thy", "radd_commute");
neuper@37906: val startsearch = dropuntil ((curry op= thy') o 
neuper@37906: 				     (#1:theory' * theory -> theory')) 
neuper@37906: 				    (rev (!theory'));
neuper@37906: length (!theory');
neuper@37906: length startsearch;
neuper@37906: if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()
neuper@38031: else error "rewtools.sml: diff.behav. in \
neuper@37906: 		 \thy_containing_thm Test radd_commute";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun thy_containing_rls ------------------------------";
neuper@37906: "----------- fun thy_containing_rls ------------------------------";
neuper@37906: "----------- fun thy_containing_rls ------------------------------";
neuper@37906: val thy' = "Biegelinie.thy";
neuper@37906: val dropthys = takewhile [] (not o (curry op= thy') o 
neuper@37906: 			     (#1:theory' * theory -> theory')) 
neuper@37906: 			 (rev (!theory'));
neuper@37906: if length (!theory') <> length dropthys then ()
neuper@38031: else error "rewtools.sml: diff.behav. in thy_containing_rls 1";
neuper@37906: val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
neuper@37906: 		    dropthys;
neuper@37906: print_depth 99; dropthy's; print_depth 3;
neuper@37906: 
neuper@37930: (*WN100819========================================================
neuper@37906: "Isac" mem dropthy's;
neuper@37906: op mem ("Isac", dropthy's);
neuper@37906: (op mem) o swap;
neuper@37906: ((op mem) o swap) (dropthy's, "Isac");
neuper@37906: curry ((op mem) o swap);
neuper@37906: curry ((op mem) o swap) dropthy's "Isac";
neuper@37906: val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o	 
neuper@37906: 			      ((#1 o #2) : rls' * (theory' * rls) -> theory'))
neuper@37906: 			     (rev (!ruleset'));
neuper@37906: print_depth 99; map (#1 o #2) startsearch; print_depth 3;
neuper@37906: if length (!ruleset') <> length startsearch then ()
neuper@38031: else error "rewtools.sml: diff.behav. in thy_containing_rls 2";
neuper@37906: 
neuper@37906: val rls' = "norm_Poly";
neuper@37906: case assoc (startsearch, rls') of
neuper@37926:     SOME (thy', _) => thyID2theory' thy'
neuper@38031:   | _ => error ("thy_containing_rls : rls '"^str^
neuper@37906: 			  "' not in !rulset' und thy '"^thy'^"'");
neuper@37906: 
neuper@37906: if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()
neuper@38031: else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun thy_containing_cal ------------------------------";
neuper@37906: "----------- fun thy_containing_cal ------------------------------";
neuper@37906: "----------- fun thy_containing_cal ------------------------------";
neuper@37906: val thy' = "Atools.thy";
neuper@37906: val dropthys = takewhile [] (not o (curry op= thy') o 
neuper@37906: 			     (#1:theory' * theory -> theory')) 
neuper@37906: 			 (rev (!theory'));
neuper@37906: length dropthys <> length (!theory');
neuper@37906: val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
neuper@37906: 		    dropthys;
neuper@37906: 
neuper@37906: (rev (!calclist'));
neuper@37906: map #1 (rev (!calclist'));
neuper@37906: map (#1 : calc -> string) (rev (!calclist'));
neuper@37906: val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
neuper@37906: 			      (#1 : calc -> string)) (rev (!calclist'));
neuper@37930: ========================================================WN100819*)
neuper@37906: 
neuper@37906: "----------- initContext Thy_ Integration-demo -------------------";
neuper@37906: "----------- initContext Thy_ Integration-demo -------------------";
neuper@37906: "----------- initContext Thy_ Integration-demo -------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"], 
neuper@37906:   ("Integrate.thy",["integrate","function"],
neuper@37906:   ["diff","integration"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: (*TODO.new_c: cvs before 071227, 11:50------------------
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: interSteps 1 ([1],Res);
neuper@37906: interSteps 1 ([1,1],Res);
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: if existpt' ([1,1,1], Frm) pt then ()
neuper@38031: else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
neuper@37906: 
neuper@37906: initContext  1 Thy_ ([1,1,1], Frm);
neuper@37906: --------------------TODO.new_c: cvs before 071227, 11:50*)
neuper@37906: 
neuper@37906: "----------- initContext..Thy_, fun context_thm ------------------";
neuper@37906: "----------- initContext..Thy_, fun context_thm ------------------";
neuper@37906: "----------- initContext..Thy_, fun context_thm ------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree      (*start of calculation, return No.1*)
neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:   ("Test.thy", 
neuper@37906:    ["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: 
neuper@37906: "----- no thy-context at result -----";
neuper@37906: val p = ([], Res);
neuper@37906: initContext 1 Thy_ p;
neuper@37906: 
neuper@37906: 
neuper@37906: interSteps 1 ([2], Res);
neuper@37906: interSteps 1 ([3,1], Res);
neuper@37906: val ((pt,_),_) = get_calc 1; show_pt pt;
neuper@37906: 
neuper@37906: val p = ([2,4], Res);
neuper@37906: val tac = Rewrite ("radd_left_commute","");
neuper@37906: initContext 1 Thy_ p;
neuper@37906: (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
neuper@37906:   --- in initContext..Thy_ ---*)
neuper@37906: val ContThm {thm,result,...} = context_thy (pt,p) tac;
neuper@37906: if thm = "thy_isac_Test-thm-radd_left_commute" 
neuper@37906:    andalso term2str result = "-2 + (1 + x) = 0" then ()
neuper@38031: else error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
neuper@37906: 
neuper@37906: val p = ([3,1,1], Frm);
neuper@37906: val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
neuper@37906: initContext 1 Thy_ p;
neuper@37906: (*Frm->Res, Rewrite_Inst "risolate_bdv_add"  -1 + x = 0 -> x = 0 + -1 * -1
neuper@37906:   --- in initContext..Thy_ ---*)
neuper@37906: val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
neuper@37906: if thm =  "thy_isac_Test-thm-risolate_bdv_add"
neuper@37906:    andalso term2str result = "x = 0 + -1 * -1" then ()
neuper@38031: else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
neuper@37906: 
neuper@37906: initContext 1 Thy_ ([2,5], Res);
neuper@37906: (*Res->Res, Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0
neuper@37906:   --- in initContext..Thy_ ---*)
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- initContext..Thy_, fun context_rls ------------------";
neuper@37906: "----------- initContext..Thy_, fun context_rls ------------------";
neuper@37906: "----------- initContext..Thy_, fun context_rls ------------------";
neuper@37906: (*using pt from above*)
neuper@37906: val p = ([1], Res);
neuper@37906: val tac = Rewrite_Set "Test_simplify";
neuper@37906: initContext 1 Thy_ p;
neuper@37906: (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
neuper@37906:   --- in initContext..Thy_ ---*)
neuper@37906: val ContRls {rls,result,...} = context_thy (pt,p) tac;
neuper@37906: if rls = "thy_isac_Test-rls-Test_simplify" 
neuper@37906:    andalso term2str result = "-1 + x = 0" then ()
neuper@38031: else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
neuper@37906: 
neuper@37906: val p = ([3,1], Frm);
neuper@37906: val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
neuper@37906: initContext 1 Thy_ p;
neuper@37906: (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 ->  x = 0 + -1 * -1
neuper@37906:   --- in initContext..Thy_ ---*)
neuper@37906: val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
neuper@37906: if rls =  "thy_isac_Test-rls-isolate_bdv"
neuper@37906:    andalso term2str result = "x = 0 + -1 * -1" then ()
neuper@38031: else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- checkContext..Thy_, fun context_thy -----------------";
neuper@37906: "----------- checkContext..Thy_, fun context_thy -----------------";
neuper@37906: "----------- checkContext..Thy_, fun context_thy -----------------";
neuper@37906: (*using pt from above*)
neuper@37906: 
neuper@37906: val p = ([2,4], Res);
neuper@37906: val tac = Rewrite ("radd_left_commute","");
neuper@37906: checkContext 1 p "thy_Test-thm-radd_left_commute";
neuper@37906: (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
neuper@37906:   --- in checkContext..Thy_ ---*)
neuper@37906: val ContThm {thm,result,...} = context_thy (pt,p) tac;
neuper@37906: if thm =  "thy_isac_Test-thm-radd_left_commute"
neuper@37906:    andalso term2str result = "-2 + (1 + x) = 0" then ()
neuper@38031: else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
neuper@37906: 
neuper@37906: val p = ([3,1,1], Frm);
neuper@37906: val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
neuper@37906: checkContext 1 p "thy_Test-thm-risolate_bdv_add";
neuper@37906: (* risolate_bdv_add:  -1 + x = 0 -> x = 0 + -1 * -1
neuper@37906:   --- in checkContext..Thy_ ---*)
neuper@37906: val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
neuper@37906: if thm =  "thy_isac_Test-thm-risolate_bdv_add"
neuper@37906:    andalso term2str result = "x = 0 + -1 * -1" then ()
neuper@38031: else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
neuper@37906: 
neuper@37906: val p = ([2,5], Res);
neuper@37906: val tac = Calculate "plus";
neuper@37906: (*checkContext..Thy_ 1 ([2,5], Res);*)
neuper@37906: (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
neuper@37906: checkContext 1 p ;
neuper@37906: (* Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0
neuper@37906:   --- in checkContext..Thy_ ---*)
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- checkContext..Thy_, fun context_rls -----------------";
neuper@37906: "----------- checkContext..Thy_, fun context_rls -----------------";
neuper@37906: "----------- checkContext..Thy_, fun context_rls -----------------";
neuper@37906: (*using pt from above*)
neuper@37906: show_pt pt;
neuper@37906: 
neuper@37906: val p = ([1], Res);
neuper@37906: val tac = Rewrite_Set "Test_simplify";
neuper@37906: checkContext 1 p "thy_isac_Test-rls-Test_simplify";
neuper@37906: (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
neuper@37906:   --- in checkContext..Thy_ ---*)
neuper@37906: val ContRls {rls,result,...} = context_thy (pt,p) tac;
neuper@37906: if rls = "thy_isac_Test-rls-Test_simplify" 
neuper@37906:    andalso term2str result = "-1 + x = 0" then ()
neuper@38031: else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
neuper@37906: 
neuper@37906: val p = ([3,1], Frm);
neuper@37906: val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
neuper@37906: checkContext 1 p "thy_Test-rls-isolate_bdv";
neuper@37906: val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
neuper@37906: if rls = "thy_isac_Test-rls-isolate_bdv" 
neuper@37906:    andalso term2str result = "x = 0 + -1 * -1" then ()
neuper@38031: else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- checkContext..Thy_ on last formula ------------------"; 
neuper@37906: "----------- checkContext..Thy_ on last formula ------------------"; 
neuper@37906: "----------- checkContext..Thy_ on last formula ------------------"; 
neuper@37906: states:=[];
neuper@37906: CalcTree      (*start of calculation, return No.1*)
neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:   ("Test.thy", 
neuper@37906:    ["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: 
neuper@37906: autoCalculate 1 CompleteCalcHead;
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: initContext 1 Thy_ ([1], Frm);
neuper@37906: checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
neuper@37906: 
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: initContext 1 Thy_ ([1], Res);
neuper@37906: checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun guh2theID ---------------------------------------";
neuper@37906: "----------- fun guh2theID ---------------------------------------";
neuper@37906: "----------- fun guh2theID ---------------------------------------";
neuper@37906: val guh = "thy_scri_ListG-thm-zip_Nil";
neuper@37906: 
neuper@37906: take_fromto 1 4 (explode guh);
neuper@37906: take_fromto 5 9 (explode guh);
neuper@37906: val rest = takerest (9,(explode guh)); 
neuper@37906: 
neuper@37906: separate "-" rest;
neuper@37906: space_implode "-" rest;
neuper@37906: commas rest;
neuper@37906: 
neuper@37906: val delim = "-";
neuper@37906: val thyID = takewhile [] (not o (curry op= delim)) rest;
neuper@37906: val rest' = dropuntil (curry op= delim) rest;
neuper@37906: val setc = take_fromto 1 5 rest';
neuper@37906: val xstr = takerest (5, rest');
neuper@37906: 
neuper@37906: if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
neuper@38031: else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
neuper@37906: "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
neuper@37906: "----------- debugging on Tests/solve_linear_as_rootpbl ----------";
neuper@37906: "----- initContext -----";
neuper@37906: states:=[];
neuper@37906: CalcTree 
neuper@37906:     [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
neuper@37906:       ("Test.thy",
neuper@37906:        ["linear","univariate","equation","test"],
neuper@37906:        ["Test","solve_linear"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalcHead;
neuper@37906: 
neuper@37906: autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: if is_curr_endof_calc pt ([1],Frm) then ()
neuper@38031: else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
neuper@37906: 
neuper@37906: autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: if not (is_curr_endof_calc pt ([1],Frm)) then ()
neuper@38031: else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
neuper@37906: if is_curr_endof_calc pt ([1],Res) then ()
neuper@38031: else error "rewtools.sml is_curr_endof_calc ([1],Res)";
neuper@37906: 
neuper@37906: initContext 1 Thy_ ([1],Res);
neuper@37906: 
neuper@37906: "----- checkContext -----";
neuper@37906: states:=[];
neuper@37906: CalcTree 
neuper@37906:     [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
neuper@37906:       ("Test.thy",
neuper@37906:        ["linear","univariate","equation","test"],
neuper@37906:        ["Test","solve_linear"]))];
neuper@37906: Iterator 1; moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: interSteps 1 ([1],Res);
neuper@37906: val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: 
neuper@37906: checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
neuper@37906: 
neuper@37906: interSteps 1 ([2],Res);
neuper@37906: val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
neuper@37906: 
neuper@37906: checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
neuper@37906: checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun string_of_thmI for_[.]_) ------------------------";
neuper@37906: "----------- fun string_of_thmI for_[.]_) ------------------------";
neuper@37906: "----------- fun string_of_thmI for_[.]_) ------------------------";
neuper@37906: "----- these work ?!?";
neuper@37906: val th = sym_thm real_minus_eq_cancel;
neuper@37906: val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
neuper@37906: val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
neuper@37906: val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
neuper@37906: 
neuper@37906: "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
neuper@37906: val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
neuper@37906: val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
neuper@37906:     applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
neuper@37906: "- compose stac as done in | appy (*leaf*) by handle_leaf";
neuper@37906: val (th, sr, E, a, v, t) = 
neuper@37906:     ("Biegelinie.thy", 
neuper@37906:      (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
neuper@37906:      [(str2term "q__::bool", str2term "q x = q_0")], 
neuper@37926:      SOME (str2term "q x = q_0"),
neuper@37906:      str2term "q__::bool", 
neuper@37906:      str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
neuper@37906: val (a', STac stac) = handle_leaf "next  " th sr E a v t;
neuper@37906: term2str stac;
neuper@37906: "--- but this \"m\" is already corrupted";
neuper@37906: val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
neuper@37906: "- because in assoc_thm'...";
neuper@37906: val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
neuper@37906: val "s"::"y"::"m"::"_"::id = explode thmid;
neuper@37969: ((num_str o (get_thm thy)) (implode id)) RS sym;
neuper@37906: ((get_thm thy) (implode id)) RS sym;
neuper@37906: "... this creates [.]";
neuper@37906: ((get_thm thy) (implode id));
neuper@37906: "... while this has _NO_ [.]";
neuper@37906: 
neuper@37906: "----- thus we repair the [.] in string_of_thmI...";
neuper@37969: val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
neuper@37906: if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
neuper@38031: else error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
neuper@37906: 		  " = " ^ string_of_thmI thm);
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
neuper@37906: "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
neuper@37906: "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
neuper@37906: states:=[];
neuper@37906: CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
neuper@37906: 	     "RandbedingungenBiegung [y 0 = 0, y L = 0]",
neuper@37906: 	     "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
neuper@37906: 	     "FunktionsVariable x"],
neuper@37906: 	    ("Biegelinie.thy",
neuper@37906: 	     ["MomentBestimmte","Biegelinien"],
neuper@37906: 	     ["IntegrierenUndKonstanteBestimmen"]))];
neuper@37906: moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalcHead;
neuper@37906: autoCalculate 1 (Step 1) (*Apply_Method*);
neuper@37906: autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
neuper@37906: "--- this was corrupted before 'fun string_of_thmI'";
neuper@37906: val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
neuper@37906: if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel", 
neuper@37906: 				 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
neuper@38031: else error "rewtools.sml: string_of_thmI ?!?";
neuper@37906: 
neuper@37906: getTactic 1 ([1],Frm);
neuper@37906: 
neuper@37906: "----------- fun filter_appl_rews --------------------------------";
neuper@37906: "----------- fun filter_appl_rews --------------------------------";
neuper@37906: "----------- fun filter_appl_rews --------------------------------";
neuper@37906: val f = str2term "a + z + 2*a + 3*z + 5 + 6";
neuper@37906: val thy = assoc_thy "Isac.thy";
neuper@37906: val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
neuper@37906: val rls = Test_simplify;
neuper@37906: (* val rls = rls_p_33;      filter_appl_rews  ---> length 2
neuper@37906:    val rls = norm_Poly;     filter_appl_rews  ---> length 1
neuper@37906:    *)
neuper@37906: if filter_appl_rews thy subst f rls =
neuper@37906:    [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
neuper@37906:     Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
neuper@37906:     Calculate "plus"] then () 
neuper@38031: else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- fun is_contained_in ---------------------------------";
neuper@37906: "----------- fun is_contained_in ---------------------------------";
neuper@37906: "----------- fun is_contained_in ---------------------------------";
neuper@37969: val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
neuper@37906: if contains_rule r1 Test_simplify then ()
neuper@38031: else error "rewtools.sml contains_rule Thm";
neuper@37906: 
neuper@38014: val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");
neuper@37906: if contains_rule r1 Test_simplify then ()
neuper@38031: else error "rewtools.sml contains_rule Calc";
neuper@37906: 
neuper@38014: val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
neuper@37906: if not (contains_rule r1 Test_simplify) then ()
neuper@38031: else error "rewtools.sml contains_rule Calc";