wneuper/isa: test/Tools/isac/Knowledge/integrate.sml@3594fcedebe9

     1 (* tests on integration over the reals

     2    author: Walther Neuper 2005

     3    (c) due to copyright terms

     4 *)

     5 trace_rewrite := false;

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

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

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

     9 "----------- parsing ------------------------------------";

    10 "----------- integrate by rewriting ---------------------";

    11 "----------- test add_new_c, is_f_x ---------------------";

    12 "----------- simplify by ruleset reducing make_ratpoly_in";

    13 "----------- integrate by ruleset -----------------------";

    14 "----------- rewrite 3rd integration in 7.27 ------------";

    15 "----------- check probem type --------------------------";

    16 "----------- check Scripts ------------------------------";

    17 "----------- me method [diff,integration] ---------------";

    18 "----------- autoCalculate [diff,integration] -----------";

    19 "----------- me method [diff,integration,named] ---------";

    20 "----------- me met [diff,integration,named] Biegelinie.Q";

    21 "----------- interSteps [diff,integration] --------------";

    22 "----------- method analog to rls 'integration' ---------";

    23 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

    24 "----------- CAS input ----------------------------------";

    25 "--------------------------------------------------------";

    26 "--------------------------------------------------------";

    27 "--------------------------------------------------------";

    29 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;

    30 they are used several times below; TODO remove duplicates*)

    31 val thy = @{theory "Integrate"};

    32 val ctxt = thy2ctxt thy;

    34 fun str2t str = parseNEW ctxt str |> the;

    35 fun term2s t = term_to_string' ctxt t;

    37 val conditions_in_integration_rules =

    38   Rls {id="conditions_in_integration_rules",

    39     preconds = [],

    40     rew_ord = ("termlessI",termlessI),

    41     erls = Erls,

    42     srls = Erls, calc = [], errpatts = [],

    43     rules = [(*for rewriting conditions in Thm's*)

    44 	    Calc ("Atools.occurs'_in",

    45 		  eval_occurs_in "#occurs_in_"),

    46 	    Thm ("not_true",num_str @{thm not_true}),

    47 	    Thm ("not_false",num_str @{thm not_false})],

    48     scr = EmptyScr};

    49 val subs = [(str2t "bdv::real", str2t "x::real")];

    50 fun rewrit thm str =

    51     fst (the (rewrite_inst_ thy tless_true

    52 			   conditions_in_integration_rules

    53 			   true subs thm str));

    56 "----------- parsing ------------------------------------";

    57 "----------- parsing ------------------------------------";

    58 "----------- parsing ------------------------------------";

    59 val t = str2t "Integral x D x";

    60 val t = str2t "Integral x^^^2 D x";

    61 case t of

    62     Const ("Integrate.Integral", _) $

    63      (Const ("Atools.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()

    64   | _ => error "integrate.sml: parsing: Integral x^^^2 D x";

    66 val t = str2t "ff x is_f_x";

    67 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()

    68 	| _ => error "integrate.sml: parsing: ff x is_f_x";

    71 "----------- integrate by rewriting ---------------------";

    72 "----------- integrate by rewriting ---------------------";

    73 "----------- integrate by rewriting ---------------------";

    74 val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");

    75 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";

    77 val str = rewrit @{thm "integral_const"} (str2t  "Integral M'/EJ D x");

    78 if term2s str = "M' / EJ * x" then ()

    79 else error "Integral M'/EJ D x   BY integral_const";

    81 val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");

    82 if term2s str = "x ^^^ 2 / 2" then ()

    83 else error "Integral x D x   BY integral_var";

    85 val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");

    86 if term2s str = "Integral x D x + Integral 1 D x" then ()

    87 else error "Integral x + 1 D x   BY integral_add";

    89 val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");

    90 if term2s str = "M' / EJ * Integral x ^^^ 3 D x" then ()

    91 else error "Integral M'/EJ * x^^^3 D x   BY integral_mult";

    93 val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");

    94 if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()

    95 else error "integrate.sml Integral x^^^3 D x";

    98 "----------- test add_new_c, is_f_x ---------------------";

    99 "----------- test add_new_c, is_f_x ---------------------";

   100 "----------- test add_new_c, is_f_x ---------------------";

   101 val term = str2t "x^^^2 * c + c_2";

   102 val cc = new_c term;

   103 if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";

   105 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;

   106 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()

   107 else error "intergrate.sml: diff. eval_add_new_c";

   109 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");

   110 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;

   112 val SOME (t',_) = rewrite_set_ thy true add_new_c term;

   113 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()

   114 else error "intergrate.sml: diff. rewrite_set add_new_c 1";

   116 val term = str2t "ff x = x^^^2*c + c_2";

   117 val SOME (t',_) = rewrite_set_ thy true add_new_c term;

   118 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()

   119 else error "intergrate.sml: diff. rewrite_set add_new_c 2";

   122 (*WN080222 replace call_new_c with add_new_c----------------------

   123 val term = str2t "new_c (c * x^^^2 + c_2)";

   124 val SOME (_,t') = eval_new_c 0 0 term 0;

   125 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()

   126 else error "integrate.sml: eval_new_c ???";

   128 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";

   129 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

   130 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()

   131 else error "integrate.sml: matches new_c = False";

   133 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";

   134 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

   135 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"

   136 then () else error "integrate.sml: matches new_c = True";

   138 val t = str2t "ff x is_f_x";

   139 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';

   140 if term2s t' = "(ff x is_f_x) = True" then ()

   141 else error "integrate.sml: eval_is_f_x --> true";

   143 val t = str2t "q_0/2 * L * x is_f_x";

   144 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';

   145 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()

   146 else error "integrate.sml: eval_is_f_x --> false";

   148 val conditions_in_integration =

   149 Rls {id="conditions_in_integration",

   150      preconds = [],

   151      rew_ord = ("termlessI",termlessI),

   152      erls = Erls,

   153      srls = Erls, calc = [], errpatts = [],

   154      rules = [Calc ("Tools.matches",eval_matches ""),

   155       	Calc ("Integrate.is'_f'_x",

   156       	      eval_is_f_x "is_f_x_"),

   157       	Thm ("not_true",num_str @{thm not_true}),

   158       	Thm ("not_false",num_str @{thm not_false})

   159       	],

   160      scr = EmptyScr};

   161 fun rewrit thm t =

   162     fst (the (rewrite_inst_ thy tless_true

   163 			    conditions_in_integration true subs thm t));

   164 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;

   165 val t = (rewrit call_for_new_c t)

   166     handle OPTION =>  str2t "no_rewrite";

   168 val t = rewrit call_for_new_c

   169 	       (str2t "ff x = q_0/2 *L*x"); term2s t;

   170 val t = (rewrit call_for_new_c

   171 	       (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))

   172     handle OPTION => (*NOT:  + new_c ..=..!!*)str2t "no_rewrite";

   173 --------------------------------------------------------------------*)

   176 "----------- simplify by ruleset reducing make_ratpoly_in";

   177 "----------- simplify by ruleset reducing make_ratpoly_in";

   178 "----------- simplify by ruleset reducing make_ratpoly_in";

   179 val thy = @{theory "Isac"};

   180 "===== test 1";

   181 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

   183 "----- stepwise from the rulesets in simplify_Integral and below-----";

   184 val rls = norm_Rational_noadd_fractions;

   185 case rewrite_set_inst_ thy true subs rls t of

   186     SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"

   187   | NONE => ();

   189 "===== test 2";

   190 val rls = order_add_mult_in;

   191 val SOME (t,[]) = rewrite_set_ thy true rls t;

   192 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()

   193 else error "integrate.sml simplify by ruleset order_add_mult_in #2";

   195 "===== test 3";

   196 val rls = discard_parentheses;

   197 val SOME (t,[]) = rewrite_set_ thy true rls t;

   198 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()

   199 else error "integrate.sml simplify by ruleset discard_parenth.. #3";

   201 "===== test 4";

   202 val rls =

   203   (append_rls "separate_bdv" collect_bdv

   204  	  [Thm ("separate_bdv", num_str @{thm separate_bdv}),

   205  		  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

   206  		 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),

   207       (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)

   208  		Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),

   209  		  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)

   210  		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})

   211        (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

   212     ]);

   213 (*show_types := true;  --- do we need type-constraint in thms? *)

   214 @{thm separate_bdv};     (*::?'a does NOT rewrite here WITHOUT type constraint*)

   215 @{thm separate_bdv_n};   (*::real ..because of ^^^, rewrites*)

   216 @{thm separate_1_bdv};   (*::?'a*)

   217 val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)

   218 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)

   219 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)

   221 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;

   222 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

   223 else error "integrate.sml simplify by ruleset separate_bdv.. #4";

   225 "===== test 5";

   226 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

   227 val rls = simplify_Integral;

   228 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

   229 (* given was:   "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)

   230 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

   231 else error "integrate.sml, simplify_Integral #99";

   233 "........... 2nd integral ........................................";

   234 "........... 2nd integral ........................................";

   235 "........... 2nd integral ........................................";

   236 val t = str2t

   237 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";

   238 val rls = simplify_Integral;

   239 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

   240 if term2str t =

   241    "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"

   242 then () else raise error "integrate.sml, simplify_Integral #198";

   244 val rls = integration_rules;

   245 val SOME (t,[]) = rewrite_set_ thy true rls t;

   246 term2str t;

   247 if term2str t =

   248    "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"

   249 then () else error "integrate.sml, simplify_Integral #199";

   252 "----------- integrate by ruleset -----------------------";

   253 "----------- integrate by ruleset -----------------------";

   254 "----------- integrate by ruleset -----------------------";

   255 val rls = "integration_rules";

   256 val subs' = [("bdv::real","x::real")];

   257 fun rewrit_sinst subs rls str =

   258     fst (the (rewrite_set_inst "Integrate" true subs rls str));

   259 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   260 val str = rewrit_sinst subs' rls "Integral x D x";

   261 val str = rewrit_sinst subs' rls "Integral c * x ^^^ 2 + c_2 D x";

   262 if str = "c * (x ^^^ 3 / 3) + c_2 * x"

   263 then () else error "integrate.sml: diff.behav. in integration_rules";

   265 val rls = "add_new_c";

   266 val str = rewrit_sinst subs' rls "c * (x ^^^ 3 / 3) + c_2 * x";

   267 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()

   268 else error "integrate.sml: diff.behav. in add_new_c simpl.";

   270 val str = rewrit_sinst subs' rls "F x = x ^^^ 3 / 3 + x";

   271 if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()

   272 else error "integrate.sml: diff.behav. in add_new_c equation";

   274 val rls = "simplify_Integral";

   275 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   276 val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";

   277 val str = rewrit_sinst subs' rls str;

   278 if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"

   279 then () else error "integrate.sml: diff.behav. in simplify_I #1";

   281 val rls = "integration";

   282 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   283 val str = rewrit_sinst subs' rls "Integral c * x ^^^ 2 + c_2 D x";

   284 if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"

   285 then () else error "integrate.sml: diff.behav. in integration #1";

   287 val str = rewrit_sinst subs' rls "Integral 3*x^^^2 + 2*x + 1 D x";

   288 if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()

   289 else error "integrate.sml: diff.behav. in integration #2";

   291 val str = rewrit_sinst subs' rls

   292 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";

   293 if str =

   294    "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

   295 then () else error "integrate.sml: diff.behav. in integration #3";

   297 val str = "Integral "^str^" D x";

   298 val str = rewrit_sinst subs' rls str;

   299 if str =

   300   "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"

   301 then () else error "integrate.sml: diff.behav. in integration #4";

   304 "----------- rewrite 3rd integration in 7.27 ------------";

   305 "----------- rewrite 3rd integration in 7.27 ------------";

   306 "----------- rewrite 3rd integration in 7.27 ------------";

   307 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);

   308 val t = str2t "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";

   309 val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;

   310 if term2str t =

   311   "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"

   312 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";

   314 val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;

   315 term2str t;

   316 if term2str t =

   317   "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

   318 then () else error "integrate.sml 3rd integration in 7.27, integration";

   321 "----------- check probem type --------------------------";

   322 "----------- check probem type --------------------------";

   323 "----------- check probem type --------------------------";

   324 val model = {Given =["functionTerm f_f", "integrateBy v_v"],

   325 	     Where =[],

   326 	     Find  =["antiDerivative F_F"],

   327 	     With  =[],

   328 	     Relate=[]}:string ppc;

   329 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;

   330 val t1 = (Thm.term_of o hd) chkmodel;

   331 val t2 = (Thm.term_of o hd o tl) chkmodel;

   332 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;

   333 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()

   334 	 | _ => error "integrate.sml: Integrate.antiDerivative ???";

   336 val model = {Given =["functionTerm f_f", "integrateBy v_v"],

   337 	     Where =[],

   338 	     Find  =["antiDerivativeName F_F"],

   339 	     With  =[],

   340 	     Relate=[]}:string ppc;

   341 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;

   342 val t1 = (Thm.term_of o hd) chkmodel;

   343 val t2 = (Thm.term_of o hd o tl) chkmodel;

   344 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;

   345 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()

   346 	 | _ => error "integrate.sml: Integrate.antiDerivativeName";

   348 "----- compare 'Find's from problem, script, formalization -------";

   349 val {ppc,...} = get_pbt ["named","integrate","function"];

   350 val ("#Find", (Const ("Integrate.antiDerivativeName", _),

   351 	       F1_ as Free ("F_F", F1_type))) = last_elem ppc;

   352 val {scr = Prog sc,... } = get_met ["diff","integration","named"];

   353 val [_,_, F2_] = formal_args sc;

   354 if F1_ = F2_ then () else error "integrate.sml: unequal find's";

   356 val ((dsc as Const ("Integrate.antiDerivativeName", _))

   357 	 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";

   358 if is_dsc dsc then () else error "integrate.sml: no description";

   359 if F1_type = F3_type then ()

   360 else error "integrate.sml: unequal types in find's";

   362 show_ptyps();

   363 val pbl = get_pbt ["integrate","function"];

   364 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()

   365 	 | _ => error "integrate.sml: Integrate.Integrate ???";

   368 "----------- check Scripts ------------------------------";

   369 "----------- check Scripts ------------------------------";

   370 "----------- check Scripts ------------------------------";

   371 val str =

   372 "Script IntegrationScript (f_f::real) (v_v::real) =               \

   373 \  (let t_t = Take (Integral f_f D v_v)                                 \

   374 \   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";

   375 val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;

   376 atomty sc;

   378 val str =

   379 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \

   380 \  (let t_t = Take (F_F v_v = Integral f_f D v_v)                         \

   381 \   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";

   382 val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;

   383 atomty sc;

   384 show_mets();

   387 "----------- me method [diff,integration] ---------------";

   388 "----------- me method [diff,integration] ---------------";

   389 "----------- me method [diff,integration] ---------------";

   390 (*exp_CalcInt_No-1.xml*)

   391 val p = e_pos'; val c = [];

   392 "----- step 0: returns nxt = Model_Problem ---";

   393 val (p,_,f,nxt,_,pt) =

   394     CalcTreeTEST

   395         [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],

   396           ("Integrate", ["integrate","function"], ["diff","integration"]))];

   397 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";

   398 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)

   399 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";

   400 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   401 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";

   402 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   403 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";

   404 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   405 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";

   406 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   407 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";

   408 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   409 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";

   410 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   411 case nxt of (_, Apply_Method ["diff", "integration"]) => ()

   412           | _ => error "integrate.sml -- me method [diff,integration] -- spec";

   413 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";

   414 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   415 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   416 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   417 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()

   418 else error "integrate.sml -- me method [diff,integration] -- end";

   421 "----------- autoCalculate [diff,integration] -----------";

   422 "----------- autoCalculate [diff,integration] -----------";

   423 "----------- autoCalculate [diff,integration] -----------";

   424 reset_states ();

   425 CalcTree

   426     [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],

   427       ("Integrate", ["integrate","function"], ["diff","integration"]))];

   428 Iterator 1;

   429 moveActiveRoot 1;

   430 autoCalculate 1 CompleteCalc;

   431 val ((pt,p),_) = get_calc 1; @{make_string} p; show_pt pt;

   432 val (Form t,_,_) = pt_extract (pt, p);

   433 if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()

   434 else error "integrate.sml -- interSteps [diff,integration] -- result";

   437 "----------- me method [diff,integration,named] ---------";

   438 "----------- me method [diff,integration,named] ---------";

   439 "----------- me method [diff,integration,named] ---------";

   440 (*exp_CalcInt_No-2.xml*)

   441 val fmz = ["functionTerm (x^^^2 + (1::real))",

   442 	   "integrateBy x","antiDerivativeName F"];

   443 val (dI',pI',mI') =

   444   ("Integrate",["named","integrate","function"],

   445    ["diff","integration","named"]);

   446 val p = e_pos'; val c = [];

   447 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   448 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   449 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   450 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);

   451 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   452 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   453 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   454 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

   455 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   456 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   457 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   458 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()

   459 else error "integrate.sml: method [diff,integration,named]";

   462 "----------- me met [diff,integration,named] Biegelinie.Q";

   463 "----------- me met [diff,integration,named] Biegelinie.Q";

   464 "----------- me met [diff,integration,named] Biegelinie.Q";

   465 (*exp_CalcInt_No-3.xml*)

   466 val fmz = ["functionTerm (- q_0)",

   467 	   "integrateBy x","antiDerivativeName Q"];

   468 val (dI',pI',mI') =

   469   ("Biegelinie",["named","integrate","function"],

   470    ["diff","integration","named"]);

   471 val p = e_pos'; val c = [];

   472 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   473 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   474 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   475 (*Error Tac Q not in ...*)

   476 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);

   477 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   478 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   479 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   480 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

   481 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   482 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   483 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

   485 if f2str f = "Q x = c + -1 * q_0 * x" then()

   486 else error "integrate.sml: method [diff,integration,named] .Q";

   489 "----------- interSteps [diff,integration] --------------";

   490 "----------- interSteps [diff,integration] --------------";

   491 "----------- interSteps [diff,integration] --------------";

   492 reset_states ();

   493 CalcTree

   494     [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],

   495       ("Integrate", ["integrate","function"], ["diff","integration"]))];

   496 Iterator 1;

   497 moveActiveRoot 1;

   498 autoCalculate 1 CompleteCalc;

   499 interSteps 1 ([1],Res);

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

   501 if existpt' ([1,3], Res) pt then ()

   502 else error "integrate.sml: interSteps on Rewrite_Set_Inst";

   505 reset_states ();

   506 CalcTree

   507 [(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],

   508   ("Integrate", ["integrate","function"], ["diff","integration","test"]))];

   509 Iterator 1;

   510 moveActiveRoot 1;

   511 autoCalculate 1 CompleteCalcHead;

   513 fetchProposedTactic 1  (*..Apply_Method*);

   514 autoCalculate 1 (Step 1);

   515 getTactic 1 ([1], Frm)  (*still empty*);

   517 fetchProposedTactic 1  (*Rewrite_Set_Inst integration_rules*);

   518 autoCalculate 1 (Step 1);

   520 fetchProposedTactic 1  (*Rewrite_Set_Inst add_new_c*);

   521 autoCalculate 1 (Step 1);

   523 fetchProposedTactic 1  (*Rewrite_Set_Inst simplify_Integral*);

   524 autoCalculate 1 (Step 1);

   526 autoCalculate 1 CompleteCalc;

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

   528 val (Form t,_,_) = pt_extract (pt, p); term2str t;

   529 if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()

   530 else error  "integrate.sml: test-script doesnt work";

   533 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

   534 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

   535 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

   536 reset_states ();

   537 CalcTree

   538 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],

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

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

   541 Iterator 1;

   542 moveActiveRoot 1;

   543 autoCalculate 1 CompleteCalc;

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

   545 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3"

   546 then () else error "Ambiguous input: Integral ?u + ?v D ?bdv ="

   548 interSteps 1 ([1],Res);

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

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

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

   552 (*getTactic 1 ([1,1,1],Frm); TODO.WN111207 kind of error unclear:

   553 @@@@@begin@@@@@

   554  1

   555 <SYSERROR>

   556   <CALCID> 1 </CALCID>

   557   <ERROR> syserror in getTactic </ERROR>

   558 </SYSERROR>

   559 @@@@@end@@@@@ *)

   561 val str = (unenclose o Thm.get_name_hint) @{thm integral_add};

   562 str = "ntegrate.integral_ad"; (*WN111207 begin+end cut off*)

   563 writeln str;

   564 (*WN111207 was outcommented already:

   565 read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));

   567 *** More than one term is type correct:

   568 *** ((Integral (?u + ?v) D ?bdv) =

   569 ***  (Integral ?u D (?bdv + (Integral ?v D ?bdv))))

   570                 ###^^^###

   571 *** ((Integral (?u + ?v) D ?bdv) =

   572 ***  ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))

   573 *)

   575 (*============ inhibit exn WN120314 ==============================================

   576 (*??? WN111205: this check succeeds erratically : asyncronous Isar/jEdit ???*)

   577 if existpt' ([1,1,5], Res) pt then ()

   578 else error "integrate.sml: interSteps on Rewrite_Set_Inst 2 ERRATICAL???";

   579 ============ inhibit exn WN120314 ==============================================*)

   582 "----------- CAS input ----------------------------------";

   583 "----------- CAS input ----------------------------------";

   584 "----------- CAS input ----------------------------------";

   585 val t = str2t "Integrate (x^^^2 + x + 1, x)";

   586 case t of Const ("Integrate.Integrate", _) $ _ => ()

   587 	| _ => error "diff.sml behav.changed for Integrate (..., x)";

   588 atomty t;

   590 reset_states ();

   591 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

   592 Iterator 1;

   593 moveActiveRoot 1;

   594 replaceFormula 1 "Integrate (x^2 + x + 1, x)";

   595 autoCalculate 1 CompleteCalc;

   596 val ((pt,p),_) = get_calc 1;

   597 val Form res = (#1 o pt_extract) (pt, ([],Res));

   598 show_pt pt;

   599 (*

   600 WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version

   601 from 2007; not touched since then.

   603 WN070703 does not work like Diff due to error in next-pos

   604 if p = ([], Res) andalso term2str res = "5 * a" then ()

   605 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";

   607 *)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Wed, 14 Feb 2018 08:05:37 +0100
changeset 59371	3594fcedebe9
parent 59255	383722bfcff5
child 59384	d92ff7591a11
permissions	-rw-r--r--