neuper@37906: (* 
neuper@37906: 
neuper@37906: use"../smltest/IsacKnowledge/diff.sml";
neuper@37906: use"diff.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: " _________________ problemtype _________________ ";
neuper@37906: "----------- for correction of diff_const ------------------------";
neuper@37906: " _________________ for correction of diff_quot  _________________ ";
neuper@37906: " _________________ differentiate by rewrite _________________ ";
neuper@37906: " ______________ differentiate: me (*+ tacs input*) ______________ ";
neuper@37906: " ________________ differentiate stdin: student active________________ ";
neuper@37906: " _________________ differentiate stdin: tutor active_________________ ";
neuper@37906: "---------------------1.5.02 me from script ---------------------";
neuper@37906: "----------- primed id -------------------------------------------";
neuper@37906: "----------- diff_conv, sym_diff_conv ----------------------------";
neuper@37906: "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
neuper@37906: "----------- autoCalculate diff after_simplification -------------";
neuper@37906: "----------- autoCalculate differentiate_equality ----------------";
neuper@37906: "----------- tests for examples ----------------------------------";
neuper@37906: "------------inform for x^2+x+1 ----------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: val thy = Diff.thy;
neuper@37906: 
neuper@37906: " _________________ problemtype _________________ ";
neuper@37906: " _________________ problemtype _________________ ";
neuper@37906: " _________________ problemtype _________________ ";
neuper@37994: val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
neuper@37906: 	   Where =[],
neuper@37994: 	   Find  =["derivative f_f'"],
neuper@37906: 	   With  =[],
neuper@37906: 	   Relate=[]}:string ppc;
neuper@37906: val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
neuper@37906: 
neuper@37906: val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", 
neuper@37994: 	   "differentiateFor x","derivative f_f'"];
neuper@37906: val chkorg = map (the o (parse Diff.thy)) org;
neuper@37906: 
neuper@37906: get_pbt ["derivative_of","function"];
neuper@37906: get_met ["diff","differentiate_on_R"];
neuper@37906: 
neuper@37906: (*erls should not be in ruleset'! Here only for tests*)
neuper@37906: ruleset' := 
neuper@37906: overwritelthy thy
neuper@37906:     (!ruleset',
neuper@37906:      [("erls",
neuper@37906:        Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI), 
neuper@37906: 	    erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
neuper@37969: 	    rules = [Thm ("refl",num_str @{thm refl}),
neuper@37969: 		     Thm ("real_le_refl",num_str @{thm real_le_refl}}),
neuper@37969: 		     Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
neuper@37969: 		     Thm ("not_true",num_str @{thm not_true}),
neuper@37969: 		     Thm ("not_false",num_str @{thm not_false}),
neuper@37969: 		     Thm ("and_true",num_str @{thm and_true}),
neuper@37969: 		     Thm ("and_false",num_str @{thm and_false}),
neuper@37969: 		     Thm ("or_true",num_str @{thm or_true}),
neuper@37969: 		     Thm ("or_false",num_str @{thm or_false}),
neuper@37969: 		     Thm ("and_commute",num_str @{and_commute}),
neuper@37969: 		     Thm ("or_commute",num_str @{or_commute}),
neuper@37906: 		     
neuper@37906: 		     Calc ("Atools.is'_const",eval_const "#is_const_"),
neuper@37906: 		     Calc ("Atools.occurs'_in", eval_occurs_in ""),
neuper@37906: 		     Calc ("Tools.matches",eval_matches ""),
neuper@37906: 		     
neuper@38014: 		     Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@37906: 		     Calc ("op *",eval_binop "#mult_"),
neuper@37906: 		     Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37906: 		     
neuper@37906: 		     Calc ("op <",eval_equ "#less_"),
neuper@37906: 		     Calc ("op <=",eval_equ "#less_equal_"),
neuper@37906: 		     
neuper@37906: 		     Calc ("Atools.ident",eval_ident "#ident_")],
neuper@37906: 	    scr = Script ((term_of o the o (parse thy)) 
neuper@37906: 			      "empty_script")
neuper@37906: 	    }:rls
neuper@37906: 	      )]);
neuper@37906:     
neuper@37906: "----------- for correction of diff_const ------------------------";
neuper@37906: "----------- for correction of diff_const ------------------------";
neuper@37906: "----------- for correction of diff_const ------------------------";
neuper@37906: (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
neuper@37991: val thy' = "Diff";
neuper@37906: val ct = "Not (x =!= a)";
neuper@37906: rewrite_set thy' false "erls" ct;
neuper@37906: val ct = "2 is_const";
neuper@37906: rewrite_set thy' false "erls" ct;
neuper@37906: 
neuper@37906: val thm = ("diff_const","");
neuper@37906: val ct = "d_d x x";
neuper@37926: val NONE =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
neuper@37906: val ct = "d_d x 2";
neuper@37926: val SOME (ctt,_) =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
neuper@37906: "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";
neuper@37906: trace_rewrite := true;
neuper@37906: val ct = "d_d s a";
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
neuper@37926: (*got: NONE instead SOME*)
neuper@37906: eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls");
neuper@37906: (*got: false instead true;   ~~~~~~~~~~~ replaced by 'is_atom'*)
neuper@37926: val SOME (ctt,_) =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
neuper@37906: if ctt = "0" then () else raise error "diff.sml: thm 'diff_const' diff.behav.";
neuper@37906: trace_rewrite := false;
neuper@37906: "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----";
neuper@37906: 
neuper@37906: val thm = ("diff_var","");
neuper@37906: val ct = "d_d x x";
neuper@37926: val SOME (ctt,_) =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
neuper@37906: val ct = "d_d x a";
neuper@37926: val NONE =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
neuper@37906: val ct = "d_d x (x+x)";
neuper@37926: val NONE =
neuper@37906: (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ for correction of diff_quot  _________________ ";
neuper@37906: " _________________ for correction of diff_quot  _________________ ";
neuper@37906: " _________________ for correction of diff_quot  _________________ ";
neuper@37991: val thy' = "Diff";
neuper@37906: val ct = "Not (x = 0)";
neuper@37906: rewrite_set thy' false "erls" ct;
neuper@37906: 
neuper@37906: val ct = "d_d x ((x+1) / (x - 1))";
neuper@37906: val thm = ("diff_quot","");
neuper@37926: val SOME (ctt,_) =
neuper@37906:     (rewrite_inst thy' "tless_true" "erls" true [("bdv","x")] thm ct);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ differentiate by rewrite _________________ ";
neuper@37906: " _________________ differentiate by rewrite _________________ ";
neuper@37906: " _________________ differentiate by rewrite _________________ ";
neuper@37991: val thy' = "Diff";
neuper@37906: val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
neuper@37906: "--- 1 ---";
neuper@37906: val thm = ("diff_sum","");
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: "--- 2 ---";
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: "--- 3 ---";
neuper@37906: val thm = ("diff_prod_const","");
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: "--- 4 ---";
neuper@37906: val thm = ("diff_pow","");
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: "--- 5 ---";
neuper@37906: val thm = ("diff_const","");
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: "--- 6 ---";
neuper@37906: val thm = ("diff_var","");
neuper@37906: val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true 
neuper@37906: 		  [("bdv","x::real")] thm ct);
neuper@37906: if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
neuper@37906: else raise error "diff.sml diff.behav. in rewrite 1";
neuper@37906: "--- 7 ---";
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: if ct="3 + 2 * x" then () else raise error "new behaviour in test-example";
neuper@37906: 
neuper@37906: val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
neuper@37906: val (ct,_) = the (rewrite_set thy' true rls ct);
neuper@37906: 
neuper@37906: 
neuper@37906: (*---
neuper@37906: val t = str2term "x ^^^ (2 - 1)";
neuper@37926: val SOME (t',_) = rewrite_set_ thy false Test_simplify t;
neuper@37906: term2str t';
neuper@37906: 
neuper@37906: val t = str2term "-1 * 1";
neuper@37926: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: " ______________ differentiate: me (*+ tacs input*) ______________ ";
neuper@37906: " ______________ differentiate: me (*+ tacs input*) ______________ ";
neuper@37906: " ______________ differentiate: me (*+ tacs input*) ______________ ";
neuper@37906: val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", 
neuper@37994: 	   "differentiateFor x","derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
neuper@37991:   ("Diff",["derivative_of","function"],
neuper@37906:    ["diff","diff_simpl"]);
neuper@37906: val p = e_pos'; val c = []; 
neuper@37906: "--- s1 ---";
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(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",
neuper@37906: Add_Given "functionTerm (d_d x (x ^^^ #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 ---";
neuper@37906: (*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 ---";
neuper@37906: (*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 ---";
neuper@37906: (*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 ---";
neuper@37906: (*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 ---";
neuper@37906: (*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 ---";
neuper@37906: (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt; 
neuper@37906: if f2str f =  "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then () 
neuper@37906: else raise error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
neuper@37906: "--- 7 ---";
neuper@37906: (*------------------------------11.3.03--------------------
neuper@37906:  trace_rewrite:=true;
neuper@37906:  val (_,_,f,_,_,_) = me nxt p c pt;
neuper@37906:  val Form' (FormKF (_,_,_,_,res)) = f;
neuper@37906:  trace_rewrite:=false;
neuper@37906: 
neuper@37906:  val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
neuper@37991:  val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct;
neuper@37906: 
neuper@37906:  trace_rewrite:=true;
neuper@37906:  val t = str2term ct; 
neuper@37906:  term2str t;
neuper@37926:  val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
neuper@37906:  term2str t';
neuper@37906:  trace_rewrite:=false;
neuper@37906: 
neuper@37926:  val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
neuper@37906:  term2str t'';
neuper@37906:  
neuper@37969:  val thm = num_str @{thm realpow_eq_oneI;
neuper@37906:  case string_of_thm thm of
neuper@37906: 
neuper@37906: 
neuper@37991:  val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m;
neuper@37906:  term2str ff; term2str ff';
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: --------------------------------11.3.03--------------------*)
neuper@37906: 
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 ---";
neuper@37906: (*val nxt =
neuper@37991: ("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;
neuper@37906: if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then ()
neuper@37906: else raise error "diff.sml: new.behav. in me (*+ tacs input*)";
neuper@37906: (*if f = EmptyMout then () else raise error "new behaviour in + tacs input";
neuper@37906: meNEW extracts Form once more*)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*---------------- 1.5.02 -----------------------------------------
neuper@37906: 
neuper@37906: " _________________ script-eval corrected _________________ ";
neuper@37906: " _________________ script-eval corrected _________________ ";
neuper@37906: " _________________ script-eval corrected _________________ ";
neuper@37991: val scr = Script (((inst_abs (assoc_thy "Test")) o 
neuper@37906: 	   term_of o the o (parse Diff.thy))
neuper@37994:   "Script Differentiate (f_f::real) (v_v::real) =                                 \
neuper@37906:    \(let f_ = Try (Repeat (Rewrite frac_conv False f_));                        \
neuper@37906:    \     f_ = Try (Repeat (Rewrite root_conv False f_));                        \
neuper@37906:    \     f_ = Repeat                                                            \
neuper@37991:    \            ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False f_)) Or \
neuper@37991:    \             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False f_)) Or \
neuper@37906:    \             (Repeat (Rewrite_Set             Test_simplify False f_)));  \
neuper@37906:    \     f_ = Try (Repeat (Rewrite sym_frac_conv False f_))                     \
neuper@37906:    \ in       Try (Repeat (Rewrite sym_root_conv False f_)))");
neuper@37906: val d = e_rls;
neuper@37906: val (dI',pI',mI') =
neuper@37991:   ("Diff",e_pblID,
neuper@37991:    ("Diff","differentiate_on_R"));
neuper@37906: val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
neuper@37906: val (p,_,_,_,_,pt) = me (mI,m) p c  EmptyPtree;
neuper@37906: val nxt = ("Specify_Theory",Specify_Theory dI');
neuper@37906: val (p,_,_,_,_,pt) = me nxt p c pt;
neuper@37906: val nxt = ("Specify_Method",Specify_Method mI');
neuper@37906: val (p,_,_,_,_,pt) = me nxt p c pt;
neuper@37906: val p = ([1],Frm):pos';
neuper@37906: 
neuper@37906: 
neuper@37906: val parseee = (term_of o the o (parse Diff.thy));
neuper@37906: val ct =   "d_d x (x ^^^ #2 + #3 * x + #4)";
neuper@37994: val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];
neuper@37906: val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
neuper@37906: 	  ([],(User', [],                [],        empty, empty,Sundef))]:ets;
neuper@37906: val l0 = [];
neuper@37906: " --------------- 1. ---------------------------------------------";
neuper@37906: val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
neuper@37906: 
neuper@37991: val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0;
neuper@37906: (*("diff_sum","")*)
neuper@37906: val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = 
neuper@37991:   locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0;
neuper@37906: val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
neuper@37906: " --------------- 2. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
neuper@37991: val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1;
neuper@37906: (*("diff_sum","")*)
neuper@37906: val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = 
neuper@37991:   locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1;
neuper@37906: val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
neuper@37906: " --------------- 3. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));
neuper@37991: val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2;
neuper@37906: (*("diff_prod_const","")*)
neuper@37906: val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = 
neuper@37991:   locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2;
neuper@37906: val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
neuper@37906: " --------------- 4. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));
neuper@37991: val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3;
neuper@37906: (*("diff_pow","")*)
neuper@37906: val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = 
neuper@37991:     locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3;
neuper@37906: val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
neuper@37906: " --------------- 5. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));
neuper@37991: val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4;
neuper@37906: (*("diff_const","")*)
neuper@37906: val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] = 
neuper@37991:     locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4;
neuper@37906: val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];
neuper@37906: " --------------- 6. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));
neuper@37991: val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5;
neuper@37906: (*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)
neuper@37906: val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] = 
neuper@37991:     locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5;
neuper@37906: val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];
neuper@37906: " --------------- 7. ---------------------------------------------";
neuper@37906: val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
neuper@37906: 
neuper@37906: 
neuper@37906:  ---------------- 1.5.02 -----------------------------------------*)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: " ________________ differentiate stdin: student active________________ ";
neuper@37906: " ________________ differentiate stdin: student active________________ ";
neuper@37906: " ________________ differentiate stdin: student active________________ ";
neuper@37906: (*
neuper@37906: proofs:= []; dials:=([],[],[]); 
neuper@37906: StdinSML 0 0 0 0 New_User;
neuper@37906: set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
neuper@37906: StdinSML 1 0 0 0 New_Proof;
neuper@37906: val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", 
neuper@37994: 	   "differentiateFor x","derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
neuper@37991:   ("Diff",["derivative_of","function"],
neuper@37906:    ["diff","differentiate_on_R"]);
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ differentiate stdin: tutor active_________________ ";
neuper@37906: " _________________ differentiate stdin: tutor active_________________ ";
neuper@37906: " _________________ differentiate stdin: tutor active_________________ ";
neuper@37906: (*proofs:= []; dials:=([],[],[]); 
neuper@37906: StdinSML 0 0 0 0 New_User;
neuper@37906: set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
neuper@37906: StdinSML 1 0 0 0 New_Proof;
neuper@37906: val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", 
neuper@37994: 	   "differentiateFor x","derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
neuper@37991:   ("Diff",["derivative_of","function"],
neuper@37906:    ["diff","differentiate_on_R"]);
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: "---------------------1.5.02 me from script ---------------------";
neuper@37906: "---------------------1.5.02 me from script ---------------------";
neuper@37906: "---------------------1.5.02 me from script ---------------------";
neuper@37906: (*exp_Diff_No-1.xml*)
neuper@37906: val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", 
neuper@37994: 	   "differentiateFor x","derivative f_f'"];
neuper@37906: val (dI',pI',mI') =
neuper@37991:   ("Diff",["derivative_of","function"],
neuper@37906:    ["diff","diff_simpl"]);
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(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;
neuper@37991: (*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;
neuper@37906: if nxt = ("End_Proof'",End_Proof') then ()
neuper@37906: else raise error "new behaviour in tests/differentiate, 1.5.02 me from script";
neuper@37906: 
neuper@37906: "----------- primed id -------------------------------------------";
neuper@37906: "----------- primed id -------------------------------------------";
neuper@37906: "----------- primed id -------------------------------------------";
neuper@37906: 
neuper@37994: val f_ = str2term "f_f::bool";
neuper@37906: val f  = str2term "A = s * (a - s)";
neuper@37981: val v_v = str2term "v_";
neuper@37906: val v  = str2term "s";
neuper@37981: val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))";
neuper@37906: atomty screxp0;
neuper@37906: 
neuper@37994: val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0;
neuper@37906: term2str screxp1;
neuper@37906: atomty screxp1;
neuper@37906: 
neuper@37926: val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1; 
neuper@37906: if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
neuper@37906: else raise error "diff.sml: diff.behav. in 'primed'";
neuper@37906: atomty f'_;
neuper@37906: 
neuper@37994: val str = "Script DiffEqScr (f_f::bool) (v_v::real) =                         \
neuper@37994: \ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_))           \
neuper@37906: \ in (((Try (Repeat (Rewrite frac_conv   False))) @@              \
neuper@37906:  \ (Try (Repeat (Rewrite root_conv   False))) @@                  \
neuper@37906:  \ (Try (Repeat (Rewrite realpow_pow False))) @@                  \
neuper@37906:  \ (Repeat                                                        \
neuper@37991:  \   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt       False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or \
neuper@37991:  \    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or \
neuper@37906:  \    (Repeat (Rewrite_Set             make_polynomial False)))) @@ \
neuper@37906:  \ (Try (Repeat (Rewrite sym_frac_conv False))) @@              \
neuper@37994:  \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
neuper@37906: ;
neuper@37906: val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- diff_conv, sym_diff_conv ----------------------------";
neuper@37906: "----------- diff_conv, sym_diff_conv ----------------------------";
neuper@37906: "----------- diff_conv, sym_diff_conv ----------------------------";
neuper@37906: val subs = [(str2term "bdv", str2term "x")];
neuper@37906: val rls = diff_conv;
neuper@37906: 
neuper@37906: val t = str2term "2/x^^^2"; 
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t = "2 * x ^^^ -2" then () else raise error "diff.sml 1/x";
neuper@37906: 
neuper@37906: val t = str2term "sqrt (x^^^3)";
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t = "x ^^^ (3 / 2)" then () else raise error "diff.sml x^1/2";
neuper@37906: 
neuper@37906: val t = str2term "2 / sqrt x^^^3";
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t = "2 * x ^^^ (-3 / 2)" then () else raise error"diff.sml x^-1/2";
neuper@37906: (* trace_rewrite := true;
neuper@37906:    trace_rewrite := false;
neuper@37906:    *)
neuper@37906: val rls = diff_sym_conv; 
neuper@37906: 
neuper@37906: val t = str2term "2 * x ^^^ -2";
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t = "2 / x ^^^ 2" then () else raise error "diff.sml sym 1/x";
neuper@37906: 
neuper@37906: 
neuper@37906: val t = str2term "x ^^^ (3 / 2)";
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t = "sqrt (x ^^^ 3)" then () else raise error"diff.sml sym x^1/x";
neuper@37906: 
neuper@37906: val t = str2term "2 * x ^^^ (-3 / 2)";
neuper@37926: val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
neuper@37906: if term2str t ="2 / sqrt (x ^^^ 3)"then()else raise error"diff.sml sym x^-1/x";
neuper@37906: 
neuper@37906: 
neuper@37906: (* trace_rewrite:=true;
neuper@37906:    *)
neuper@37906: (* trace_rewrite:=false;
neuper@37906:    *)
neuper@37906: (*@@@@*)
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
neuper@37906: "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
neuper@37906: "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
neuper@37906:    (*"functionTerm ((x^3)^5)",*)
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
neuper@37991:   ("Isac", ["derivative_of","function"],
neuper@37906:   ["diff","differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = 
neuper@37906: 			  "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
neuper@37906: else raise error "diff.sml: differentiate_on_R 2/x^2 changed";
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm (x^3 * x^5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
neuper@37991:   ("Isac", ["derivative_of","function"],
neuper@37906:   ["diff","differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: (* trace_rewrite := true;
neuper@37906:    trace_script := true;
neuper@37906:    *)
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: (* trace_rewrite := false;
neuper@37906:    trace_script := false;
neuper@37906:    *)
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: 
neuper@37906: if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = 
neuper@37906: 			 "8 * x ^^^ 7" then () 
neuper@37906: else raise error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- autoCalculate diff after_simplification -------------";
neuper@37906: "----------- autoCalculate diff after_simplification -------------";
neuper@37906: "----------- autoCalculate diff after_simplification -------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm (x^3 * x^5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
neuper@37991:   ("Isac", ["derivative_of","function"],
neuper@37906:   ["diff","after_simplification"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: (* trace_rewrite := true;
neuper@37906:    trace_script := true;
neuper@37906:    *)
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: (* trace_rewrite := false;
neuper@37906:    trace_script := false;
neuper@37906:    *)
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =  "8 * x ^^^ 7"
neuper@37906: then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm ((x^3)^5)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
neuper@37991:   ("Isac", ["derivative_of","function"],
neuper@37906:   ["diff","after_simplification"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
neuper@37906: then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- autoCalculate differentiate_equality ----------------";
neuper@37906: "----------- autoCalculate differentiate_equality ----------------";
neuper@37906: "----------- autoCalculate differentiate_equality ----------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37994: [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"], 
neuper@37991:   ("Isac", ["named","derivative_of","function"],
neuper@37906:   ["diff","differentiate_equality"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalc;
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- tests for examples ----------------------------------";
neuper@37906: "----------- tests for examples ----------------------------------";
neuper@37906: "----------- tests for examples ----------------------------------";
neuper@37906: "----- parse errors";
neuper@37906: (*str2term "F  =  sqrt( y^2 - O) * (z + O^2)";
neuper@37906: str2term "O";*)
neuper@37906: str2term "OO";
neuper@37906: 
neuper@37906: "----- thm 'diff_prod_const'";
neuper@37906: val subs = [(str2term "bdv", str2term "l")];
neuper@37906: val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))";
neuper@37906: (*
neuper@37906: trace_rewrite := true;
neuper@37906: rewrite_inst_ Isac.thy tless_true erls_diff true subs diff_prod_const f;
neuper@37906: trace_rewrite := false;
neuper@37906: *)
neuper@37906: 
neuper@37906: "------------inform for x^2+x+1 ----------------------------------";
neuper@37906: "------------inform for x^2+x+1 ----------------------------------";
neuper@37906: "------------inform for x^2+x+1 ----------------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["functionTerm (x^2 + x + 1)",
neuper@37994:    "differentiateFor x", "derivative f_f'"], 
neuper@37991:   ("Isac", ["derivative_of","function"],
neuper@37906:   ["diff","differentiate_on_R"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1;
neuper@37906: autoCalculate 1 CompleteCalcHead;
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: autoCalculate 1 (Step 1);
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: appendFormula 1 "2*x + d_d x x + d_d x 1";
neuper@37906: val ((pt,p),_) = get_calc 1; show_pt pt;
neuper@37906: if existpt' ([3], Res) pt then ()
neuper@37906: else raise error  "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";