wneuper/isa: test/Tools/isac/Interpret/rewtools.sml@73dc85c025ab

     1 (* Title: test for rewtools.sml

     2    authors: Walther Neuper 2000, 2006

     3 *)

     5 "--------------------------------------------------------";

     6 "--------------------------------------------------------";

     7 "table of contents --------------------------------------";

     8 "--------------------------------------------------------";

     9 (*============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! =================

    10 "----------- fun make_isab ------------------------------";

    11 "----------- fun collect_isab_thys ----------------------";

    12 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ===============*)

    13 "----------- fun thy_containing_rls ---------------------";

    14 "----------- fun thy_containing_cal ---------------------";

    15 (*============ inhibit exn WN120321 ==============================================

    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 ============ inhibit exn WN120321 ==============================================*)

    31 "-------- build fun get_bdv_subst --------------------------------";

    32 "--------------------------------------------------------";

    33 "--------------------------------------------------------";

    35 "----------- fun make_isab ------------------------------";

    36 "----------- fun make_isab ------------------------------";

    37 (*============ inhibit exn WN120321 ==============================================

    38 "----------- fun make_isab ------------------------------";

    39 (* rlsthmsNOTisac: contains thms in rls requested from Isabelle ---" *)

    40 map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)

    41 ["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",

    42  "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",

    43  "sym_real_mult_minus1", "distrib_right", "distrib_left",

    44  "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",

    45  "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",

    46  "add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",

    47  "order_refl", "minus_minus", "mult_commute", "mult_assoc",

    48  "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",

    49  "right_minus", "sym_add_assoc", "left_diff_distrib",

    50  "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",

    51  "times_divide_eq_left", "divide_divide_eq_left",

    52  "divide_divide_eq_right", "divide_1", "add_divide_distrib",

    53  "sym_rmult_assoc"];

    54 if length rlsthmsNOTisac > 34 then ()

    55 else error "rewtools.sml: some rlsthmsNOTisac dropped";

    57 "----- FIXME.WN11xxxx: rlsthmsNOTisac DOES contain thms from isac ---";

    58 map (thmID_of_derivation_name o #1) rlsthmsNOTisac;

    59 "----- FIXME.WN11xxxx: sym_* in rlsthmsNOTisac DOES contain thms from isac ---";

    60 val symthms = [("real_mult_minus1", @{thm real_mult_minus1}),

    61                ("realpow_twoI", @{thm realpow_twoI}),

    62                ("realpow_addI", @{thm realpow_addI}),

    63                ("real_mult_2", @{thm real_mult_2}),

    64                ("mult_assoc", @{thm mult_assoc}),

    65                ("add_assoc", @{thm add_assoc}),

    66                ("rmult_assoc", @{thm rmult_assoc})];

    67 map (Thm.derivation_name o #2) symthms;

    69 "----------- fun collect_isab_thys ----------------------";

    70 "----------- fun collect_isab_thys ----------------------";

    71 "----------- fun collect_isab_thys ----------------------";

    72 val ancestors = Theory.ancestors_of @{theory "Complex_Main"};

    73 val isabthms = (flat o (map Theory.axioms_of)) ancestors;

    75 val isacrules = (flat o (map (thms_of_rls o #2 o #2)))

    76   (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));

    77 (*thms from rulesets*)

    78 (*=== inhibit exn AK110725 =============================================================

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

    80 		 (map (PureThy.all_thms_of_rls o #2 o #2)))

    81 		   (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));

    82 length isacrlsthms;

    83 (*takes a few seconds...

    84 val isacrlsthms = gen_distinct eq_thmI isacrlsthms;

    85 length isacrlsthms;

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

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

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

    89 ...*)

    92 (!theory');

    93 map #2 (!theory');

    94 map (PureThy.all_thms_of o #2) (!theory');

    95 val isacthms = (flat o (map (PureThy.all_thms_of o #2))) (!theory');

    96 (*takes a few seconds...

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

    98 length rlsthmsNOTisac;

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

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

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

   102 ...*)

   104 "----- for 'fun make_isab_thm_thy'";

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

   106 inter eq_thmI;

   107 (inter eq_thmI);

   108 (inter eq_thmI) isacrlsthms;

   109 (*takes a few seconds...

   110 curry (inter eq_thmI) isacrlsthms (PureThy.all_thms_of (nth 9 ancestors));

   112 val thy = (nth 52 ancestors);

   113 val sec = ((inter eq_thmI) isacrlsthms o PureThy.all_thms_of) (nth 52 ancestors);

   114 length (PureThy.all_thms_of (nth 9 ancestors));

   115 length sec;

   116 ...*)

   117 (*takes 1 minute...

   118 print_depth 99;

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

   120 print_depth 3;

   121 *)

   123 (*takes some seconds...

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

   125 		       ((#ancestors o rep_theory) first_isac_thy);

   126 print_depth 99; isab_thm_thy; print_depth 3;

   127 *)

   128 === inhibit exn AK110725 =============================================================*)

   129 ============ inhibit exn WN120321 ==============================================*)

   133 "----------- fun thy_containing_rls ---------------------";

   134 "----------- fun thy_containing_rls ---------------------";

   135 "----------- fun thy_containing_rls ---------------------";

   136 infix mem; (*from Isabelle2002*)

   137 fun x mem [] = false

   138   | x mem (y :: ys) = x = y orelse x mem ys;

   140 val thy' = "Biegelinie";

   141     val dropthys =

   142       takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

   143         (rev (!theory'));

   145 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

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

   147 else error "thy_containing_rls changed 1";

   149 		    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;

   151 if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"](*, "Biegelinie",..,"Test",.*)

   152 then () else error "thy_containing_rls changed ancestors_rls";

   154 "Isac" mem dropthys';

   155 op mem ("Isac", dropthys');

   156 (op mem) o swap;

   157 ((op mem) o swap) (dropthys', "Isac");

   158 curry ((op mem) o swap);

   159 curry ((op mem) o swap) dropthys' "Isac";

   160 		val ancestors_rls =

   161 		  filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

   162 		     (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));

   164 take (10, map #1 ancestors_rls) =

   165   ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation",

   166    "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)

   168 (* WN120523 popped up again ?!?!?

   169 if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then ()

   170 else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";

   171 *)

   173 val rls' = "norm_Poly";

   174 case assoc (ancestors_rls, rls') of

   175     SOME (thy', _) => thyID2theory' thy'

   176   | _ => error ("thy_containing_rls : rls '" ^ rls' ^

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

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

   180 else error "thy_containing_rls 3: changed with (Biegelinie, norm_Poly)";

   182 "~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie" ,"norm_Poly");

   183     val rls' = strip_thy rls'

   184     val thy' = thyID2theory' thy'

   185     val dropthys =

   186       takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

   187         (rev (!theory'));

   189 map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*)

   191     val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;

   192 		    val ancestors_rls =

   193 		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

   194 		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));

   196 case assoc (ancestors_rls, rls') of

   197   SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()

   198 | _ => error "thy_containing_rls changed 2";

   199 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

   202 "----------- fun thy_containing_cal ---------------------";

   203 "----------- fun thy_containing_cal ---------------------";

   204 "----------- fun thy_containing_cal ---------------------";

   205 val thy' = "Atools";

   206     val dropthys =

   207       takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

   208         (rev (!theory'));

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

   212     val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;

   214 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

   215 if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",

   216   "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",

   217   "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",

   218   "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)

   219 then () else error "thy_containing_cal changed ancestors_rls for Atools";

   221 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev;

   222 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1;

   223 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string);

   225     val ancestors_cal =

   226       filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))

   227         (Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev);

   229 if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus")

   230                     (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*)

   231 then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed";

   232 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

   234 "----------- initContext Thy_ Integration-demo ----------";

   235 "----------- initContext Thy_ Integration-demo ----------";

   236 "----------- initContext Thy_ Integration-demo ----------";

   237 states:=[];

   238 CalcTree

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

   240   ("Integrate",["integrate","function"],

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

   242 Iterator 1;

   243 moveActiveRoot 1;

   244 autoCalculate 1 CompleteCalc;

   245 interSteps 1 ([1],Res);

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

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

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

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

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

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

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

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

   255 states:=[]; (*start of calculation, return No.1*)

   256 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   257   ("Test", ["sqroot-test","univariate","equation","test"],

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

   259 Iterator 1; moveActiveRoot 1;

   260 autoCalculate 1 CompleteCalc;

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

   263 val p = ([], Res);

   264 initContext 1 Thy_ p;

   266 interSteps 1 ([2], Res);

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

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

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

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

   272 (*============ inhibit exn WN120321 ==============================================

   273 initContext 1 Thy_ p;

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

   275   --- in initContext..Thy_ ---*)

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

   277 (*WN130621: thm = "thy_isac_WN120320: AT Isa2009-2-->11 BROKEN": guh !!!!!!!!!!!!!!!!!!!!!!!!!*)

   278 if thm = "thy_isac_Test-thm-radd_left_commute"

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

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

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

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

   285 initContext 1 Thy_ p;

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

   287   --- in initContext..Thy_ ---*)

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

   289 if thm =  "thy_isac_Test-thm-risolate_bdv_add"

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

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

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

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

   295   --- in initContext..Thy_ ---*)

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

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

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

   301 (*using pt from above*)

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

   303 val tac = Rewrite_Set "Test_simplify";

   304 initContext 1 Thy_ p;

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

   306   --- in initContext..Thy_ ---*)

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

   308 if rls = "thy_isac_Test-rls-Test_simplify"

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

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

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

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

   314 initContext 1 Thy_ p;

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

   316   --- in initContext..Thy_ ---*)

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

   318 if rls =  "thy_isac_Test-rls-isolate_bdv"

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

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

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

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

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

   325 (*using pt from above*)

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

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

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

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

   331   --- in checkContext..Thy_ ---*)

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

   333 if thm =  "thy_isac_Test-thm-radd_left_commute"

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

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

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

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

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

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

   341   --- in checkContext..Thy_ ---*)

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

   343 if thm =  "thy_isac_Test-thm-risolate_bdv_add"

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

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

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

   348 val tac = Calculate "plus";

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

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

   351 checkContext 1 p ;

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

   353   --- in checkContext..Thy_ ---*)

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

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

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

   358 (*using pt from above*)

   359 show_pt pt;

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

   362 val tac = Rewrite_Set "Test_simplify";

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

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

   365   --- in checkContext..Thy_ ---*)

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

   367 if rls = "thy_isac_Test-rls-Test_simplify"

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

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

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

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

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

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

   375 if rls = "thy_isac_Test-rls-isolate_bdv"

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

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

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

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

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

   382 states:=[]; (*start of calculation, return No.1*)

   383 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   384   ("Test", ["sqroot-test","univariate","equation","test"],

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

   386 Iterator 1; moveActiveRoot 1;

   388 autoCalculate 1 CompleteCalcHead;

   389 autoCalculate 1 (Step 1);

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

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

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

   394 autoCalculate 1 (Step 1);

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

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

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

   399 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)

   402 "----------- fun guh2theID ------------------------------";

   403 "----------- fun guh2theID ------------------------------";

   404 "----------- fun guh2theID ------------------------------";

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

   407 print_depth 3; (*999*)

   408 take_fromto 1 4 (Symbol.explode guh);

   409 take_fromto 5 9 (Symbol.explode guh);

   410 val rest = takerest (9,(Symbol.explode guh));

   412 separate "-" rest;

   413 space_implode "-" rest;

   414 commas rest;

   416 val delim = "-";

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

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

   419 val setc = take_fromto 1 5 rest';

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

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

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

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

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

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

   429 "----- initContext -----";

   430 states:=[];

   431 CalcTree

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

   433       ("Test",

   434        ["LINEAR","univariate","equation","test"],

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

   436 Iterator 1; moveActiveRoot 1;

   437 autoCalculate 1 CompleteCalcHead;

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

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

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

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

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

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

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

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

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

   452 "----- checkContext -----";

   453 states:=[];

   454 CalcTree

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

   456       ("Test",

   457        ["LINEAR","univariate","equation","test"],

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

   459 Iterator 1; moveActiveRoot 1;

   460 autoCalculate 1 CompleteCalc;

   461 interSteps 1 ([1],Res);

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

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

   466 interSteps 1 ([2],Res);

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

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

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

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

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

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

   476 "----- these work ?!?";

   477 (*========== inhibit exn 110718 ================================================

   478 (* ERROR: constructor real_minus_eq_cancel has not been declared *)

   479 val th = sym_thm real_minus_eq_cancel;

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

   481 val th'= mk_thm ( @{theory "Isac"} ) ((de_quote o string_of_thm) real_minus_eq_cancel);

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

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

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

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

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

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

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

   491     ("Biegelinie",

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

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

   494      SOME (str2term "q x = q_0"),

   495      str2term "q__::bool",

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

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

   498 term2str stac;

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

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

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

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

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

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

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

   506 "... this creates [.]";

   507 ((get_thm thy) (implode id));

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

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

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

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

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

   514 		  " = " ^ string_of_thmI thm);

   515 ========== inhibit exn 110718 ================================================*)

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

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

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

   520 states:=[];

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

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

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

   524 	     "FunktionsVariable x"],

   525 	    ("Biegelinie",

   526 	     ["MomentBestimmte","Biegelinien"],

   527 	     ["IntegrierenUndKonstanteBestimmen"]))];

   528 moveActiveRoot 1;

   529 autoCalculate 1 CompleteCalcHead;

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

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

   532 (*========== inhibit exn 110718 ================================================

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

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

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

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

   538 else error "rewtools.sml: string_of_thmI ?!?";

   540 getTactic 1 ([1],Frm);

   541 "----------- fun filter_appl_rews -----------------------";

   542 "----------- fun filter_appl_rews -----------------------";

   543 "----------- fun filter_appl_rews -----------------------";

   544 val f = str2term "a + z + 2*a + 3*z + 5 + 6";

   545 val thy = assoc_thy "Isac";

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

   547 val rls = Test_simplify;

   548 (* val rls = rls_p_33;      filter_appl_rews  ---> length 2

   549    val rls = norm_Poly;     filter_appl_rews  ---> length 1

   550    *)

   551 if filter_appl_rews thy subst f rls =

   552    [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

   553     Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),

   554     Calculate "plus"] then ()

   555 else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";

   556 ============ inhibit exn 110718 ==============================================*)

   559 "----------- fun is_contained_in ------------------------";

   560 "----------- fun is_contained_in ------------------------";

   561 "----------- fun is_contained_in ------------------------";

   562 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});

   563 if contains_rule r1 Test_simplify then ()

   564 else error "rewtools.sml contains_rule Thm";

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

   567 if contains_rule r1 Test_simplify then ()

   568 else error "rewtools.sml contains_rule Calc";

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

   571 if not (contains_rule r1 Test_simplify) then ()

   572 else error "rewtools.sml contains_rule Calc";

   575 "-------- build fun get_bdv_subst --------------------------------";

   576 "-------- build fun get_bdv_subst --------------------------------";

   577 "-------- build fun get_bdv_subst --------------------------------";

   578 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];

   579 val env = [(str2term "v_v", str2term "x")];

   580 subst2str env = "[\"\n(v_v, x)\"]";

   582 "~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);

   583     fun scan (Const _) = NONE

   584       | scan (Free _) = NONE

   585       | scan (Var _) = NONE

   586       | scan (Bound _) = NONE

   587       | scan (t as Const ("List.list.Cons", _) $

   588          (Const ("Product_Type.Pair", _) $ Free (str, _) $ _) $ _) =

   589            if is_bdv_subst t then SOME t else NONE

   590       | scan (Abs (_, _, body)) = scan body

   591       | scan (t1 $ t2) =

   592           case scan t1 of

   593             NONE => scan t2

   594           | SOME subst => SOME subst

   596 val SOME tm = scan prog;

   597 val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair: subst;

   598 if term2str tm = "[(bdv, v_v)]" then () else error "get_bdv_subst changed 1";

   600 if subst2subs subst = ["(bdv, x)"] then () else error "get_bdv_subst changed 2";

   602 case get_bdv_subst prog env of

   603   (SOME ["(bdv, x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()

   604 | _ => error "get_bdv_subst changed 3";

   606 val (SOME subs, _) = get_bdv_subst prog env;

   607 Rewrite_Inst (subs, ("diff_sin_chain","")) (*<<<----- this is the intended usage*)

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55279	130688f277ba
child 55397	71f7fd375e7d
permissions	-rw-r--r--