wneuper/isa: comparison test/Tools/isac/Knowledge/diff.sml

equal deleted inserted replaced

-:24609758d219
+:028442673981
 "----------- 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.thy";
+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;
 " _________________ for correction of diff_quot  _________________ ";
 " _________________ for correction of diff_quot  _________________ ";
 " _________________ for correction of diff_quot  _________________ ";
-val thy' = "Diff.thy";
+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","");
 " _________________ differentiate by rewrite _________________ ";
 " _________________ differentiate by rewrite _________________ ";
 " _________________ differentiate by rewrite _________________ ";
-val thy' = "Diff.thy";
+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);
 " ______________ differentiate: me (*+ tacs input*) ______________ ";
 " ______________ differentiate: me (*+ tacs input*) ______________ ";
 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
 	   "differentiateFor x","derivative f_'_"];
 val (dI',pI',mI') =
-("Diff.thy",["derivative_of","function"],
+("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;
 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.thy" false "make_polynomial" ct;
+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;
 val thm = num_str @{thm realpow_eq_oneI;
 case string_of_thm thm of
-val Rewrite_Set' ("Diff.thy",false,"make_polynomial",ff,(ff',[])) = m;
+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.thy","differentiate_on_R"));*)
+("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 ()
 (*---------------- 1.5.02 -----------------------------------------
 " _________________ script-eval corrected _________________ ";
 " _________________ script-eval corrected _________________ ";
 " _________________ script-eval corrected _________________ ";
-val scr = Script (((inst_abs (assoc_thy "Test.thy")) o
+val scr = Script (((inst_abs (assoc_thy "Test")) o
 	   term_of o the o (parse Diff.thy))
-"Script Differentiate (f_::real) (v_::real) =                                 \
+"Script Differentiate (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_)] diff_sum        False f_)) Or \
+\            ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False f_)) Or \
+\             (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False f_)) Or \
-\             (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        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.thy",e_pblID,
+("Diff",e_pblID,
-("Diff.thy","differentiate_on_R"));
+("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 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.thy" (pt,p) scr ets0 l0;
+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.thy" m' (pt,p) (scr,d) ets0 l0;
+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.thy" (pt,p) scr ets1 l1;
+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.thy" m' (pt,p) (scr,d) ets1 l1;
+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.thy" (pt,p) scr ets2 l2;
+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.thy" m' (pt,p) (scr,d) ets2 l2;
+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.thy" (pt,p) scr ets3 l3;
+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.thy" m' (pt,p) (scr,d) ets3 l3;
+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.thy" (pt,p) scr ets4 l4;
+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.thy" m' (pt,p) (scr,d) ets4 l4;
+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.thy" (pt,p) scr ets5 l5;
+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.thy" m' (pt,p) (scr,d) ets5 l5;
+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");
 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_'_"];
 val (dI',pI',mI') =
-("Diff.thy",["derivative_of","function"],
+("Diff",["derivative_of","function"],
 ["diff","differentiate_on_R"]);
 *)
 " _________________ differentiate stdin: tutor active_________________ ";
 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_'_"];
 val (dI',pI',mI') =
-("Diff.thy",["derivative_of","function"],
+("Diff",["derivative_of","function"],
 ["diff","differentiate_on_R"]);
 *)
 "---------------------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_'_"];
 val (dI',pI',mI') =
-("Diff.thy",["derivative_of","function"],
+("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;
-(*nxt = ("Apply_Method",Apply_Method ("Diff.thy","differentiate_on_R*)
+(*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 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_::bool) (v_::real) =                         \
+val str = "Script DiffEqScr (f_::bool) (v_v::real) =                         \
 \ (let 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_)] diff_sum        False)) Or \
+\   ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum        False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod       False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod       False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot       True )) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot       True )) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin        False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin        False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain  False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain  False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos        False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos        False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain  False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain  False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow        False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow        False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain  False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain  False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln         False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln         False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain   False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain   False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp        False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp        False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain  False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain  False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt       False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt       False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_const      False)) Or \
+\    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or \
-\    (Repeat (Rewrite_Inst [(bdv,v_)] diff_var        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'_)"
 ;
 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
 states:=[];
 CalcTree
 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
 (*"functionTerm ((x^3)^5)",*)
 "differentiateFor x", "derivative f_'_"],
-("Isac.thy", ["derivative_of","function"],
+("Isac", ["derivative_of","function"],
 ["diff","differentiate_on_R"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 "-----------------------------------------------------------------";
 states:=[];
 CalcTree
 [(["functionTerm (x^3 * x^5)",
 "differentiateFor x", "derivative f_'_"],
-("Isac.thy", ["derivative_of","function"],
+("Isac", ["derivative_of","function"],
 ["diff","differentiate_on_R"]))];
 Iterator 1;
 moveActiveRoot 1;
 (* trace_rewrite := true;
 trace_script := true;
 "----------- autoCalculate diff after_simplification -------------";
 states:=[];
 CalcTree
 [(["functionTerm (x^3 * x^5)",
 "differentiateFor x", "derivative f_'_"],
-("Isac.thy", ["derivative_of","function"],
+("Isac", ["derivative_of","function"],
 ["diff","after_simplification"]))];
 Iterator 1;
 moveActiveRoot 1;
 (* trace_rewrite := true;
 trace_script := true;
 "-----------------------------------------------------------------";
 states:=[];
 CalcTree
 [(["functionTerm ((x^3)^5)",
 "differentiateFor x", "derivative f_'_"],
-("Isac.thy", ["derivative_of","function"],
+("Isac", ["derivative_of","function"],
 ["diff","after_simplification"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 "----------- autoCalculate differentiate_equality ----------------";
 "----------- autoCalculate differentiate_equality ----------------";
 states:=[];
 CalcTree
 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"],
-("Isac.thy", ["named","derivative_of","function"],
+("Isac", ["named","derivative_of","function"],
 ["diff","differentiate_equality"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalc;
 val ((pt,p),_) = get_calc 1; show_pt pt;
 "------------inform for x^2+x+1 ----------------------------------";
 states:=[];
 CalcTree
 [(["functionTerm (x^2 + x + 1)",
 "differentiateFor x", "derivative f_'_"],
-("Isac.thy", ["derivative_of","function"],
+("Isac", ["derivative_of","function"],
 ["diff","differentiate_on_R"]))];
 Iterator 1;
 moveActiveRoot 1;
 autoCalculate 1 CompleteCalcHead;
 autoCalculate 1 (Step 1);

branch	isac-update-Isa09-2
changeset 37991	028442673981
parent 37981	b2877b9d455a
child 37994	eb4c556a525b