walther@60330: (* Title: test/Tools/isac/Knowledge/diff.sml
walther@60330:    Author: Walther Neuper
walther@60330:    Use is subject to license terms.
neuper@37906: *)
walther@60330: "-----------------------------------------------------------------------------------------------";
walther@60330: "-----------------------------------------------------------------------------------------------";
walther@60330: "table of contents -----------------------------------------------------------------------------";
walther@60330: "-----------------------------------------------------------------------------------------------";
neuper@38081: "----------- problemtype --------------------------------";
neuper@38081: "----------- for correction of diff_const ---------------";
neuper@38081: "----------- for correction of diff_quot ----------------";
neuper@38081: "----------- differentiate by rewrite -------------------";
neuper@38081: "----------- differentiate: me (*+ tacs input*) ---------";
neuper@38081: "----------- 1.5.02 me from script ----------------------";
neuper@38081: "----------- primed id ----------------------------------";
neuper@38081: "----------- diff_conv, sym_diff_conv -------------------";
walther@60242: "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
wneuper@59248: "----------- autoCalculate diff after_simplification ----";
wneuper@59248: "----------- autoCalculate differentiate_equality -------";
neuper@38081: "----------- tests for examples -------------------------";
walther@60242: "------------inform for x \<up> 2+x+1 -------------------------";
neuper@38081: "--------------------------------------------------------";
neuper@38081: "--------------------------------------------------------";
neuper@38081: "--------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@41929: val thy = @{theory "Diff"};
Walther@60424: val ctxt = Proof_Context.init_global thy;
neuper@37906: 
neuper@38081: "----------- problemtype --------------------------------";
neuper@38081: "----------- problemtype --------------------------------";
neuper@38081: "----------- problemtype --------------------------------";
neuper@37994: val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
neuper@37906: 	   Where =[],
neuper@37994: 	   Find  =["derivative f_f'"],
neuper@37906: 	   With  =[],
Walther@60586: 	   Relate=[]}:string model;
Walther@60424: val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt;
neuper@37906: 
walther@60242: val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))", 
walther@59997: 	   "differentiateFor x", "derivative f_f'"];
Walther@60424: val chkorg = map (TermC.parseNEW' ctxt) org;
neuper@37906: 
Walther@60559: Problem.from_store @{context} ["derivative_of", "function"];
Walther@60559: MethodC.from_store ctxt ["diff", "differentiate_on_R"];
neuper@37906: 
neuper@38081: "----------- for correction of diff_const ---------------";
neuper@38081: "----------- for correction of diff_const ---------------";
neuper@38081: "----------- for correction of diff_const ---------------";
Walther@60500: val ctxt = Proof_Context.init_global @{theory};
Walther@60586: (*re-evaluate this file, otherwise > *** ME_Isa: 'asm_rls' not known*)
Walther@60424: val t = TermC.parseNEW' ctxt "Not (x =!= a)";
Walther@60500: case rewrite_set_ ctxt false erls_diff t of
wenzelm@60309:   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
wneuper@59384: | _ => error "rewrite_set_  Not (x =!= a)  changed";
neuper@37906: 
Walther@60424: val t = TermC.parseNEW' ctxt "2 is_num";
Walther@60500: case rewrite_set_ ctxt false erls_diff t of
wenzelm@60309:   SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
walther@60387: | _ => error "rewrite_set_   2 is_num   changed";
neuper@37906: 
walther@59965: val thm = @{thm diff_const};
Walther@60424: val ct = TermC.parseNEW' ctxt "d_d x x";
walther@59656: val subst = [(@{term "bdv::real"}, @{term "x::real"})];
Walther@60500: val NONE = (rewrite_inst_ ctxt tless_true erls_diff false subst thm ct);
neuper@37906: 
neuper@38081: "----------- for correction of diff_quot ----------------";
neuper@38081: "----------- for correction of diff_quot ----------------";
neuper@38081: "----------- for correction of diff_quot ----------------";
wneuper@59384: val thy = @{theory "Diff"};
Walther@60500: val ctxt = Proof_Context.init_global thy;
Walther@60424: val ct = TermC.parseNEW' ctxt "Not (x = 0)";
Walther@60500: rewrite_set_ ctxt false erls_diff ct;
neuper@37906: 
Walther@60424: val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))";
wneuper@59384: val thm = @{thm diff_quot};
neuper@37926: val SOME (ctt,_) =
Walther@60500:     (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: 
neuper@38081: "----------- differentiate by rewrite -------------------";
neuper@38081: "----------- differentiate by rewrite -------------------";
neuper@38081: "----------- differentiate by rewrite -------------------";
wneuper@59384: val thy = @{theory "Diff"};
Walther@60500: val ctxt = Proof_Context.init_global thy;
Walther@60424: val ct = TermC.parseNEW' ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
neuper@37906: "--- 1 ---";
wneuper@59384: val thm = @{thm "diff_sum"};
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: "--- 2 ---";
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: "--- 3 ---";
wneuper@59384: val thm = @{thm "diff_prod_const"};
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: "--- 4 ---";
wneuper@59384: val thm = @{thm "diff_pow"};
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: "--- 5 ---";
wneuper@59384: val thm = @{thm "diff_const"};
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
neuper@37906: "--- 6 ---";
wneuper@59384: val thm = @{thm "diff_var"};
Walther@60500: val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
walther@60242: if UnparseC.term ct = "2 * x \<up> (2 - 1) + 3 * 1 + 0" then ()
neuper@38031: else error "diff.sml diff.behav. in rewrite 1";
neuper@37906: "--- 7 ---";
wneuper@59384: "--- 7 ---";
wneuper@59384: val rls = Test_simplify;
Walther@60424: val ct = TermC.parseNEW' ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
Walther@60500: val (ct, _) = the (rewrite_set_ ctxt true rls ct);
walther@59868: if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
neuper@37906: 
neuper@38081: "----------- differentiate: me (*+ tacs input*) ---------";
neuper@38081: "----------- differentiate: me (*+ tacs input*) ---------";
neuper@38081: "----------- differentiate: me (*+ tacs input*) ---------";
walther@60242: val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)", 
walther@59997: 	   "differentiateFor x", "derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
walther@59997:   ("Diff",["derivative_of", "function"],
walther@59997:    ["diff", "diff_simpl"]);
neuper@37906: val p = e_pos'; val c = []; 
neuper@37906: "--- s1 ---";
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s2 ---";
neuper@37906: (*val nxt = ("Add_Given",
walther@60242: Add_Given "functionTerm (d_d x (x \<up> #2 + #3 * x + #4))");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s3 ---";
neuper@37906: (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s4 ---";
neuper@37994: (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s5 ---";
neuper@37906: (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s6 ---";
neuper@37906: (*val nxt = ("Specify_Problem",Specify_Problem pI');*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s7 ---";
neuper@37906: (*val nxt = ("Specify_Method",Specify_Method mI');*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s8 ---";
neuper@37906: (*val nxt = ("Apply_Method",Apply_Method mI');*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 1 ---";
walther@59997: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 2 ---";
walther@59997: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum", "")));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
neuper@37906: "--- 3 ---";
wneuper@59497: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
neuper@37906: "--- 4 ---";
walther@59997: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow", "")));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
neuper@37906: "--- 5 ---";
wneuper@59497: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
neuper@37906: "--- 6 ---";
walther@59997: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var", "")));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
walther@60242: if f2str f =  "2 * x \<up> (2 - 1) + 3 * 1 + 0" then () 
walther@60242: else error "diff.sml: diff.behav. in d_d x \<up> 2 + 3 * x + 4";
neuper@37906: "--- 7 ---";
neuper@37906: (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 8 ---";
walther@59997: (*val nxt = ("Check_Postcond",Check_Postcond ("Diff", "differentiate_on_R"));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 9 ---";
neuper@37906: (*val nxt = ("End_Proof'",End_Proof');*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@59253: if f2str f = "3 + 2 * x"
walther@59749:   then case nxt of End_Proof' => ()
wneuper@59253:   | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
wneuper@59253: else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
walther@59814: (*if f = EmptyMout then () else error "new behaviour in + tacs input"*)
neuper@37906: 
neuper@38081: "----------- 1.5.02 me from script ----------------------";
neuper@38081: "----------- 1.5.02 me from script ----------------------";
neuper@38081: "----------- 1.5.02 me from script ----------------------";
walther@60329: (*exp_Diff_No- 1.xml*)
walther@60242: val fmz = ["functionTerm (x \<up> 2 + 3 * x + 4)", 
walther@59997: 	   "differentiateFor x", "derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
walther@59997:   ("Diff",["derivative_of", "function"],
walther@59997:    ["diff", "diff_simpl"]);
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59997: (*nxt = ("Apply_Method",Apply_Method ("Diff", "differentiate_on_R*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@59749: case nxt of End_Proof' => ()
wneuper@59253: | _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
neuper@37906: 
neuper@38081: "----------- primed id ----------------------------------";
neuper@38081: "----------- primed id ----------------------------------";
neuper@38081: "----------- primed id ----------------------------------";
Walther@60500: val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
Walther@60565: val f_ = TermC.parse_test @{context} "f_f::bool";
Walther@60565: val f  = TermC.parse_test @{context} "A = s * (a - s)";
Walther@60565: val v_ = TermC.parse_test @{context} "v_v";
Walther@60565: val v  = TermC.parse_test @{context} "s";
Walther@60565: val screxp0 = TermC.parse_test @{context} "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
Walther@60650: TermC.atom_trace_detail @{context} screxp0;
neuper@37906: 
neuper@38081: val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
walther@59868: UnparseC.term screxp1;
Walther@60650: TermC.atom_trace_detail @{context} screxp1;
neuper@37906: 
Walther@60500: val SOME (f'_,_) = rewrite_set_ ctxt false srls_diff screxp1; 
walther@59868: if UnparseC.term f'_= "Take (A' = d_d s (s * (a - s)))" then ()
neuper@38031: else error "diff.sml: diff.behav. in 'primed'";
Walther@60650: TermC.atom_trace_detail @{context} f'_;
neuper@37906: 
wneuper@59585: val str = "Program DiffEqScr (f_f::bool) (v_v::real) =                         \
neuper@38081: \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))           \
walther@59637: \ in (((Try (Repeat (Rewrite frac_conv))) #>              \
walther@59637:  \ (Try (Repeat (Rewrite root_conv))) #>                  \
walther@59637:  \ (Try (Repeat (Rewrite realpow_pow))) #>                  \
neuper@37906:  \ (Repeat                                                        \
walther@59635:  \   ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum        )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod       )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot       )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin        )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain  )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos        )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain  )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow        )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain  )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln         )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain   )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp        )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain  )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt       )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const      )) Or \
walther@59635:  \    (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var        )) Or \
walther@59637:  \    (Repeat (Rewrite_Set             make_polynomial)))) #> \
walther@59637:  \ (Try (Repeat (Rewrite sym_frac_conv))) #>              \
walther@59635:  \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
neuper@37906: ;
Walther@60424: val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
neuper@37906: 
neuper@37906: 
neuper@38081: "----------- diff_conv, sym_diff_conv -------------------";
neuper@38081: "----------- diff_conv, sym_diff_conv -------------------";
neuper@38081: "----------- diff_conv, sym_diff_conv -------------------";
Walther@60565: val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];
neuper@37906: val rls = diff_conv;
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "2/x \<up> 2"; 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60329: if UnparseC.term t = "2 * x \<up> - 2" then () else error "diff.sml 1/x";
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "sqrt (x \<up> 3)";
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60242: if UnparseC.term t = "x \<up> (3 / 2)" then () else error "diff.sml x \<up> 1/2";
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "2 / sqrt x \<up> 3";
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60341: if UnparseC.term t = "2 * x \<up> (- 3 / 2)" then () else error "diff.sml x \<up> - 1/2";
walther@60341: 
walther@60341: val rls = diff_sym_conv;
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "2 * x \<up> - 2";
Walther@60500: val SOME (t, _) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60242: if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "x \<up> (3 / 2)";
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60341: if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "2 * x \<up> (-3 / 2)";
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt false subs rls t; UnparseC.term t;
walther@60329: if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
neuper@37906: 
neuper@37906: 
walther@60242: "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
walther@60242: "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
walther@60242: "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@60242: [(["functionTerm (x \<up> 2 + x+ 1/x + 2/x \<up> 2)",
walther@60242:    (*"functionTerm ((x \<up> 3) \<up> 5)",*)
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
walther@59997:   ("Isac_Knowledge", ["derivative_of", "function"],
walther@59997:   ["diff", "differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59868: if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = 
walther@60341: 			  "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()
walther@60242: else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
neuper@37906: 
neuper@38081: "---------------------------------------------------------";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@60242: [(["functionTerm (x \<up> 3 * x  \<up>  5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
walther@59997:   ("Isac_Knowledge", ["derivative_of", "function"],
walther@59997:   ["diff", "differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
walther@59627: autoCalculate 1 CompleteCalc;
walther@60330: (* Rewrite.trace_on := false; (*true false*)
walther@59901:    LItool.trace_on := false;
neuper@37906:    *)
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
neuper@37906: 
walther@59868: if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = 
walther@60242: 			 "8 * x \<up> 7" then () 
walther@60242: else error "diff.sml: differentiate_on_R (x \<up> 3 * x \<up> 5) changed";
neuper@37906: 
wneuper@59248: "----------- autoCalculate diff after_simplification ----";
wneuper@59248: "----------- autoCalculate diff after_simplification ----";
wneuper@59248: "----------- autoCalculate diff after_simplification ----";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@60242: [(["functionTerm (x \<up> 3 * x \<up> 5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
walther@59997:   ("Isac_Knowledge", ["derivative_of", "function"],
walther@59997:   ["diff", "after_simplification"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
walther@60330: (* Rewrite.trace_on := false; (*true false*)
walther@59901:    LItool.trace_on := true;
neuper@37906:    *)
wneuper@59248: autoCalculate 1 CompleteCalc;
walther@60341: (* Rewrite.trace_on := false; (*true false*)
walther@59901:    LItool.trace_on := false;
neuper@37906:    *)
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@60242: if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =  "8 * x \<up> 7"
neuper@38031: then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
neuper@37906: 
neuper@38081: "--------------------------------------------------------";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@60242: [(["functionTerm ((x \<up> 3) \<up> 5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
walther@59997:   ("Isac_Knowledge", ["derivative_of", "function"],
walther@59997:   ["diff", "after_simplification"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@60242: if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
neuper@38031: then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
neuper@37906: 
wneuper@59248: "----------- autoCalculate differentiate_equality -------";
wneuper@59248: "----------- autoCalculate differentiate_equality -------";
wneuper@59248: "----------- autoCalculate differentiate_equality -------";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
neuper@42393: [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"], 
walther@59997:   ("Isac_Knowledge", ["named", "derivative_of", "function"],
walther@59997:   ["diff", "differentiate_equality"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalc;
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
neuper@37906: 
neuper@38081: "----------- tests for examples -------------------------";
neuper@38081: "----------- tests for examples -------------------------";
neuper@38081: "----------- tests for examples -------------------------";
walther@60230: "----- TermC.parse errors";
Walther@60565: (*TermC.parse_test @{context} "F  =  sqrt( y \<up> 2 - O) * (z + O \<up> 2)";
Walther@60565: TermC.parse_test @{context} "O";
Walther@60565: TermC.parse_test @{context} "OO"; ---errors*)
Walther@60565: TermC.parse_test @{context} "OOO";
neuper@37906: 
neuper@37906: "----- thm 'diff_prod_const'";
Walther@60565: val subs = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "l")];
Walther@60565: val f = TermC.parse_test @{context} "G' = d_d l (l * sqrt (7 * s \<up> 2 - l \<up> 2))";
neuper@37906: 
walther@60242: "------------inform for x \<up> 2+x+1 -------------------------";
walther@60242: "------------inform for x \<up> 2+x+1 -------------------------";
walther@60242: "------------inform for x \<up> 2+x+1 -------------------------";
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@60242: [(["functionTerm (x \<up> 2 + x + 1)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
walther@59997:   ("Isac_Knowledge", ["derivative_of", "function"],
walther@59997:   ["diff", "differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
wneuper@59248: autoCalculate 1 CompleteCalcHead;
walther@59747: autoCalculate 1 (Steps 1);
walther@59747: autoCalculate 1 (Steps 1);
walther@59747: autoCalculate 1 (Steps 1);
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
wneuper@59123: appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
neuper@37906: if existpt' ([3], Res) pt then ()
walther@60242: else error  "diff.sml: inform d_d x (x \<up> 2 + x + 1) doesnt work";
neuper@38081: