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

     1 (* tests on integration over the reals

     2    author: Walther Neuper

     3    050814, 08:51

     4    (c) due to copyright terms

     6 use"../smltest/IsacKnowledge/integrate.sml";

     7 use"integrate.sml";

     8 *)

     9 val thy = theory "Integrate";

    11 "--------------------------------------------------------";

    12 "table of contents --------------------------------------";

    13 "--------------------------------------------------------";

    14 "----------- parsing ------------------------------------";

    15 "----------- integrate by rewriting ---------------------";

    16 "----------- test add_new_c, is_f_x ---------------------";

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

    18 "----------- simplify by extending make_polynomial_in ---";

    19 "----------- integrate by ruleset -----------------------";

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

    21 "----------- check probem type --------------------------";

    22 "----------- check Scripts ------------------------------";

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

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

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

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

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

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

    29 "----------- CAS input ----------------------------------";

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

    31 "--------------------------------------------------------";

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

    36 "----------- parsing ------------------------------------";

    37 "----------- parsing ------------------------------------";

    38 "----------- parsing ------------------------------------";

    39 fun str2term str = (term_of o the o (parse thy)) str;

    40 fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;

    42 val t = str2term "Integral x D x";

    43 val t = str2term "Integral x^^^2 D x";

    44 atomty t;

    46 val t = str2term "ff x is_f_x";

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

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

    51 "----------- integrate by rewriting ---------------------";

    52 "----------- integrate by rewriting ---------------------";

    53 "----------- integrate by rewriting ---------------------";

    54 val conditions_in_integration_rules =

    55 Rls {id="conditions_in_integration_rules",

    56      preconds = [],

    57      rew_ord = ("termlessI",termlessI),

    58      erls = Erls,

    59      srls = Erls, calc = [],

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

    61 	      Calc ("Atools.occurs'_in",

    62 		    eval_occurs_in "#occurs_in_"),

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

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

    65 	      ],

    66      scr = EmptyScr};

    67 val subs = [(str2term "bdv", str2term "x")];

    68 fun rewrit thm str =

    69     fst (the (rewrite_inst_ thy tless_true

    70 			   conditions_in_integration_rules

    71 			   true subs thm str));

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

    73 term2s str;

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

    75 term2s str;

    76 val str = (rewrit @{thm "integral_const"} (str2term "Integral x D x"))

    77     handle OPTION => str2term "no_rewrite";

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

    80 term2s str;

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

    82     handle OPTION => str2term "no_rewrite";

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

    85 term2s str;

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

    88 term2s str;

    89 val str = (rewrit @{thm "integral_mult"} (str2term "Integral x * x D x"))

    90     handle OPTION => str2term "no_rewrite";

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

    93 term2s str;

    96 "----------- test add_new_c, is_f_x ---------------------";

    97 "----------- test add_new_c, is_f_x ---------------------";

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

    99 val term = str2term "x^^^2*c + c_2";

   100 val cc = new_c term;

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

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

   104 "####1###################################################";

   105 term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +";

   106 "####2###################################################";

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

   109 else raise error "intergrate.sml: diff. eval_add_new_c";

   111 "####3###################################################";

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

   114 val SOME (thmstr, thm) = get_calculation1_ thy cc term;

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

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

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

   120 val term = str2term "ff x = x^^^2*c + c_2";

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

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

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

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

   127 val term = str2term "new_c (c * x^^^2 + c_2)";

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

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

   130 else raise error "integrate.sml: eval_new_c ???";

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

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

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

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

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

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

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

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

   142 val t = str2term "ff x is_f_x";

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

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

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

   147 val t = str2term "q_0/2 * L * x is_f_x";

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

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

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

   152 val conditions_in_integration =

   153 Rls {id="conditions_in_integration",

   154      preconds = [],

   155      rew_ord = ("termlessI",termlessI),

   156      erls = Erls,

   157      srls = Erls, calc = [],

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

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

   160       	      eval_is_f_x "is_f_x_"),

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

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

   163       	],

   164      scr = EmptyScr};

   165 fun rewrit thm t =

   166     fst (the (rewrite_inst_ thy tless_true

   167 			    conditions_in_integration true subs thm t));

   168 val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t;

   169 val t = (rewrit call_for_new_c t)

   170     handle OPTION =>  str2term "no_rewrite";

   172 val t = rewrit call_for_new_c

   173 	       (str2term "ff x = q_0/2 *L*x"); term2s t;

   174 val t = (rewrit call_for_new_c

   175 	       (str2term "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))

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

   177 --------------------------------------------------------------------*)

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

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

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

   183 val thy = Isac.thy;

   184 val subs = [(str2term"bdv",str2term"x")];

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

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

   188 (*###*)val rls = norm_Rational_noadd_fractions;

   189 case rewrite_set_inst_ thy true subs rls t of

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

   191   | NONE => ();

   192 (* WN051028 Rational.ML 'rat_mult_div_pow' with erls = e_rls

   193 applies 'rat_mult_poly_r'="?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"

   194 to "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI"

   195 and keeps "..." is_polyexp" as an assumption.

   196 AFTER CORRECTION in Integrate.ML as above*)

   198 (*###*)val rls = order_add_mult_in;

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

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

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

   203 (*###*)val rls = discard_parentheses;

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

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

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

   208 val rls =

   209     (append_rls "separate_bdv"

   210  	       collect_bdv

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

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

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

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

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

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

   217                ]);

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

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

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

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

   224 val rls = simplify_Integral;

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

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

   227 else raise error "integrate.sml, simplify_Integral #99";

   229 "........... 2nd integral ........................................";

   230 "........... 2nd integral ........................................";

   231 "........... 2nd integral ........................................";

   232 val t = str2term

   233 	    "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + \

   234 	    \-1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";

   235 val rls = simplify_Integral;

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

   237 if term2str t =

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

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

   241 val rls = integration_rules;

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

   243 if term2str t =

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

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

   249 "----------- simplify by extending make_polynomial_in ---";

   250 "----------- simplify by extending make_polynomial_in ---";

   251 "----------- simplify by extending make_polynomial_in ---";

   252 trace_rewrite:=true;

   253 trace_rewrite:=false;

   254 (*postponed: see *)

   257 "----------- integrate by ruleset -----------------------";

   258 "----------- integrate by ruleset -----------------------";

   259 "----------- integrate by ruleset -----------------------";

   260 val rls = "integration_rules";

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

   262 fun rewrit_sinst subs rls str =

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

   264 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   265 val str = rewrit_sinst subs rls "Integral x D x";

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

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

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

   270 val rls = "add_new_c";

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

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

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

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

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

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

   279 val rls = "simplify_Integral";

   280 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

   282 val str = rewrit_sinst subs rls str;

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

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

   286 val rls = "integration";

   287 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

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

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

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

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

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

   296 val str = rewrit_sinst subs rls

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

   298 if str =

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

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

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

   303 val str = rewrit_sinst subs rls str;

   304 if str =

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

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

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

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

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

   312 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);

   313 val bdv = [(str2term"bdv", str2term"x")];

   314 val t = str2term

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

   316 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;

   317 if term2str t =

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

   319 else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";

   321 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;

   322 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

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

   326 "----------- check probem type --------------------------";

   327 "----------- check probem type --------------------------";

   328 "----------- check probem type --------------------------";

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

   330 	     Where =[],

   331 	     Find  =["antiDerivative F_"],

   332 	     With  =[],

   333 	     Relate=[]}:string ppc;

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

   335 val t1 = (term_of o hd) chkmodel;

   336 val t2 = (term_of o hd o tl) chkmodel;

   337 val t3 = (term_of o hd o tl o tl) chkmodel;

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

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

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

   342 	     Where =[],

   343 	     Find  =["antiDerivativeName F_"],

   344 	     With  =[],

   345 	     Relate=[]}:string ppc;

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

   347 val t1 = (term_of o hd) chkmodel;

   348 val t2 = (term_of o hd o tl) chkmodel;

   349 val t3 = (term_of o hd o tl o tl) chkmodel;

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

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

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

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

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

   356 	       F1_ as Free ("F_", F1_type))) = last_elem ppc;

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

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

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

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

   362 	 $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff";

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

   364 if F1_type = F3_type then ()

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

   367 show_ptyps();

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

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

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

   373 "----------- check Scripts ------------------------------";

   374 "----------- check Scripts ------------------------------";

   375 "----------- check Scripts ------------------------------";

   376 val str =

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

   378 \  (let t_ = Take (Integral f_ D v_v)                                 \

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

   380 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   381 atomty sc;

   383 val str =

   384 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \

   385 \  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \

   386 \   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";

   387 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   388 atomty sc;

   389 show_mets();

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

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

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

   395 (*exp_CalcInt_No-1.xml*)

   396 val fmz = ["functionTerm (x^^^2 + 1)",

   397 	   "integrateBy x","antiDerivative FF"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   414 else raise error "integrate.sml: method [diff,integration]";

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

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

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

   420 (*exp_CalcInt_No-2.xml*)

   421 val fmz = ["functionTerm (x^^^2 + 1)",

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   445 (*exp_CalcInt_No-3.xml*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   472 states:=[];

   473 CalcTree

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

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

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

   477 Iterator 1;

   478 moveActiveRoot 1;

   479 autoCalculate 1 CompleteCalc;

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

   482 interSteps 1 ([1],Res);

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

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

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

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

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

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

   491 store_met

   492     (prep_met thy "met_testint" [] e_metID

   493 	      (["diff","integration","test"],

   494 	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),

   495 		("#Find"  ,["antiDerivative F_"])

   496 		],

   497 	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [],

   498 		srls = e_rls,

   499 		prls=e_rls,

   500 	     crls = Atools_erls, nrls = e_rls},

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

   502 \  (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \

   503 \    (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False)         @@ \

   504 \    (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"

   505 ));

   507 states:=[];

   508 CalcTree

   509 [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x",

   510    "antiDerivative FF"],

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

   512   ["diff","integration","test"]))];

   513 Iterator 1;

   514 moveActiveRoot 1;

   515 autoCalculate 1 CompleteCalcHead;

   517 fetchProposedTactic 1  (*..Apply_Method*);

   518 autoCalculate 1 (Step 1);

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

   521 fetchProposedTactic 1  (*Rewrite_Set_Inst integration_rules*);

   522 autoCalculate 1 (Step 1);

   524 fetchProposedTactic 1  (*Rewrite_Set_Inst add_new_c*);

   525 autoCalculate 1 (Step 1);

   527 fetchProposedTactic 1  (*Rewrite_Set_Inst simplify_Integral*);

   528 autoCalculate 1 (Step 1);

   530 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

   539 states:=[];

   540 CalcTree

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

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

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

   544 Iterator 1;

   545 moveActiveRoot 1;

   546 autoCalculate 1 CompleteCalc;

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

   549 interSteps 1 ([1],Res);

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

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

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

   553 getTactic 1 ([1,1,1],Frm);

   555 val str = (unenclose o string_of_thm) integral_add;

   556 writeln str;

   557 (*

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

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

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

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

   563                 ###^^^###

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

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

   566 *)

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

   569 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2";

   572 "----------- CAS input ----------------------------------";

   573 "----------- CAS input ----------------------------------";

   574 "----------- CAS input ----------------------------------";

   575 val t = str2term "Integrate (x^^^2 + x + 1, x)";

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

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

   578 atomty t;

   580 states:=[];

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

   582 Iterator 1;

   583 moveActiveRoot 1;

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

   585 autoCalculate 1 CompleteCalc;

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

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

   588 show_pt pt;

   589 (* WN070703 does not work like Diff due to error in next-pos

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

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

   592 *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 23 Sep 2010 12:56:51 +0200
branch	isac-update-Isa09-2
changeset 38013	e4f42a63d665
parent 38010	a37a3ab989f4
child 38014	3e11e3c2dc42
permissions	-rw-r--r--