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

     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 = Print_Mode.setmp [] (Syntax.string_of_term

    41 					(ProofContext.init_global thy)) t;

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

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

    45 atomty t;

    47 val t = str2term "ff x is_f_x";

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

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

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

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

    54 "----------- integrate by rewriting ---------------------";

    55 val conditions_in_integration_rules =

    56 Rls {id="conditions_in_integration_rules",

    57      preconds = [],

    58      rew_ord = ("termlessI",termlessI),

    59      erls = Erls,

    60      srls = Erls, calc = [],

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

    62 	      Calc ("Atools.occurs'_in",

    63 		    eval_occurs_in "#occurs_in_"),

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

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

    66 	      ],

    67      scr = EmptyScr};

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

    69 fun rewrit thm str =

    70     fst (the (rewrite_inst_ thy tless_true

    71 			   conditions_in_integration_rules

    72 			   true subs thm str));

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

    74 term2s str;

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

    76 term2s str;

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

    78     handle OPTION => str2term "no_rewrite";

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

    81 term2s str;

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

    83     handle OPTION => str2term "no_rewrite";

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

    86 term2s str;

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

    89 term2s str;

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

    91     handle OPTION => str2term "no_rewrite";

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

    94 term2s str;

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

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

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

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

   101 val cc = new_c term;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   132 val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c 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 + new_c x ^^^ 2 / 2) = True"

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

   137 val t = str2term "ff x is_f_x";

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

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

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

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

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

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

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

   147 val conditions_in_integration =

   148 Rls {id="conditions_in_integration",

   149      preconds = [],

   150      rew_ord = ("termlessI",termlessI),

   151      erls = Erls,

   152      srls = Erls, calc = [],

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

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

   155       	      eval_is_f_x "is_f_x_"),

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

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

   158       	],

   159      scr = EmptyScr};

   160 fun rewrit thm t =

   161     fst (the (rewrite_inst_ thy tless_true

   162 			    conditions_in_integration true subs thm t));

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

   164 val t = (rewrit call_for_new_c t)

   165     handle OPTION =>  str2term "no_rewrite";

   167 val t = rewrit call_for_new_c

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

   169 val t = (rewrit call_for_new_c

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

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

   172 --------------------------------------------------------------------*)

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

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

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

   178 val thy = theory "Isac";

   179 "===== test 1";

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

   181 val t = str2term "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"

   204  	       collect_bdv

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

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

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

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

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

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

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

   212                 (*"?bdv / ?b = (1::?'a) / ?b * ?bdv"*)

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

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

   215                ]);

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

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

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

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

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

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

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

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

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

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

   228 "===== test 5";

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

   230 val rls = simplify_Integral;

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

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

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

   236 "........... 2nd integral ........................................";

   237 "........... 2nd integral ........................................";

   238 "........... 2nd integral ........................................";

   239 val t = str2term

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

   241 val rls = simplify_Integral;

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

   243 term2str t;

   245 (*===== inhibit exn ============================================================

   246 if term2str t =

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

   248 GOON: still 2*3 TODO...

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

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

   253 trace_rewrite := true;

   254 tracing "====== test 4 =============================";

   255 tracing "====== test 4 =============================";

   256 term2str t;

   257 trace_rewrite := false;

   259 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   260 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   262 val rls = integration_rules;

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

   264 if term2str t =

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

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

   270 "----------- simplify by extending make_polynomial_in ---";

   271 "----------- simplify by extending make_polynomial_in ---";

   272 "----------- simplify by extending make_polynomial_in ---";

   273 trace_rewrite:=true;

   274 trace_rewrite:=false;

   275 (*postponed: see *)

   278 "----------- integrate by ruleset -----------------------";

   279 "----------- integrate by ruleset -----------------------";

   280 "----------- integrate by ruleset -----------------------";

   281 val rls = "integration_rules";

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

   283 fun rewrit_sinst subs rls str =

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

   285 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

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

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

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

   291 val rls = "add_new_c";

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

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

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

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

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

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

   300 val rls = "simplify_Integral";

   301 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

   303 val str = rewrit_sinst subs rls str;

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

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

   307 val rls = "integration";

   308 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

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

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

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

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

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

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

   317 val str = rewrit_sinst subs rls

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

   319 if str =

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

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

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

   324 val str = rewrit_sinst subs rls str;

   325 if str =

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

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

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

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

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

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

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

   335 val t = str2term

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

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

   338 if term2str t =

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

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

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

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

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

   347 "----------- check probem type --------------------------";

   348 "----------- check probem type --------------------------";

   349 "----------- check probem type --------------------------";

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

   351 	     Where =[],

   352 	     Find  =["antiDerivative F_"],

   353 	     With  =[],

   354 	     Relate=[]}:string ppc;

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

   356 val t1 = (term_of o hd) chkmodel;

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

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

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

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

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

   363 	     Where =[],

   364 	     Find  =["antiDerivativeName F_"],

   365 	     With  =[],

   366 	     Relate=[]}:string ppc;

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

   368 val t1 = (term_of o hd) chkmodel;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   385 if F1_type = F3_type then ()

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

   388 show_ptyps();

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

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

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

   394 "----------- check Scripts ------------------------------";

   395 "----------- check Scripts ------------------------------";

   396 "----------- check Scripts ------------------------------";

   397 val str =

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

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

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

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

   402 atomty sc;

   404 val str =

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

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

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

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

   409 atomty sc;

   410 show_mets();

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

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

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

   416 (*exp_CalcInt_No-1.xml*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   441 (*exp_CalcInt_No-2.xml*)

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

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

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

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

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

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

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

   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(*nxt <- Add_Find *);

   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;

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

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

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

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

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

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

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

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

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

   466 (*exp_CalcInt_No-3.xml*)

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

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

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

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

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

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

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

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

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

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

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

   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;

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

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

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

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

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

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

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

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

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

   493 states:=[];

   494 CalcTree

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

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

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

   498 Iterator 1;

   499 moveActiveRoot 1;

   500 autoCalculate 1 CompleteCalc;

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

   503 interSteps 1 ([1],Res);

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

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

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

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

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

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

   512 store_met

   513     (prep_met thy "met_testint" [] e_metID

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

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

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

   517 		],

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

   519 		srls = e_rls,

   520 		prls=e_rls,

   521 	     crls = Atools_erls, nrls = e_rls},

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

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

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

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

   526 ));

   528 states:=[];

   529 CalcTree

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

   531    "antiDerivative FF"],

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

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

   534 Iterator 1;

   535 moveActiveRoot 1;

   536 autoCalculate 1 CompleteCalcHead;

   538 fetchProposedTactic 1  (*..Apply_Method*);

   539 autoCalculate 1 (Step 1);

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

   542 fetchProposedTactic 1  (*Rewrite_Set_Inst integration_rules*);

   543 autoCalculate 1 (Step 1);

   545 fetchProposedTactic 1  (*Rewrite_Set_Inst add_new_c*);

   546 autoCalculate 1 (Step 1);

   548 fetchProposedTactic 1  (*Rewrite_Set_Inst simplify_Integral*);

   549 autoCalculate 1 (Step 1);

   551 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

   560 states:=[];

   561 CalcTree

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

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

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

   565 Iterator 1;

   566 moveActiveRoot 1;

   567 autoCalculate 1 CompleteCalc;

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

   570 interSteps 1 ([1],Res);

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

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

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

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

   576 val str = (unenclose o string_of_thm) integral_add;

   577 writeln str;

   578 (*

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

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

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

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

   584                 ###^^^###

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

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

   587 *)

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

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

   593 "----------- CAS input ----------------------------------";

   594 "----------- CAS input ----------------------------------";

   595 "----------- CAS input ----------------------------------";

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

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

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

   599 atomty t;

   601 states:=[];

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

   603 Iterator 1;

   604 moveActiveRoot 1;

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

   606 autoCalculate 1 CompleteCalc;

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

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

   609 show_pt pt;

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

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

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

   613 *)

   615 ===== inhibit exn ============================================================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38030	95d956108461
child 38048	377d9061ec3e
permissions	-rw-r--r--