Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/diff.sml
author wneuper <Walther.Neuper@jku.at>
Wed, 11 Jan 2023 11:38:01 +0100
changeset 60650 06ec8abfd3bc
parent 60586 007ef64dbb08
child 60660 c4b24621077e
permissions -rw-r--r--
eliminate use of Thy_Info 12: TermC partially 
     1 (* Title: test/Tools/isac/Knowledge/diff.sml

     2    Author: Walther Neuper

     3    Use is subject to license terms.

     4 *)

     5 "-----------------------------------------------------------------------------------------------";

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

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

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

     9 "----------- problemtype --------------------------------";

    10 "----------- for correction of diff_const ---------------";

    11 "----------- for correction of diff_quot ----------------";

    12 "----------- differentiate by rewrite -------------------";

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

    14 "----------- 1.5.02 me from script ----------------------";

    15 "----------- primed id ----------------------------------";

    16 "----------- diff_conv, sym_diff_conv -------------------";

    17 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";

    18 "----------- autoCalculate diff after_simplification ----";

    19 "----------- autoCalculate differentiate_equality -------";

    20 "----------- tests for examples -------------------------";

    21 "------------inform for x \<up> 2+x+1 -------------------------";

    22 "--------------------------------------------------------";

    23 "--------------------------------------------------------";

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

    25 

    26 

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

    28 val ctxt = Proof_Context.init_global thy;

    29 

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

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

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

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

    34 	   Where =[],

    35 	   Find  =["derivative f_f'"],

    36 	   With  =[],

    37 	   Relate=[]}:string model;

    38 val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt;

    39 

    40 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", 

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

    42 val chkorg = map (TermC.parseNEW' ctxt) org;

    43 

    44 Problem.from_store @{context} ["derivative_of", "function"];

    45 MethodC.from_store ctxt ["diff", "differentiate_on_R"];

    46 

    47 "----------- for correction of diff_const ---------------";

    48 "----------- for correction of diff_const ---------------";

    49 "----------- for correction of diff_const ---------------";

    50 val ctxt = Proof_Context.init_global @{theory};

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

    52 val t = TermC.parseNEW' ctxt "Not (x =!= a)";

    53 case rewrite_set_ ctxt false erls_diff t of

    54   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()

    55 | _ => error "rewrite_set_  Not (x =!= a)  changed";

    56 

    57 val t = TermC.parseNEW' ctxt "2 is_num";

    58 case rewrite_set_ ctxt false erls_diff t of

    59   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()

    60 | _ => error "rewrite_set_   2 is_num   changed";

    61 

    62 val thm = @{thm diff_const};

    63 val ct = TermC.parseNEW' ctxt "d_d x x";

    64 val subst = [(@{term "bdv::real"}, @{term "x::real"})];

    65 val NONE = (rewrite_inst_ ctxt tless_true erls_diff false subst thm ct);

    66 

    67 "----------- for correction of diff_quot ----------------";

    68 "----------- for correction of diff_quot ----------------";

    69 "----------- for correction of diff_quot ----------------";

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

    71 val ctxt = Proof_Context.init_global thy;

    72 val ct = TermC.parseNEW' ctxt "Not (x = 0)";

    73 rewrite_set_ ctxt false erls_diff ct;

    74 

    75 val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))";

    76 val thm = @{thm diff_quot};

    77 val SOME (ctt,_) =

    78     (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

    79 

    80 "----------- differentiate by rewrite -------------------";

    81 "----------- differentiate by rewrite -------------------";

    82 "----------- differentiate by rewrite -------------------";

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

    84 val ctxt = Proof_Context.init_global thy;

    85 val ct = TermC.parseNEW' ctxt "d_d x (x \<up> 2 + 3 * x + 4)";

    86 "--- 1 ---";

    87 val thm = @{thm "diff_sum"};

    88 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

    89 "--- 2 ---";

    90 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

    91 "--- 3 ---";

    92 val thm = @{thm "diff_prod_const"};

    93 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

    94 "--- 4 ---";

    95 val thm = @{thm "diff_pow"};

    96 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

    97 "--- 5 ---";

    98 val thm = @{thm "diff_const"};

    99 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

   100 "--- 6 ---";

   101 val thm = @{thm "diff_var"};

   102 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

   103 if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()

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

   105 "--- 7 ---";

   106 "--- 7 ---";

   107 val rls = Test_simplify;

   108 val ct = TermC.parseNEW' ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";

   109 val (ct, _) = the (rewrite_set_ ctxt true rls ct);

   110 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";

   111 

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

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

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

   115 val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)", 

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

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

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

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

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

   121 "--- s1 ---";

   122 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

   124 "--- s2 ---";

   125 (*val nxt = ("Add_Given",

   126 Add_Given "functionTerm (d_d x (x \<up> #2 + #3 * x + #4))");*)

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

   128 "--- s3 ---";

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

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

   131 "--- s4 ---";

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

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

   134 "--- s5 ---";

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

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

   137 "--- s6 ---";

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

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

   140 "--- s7 ---";

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

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

   143 "--- s8 ---";

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

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

   146 "--- 1 ---";

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

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

   149 "--- 2 ---";

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

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

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

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

   154 "--- 3 ---";

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

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

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

   158 "--- 4 ---";

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

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

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

   162 "--- 5 ---";

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

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

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

   166 "--- 6 ---";

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

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

   169 if f2str f =  "2 * x \<up> (2 - 1) + 3 * 1 + 0" then () 

   170 else error "diff.sml: diff.behav. in d_d x \<up> 2 + 3 * x + 4";

   171 "--- 7 ---";

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

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

   174 "--- 8 ---";

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

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

   177 "--- 9 ---";

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

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

   180 if f2str f = "3 + 2 * x"

   181   then case nxt of End_Proof' => ()

   182   | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"

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

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

   185 

   186 "----------- 1.5.02 me from script ----------------------";

   187 "----------- 1.5.02 me from script ----------------------";

   188 "----------- 1.5.02 me from script ----------------------";

   189 (*exp_Diff_No- 1.xml*)

   190 val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)", 

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

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

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

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

   195 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

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

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

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

   205 

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

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

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

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

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

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

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

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

   214 case nxt of End_Proof' => ()

   215 | _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";

   216 

   217 "----------- primed id ----------------------------------";

   218 "----------- primed id ----------------------------------";

   219 "----------- primed id ----------------------------------";

   220 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};

   221 val f_ = TermC.parse_test @{context} "f_f::bool";

   222 val f  = TermC.parse_test @{context} "A = s * (a - s)";

   223 val v_ = TermC.parse_test @{context} "v_v";

   224 val v  = TermC.parse_test @{context} "s";

   225 val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";

   226 TermC.atom_trace_detail @{context} screxp0;

   227 

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

   229 UnparseC.term screxp1;

   230 TermC.atom_trace_detail @{context} screxp1;

   231 

   232 val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; 

   233 if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()

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

   235 TermC.atom_trace_detail @{context} f'_;

   236 

   237 val str = "Program DiffEqScr (f_f::bool) (v_v::real) =                         \

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

   239 \ in (((Try (Repeat (Rewrite frac_conv))) #>              \

   240  \ (Try (Repeat (Rewrite root_conv))) #>                  \

   241  \ (Try (Repeat (Rewrite realpow_pow))) #>                  \

   242  \ (Repeat                                                        \

   243  \   ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum        )) Or \

   244  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \

   245  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod       )) Or \

   246  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot       )) Or \

   247  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin        )) Or \

   248  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain  )) Or \

   249  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos        )) Or \

   250  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain  )) Or \

   251  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow        )) Or \

   252  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain  )) Or \

   253  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln         )) Or \

   254  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain   )) Or \

   255  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp        )) Or \

   256  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain  )) Or \

   257  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt       )) Or \

   258  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \

   259  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const      )) Or \

   260  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var        )) Or \

   261  \    (Repeat (Rewrite_Set             make_polynomial)))) #> \

   262  \ (Try (Repeat (Rewrite sym_frac_conv))) #>              \

   263  \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"

   264 ;

   265 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;

   266 

   267 

   268 "----------- diff_conv, sym_diff_conv -------------------";

   269 "----------- diff_conv, sym_diff_conv -------------------";

   270 "----------- diff_conv, sym_diff_conv -------------------";

   271 val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];

   272 val rls = diff_conv;

   273 

   274 val t = TermC.parse_test @{context} "2/x \<up> 2"; 

   275 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   276 if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";

   277 

   278 val t = TermC.parse_test @{context} "sqrt (x \<up> 3)";

   279 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   280 if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";

   281 

   282 val t = TermC.parse_test @{context} "2 / sqrt x \<up> 3";

   283 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   284 if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";

   285 

   286 val rls = diff_sym_conv;

   287 

   288 val t = TermC.parse_test @{context} "2 * x \<up> - 2";

   289 val SOME (t, _) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   290 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";

   291 

   292 val t = TermC.parse_test @{context} "x \<up> (3 / 2)";

   293 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   294 if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";

   295 

   296 val t = TermC.parse_test @{context} "2 * x \<up> (-3 / 2)";

   297 val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;

   298 if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";

   299 

   300 

   301 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";

   302 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";

   303 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";

   304 States.reset ();

   305 CalcTree @{context}

   306 [(["functionTerm (x \<up> 2 + x+ 1/x + 2/x \<up> 2)",

   307    (*"functionTerm ((x \<up> 3) \<up> 5)",*)

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

   309   ("Isac_Knowledge", ["derivative_of", "function"],

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

   311 Iterator 1;

   312 moveActiveRoot 1;

   313 autoCalculate 1 CompleteCalc;

   314 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   315 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = 

   316 			  "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()

   317 else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";

   318 

   319 "---------------------------------------------------------";

   320 States.reset ();

   321 CalcTree @{context}

   322 [(["functionTerm (x \<up> 3 * x  \<up>  5)",

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

   324   ("Isac_Knowledge", ["derivative_of", "function"],

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

   326 Iterator 1;

   327 moveActiveRoot 1;

   328 autoCalculate 1 CompleteCalc;

   329 (* Rewrite.trace_on := false; (*true false*)

   330    LItool.trace_on := false;

   331    *)

   332 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   333 

   334 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = 

   335 			 "8 * x \<up> 7" then () 

   336 else error "diff.sml: differentiate_on_R (x \<up> 3 * x \<up> 5) changed";

   337 

   338 "----------- autoCalculate diff after_simplification ----";

   339 "----------- autoCalculate diff after_simplification ----";

   340 "----------- autoCalculate diff after_simplification ----";

   341 States.reset ();

   342 CalcTree @{context}

   343 [(["functionTerm (x \<up> 3 * x \<up> 5)",

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

   345   ("Isac_Knowledge", ["derivative_of", "function"],

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

   347 Iterator 1;

   348 moveActiveRoot 1;

   349 (* Rewrite.trace_on := false; (*true false*)

   350    LItool.trace_on := true;

   351    *)

   352 autoCalculate 1 CompleteCalc;

   353 (* Rewrite.trace_on := false; (*true false*)

   354    LItool.trace_on := false;

   355    *)

   356 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   357 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =  "8 * x \<up> 7"

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

   359 

   360 "--------------------------------------------------------";

   361 States.reset ();

   362 CalcTree @{context}

   363 [(["functionTerm ((x \<up> 3) \<up> 5)",

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

   365   ("Isac_Knowledge", ["derivative_of", "function"],

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

   367 Iterator 1;

   368 moveActiveRoot 1;

   369 autoCalculate 1 CompleteCalc;

   370 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   371 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"

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

   373 

   374 "----------- autoCalculate differentiate_equality -------";

   375 "----------- autoCalculate differentiate_equality -------";

   376 "----------- autoCalculate differentiate_equality -------";

   377 States.reset ();

   378 CalcTree @{context}

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

   380   ("Isac_Knowledge", ["named", "derivative_of", "function"],

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

   382 Iterator 1;

   383 moveActiveRoot 1;

   384 autoCalculate 1 CompleteCalc;

   385 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   386 

   387 "----------- tests for examples -------------------------";

   388 "----------- tests for examples -------------------------";

   389 "----------- tests for examples -------------------------";

   390 "----- TermC.parse errors";

   391 (*TermC.parse_test @{context} "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";

   392 TermC.parse_test @{context} "O";

   393 TermC.parse_test @{context} "OO"; ---errors*)

   394 TermC.parse_test @{context} "OOO";

   395 

   396 "----- thm 'diff_prod_const'";

   397 val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "l")];

   398 val f = TermC.parse_test @{context} "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";

   399 

   400 "------------inform for x \<up> 2+x+1 -------------------------";

   401 "------------inform for x \<up> 2+x+1 -------------------------";

   402 "------------inform for x \<up> 2+x+1 -------------------------";

   403 States.reset ();

   404 CalcTree @{context}

   405 [(["functionTerm (x \<up> 2 + x + 1)",

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

   407   ("Isac_Knowledge", ["derivative_of", "function"],

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

   409 Iterator 1;

   410 moveActiveRoot 1;

   411 autoCalculate 1 CompleteCalcHead;

   412 autoCalculate 1 (Steps 1);

   413 autoCalculate 1 (Steps 1);

   414 autoCalculate 1 (Steps 1);

   415 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

   416 appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);

   417 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

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

   419 else error  "diff.sml: inform d_d x (x \<up> 2 + x + 1) doesnt work";

   420
wneuper/isa