wneuper/isac: src/smltest/ME/rewtools.sml@102894651e0e

     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";

     6 use"rewtools.sml";

     7 *)

     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 "-----------------------------------------------------------------";

    30 "-----------------------------------------------------------------";

    34 "----------- fun collect_isab_thys -------------------------------";

    35 "----------- fun collect_isab_thys -------------------------------";

    36 "----------- fun collect_isab_thys -------------------------------";

    37 val thy = first_isac_thy (*def. in Script/ListG.ML*);

    38 val {ancestors,...} = rep_theory thy;

    39 print_depth 99; map string_of_thy ancestors; print_depth 3;

    40 length ancestors;

    41 val ancestors = (#ancestors o rep_theory) first_isac_thy;

    42 length ancestors;

    43 print_depth 99; map theory2theory' ancestors; print_depth 3;

    44 val isabthms = (flat o (map thms_of)) ancestors;

    45 length isabthms;

    47 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');

    48 (*thms from rulesets*)

    49 val isacrlsthms = ((map rep_thm_G') o flat o

    50 		(map (thms_of_rls o #2 o #2))) (!ruleset');

    51 length isacrlsthms;

    52 (*takes a few seconds...

    53 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;

    54 length isacrlsthms;

    55 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";

    56 print_depth 99; map #1 isacrlsthms; print_depth 3;

    57 "----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";

    58 ...*)

    60 (!theory');

    61 map #2 (!theory');

    62 map (thms_of o #2) (!theory');

    63 val isacthms = (flat o (map (thms_of o #2))) (!theory');

    64 (*takes a few seconds...

    65 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

    66 length rlsthmsNOTisac;

    67 "----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";

    68 print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;

    69 "----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";

    70 ...*)

    72 "----- for 'fun make_isab_thm_thy'";

    73 gen_inter eq_thmI (isacrlsthms, (thms_of (nth 1 ancestors)));

    74 gen_inter eq_thmI;

    75 curry (gen_inter eq_thmI);

    76 curry (gen_inter eq_thmI) isacrlsthms;

    77 (*takes a few seconds...

    78 curry (gen_inter eq_thmI) isacrlsthms (thms_of (nth 9 ancestors));

    80 val thy = (nth 52 ancestors);

    81 val sec = (curry (gen_inter eq_thmI) isacrlsthms o thms_of) (nth 52 ancestors);

    82 length (thms_of (nth 9 ancestors));

    83 length sec;

    84 ...*)

    86 (*takes 1 minute...

    87 print_depth 99;

    88 map (curry (gen_inter eq_thmI) rlsthmsNOTisac o thms_of) ancestors;

    89 print_depth 3;

    90 *)

    92 (*takes some seconds...

    93 val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))

    94 		       ((#ancestors o rep_theory) first_isac_thy);

    95 print_depth 99; isab_thm_thy; print_depth 3;

    96 *)

    99 "----------- fun thy_containing_thm ------------------------------";

   100 "----------- fun thy_containing_thm ------------------------------";

   101 "----------- fun thy_containing_thm ------------------------------";

   102 val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));

   103 if thy_contains_thm str ("XXX",thy) then ()

   104 else raise error "rewtools.sml: NOT thy_contains_thm \

   105 		 \(real_diff_minus,(Root.thy,.";

   106 (rev (!theory'));

   107 dropuntil (curry op= thy');

   108 dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));

   109 val startsearch = dropuntil ((curry op= thy') o

   110 			     (#1:theory' * theory -> theory'))

   111 			    (rev (!theory'));

   112 if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()

   113 else raise error "rewtools.sml: NOT thy_containin_thm \

   114 		 \(real_diff_minus,(Root.thy,.";

   116 "----- search the same theorem somewhere further below in the list";

   117 if thy_contains_thm str ("XXX",Poly.thy) then ()

   118 else raise error "rewtools.sml: NOT thy_contains_thm \

   119 		 \(real_diff_minus,(Poly.thy,.";

   120 if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()

   121 else raise error "rewtools.sml: NOT thy_containing_thm \

   122 		 \(real_diff_minus,(Poly.thy,.";

   124 "----- second test -------------------------------";

   125 show_thes();

   126 (*args vor thy_containing_thm...*)

   127 val (thy',str) = ("Test.thy", "radd_commute");

   128 val startsearch = dropuntil ((curry op= thy') o

   129 				     (#1:theory' * theory -> theory'))

   130 				    (rev (!theory'));

   131 length (!theory');

   132 length startsearch;

   133 if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()

   134 else raise error "rewtools.sml: diff.behav. in \

   135 		 \thy_containing_thm Test radd_commute";

   138 "----------- fun thy_containing_rls ------------------------------";

   139 "----------- fun thy_containing_rls ------------------------------";

   140 "----------- fun thy_containing_rls ------------------------------";

   141 val thy' = "Biegelinie.thy";

   142 val dropthys = takewhile [] (not o (curry op= thy') o

   143 			     (#1:theory' * theory -> theory'))

   144 			 (rev (!theory'));

   145 if length (!theory') <> length dropthys then ()

   146 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 1";

   147 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))

   148 		    dropthys;

   149 print_depth 99; dropthy's; print_depth 3;

   151 "Isac" mem dropthy's;

   152 op mem ("Isac", dropthy's);

   153 (op mem) o swap;

   154 ((op mem) o swap) (dropthy's, "Isac");

   155 curry ((op mem) o swap);

   156 curry ((op mem) o swap) dropthy's "Isac";

   157 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o

   158 			      ((#1 o #2) : rls' * (theory' * rls) -> theory'))

   159 			     (rev (!ruleset'));

   160 print_depth 99; map (#1 o #2) startsearch; print_depth 3;

   161 if length (!ruleset') <> length startsearch then ()

   162 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 2";

   164 val rls' = "norm_Poly";

   165 case assoc (startsearch, rls') of

   166     Some (thy', _) => thyID2theory' thy'

   167   | _ => raise error ("thy_containing_rls : rls '"^str^

   168 			  "' not in !rulset' und thy '"^thy'^"'");

   170 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()

   171 else raise error "rewtools.sml: diff.behav. in thy_containing_rls 3";

   174 "----------- fun thy_containing_cal ------------------------------";

   175 "----------- fun thy_containing_cal ------------------------------";

   176 "----------- fun thy_containing_cal ------------------------------";

   177 val thy' = "Atools.thy";

   178 val dropthys = takewhile [] (not o (curry op= thy') o

   179 			     (#1:theory' * theory -> theory'))

   180 			 (rev (!theory'));

   181 length dropthys <> length (!theory');

   182 val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))

   183 		    dropthys;

   185 (rev (!calclist'));

   186 map #1 (rev (!calclist'));

   187 map (#1 : calc -> string) (rev (!calclist'));

   188 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o

   189 			      (#1 : calc -> string)) (rev (!calclist'));

   191 "----------- initContext Thy_ Integration-demo -------------------";

   192 "----------- initContext Thy_ Integration-demo -------------------";

   193 "----------- initContext Thy_ Integration-demo -------------------";

   194 states:=[];

   195 CalcTree

   196 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],

   197   ("Integrate.thy",["integrate","function"],

   198   ["diff","integration"]))];

   199 Iterator 1;

   200 moveActiveRoot 1;

   201 (*TODO.new_c: cvs before 071227, 11:50------------------

   202 autoCalculate 1 CompleteCalc;

   203 interSteps 1 ([1],Res);

   204 interSteps 1 ([1,1],Res);

   205 val ((pt,p),_) = get_calc 1; show_pt pt;

   206 if existpt' ([1,1,1], Frm) pt then ()

   207 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";

   209 initContext  1 Thy_ ([1,1,1], Frm);

   210 --------------------TODO.new_c: cvs before 071227, 11:50*)

   212 "----------- initContext..Thy_, fun context_thm ------------------";

   213 "----------- initContext..Thy_, fun context_thm ------------------";

   214 "----------- initContext..Thy_, fun context_thm ------------------";

   215 states:=[];

   216 CalcTree      (*start of calculation, return No.1*)

   217 [(["equality (x+1=2)", "solveFor x","solutions L"],

   218   ("Test.thy",

   219    ["sqroot-test","univariate","equation","test"],

   220    ["Test","squ-equ-test-subpbl1"]))];

   221 Iterator 1; moveActiveRoot 1;

   222 autoCalculate 1 CompleteCalc;

   224 "----- no thy-context at result -----";

   225 val p = ([], Res);

   226 initContext 1 Thy_ p;

   229 interSteps 1 ([2], Res);

   230 interSteps 1 ([3,1], Res);

   231 val ((pt,_),_) = get_calc 1; show_pt pt;

   233 val p = ([2,4], Res);

   234 val tac = Rewrite ("radd_left_commute","");

   235 initContext 1 Thy_ p;

   236 (*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0

   237   --- in initContext..Thy_ ---*)

   238 val ContThm {thm,result,...} = context_thy (pt,p) tac;

   239 if thm = "thy_isac_Test-thm-radd_left_commute"

   240    andalso term2str result = "-2 + (1 + x) = 0" then ()

   241 else raise error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";

   243 val p = ([3,1,1], Frm);

   244 val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));

   245 initContext 1 Thy_ p;

   246 (*Frm->Res, Rewrite_Inst "risolate_bdv_add"  -1 + x = 0 -> x = 0 + -1 * -1

   247   --- in initContext..Thy_ ---*)

   248 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;

   249 if thm =  "thy_isac_Test-thm-risolate_bdv_add"

   250    andalso term2str result = "x = 0 + -1 * -1" then ()

   251 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

   253 initContext 1 Thy_ ([2,5], Res);

   254 (*Res->Res, Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0

   255   --- in initContext..Thy_ ---*)

   258 "----------- initContext..Thy_, fun context_rls ------------------";

   259 "----------- initContext..Thy_, fun context_rls ------------------";

   260 "----------- initContext..Thy_, fun context_rls ------------------";

   261 (*using pt from above*)

   262 val p = ([1], Res);

   263 val tac = Rewrite_Set "Test_simplify";

   264 initContext 1 Thy_ p;

   265 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

   266   --- in initContext..Thy_ ---*)

   267 val ContRls {rls,result,...} = context_thy (pt,p) tac;

   268 if rls = "thy_isac_Test-rls-Test_simplify"

   269    andalso term2str result = "-1 + x = 0" then ()

   270 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

   272 val p = ([3,1], Frm);

   273 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");

   274 initContext 1 Thy_ p;

   275 (*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 ->  x = 0 + -1 * -1

   276   --- in initContext..Thy_ ---*)

   277 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

   278 if rls =  "thy_isac_Test-rls-isolate_bdv"

   279    andalso term2str result = "x = 0 + -1 * -1" then ()

   280 else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";

   284 "----------- checkContext..Thy_, fun context_thy -----------------";

   285 "----------- checkContext..Thy_, fun context_thy -----------------";

   286 "----------- checkContext..Thy_, fun context_thy -----------------";

   287 (*using pt from above*)

   289 val p = ([2,4], Res);

   290 val tac = Rewrite ("radd_left_commute","");

   291 checkContext 1 p "thy_Test-thm-radd_left_commute";

   292 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0

   293   --- in checkContext..Thy_ ---*)

   294 val ContThm {thm,result,...} = context_thy (pt,p) tac;

   295 if thm =  "thy_isac_Test-thm-radd_left_commute"

   296    andalso term2str result = "-2 + (1 + x) = 0" then ()

   297 else raise error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";

   299 val p = ([3,1,1], Frm);

   300 val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));

   301 checkContext 1 p "thy_Test-thm-risolate_bdv_add";

   302 (* risolate_bdv_add:  -1 + x = 0 -> x = 0 + -1 * -1

   303   --- in checkContext..Thy_ ---*)

   304 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;

   305 if thm =  "thy_isac_Test-thm-risolate_bdv_add"

   306    andalso term2str result = "x = 0 + -1 * -1" then ()

   307 else raise error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";

   309 val p = ([2,5], Res);

   310 val tac = Calculate "plus";

   311 (*checkContext..Thy_ 1 ([2,5], Res);*)

   312 (*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)

   313 checkContext 1 p ;

   314 (* Calculate "plus"  -2 + (1 + x) = 0 -> -1 + x = 0

   315   --- in checkContext..Thy_ ---*)

   318 "----------- checkContext..Thy_, fun context_rls -----------------";

   319 "----------- checkContext..Thy_, fun context_rls -----------------";

   320 "----------- checkContext..Thy_, fun context_rls -----------------";

   321 (*using pt from above*)

   322 show_pt pt;

   324 val p = ([1], Res);

   325 val tac = Rewrite_Set "Test_simplify";

   326 checkContext 1 p "thy_isac_Test-rls-Test_simplify";

   327 (*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0

   328   --- in checkContext..Thy_ ---*)

   329 val ContRls {rls,result,...} = context_thy (pt,p) tac;

   330 if rls = "thy_isac_Test-rls-Test_simplify"

   331    andalso term2str result = "-1 + x = 0" then ()

   332 else raise error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";

   334 val p = ([3,1], Frm);

   335 val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");

   336 checkContext 1 p "thy_Test-rls-isolate_bdv";

   337 val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;

   338 if rls = "thy_isac_Test-rls-isolate_bdv"

   339    andalso term2str result = "x = 0 + -1 * -1" then ()

   340 else raise error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";

   343 "----------- checkContext..Thy_ on last formula ------------------";

   344 "----------- checkContext..Thy_ on last formula ------------------";

   345 "----------- checkContext..Thy_ on last formula ------------------";

   346 states:=[];

   347 CalcTree      (*start of calculation, return No.1*)

   348 [(["equality (x+1=2)", "solveFor x","solutions L"],

   349   ("Test.thy",

   350    ["sqroot-test","univariate","equation","test"],

   351    ["Test","squ-equ-test-subpbl1"]))];

   352 Iterator 1; moveActiveRoot 1;

   354 autoCalculate 1 CompleteCalcHead;

   355 autoCalculate 1 (Step 1);

   356 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   357 initContext 1 Thy_ ([1], Frm);

   358 checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";

   360 autoCalculate 1 (Step 1);

   361 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   362 initContext 1 Thy_ ([1], Res);

   363 checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";

   367 "----------- fun guh2theID ---------------------------------------";

   368 "----------- fun guh2theID ---------------------------------------";

   369 "----------- fun guh2theID ---------------------------------------";

   370 val guh = "thy_scri_ListG-thm-zip_Nil";

   372 take_fromto 1 4 (explode guh);

   373 take_fromto 5 9 (explode guh);

   374 val rest = takerest (9,(explode guh));

   376 separate "-" rest;

   377 space_implode "-" rest;

   378 commas rest;

   380 val delim = "-";

   381 val thyID = takewhile [] (not o (curry op= delim)) rest;

   382 val rest' = dropuntil (curry op= delim) rest;

   383 val setc = take_fromto 1 5 rest';

   384 val xstr = takerest (5, rest');

   386 if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()

   387 else raise error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";

   390 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";

   391 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";

   392 "----------- debugging on Tests/solve_linear_as_rootpbl ----------";

   393 "----- initContext -----";

   394 states:=[];

   395 CalcTree

   396     [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],

   397       ("Test.thy",

   398        ["linear","univariate","equation","test"],

   399        ["Test","solve_linear"]))];

   400 Iterator 1; moveActiveRoot 1;

   401 autoCalculate 1 CompleteCalcHead;

   403 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   404 if is_curr_endof_calc pt ([1],Frm) then ()

   405 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm)";

   407 autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   408 if not (is_curr_endof_calc pt ([1],Frm)) then ()

   409 else raise error "rewtools.sml is_curr_endof_calc ([1],Frm) not";

   410 if is_curr_endof_calc pt ([1],Res) then ()

   411 else raise error "rewtools.sml is_curr_endof_calc ([1],Res)";

   413 initContext 1 Thy_ ([1],Res);

   415 "----- checkContext -----";

   416 states:=[];

   417 CalcTree

   418     [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],

   419       ("Test.thy",

   420        ["linear","univariate","equation","test"],

   421        ["Test","solve_linear"]))];

   422 Iterator 1; moveActiveRoot 1;

   423 autoCalculate 1 CompleteCalc;

   424 interSteps 1 ([1],Res);

   425 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   427 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";

   429 interSteps 1 ([2],Res);

   430 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;

   432 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";

   433 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";

   436 "----------- fun string_of_thmI for_[.]_) ------------------------";

   437 "----------- fun string_of_thmI for_[.]_) ------------------------";

   438 "----------- fun string_of_thmI for_[.]_) ------------------------";

   439 "----- these work ?!?";

   440 val th = sym_thm real_minus_eq_cancel;

   441 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));

   442 val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);

   443 val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);

   445 "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";

   446 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;

   447 val Appl (Rewrite' (_,_,_,_,thm',_,_)) =

   448     applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));

   449 "- compose stac as done in | appy (*leaf*) by handle_leaf";

   450 val (th, sr, E, a, v, t) =

   451     ("Biegelinie.thy",

   452      (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],

   453      [(str2term "q__::bool", str2term "q x = q_0")],

   454      Some (str2term "q x = q_0"),

   455      str2term "q__::bool",

   456      str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");

   457 val (a', STac stac) = handle_leaf "next  " th sr E a v t;

   458 term2str stac;

   459 "--- but this \"m\" is already corrupted";

   460 val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;

   461 "- because in assoc_thm'...";

   462 val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));

   463 val "s"::"y"::"m"::"_"::id = explode thmid;

   464 ((num_str o (get_thm thy)) (implode id)) RS sym;

   465 ((get_thm thy) (implode id)) RS sym;

   466 "... this creates [.]";

   467 ((get_thm thy) (implode id));

   468 "... while this has _NO_ [.]";

   470 "----- thus we repair the [.] in string_of_thmI...";

   471 val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;

   472 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()

   473 else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^

   474 		  " = " ^ string_of_thmI thm);

   477 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";

   478 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";

   479 "----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";

   480 states:=[];

   481 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

   482 	     "RandbedingungenBiegung [y 0 = 0, y L = 0]",

   483 	     "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

   484 	     "FunktionsVariable x"],

   485 	    ("Biegelinie.thy",

   486 	     ["MomentBestimmte","Biegelinien"],

   487 	     ["IntegrierenUndKonstanteBestimmen"]))];

   488 moveActiveRoot 1;

   489 autoCalculate 1 CompleteCalcHead;

   490 autoCalculate 1 (Step 1) (*Apply_Method*);

   491 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);

   492 "--- this was corrupted before 'fun string_of_thmI'";

   493 val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;

   494 if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",

   495 				 "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()

   496 else raise error "rewtools.sml: string_of_thmI ?!?";

   498 getTactic 1 ([1],Frm);

   500 "----------- fun filter_appl_rews --------------------------------";

   501 "----------- fun filter_appl_rews --------------------------------";

   502 "----------- fun filter_appl_rews --------------------------------";

   503 val f = str2term "a + z + 2*3*x + 4*a + 5+6";

   504 val thy = assoc_thy "Isac.thy";

   505 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];

   506 val rls = Test_simplify;

   507 val Rls {rew_ord = ro, erls, rules,...} = rls;

   509 (*

   511 rewrite_ thy ro erls false thm f;

   513 rewrite_inst_ thy ro erls false subst thm f;

   515 print_depth 19;

   516  Test_simplify;

   517 print_depth 3;

   519 *)

author	wneuper
	Mon, 31 Dec 2007 14:18:53 +0100
branch	start-work-070517
changeset 268	102894651e0e
parent 262	5d65487829c7
child 269	3377abafed6c
permissions	-rw-r--r--