wneuper/isa: test/Tools/isac/Interpret/rewtools.sml@460c24a6a6ba

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

    41 length ancestors;

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

    43 length ancestors;

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

    45 val isabthms = (flat o (map PureThy.all_thms_of)) ancestors;

    46 length isabthms;

    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');

    52 length isacrlsthms;

    53 (*takes a few seconds...

    54 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;

    55 length 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 -----^^^^^^^^^^^^^^^^^^^^^";

    59 ...*)

    61 (!theory');

    62 map #2 (!theory');

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

    71 ...*)

    73 "----- for 'fun make_isab_thm_thy'";

    74 inter eq_thmI isacrlsthms (PureThy.all_thms_of (nth 1 ancestors));

    75 inter eq_thmI;

    76 (inter eq_thmI);

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

    84 length sec;

    85 ...*)

    87 (*takes 1 minute...

    88 print_depth 99;

    89 map ((inter eq_thmI) rlsthmsNOTisac o PureThy.all_thms_of) ancestors;

    90 print_depth 3;

    91 *)

    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;

    97 *)

   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 error "rewtools.sml: NOT thy_contains_thm \

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

   107 (rev (!theory'));

   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'))

   112 			    (rev (!theory'));

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

   114 else 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 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 error "rewtools.sml: NOT thy_containing_thm \

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

   125 "----- second test -------------------------------";

   126 show_thes();

   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'))

   131 				    (rev (!theory'));

   132 length (!theory');

   133 length startsearch;

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

   135 else 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'))

   145 			 (rev (!theory'));

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

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

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

   149 		    dropthys;

   150 print_depth 99; dropthy's; print_depth 3;

   152 (*WN100819========================================================

   153 "Isac" mem dropthy's;

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

   155 (op mem) o swap;

   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'))

   161 			     (rev (!ruleset'));

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

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

   164 else 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   | _ => 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 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'))

   182 			 (rev (!theory'));

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

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

   185 		    dropthys;

   187 (rev (!calclist'));

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

   197 states:=[];

   198 CalcTree

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

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

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

   202 Iterator 1;

   203 moveActiveRoot 1;

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

   218 states:=[];

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

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

   221   ("Test.thy",

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

   228 val p = ([], Res);

   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 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 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*)

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

   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 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 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 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 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 !!!!!!!!!!!!!!!!*)

   316 checkContext 1 p ;

   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*)

   325 show_pt pt;

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

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

   349 states:=[];

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

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

   352   ("Test.thy",

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

   379 separate "-" rest;

   380 space_implode "-" rest;

   381 commas rest;

   383 val delim = "-";

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

   397 states:=[];

   398 CalcTree

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

   400       ("Test.thy",

   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 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 error "rewtools.sml is_curr_endof_calc ([1],Frm) not";

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

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

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

   418 "----- checkContext -----";

   419 states:=[];

   420 CalcTree

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

   422       ("Test.thy",

   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) =

   454     ("Biegelinie.thy",

   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;

   461 term2str stac;

   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 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) ..._[.]_)-----";

   483 states:=[];

   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"],

   488 	    ("Biegelinie.thy",

   489 	     ["MomentBestimmte","Biegelinien"],

   490 	     ["IntegrierenUndKonstanteBestimmen"]))];

   491 moveActiveRoot 1;

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

   512    *)

   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 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 @{thm real_diff_minus});

   524 if contains_rule r1 Test_simplify then ()

   525 else error "rewtools.sml contains_rule Thm";

   527 val r1 = Calc ("Groups.plus_class.plus", eval_binop "#add_");

   528 if contains_rule r1 Test_simplify then ()

   529 else error "rewtools.sml contains_rule Calc";

   531 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");

   532 if not (contains_rule r1 Test_simplify) then ()

   533 else error "rewtools.sml contains_rule Calc";

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38014	3e11e3c2dc42
child 38050	4c52ad406c20
permissions	-rw-r--r--