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

     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 = Integrate.thy;

    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 ruleset 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 method [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 Integrate.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_ Integrate.thy tless_true

    70 			   conditions_in_integration_rules

    71 			   true subs thm str));

    72 val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str;

    73 val str = rewrit integral_const (str2term  "Integral M'/EJ D x"); term2s str;

    74 val str = (rewrit integral_const (str2term "Integral x D x"))

    75     handle OPTION => str2term "no_rewrite";

    77 val str = rewrit integral_var (str2term "Integral x D x"); term2s str;

    78 val str = (rewrit integral_var (str2term "Integral a D x"))

    79     handle OPTION => str2term "no_rewrite";

    81 val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str;

    83 val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str;

    84 val str = (rewrit integral_mult (str2term "Integral x * x D x"))

    85     handle OPTION => str2term "no_rewrite";

    87 val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str;

    90 "----------- test add_new_c, is_f_x ------------------------------";

    91 "----------- test add_new_c, is_f_x ------------------------------";

    92 "----------- test add_new_c, is_f_x ------------------------------";

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

    94 val cc = new_c term;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   130 val t = str2term "ff x is_f_x";

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

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

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

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

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

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

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

   140 val conditions_in_integration =

   141 Rls {id="conditions_in_integration",

   142      preconds = [],

   143      rew_ord = ("termlessI",termlessI),

   144      erls = Erls,

   145      srls = Erls, calc = [],

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

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

   148       	      eval_is_f_x "is_f_x_"),

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

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

   151       	],

   152      scr = EmptyScr};

   153 fun rewrit thm t =

   154     fst (the (rewrite_inst_ Integrate.thy tless_true

   155 			    conditions_in_integration true subs thm t));

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

   157 val t = (rewrit call_for_new_c t)

   158     handle OPTION =>  str2term "no_rewrite";

   160 val t = rewrit call_for_new_c

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

   162 val t = (rewrit call_for_new_c

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

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

   165 --------------------------------------------------------------------*)

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

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

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

   171 val thy = Isac.thy;

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

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

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

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

   177 case rewrite_set_inst_ thy true subs rls t of

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

   179   | NONE => ();

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

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

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

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

   184 AFTER CORRECTION in Integrate.ML as above*)

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

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

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

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

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

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

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

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

   196 val rls =

   197     (append_rls "separate_bdv"

   198  	       collect_bdv

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

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

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

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

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

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

   205                ]);

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

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

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

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

   212 val rls = simplify_Integral;

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

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

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

   217 "........... 2nd integral ........................................";

   218 "........... 2nd integral ........................................";

   219 "........... 2nd integral ........................................";

   220 val t = str2term

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

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

   223 val rls = simplify_Integral;

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

   225 if term2str t =

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

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

   229 val rls = integration_rules;

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

   231 if term2str t =

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

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

   237 "----------- simplify by ruleset extending make_polynomial_in ----";

   238 "----------- simplify by ruleset extending make_polynomial_in ----";

   239 "----------- simplify by ruleset extending make_polynomial_in ----";

   240 trace_rewrite:=true;

   241 trace_rewrite:=false;

   242 (*postponed: see *)

   245 "----------- integrate by ruleset --------------------------------";

   246 "----------- integrate by ruleset --------------------------------";

   247 "----------- integrate by ruleset --------------------------------";

   248 val rls = "integration_rules";

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

   250 fun rewrit_sinst subs rls str =

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

   252 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

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

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

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

   258 val rls = "add_new_c";

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

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

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

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

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

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

   267 val rls = "simplify_Integral";

   268 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

   270 val str = rewrit_sinst subs rls str;

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

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

   274 val rls = "integration";

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

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

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

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

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

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

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

   284 val str = rewrit_sinst subs rls

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

   286 if str =

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

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

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

   291 val str = rewrit_sinst subs rls str;

   292 if str =

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

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

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

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

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

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

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

   302 val t = str2term

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

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

   305 if term2str t =

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

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

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

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

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

   314 "----------- check probem type -----------------------------------";

   315 "----------- check probem type -----------------------------------";

   316 "----------- check probem type -----------------------------------";

   317 val model = {Given =["functionTerm f_", "integrateBy v_v"],

   318 	     Where =[],

   319 	     Find  =["antiDerivative F_"],

   320 	     With  =[],

   321 	     Relate=[]}:string ppc;

   322 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;

   323 val t1 = (term_of o hd) chkmodel;

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

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

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

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

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

   330 	     Where =[],

   331 	     Find  =["antiDerivativeName F_"],

   332 	     With  =[],

   333 	     Relate=[]}:string ppc;

   334 val chkmodel = ((map (the o (parse Integrate.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.antiDerivativeName", _) $ _ => ()

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

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

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

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

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

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

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

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

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

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

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

   352 if F1_type = F3_type then ()

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

   355 show_ptyps();

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

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

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

   361 "----------- check Scripts ---------------------------------------";

   362 "----------- check Scripts ---------------------------------------";

   363 "----------- check Scripts ---------------------------------------";

   364 val str =

   365 "Script IntegrationScript (f_::real) (v_v::real) =               \

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

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

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

   369 atomty sc;

   371 val str =

   372 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \

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

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

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

   376 atomty sc;

   377 show_mets();

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

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

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

   383 (*exp_CalcInt_No-1.xml*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   408 (*exp_CalcInt_No-2.xml*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   430 "----------- me method [diff,integration,named] Biegelinie.Q -----";

   431 "----------- me method [diff,integration,named] Biegelinie.Q -----";

   432 "----------- me method [diff,integration,named] Biegelinie.Q -----";

   433 (*exp_CalcInt_No-3.xml*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   460 states:=[];

   461 CalcTree

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

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

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

   465 Iterator 1;

   466 moveActiveRoot 1;

   467 autoCalculate 1 CompleteCalc;

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

   470 interSteps 1 ([1],Res);

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

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

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

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

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

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

   479 store_met

   480     (prep_met Integrate.thy "met_testint" [] e_metID

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

   482 	       [("#Given" ,["functionTerm f_", "integrateBy v_v"]),

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

   484 		],

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

   486 		srls = e_rls,

   487 		prls=e_rls,

   488 	     crls = Atools_erls, nrls = e_rls},

   489 "Script IntegrationScript (f_::real) (v_v::real) =             \

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

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

   492 \    (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))"

   493 ));

   495 states:=[];

   496 CalcTree

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

   498    "antiDerivative FF"],

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

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

   501 Iterator 1;

   502 moveActiveRoot 1;

   503 autoCalculate 1 CompleteCalcHead;

   505 fetchProposedTactic 1  (*..Apply_Method*);

   506 autoCalculate 1 (Step 1);

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

   509 fetchProposedTactic 1  (*Rewrite_Set_Inst integration_rules*);

   510 autoCalculate 1 (Step 1);

   512 fetchProposedTactic 1  (*Rewrite_Set_Inst add_new_c*);

   513 autoCalculate 1 (Step 1);

   515 fetchProposedTactic 1  (*Rewrite_Set_Inst simplify_Integral*);

   516 autoCalculate 1 (Step 1);

   518 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

   527 states:=[];

   528 CalcTree

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

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

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

   532 Iterator 1;

   533 moveActiveRoot 1;

   534 autoCalculate 1 CompleteCalc;

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

   537 interSteps 1 ([1],Res);

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

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

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

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

   543 val str = (unenclose o string_of_thm) integral_add;

   544 writeln str;

   545 (*

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

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

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

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

   551                 ###^^^###

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

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

   554 *)

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

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

   559 "----------- CAS input -------------------------------------------";

   560 "----------- CAS input -------------------------------------------";

   561 "----------- CAS input -------------------------------------------";

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

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

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

   565 atomty t;

   567 states:=[];

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

   569 Iterator 1;

   570 moveActiveRoot 1;

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

   572 autoCalculate 1 CompleteCalc;

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

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

   575 show_pt pt;

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

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

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

   579 *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 08 Sep 2010 16:47:22 +0200
branch	isac-update-Isa09-2
changeset 37991	028442673981
parent 37981	b2877b9d455a
child 37994	eb4c556a525b
permissions	-rw-r--r--