(* Title: test/Tools/isac/Knowledge/diff.sml

   Author: Walther Neuper

   Use is subject to license terms.

*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val thy = @{theory "Diff"};

val ctxt = Proof_Context.init_global thy;

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

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

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

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

	   Where =[],

	   Find  =["derivative f_f'"],

	   With  =[],

	   Relate=[]}:string model;

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

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

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

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

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

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

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

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

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

val ctxt = Proof_Context.init_global @{theory};

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

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

case rewrite_set_ ctxt false erls_diff t of

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

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

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

case rewrite_set_ ctxt false erls_diff t of

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

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

val thm = @{thm diff_const};

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

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

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

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

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

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

val thy = @{theory "Diff"};

val ctxt = Proof_Context.init_global thy;

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

rewrite_set_ ctxt false erls_diff ct;

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

val thm = @{thm diff_quot};

val SOME (ctt,_) =

    (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);

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

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

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

val thy = @{theory "Diff"};

val ctxt = Proof_Context.init_global thy;

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

"--- 1 ---";

val thm = @{thm "diff_sum"};

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

"--- 2 ---";

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

"--- 3 ---";

val thm = @{thm "diff_prod_const"};

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

"--- 4 ---";

val thm = @{thm "diff_pow"};

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

"--- 5 ---";

val thm = @{thm "diff_const"};

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

"--- 6 ---";

val thm = @{thm "diff_var"};

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

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

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

"--- 7 ---";

"--- 7 ---";

val rls = Test_simplify;

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

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

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

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

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

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

val fmz = ["functionTerm (x \<up> 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) = Test_Code.init_calc @{context} [(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 \<up> #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 \<up> (2 - 1) + 3 * 1 + 0" then () 

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

"--- 7 ---";

(*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 f2str f = "3 + 2 * x"

  then case nxt of End_Proof' => ()

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

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

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

"----------- 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 \<up> 2 + 3 * x + 4)", 

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

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

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

   ["diff", "diff_simpl"]);

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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;

case nxt of End_Proof' => ()

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

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

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

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

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

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

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

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

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

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

TermC.atom_trace_detail @{context} screxp0;

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

UnparseC.term screxp1;

TermC.atom_trace_detail @{context} screxp1;

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

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

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

TermC.atom_trace_detail @{context} f'_;

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

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

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

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

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

 \ (Repeat                                                        \

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

;

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

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

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

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

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

val rls = diff_conv;

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

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

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

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

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

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

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

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

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

val rls = diff_sym_conv;

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

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

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

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

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

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

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

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

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

   LItool.trace_on := false;

   *)

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

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

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

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

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

Iterator 1;

moveActiveRoot 1;

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

   LItool.trace_on := true;

   *)

autoCalculate 1 CompleteCalc;

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

   LItool.trace_on := false;

   *)

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

TermC.parse_test @{context} "O";

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

TermC.parse_test @{context} "OOO";

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

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

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

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

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

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

States.reset ();

CalcTree @{context}

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

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Steps 1);

autoCalculate 1 (Steps 1);

autoCalculate 1 (Steps 1);

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

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

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

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

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