(* 

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

use"diff.sml";

*)

"-----------------------------------------------------------------";

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

"-----------------------------------------------------------------";

" _________________ problemtype _________________ ";

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

" _________________ for correction of diff_quot  _________________ ";

" _________________ differentiate by rewrite _________________ ";

" ______________ differentiate: me (*+ tacs input*) ______________ ";

" ________________ differentiate stdin: student active________________ ";

" _________________ differentiate stdin: tutor active_________________ ";

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

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

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

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

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

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

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

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

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

val thy = Diff.thy;

" _________________ problemtype _________________ ";

" _________________ problemtype _________________ ";

" _________________ problemtype _________________ ";

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

	   Where =[],

	   Find  =["derivative f_f'"],

	   With  =[],

	   Relate=[]}:string ppc;

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

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

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

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

get_pbt ["derivative_of","function"];

get_met ["diff","differentiate_on_R"];

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

ruleset' := 

overwritelthy thy

    (!ruleset',

     [("erls",

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

	    erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)

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

		     Thm ("real_le_refl",num_str @{thm real_le_refl}}),

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

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

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

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

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

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

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

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

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

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

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

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

		     Calc ("op +",eval_binop "#add_"),

		     Calc ("op *",eval_binop "#mult_"),

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

		     Calc ("op <",eval_equ "#less_"),

		     Calc ("op <=",eval_equ "#less_equal_"),

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

	    scr = Script ((term_of o the o (parse thy)) 

			      "empty_script")

	    }:rls

	      )]);

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

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

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

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

val thy' = "Diff";

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

rewrite_set thy' false "erls" ct;

val ct = "2 is_const";

rewrite_set thy' false "erls" ct;

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

val ct = "d_d x x";

val NONE =

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

val ct = "d_d x 2";

val SOME (ctt,_) =

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

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

trace_rewrite := true;

val ct = "d_d s a";

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

(*got: NONE instead SOME*)

eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls");

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

val SOME (ctt,_) =

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

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

trace_rewrite := false;

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

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

val ct = "d_d x x";

val SOME (ctt,_) =

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

val ct = "d_d x a";

val NONE =

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

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

val NONE =

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

" _________________ for correction of diff_quot  _________________ ";

" _________________ for correction of diff_quot  _________________ ";

" _________________ for correction of diff_quot  _________________ ";

val thy' = "Diff";

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

rewrite_set thy' false "erls" ct;

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

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

val SOME (ctt,_) =

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

" _________________ differentiate by rewrite _________________ ";

" _________________ differentiate by rewrite _________________ ";

" _________________ differentiate by rewrite _________________ ";

val thy' = "Diff";

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

"--- 1 ---";

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

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

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

"--- 2 ---";

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

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

"--- 3 ---";

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

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

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

"--- 4 ---";

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

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

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

"--- 5 ---";

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

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

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

"--- 6 ---";

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

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

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

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

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

"--- 7 ---";

val rls = ("Test_simplify");

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

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

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

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

(*---

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

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

term2str t';

val t = str2term "-1 * 1";

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

*)

" ______________ differentiate: me (*+ tacs input*) ______________ ";

" ______________ differentiate: me (*+ tacs input*) ______________ ";

" ______________ differentiate: me (*+ tacs input*) ______________ ";

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

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

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

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

   ["diff","diff_simpl"]);

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

"--- s1 ---";

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

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

"--- s2 ---";

(*val nxt = ("Add_Given",

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

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

"--- s3 ---";

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

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

"--- s4 ---";

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

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

"--- s5 ---";

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

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

"--- s6 ---";

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

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

"--- s7 ---";

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

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

"--- s8 ---";

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

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

"--- 1 ---";

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

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

"--- 2 ---";

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

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

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

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

"--- 3 ---";

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

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

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

"--- 4 ---";

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

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

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

"--- 5 ---";

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

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

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

"--- 6 ---";

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

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

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

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

"--- 7 ---";

(*------------------------------11.3.03--------------------

 trace_rewrite:=true;

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

 val Form' (FormKF (_,_,_,_,res)) = f;

 trace_rewrite:=false;

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

 val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct;

 trace_rewrite:=true;

 val t = str2term ct; 

 term2str t;

 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;

 term2str t';

 trace_rewrite:=false;

 val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';

 term2str t'';

 val thm = num_str @{thm realpow_eq_oneI;

 case string_of_thm thm of

 val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m;

 term2str ff; term2str ff';

--------------------------------11.3.03--------------------*)

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

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

"--- 8 ---";

(*val nxt =

("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)

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

"--- 9 ---";

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

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

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

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

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

meNEW extracts Form once more*)

(*---------------- 1.5.02 -----------------------------------------

" _________________ script-eval corrected _________________ ";

" _________________ script-eval corrected _________________ ";

" _________________ script-eval corrected _________________ ";

val scr = Script (((inst_abs (assoc_thy "Test")) o 

	   term_of o the o (parse Diff.thy))

  "Script Differentiate (f_f::real) (v_v::real) =                                 \

   \(let f_ = Try (Repeat (Rewrite frac_conv False f_));                        \

   \     f_ = Try (Repeat (Rewrite root_conv False f_));                        \

   \     f_ = Repeat                                                            \

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

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

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

   \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       False f_)) Or \

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

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

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

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

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

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

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

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

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

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

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

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

   \             (Repeat (Rewrite_Set             Test_simplify False f_)));  \

   \     f_ = Try (Repeat (Rewrite sym_frac_conv False f_))                     \

   \ in       Try (Repeat (Rewrite sym_root_conv False f_)))");

val d = e_rls;

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

  ("Diff",e_pblID,

   ("Diff","differentiate_on_R"));

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

val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));

val (p,_,_,_,_,pt) = me (mI,m) p c  EmptyPtree;

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

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

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

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

val p = ([1],Frm):pos';

val parseee = (term_of o the o (parse Diff.thy));

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

val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];

val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),

	  ([],(User', [],                [],        empty, empty,Sundef))]:ets;

val l0 = [];

" --------------- 1. ---------------------------------------------";

val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));

val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0;

(*("diff_sum","")*)

val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = 

  locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0;

val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];

" --------------- 2. ---------------------------------------------";

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));

val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1;

(*("diff_sum","")*)

val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = 

  locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1;

val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];

" --------------- 3. ---------------------------------------------";

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));

val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2;

(*("diff_prod_const","")*)

val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = 

  locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2;

val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];

" --------------- 4. ---------------------------------------------";

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));

val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3;

(*("diff_pow","")*)

val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = 

    locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3;

val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];

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

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));

val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4;

(*("diff_const","")*)

val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] = 

    locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4;

val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];

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

val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));

val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5;

(*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)

val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] = 

    locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5;

val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];

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

val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");

 ---------------- 1.5.02 -----------------------------------------*)

" ________________ differentiate stdin: student active________________ ";

" ________________ differentiate stdin: student active________________ ";

" ________________ differentiate stdin: student active________________ ";

(*

proofs:= []; dials:=([],[],[]); 

StdinSML 0 0 0 0 New_User;

set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)

StdinSML 1 0 0 0 New_Proof;

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

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

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

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

   ["diff","differentiate_on_R"]);

*)

" _________________ differentiate stdin: tutor active_________________ ";

" _________________ differentiate stdin: tutor active_________________ ";

" _________________ differentiate stdin: tutor active_________________ ";

(*proofs:= []; dials:=([],[],[]); 

StdinSML 0 0 0 0 New_User;

set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)

StdinSML 1 0 0 0 New_Proof;

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

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

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

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

   ["diff","differentiate_on_R"]);

*)

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

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

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

(*exp_Diff_No-1.xml*)

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

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

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

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

   ["diff","diff_simpl"]);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val f_ = str2term "f_f::bool";

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

val v_v = str2term "v_";

val v  = str2term "s";

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

atomty screxp0;

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

term2str screxp1;

atomty screxp1;

val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1; 

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

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

atomty f'_;

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

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

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

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

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

 \ (Repeat                                                        \

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

;

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

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

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

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

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

val rls = diff_conv;

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

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

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

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

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

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

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

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

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

(* trace_rewrite := true;

   trace_rewrite := false;

   *)

val rls = diff_sym_conv; 

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

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

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

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

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

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

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

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

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

(* trace_rewrite:=true;

   *)

(* trace_rewrite:=false;

   *)

(*@@@@*)

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

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

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

states:=[];

CalcTree

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

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

"-----------------------------------------------------------------";

states:=[];

CalcTree

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

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

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

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

Iterator 1;

moveActiveRoot 1;

(* trace_rewrite := true;

   trace_script := true;

   *)

autoCalculate 1 CompleteCalc;

(* trace_rewrite := false;

   trace_script := false;

   *)

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

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

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

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

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

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

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

states:=[];

CalcTree

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

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

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

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

Iterator 1;

moveActiveRoot 1;

(* trace_rewrite := true;

   trace_script := true;

   *)

autoCalculate 1 CompleteCalc;

(* trace_rewrite := false;

   trace_script := false;

   *)

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

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

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

"-----------------------------------------------------------------";

states:=[];

CalcTree

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

states:=[];

CalcTree

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

"----- parse errors";

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

str2term "O";*)

str2term "OO";

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

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

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

(*

trace_rewrite := true;

rewrite_inst_ Isac.thy tless_true erls_diff true subs diff_prod_const f;

trace_rewrite := false;

*)

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

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

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

states:=[];

CalcTree

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);

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

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

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

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

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