wneuper/isa: test/Tools/isac/Knowledge/diff.sml@c3f399ce32af

     1 (*

     3 use"../smltest/IsacKnowledge/diff.sml";

     4 use"diff.sml";

     5 *)

     7 "--------------------------------------------------------";

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

     9 "table of contents --------------------------------------";

    10 "--------------------------------------------------------";

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

    12 "----------- for correction of diff_const ---------------";

    13 "----------- for correction of diff_quot ----------------";

    14 "----------- differentiate by rewrite -------------------";

    15 "----------- differentiate: me (*+ tacs input*) ---------";

    16 "----------- 1.5.02 me from script ----------------------";

    17 "----------- primed id ----------------------------------";

    18 "----------- diff_conv, sym_diff_conv -------------------";

    19 "----------- autoCalculate differentiate_on_R 2/x^2 -----";

    20 "----------- autoCalculate diff after_simplification ----";

    21 "----------- autoCalculate differentiate_equality -------";

    22 "----------- tests for examples -------------------------";

    23 "------------inform for x^2+x+1 -------------------------";

    24 "--------------------------------------------------------";

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

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

    29 val thy = @{theory "Diff"};

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

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

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

    34 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],

    35 	   Where =[],

    36 	   Find  =["derivative f_f'"],

    37 	   With  =[],

    38 	   Relate=[]}:string ppc;

    39 val chkpbt = ((map (the o (parse thy))) o ppc2list) pbt;

    41 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",

    42 	   "differentiateFor x","derivative f_f'"];

    43 val chkorg = map (the o (parse thy)) org;

    45 get_pbt ["derivative_of","function"];

    46 get_met ["diff","differentiate_on_R"];

    48 (*erls should not be in ruleset'! Here only for tests*)

    49 ruleset' :=

    50 overwritelthy thy

    51     (!ruleset',

    52      [("erls",

    53        Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),

    54 	    erls = e_rls, srls = Erls, calc = [], errpatts = [],

    55 	    rules = [Thm ("refl",num_str @{thm refl}),

    56 		     Thm ("order_refl",num_str @{thm order_refl}),

    57 		     Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),

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

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

    60 		     Thm ("and_true",num_str @{thm and_true}),

    61 		     Thm ("and_false",num_str @{thm and_false}),

    62 		     Thm ("or_true",num_str @{thm or_true}),

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

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

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

    67 		     Calc ("Atools.is'_const",eval_const "#is_const_"),

    68 		     Calc ("Atools.occurs'_in", eval_occurs_in ""),

    69 		     Calc ("Tools.matches",eval_matches ""),

    71 		     Calc ("Groups.plus_class.plus",eval_binop "#add_"),

    72 		     Calc ("Groups.times_class.times",eval_binop "#mult_"),

    73 		     Calc ("Atools.pow" ,eval_binop "#power_"),

    75 		     Calc ("Orderings.ord_class.less",eval_equ "#less_"),

    76 		     Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),

    78 		     Calc ("Atools.ident",eval_ident "#ident_")],

    79 	    scr = Prog ((term_of o the o (parse thy))

    80 			      "empty_script")

    81 	    }:rls

    82 	      )]);

    84 "----------- for correction of diff_const ---------------";

    85 "----------- for correction of diff_const ---------------";

    86 "----------- for correction of diff_const ---------------";

    87 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)

    88 val thy' = "Diff";

    89 val ct = "Not (x =!= a)";

    90 rewrite_set thy' false "erls" ct;

    91 val ct = "2 is_const";

    92 rewrite_set thy' false "erls" ct;

    94 val thm = ("diff_const","");

    95 val ct = "d_d x x";

    96 val NONE =

    97     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);

    98 val ct = "d_d x 2";

    99 val SOME (ctt,_) =

   100     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);

   101 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";

   102 trace_rewrite := false;

   103 val ct = "d_d s a";

   104     (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);

   105 (*got: NONE instead SOME*)

   106 eval_true (@{theory "Isac"}) [str2term "a is_const"] (assoc_rls"erls");

   107 (*got: false instead true;   ~~~~~~~~~~~ replaced by 'is_atom'*)

   108 val SOME (ctt,_) =

   109     (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);

   110 if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav.";

   111 trace_rewrite := false;

   112 "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----";

   114 val thm = ("diff_var","");

   115 val ct = "d_d x x";

   116 val SOME (ctt,_) =

   117     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);

   118 val ct = "d_d x a";

   119 val NONE =

   120     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);

   121 val ct = "d_d x (x+x)";

   122 val NONE =

   123 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);

   126 "----------- for correction of diff_quot ----------------";

   127 "----------- for correction of diff_quot ----------------";

   128 "----------- for correction of diff_quot ----------------";

   129 val thy' = "Diff";

   130 val ct = "Not (x = 0)";

   131 rewrite_set thy' false "erls" ct;

   133 val ct = "d_d x ((x+1) / (x - 1))";

   134 val thm = ("diff_quot","");

   135 val SOME (ctt,_) =

   136     (rewrite_inst thy' "tless_true" "erls" true [("bdv","x")] thm ct);

   139 "----------- differentiate by rewrite -------------------";

   140 "----------- differentiate by rewrite -------------------";

   141 "----------- differentiate by rewrite -------------------";

   142 val thy' = "Diff";

   143 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";

   144 "--- 1 ---";

   145 val thm = ("diff_sum","");

   146 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   147 		  [("bdv","x::real")] thm ct);

   148 "--- 2 ---";

   149 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   150 		  [("bdv","x::real")] thm ct);

   151 "--- 3 ---";

   152 val thm = ("diff_prod_const","");

   153 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   154 		  [("bdv","x::real")] thm ct);

   155 "--- 4 ---";

   156 val thm = ("diff_pow","");

   157 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   158 		  [("bdv","x::real")] thm ct);

   159 "--- 5 ---";

   160 val thm = ("diff_const","");

   161 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   162 		  [("bdv","x::real")] thm ct);

   163 "--- 6 ---";

   164 val thm = ("diff_var","");

   165 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true

   166 		  [("bdv","x::real")] thm ct);

   167 if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()

   168 else error "diff.sml diff.behav. in rewrite 1";

   169 "--- 7 ---";

   170 val rls = ("Test_simplify");

   171 val (ct,_) = the (rewrite_set thy' false rls ct);

   172 if ct="3 + 2 * x" then () else error "new behaviour in test-example";

   174 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";

   175 val (ct,_) = the (rewrite_set thy' true rls ct);

   177 (*---

   178 val t = str2term "x ^^^ (2 - 1)";

   179 val SOME (t',_) = rewrite_set_ thy false Test_simplify t;

   180 term2str t';

   182 val t = str2term "-1 * 1";

   183 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;

   184 *)

   186 "----------- differentiate: me (*+ tacs input*) ---------";

   187 "----------- differentiate: me (*+ tacs input*) ---------";

   188 "----------- differentiate: me (*+ tacs input*) ---------";

   189 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",

   190 	   "differentiateFor x","derivative f_f'"];

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

   192   ("Diff",["derivative_of","function"],

   193    ["diff","diff_simpl"]);

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

   195 "--- s1 ---";

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

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

   198 "--- s2 ---";

   199 (*val nxt = ("Add_Given",

   200 Add_Given "functionTerm (d_d x (x ^^^ #2 + #3 * x + #4))");*)

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

   202 "--- s3 ---";

   203 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)

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

   205 "--- s4 ---";

   206 (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)

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

   208 "--- s5 ---";

   209 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)

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

   211 "--- s6 ---";

   212 (*val nxt = ("Specify_Problem",Specify_Problem pI');*)

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

   214 "--- s7 ---";

   215 (*val nxt = ("Specify_Method",Specify_Method mI');*)

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

   217 "--- s8 ---";

   218 (*val nxt = ("Apply_Method",Apply_Method mI');*)

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

   220 "--- 1 ---";

   221 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)

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

   223 "--- 2 ---";

   224 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)

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

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

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

   228 "--- 3 ---";

   229 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)

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

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

   232 "--- 4 ---";

   233 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_pow","")));*)

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

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

   236 "--- 5 ---";

   237 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)

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

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

   240 "--- 6 ---";

   241 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)

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

   243 if f2str f =  "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()

   244 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";

   245 "--- 7 ---";

   246 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)

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

   248 "--- 8 ---";

   249 (*val nxt = ("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)

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

   251 "--- 9 ---";

   252 (*val nxt = ("End_Proof'",End_Proof');*)

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

   254 if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then ()

   255 else error "diff.sml: new.behav. in me (*+ tacs input*)";

   256 (*if f = EmptyMout then () else error "new behaviour in + tacs input";

   257 meNEW extracts Form once more*)

   259 "----------- 1.5.02 me from script ----------------------";

   260 "----------- 1.5.02 me from script ----------------------";

   261 "----------- 1.5.02 me from script ----------------------";

   262 (*exp_Diff_No-1.xml*)

   263 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",

   264 	   "differentiateFor x","derivative f_f'"];

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

   266   ("Diff",["derivative_of","function"],

   267    ["diff","diff_simpl"]);

   268 (*val p = e_pos'; val c = [];

   269 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   270 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

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

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

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

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

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

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

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

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

   279 (*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)

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

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

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

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

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

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

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

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

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

   290 if nxt = ("End_Proof'",End_Proof') then ()

   291 else error "new behaviour in tests/differentiate, 1.5.02 me from script";

   293 "----------- primed id ----------------------------------";

   294 "----------- primed id ----------------------------------";

   295 "----------- primed id ----------------------------------";

   296 val f_ = str2term "f_f::bool";

   297 val f  = str2term "A = s * (a - s)";

   298 val v_ = str2term "v_v";

   299 val v  = str2term "s";

   300 val screxp0 = str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";

   301 atomty screxp0;

   303 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;

   304 term2str screxp1;

   305 atomty screxp1;

   307 val SOME (f'_,_) = rewrite_set_ (@{theory "Isac"}) false srls_diff screxp1;

   308 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()

   309 else error "diff.sml: diff.behav. in 'primed'";

   310 atomty f'_;

   312 val str = "Script DiffEqScr (f_f::bool) (v_v::real) =                         \

   313 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))           \

   314 \ in (((Try (Repeat (Rewrite frac_conv   False))) @@              \

   315  \ (Try (Repeat (Rewrite root_conv   False))) @@                  \

   316  \ (Try (Repeat (Rewrite realpow_pow False))) @@                  \

   317  \ (Repeat                                                        \

   318  \   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or \

   319  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \

   320  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or \

   321  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or \

   322  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or \

   323  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or \

   324  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or \

   325  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or \

   326  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or \

   327  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or \

   328  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or \

   329  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or \

   330  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or \

   331  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or \

   332  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt       False)) Or \

   333  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \

   334  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or \

   335  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or \

   336  \    (Repeat (Rewrite_Set             make_polynomial False)))) @@ \

   337  \ (Try (Repeat (Rewrite sym_frac_conv False))) @@              \

   338  \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"

   339 ;

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

   343 "----------- diff_conv, sym_diff_conv -------------------";

   344 "----------- diff_conv, sym_diff_conv -------------------";

   345 "----------- diff_conv, sym_diff_conv -------------------";

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

   347 val rls = diff_conv;

   349 val t = str2term "2/x^^^2";

   350 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   351 if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";

   353 val t = str2term "sqrt (x^^^3)";

   354 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   355 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";

   357 val t = str2term "2 / sqrt x^^^3";

   358 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   359 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";

   360 (* trace_rewrite := true;

   361    trace_rewrite := false;

   362    *)

   363 val rls = diff_sym_conv;

   365 val t = str2term "2 * x ^^^ -2";

   366 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   367 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";

   370 val t = str2term "x ^^^ (3 / 2)";

   371 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   372 if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";

   374 val t = str2term "2 * x ^^^ (-3 / 2)";

   375 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;

   376 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";

   379 (* trace_rewrite:=true;

   380    *)

   381 (* trace_rewrite:=false;

   382    *)

   383 (*@@@@*)

   385 "----------- autoCalculate differentiate_on_R 2/x^2 -----";

   386 "----------- autoCalculate differentiate_on_R 2/x^2 -----";

   387 "----------- autoCalculate differentiate_on_R 2/x^2 -----";

   388 states:=[];

   389 CalcTree

   390 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",

   391    (*"functionTerm ((x^3)^5)",*)

   392    "differentiateFor x", "derivative f_f'"],

   393   ("Isac", ["derivative_of","function"],

   394   ["diff","differentiate_on_R"]))];

   395 Iterator 1;

   396 moveActiveRoot 1;

   397 autoCalculate 1 CompleteCalc;

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

   399 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =

   400 			  "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()

   401 else error "diff.sml: differentiate_on_R 2/x^2 changed";

   403 "---------------------------------------------------------";

   404 states:=[];

   405 CalcTree

   406 [(["functionTerm (x^3 * x^5)",

   407    "differentiateFor x", "derivative f_f'"],

   408   ("Isac", ["derivative_of","function"],

   409   ["diff","differentiate_on_R"]))];

   410 Iterator 1;

   411 moveActiveRoot 1;

   412 (* trace_rewrite := true;

   413    trace_script := true;

   414    *)

   415 autoCalculate 1 CompleteCalc;

   416 (* trace_rewrite := false;

   417    trace_script := false;

   418    *)

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

   421 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =

   422 			 "8 * x ^^^ 7" then ()

   423 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";

   425 "----------- autoCalculate diff after_simplification ----";

   426 "----------- autoCalculate diff after_simplification ----";

   427 "----------- autoCalculate diff after_simplification ----";

   428 states:=[];

   429 CalcTree

   430 [(["functionTerm (x^3 * x^5)",

   431    "differentiateFor x", "derivative f_f'"],

   432   ("Isac", ["derivative_of","function"],

   433   ["diff","after_simplification"]))];

   434 Iterator 1;

   435 moveActiveRoot 1;

   436 (* trace_rewrite := true;

   437    trace_script := true;

   438    *)

   439 autoCalculate 1 CompleteCalc;

   440 (* trace_rewrite := false;

   441    trace_script := false;

   442    *)

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

   444 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =  "8 * x ^^^ 7"

   445 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";

   447 "--------------------------------------------------------";

   448 states:=[];

   449 CalcTree

   450 [(["functionTerm ((x^3)^5)",

   451    "differentiateFor x", "derivative f_f'"],

   452   ("Isac", ["derivative_of","function"],

   453   ["diff","after_simplification"]))];

   454 Iterator 1;

   455 moveActiveRoot 1;

   456 autoCalculate 1 CompleteCalc;

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

   458 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"

   459 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";

   461 "----------- autoCalculate differentiate_equality -------";

   462 "----------- autoCalculate differentiate_equality -------";

   463 "----------- autoCalculate differentiate_equality -------";

   464 states:=[];

   465 CalcTree

   466 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],

   467   ("Isac", ["named","derivative_of","function"],

   468   ["diff","differentiate_equality"]))];

   469 Iterator 1;

   470 moveActiveRoot 1;

   471 autoCalculate 1 CompleteCalc;

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

   474 "----------- tests for examples -------------------------";

   475 "----------- tests for examples -------------------------";

   476 "----------- tests for examples -------------------------";

   477 "----- parse errors";

   478 (*str2term "F  =  sqrt( y^^^2 - O) * (z + O^^^2)";

   479 str2term "O";

   480 str2term "OO"; ---errors*)

   481 str2term "OOO";

   483 "----- thm 'diff_prod_const'";

   484 val subs = [(str2term "bdv", str2term "l")];

   485 val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))";

   487 "------------inform for x^2+x+1 -------------------------";

   488 "------------inform for x^2+x+1 -------------------------";

   489 "------------inform for x^2+x+1 -------------------------";

   490 states:=[];

   491 CalcTree

   492 [(["functionTerm (x^2 + x + 1)",

   493    "differentiateFor x", "derivative f_f'"],

   494   ("Isac", ["derivative_of","function"],

   495   ["diff","differentiate_on_R"]))];

   496 Iterator 1;

   497 moveActiveRoot 1;

   498 autoCalculate 1 CompleteCalcHead;

   499 autoCalculate 1 (Step 1);

   500 autoCalculate 1 (Step 1);

   501 autoCalculate 1 (Step 1);

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

   503 appendFormula 1 "2*x + d_d x x + d_d x 1";

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

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

   506 else error  "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 02 Sep 2013 16:16:08 +0200
changeset 52101	c3f399ce32af
parent 48790	98df8f6dc3f9
child 52142	e7febad0c988
permissions	-rw-r--r--