1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:17:29 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:20:03 2010 +0200
1.3 @@ -64,11 +64,11 @@
1.4 ML> val c = (the o (parse thy)) s;
1.5 val c =
1.6 "Script make_fun_by_new_variable =
1.7 - Input [Real f_, Real v_v, BoolList eqs_]
1.8 + Input [Real f_f, Real v_v, BoolList eqs]
1.9 Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
1.10 Bool e2_, BoolList s_1, BoolList s_2]
1.11 Tacs [SEQU
1.12 - [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
1.13 + [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_];
1.14 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
1.15 e1_ = (hd o filter (Testvar v1_)) es_;
1.16 e2_ = (hd o filter (Testvar v2_)) es_
1.17 @@ -84,10 +84,10 @@
1.18 ML> val c = (the o (parse thy)) s;
1.19 val c =
1.20 "Script make_fun_explicit =
1.21 - Input [Real f_, Real v_v, BoolList eqs_]
1.22 + Input [Real f_f, Real v_v, BoolList eqs]
1.23 Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
1.24 Tacs [SEQU
1.25 - [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
1.26 + [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]);
1.27 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
1.28 in Subproblem Spec (R, [univar, equation], no_met)
1.29 InOut [In eq_, In v1_, Out ss_]],
2.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:17:29 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:20:03 2010 +0200
2.3 @@ -26,9 +26,9 @@
2.4
2.5 prep_pbt DiffAppl.thy
2.6 (["DiffAppl","make","function"]:pblID,
2.7 - [("#Given" ,"functionOf f_"),
2.8 + [("#Given" ,"functionOf f_f"),
2.9 ("#Given" ,"boundVariable v_v"),
2.10 - ("#Given" ,"equalities eqs_"),
2.11 + ("#Given" ,"equalities eqs"),
2.12 ("#Find" ,"functionTerm f_0_")
2.13 ]),
2.14
2.15 @@ -43,7 +43,7 @@
2.16 prep_pbt DiffAppl.thy
2.17 (["DiffAppl","find_values","tool"]:pblID,
2.18 [("#Given" ,"maxArgument ma_"),
2.19 - ("#Given" ,"functionTerm f_"),
2.20 + ("#Given" ,"functionTerm f_f"),
2.21 ("#Given" ,"boundVariable v_v"),
2.22 ("#Find" ,"valuesFor vls_"),
2.23 ("#Relate","additionalRels rs_")
2.24 @@ -68,9 +68,9 @@
2.25
2.26 (("DiffAppl","make_fun_by_new_variable"):metID,
2.27 {ppc = prep_met DiffAppl.thy
2.28 - [("#Given" ,"functionOf f_"),
2.29 + [("#Given" ,"functionOf f_f"),
2.30 ("#Given" ,"boundVariable v_v"),
2.31 - ("#Given" ,"equalities eqs_"),
2.32 + ("#Given" ,"equalities eqs"),
2.33 ("#Find" ,"functionTerm f_0_")
2.34 ],
2.35 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
2.36 @@ -78,9 +78,9 @@
2.37
2.38 (("DiffAppl","make_fun_by_explicit"):metID,
2.39 {ppc = prep_met DiffAppl.thy
2.40 - [("#Given" ,"functionOf f_"),
2.41 + [("#Given" ,"functionOf f_f"),
2.42 ("#Given" ,"boundVariable v_v"),
2.43 - ("#Given" ,"equalities eqs_"),
2.44 + ("#Given" ,"equalities eqs"),
2.45 ("#Find" ,"functionTerm f_0_")
2.46 ],
2.47 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:17:29 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:20:03 2010 +0200
3.3 @@ -96,21 +96,21 @@
3.4 store_pbt
3.5 (prep_pbt thy "pbl_fun_make" [] e_pblID
3.6 (["make","function"]:pblID,
3.7 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
3.8 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
3.9 ("#Find" ,["functionEq f_1_"])
3.10 ],
3.11 e_rls, NONE, []));
3.12 store_pbt
3.13 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
3.14 (["by_explicit","make","function"]:pblID,
3.15 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
3.16 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
3.17 ("#Find" ,["functionEq f_1_"])
3.18 ],
3.19 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
3.20 store_pbt
3.21 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
3.22 (["by_new_variable","make","function"]:pblID,
3.23 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
3.24 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
3.25 (*WN.12.5.03: precond for distinction still missing*)
3.26 ("#Find" ,["functionEq f_1_"])
3.27 ],
3.28 @@ -134,7 +134,7 @@
3.29 store_pbt
3.30 (prep_pbt thy "pbl_tool_findvals" [] e_pblID
3.31 (["find_values","tool"]:pblID,
3.32 - [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]),
3.33 + [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]),
3.34 ("#Find" ,["valuesFor vls_"]),
3.35 ("#Relate",["additionalRels rs_"])
3.36 ],
3.37 @@ -179,15 +179,15 @@
3.38 store_met
3.39 (prep_met thy "met_diffapp_funnew" [] e_metID
3.40 (["DiffApp","make_fun_by_new_variable"]:metID,
3.41 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
3.42 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
3.43 ("#Find" ,["functionEq f_1_"])
3.44 ],
3.45 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
3.46 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
3.47 - "Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^
3.48 - " (eqs_::bool list) = " ^
3.49 - "(let h_ = (hd o (filterVar f_)) eqs_; " ^
3.50 - " es_ = dropWhile (ident h_) eqs_; " ^
3.51 + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
3.52 + " (eqs::bool list) = " ^
3.53 + "(let h_ = (hd o (filterVar f_)) eqs; " ^
3.54 + " es_ = dropWhile (ident h_) eqs; " ^
3.55 " vs_ = dropWhile (ident f_) (Vars h_); " ^
3.56 " v_1 = nth_ 1 vs_; " ^
3.57 " v_2 = nth_ 2 vs_; " ^
3.58 @@ -204,16 +204,16 @@
3.59 store_met
3.60 (prep_met thy "met_diffapp_funexp" [] e_metID
3.61 (["DiffApp","make_fun_by_explicit"]:metID,
3.62 - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]),
3.63 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
3.64 ("#Find" ,["functionEq f_1_"])
3.65 ],
3.66 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
3.67 crls = eval_rls, nrls=norm_Rational
3.68 (*, asm_rls=[],asm_thm=[]*)},
3.69 - "Script Make_fun_by_explicit (f_::real) (v_v::real) " ^
3.70 - " (eqs_::bool list) = " ^
3.71 - " (let h_ = (hd o (filterVar f_)) eqs_; " ^
3.72 - " e_1 = hd (dropWhile (ident h_) eqs_); " ^
3.73 + "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
3.74 + " (eqs::bool list) = " ^
3.75 + " (let h_ = (hd o (filterVar f_)) eqs; " ^
3.76 + " e_1 = hd (dropWhile (ident h_) eqs); " ^
3.77 " vs_ = dropWhile (ident f_) (Vars h_); " ^
3.78 " v_1 = hd (dropWhile (ident v_v) vs_); " ^
3.79 " (s_1::bool list)= " ^
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:17:29 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:20:03 2010 +0200
4.3 @@ -337,22 +337,22 @@
4.4 store_pbt
4.5 (prep_pbt thy "pbl_fun_integ" [] e_pblID
4.6 (["integrate","function"],
4.7 - [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
4.8 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
4.9 ("#Find" ,["antiDerivative F_"])
4.10 ],
4.11 append_rls "e_rls" e_rls [(*for preds in where_*)],
4.12 - SOME "Integrate (f_, v_v)",
4.13 + SOME "Integrate (f_f, v_v)",
4.14 [["diff","integration"]]));
4.15
4.16 (*here "named" is used differently from Differentiation"*)
4.17 store_pbt
4.18 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
4.19 (["named","integrate","function"],
4.20 - [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
4.21 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
4.22 ("#Find" ,["antiDerivativeName F_"])
4.23 ],
4.24 append_rls "e_rls" e_rls [(*for preds in where_*)],
4.25 - SOME "Integrate (f_, v_v)",
4.26 + SOME "Integrate (f_f, v_v)",
4.27 [["diff","integration","named"]]));
4.28
4.29 (** methods **)
4.30 @@ -360,14 +360,14 @@
4.31 store_met
4.32 (prep_met thy "met_diffint" [] e_metID
4.33 (["diff","integration"],
4.34 - [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
4.35 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
4.36 ("#Find" ,["antiDerivative F_"])
4.37 ],
4.38 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
4.39 srls = e_rls,
4.40 prls=e_rls,
4.41 crls = Atools_erls, nrls = e_rls},
4.42 -"Script IntegrationScript (f_::real) (v_v::real) = " ^
4.43 +"Script IntegrationScript (f_f::real) (v_v::real) = " ^
4.44 " (let t_ = Take (Integral f_ D v_v) " ^
4.45 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
4.46 ));
4.47 @@ -375,14 +375,14 @@
4.48 store_met
4.49 (prep_met thy "met_diffint_named" [] e_metID
4.50 (["diff","integration","named"],
4.51 - [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
4.52 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
4.53 ("#Find" ,["antiDerivativeName F_"])
4.54 ],
4.55 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
4.56 srls = e_rls,
4.57 prls=e_rls,
4.58 crls = Atools_erls, nrls = e_rls},
4.59 -"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^
4.60 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^
4.61 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^
4.62 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
4.63 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) "
5.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 17:17:29 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 17:20:03 2010 +0200
5.3 @@ -549,7 +549,7 @@
5.4 (prep_pbt thy
5.5 (["thy"],
5.6 [("#Given" ,"boolTestGiven g_"),
5.7 - ("#Find" ,"boolTestFind f_")
5.8 + ("#Find" ,"boolTestFind f_f")
5.9 ],
5.10 []));
5.11
5.12 @@ -557,7 +557,7 @@
5.13 (prep_pbt thy
5.14 (["testeq","thy"],
5.15 [("#Given" ,"boolTestGiven g_"),
5.16 - ("#Find" ,"boolTestFind f_")
5.17 + ("#Find" ,"boolTestFind f_f")
5.18 ],
5.19 []));
5.20
5.21 @@ -604,7 +604,7 @@
5.22 (*, prep_met thy (*test for equations*)
5.23 (["Test","testeq"]:metID,
5.24 [("#Given" ,["boolTestGiven g_"]),
5.25 - ("#Find" ,["boolTestFind f_"])
5.26 + ("#Find" ,["boolTestFind f_f"])
5.27 ],
5.28 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
5.29 asm_thm=[("square_equation_left","")]},
6.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:17:29 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:20:03 2010 +0200
6.3 @@ -32,15 +32,15 @@
6.4 " _________________ problemtype _________________ ";
6.5 " _________________ problemtype _________________ ";
6.6 " _________________ problemtype _________________ ";
6.7 -val pbt = {Given =["functionTerm f_", "differentiateFor v_v"],
6.8 +val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
6.9 Where =[],
6.10 - Find =["derivative f_'_"],
6.11 + Find =["derivative f_f'"],
6.12 With =[],
6.13 Relate=[]}:string ppc;
6.14 val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
6.15
6.16 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
6.17 - "differentiateFor x","derivative f_'_"];
6.18 + "differentiateFor x","derivative f_f'"];
6.19 val chkorg = map (the o (parse Diff.thy)) org;
6.20
6.21 get_pbt ["derivative_of","function"];
6.22 @@ -195,7 +195,7 @@
6.23 " ______________ differentiate: me (*+ tacs input*) ______________ ";
6.24 " ______________ differentiate: me (*+ tacs input*) ______________ ";
6.25 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
6.26 - "differentiateFor x","derivative f_'_"];
6.27 + "differentiateFor x","derivative f_f'"];
6.28 val (dI',pI',mI') =
6.29 ("Diff",["derivative_of","function"],
6.30 ["diff","diff_simpl"]);
6.31 @@ -211,7 +211,7 @@
6.32 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
6.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.34 "--- s4 ---";
6.35 -(*val nxt = ("Add_Find",Add_Find "derivative f_'_");*)
6.36 +(*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
6.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.38 "--- s5 ---";
6.39 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
6.40 @@ -305,7 +305,7 @@
6.41 " _________________ script-eval corrected _________________ ";
6.42 val scr = Script (((inst_abs (assoc_thy "Test")) o
6.43 term_of o the o (parse Diff.thy))
6.44 - "Script Differentiate (f_::real) (v_v::real) = \
6.45 + "Script Differentiate (f_f::real) (v_v::real) = \
6.46 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
6.47 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
6.48 \ f_ = Repeat \
6.49 @@ -344,7 +344,7 @@
6.50
6.51 val parseee = (term_of o the o (parse Diff.thy));
6.52 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
6.53 -val envvv = [(parseee"f_",parseee ct),(parseee"v_",parseee"x")];
6.54 +val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];
6.55 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
6.56 ([],(User', [], [], empty, empty,Sundef))]:ets;
6.57 val l0 = [];
6.58 @@ -410,7 +410,7 @@
6.59 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
6.60 StdinSML 1 0 0 0 New_Proof;
6.61 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
6.62 - "differentiateFor x","derivative f_'_"];
6.63 + "differentiateFor x","derivative f_f'"];
6.64 val (dI',pI',mI') =
6.65 ("Diff",["derivative_of","function"],
6.66 ["diff","differentiate_on_R"]);
6.67 @@ -425,7 +425,7 @@
6.68 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
6.69 StdinSML 1 0 0 0 New_Proof;
6.70 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
6.71 - "differentiateFor x","derivative f_'_"];
6.72 + "differentiateFor x","derivative f_f'"];
6.73 val (dI',pI',mI') =
6.74 ("Diff",["derivative_of","function"],
6.75 ["diff","differentiate_on_R"]);
6.76 @@ -437,7 +437,7 @@
6.77 "---------------------1.5.02 me from script ---------------------";
6.78 (*exp_Diff_No-1.xml*)
6.79 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
6.80 - "differentiateFor x","derivative f_'_"];
6.81 + "differentiateFor x","derivative f_f'"];
6.82 val (dI',pI',mI') =
6.83 ("Diff",["derivative_of","function"],
6.84 ["diff","diff_simpl"]);
6.85 @@ -470,14 +470,14 @@
6.86 "----------- primed id -------------------------------------------";
6.87 "----------- primed id -------------------------------------------";
6.88
6.89 -val f_ = str2term "f_::bool";
6.90 +val f_ = str2term "f_f::bool";
6.91 val f = str2term "A = s * (a - s)";
6.92 val v_v = str2term "v_";
6.93 val v = str2term "s";
6.94 val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))";
6.95 atomty screxp0;
6.96
6.97 -val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
6.98 +val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0;
6.99 term2str screxp1;
6.100 atomty screxp1;
6.101
6.102 @@ -486,8 +486,8 @@
6.103 else raise error "diff.sml: diff.behav. in 'primed'";
6.104 atomty f'_;
6.105
6.106 -val str = "Script DiffEqScr (f_::bool) (v_v::real) = \
6.107 -\ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
6.108 +val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
6.109 +\ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
6.110 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
6.111 \ (Try (Repeat (Rewrite root_conv False))) @@ \
6.112 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
6.113 @@ -512,7 +512,7 @@
6.114 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
6.115 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
6.116 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
6.117 - \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)"
6.118 + \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
6.119 ;
6.120 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
6.121
6.122 @@ -567,7 +567,7 @@
6.123 CalcTree
6.124 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
6.125 (*"functionTerm ((x^3)^5)",*)
6.126 - "differentiateFor x", "derivative f_'_"],
6.127 + "differentiateFor x", "derivative f_f'"],
6.128 ("Isac", ["derivative_of","function"],
6.129 ["diff","differentiate_on_R"]))];
6.130 Iterator 1;
6.131 @@ -582,7 +582,7 @@
6.132 states:=[];
6.133 CalcTree
6.134 [(["functionTerm (x^3 * x^5)",
6.135 - "differentiateFor x", "derivative f_'_"],
6.136 + "differentiateFor x", "derivative f_f'"],
6.137 ("Isac", ["derivative_of","function"],
6.138 ["diff","differentiate_on_R"]))];
6.139 Iterator 1;
6.140 @@ -607,7 +607,7 @@
6.141 states:=[];
6.142 CalcTree
6.143 [(["functionTerm (x^3 * x^5)",
6.144 - "differentiateFor x", "derivative f_'_"],
6.145 + "differentiateFor x", "derivative f_f'"],
6.146 ("Isac", ["derivative_of","function"],
6.147 ["diff","after_simplification"]))];
6.148 Iterator 1;
6.149 @@ -627,7 +627,7 @@
6.150 states:=[];
6.151 CalcTree
6.152 [(["functionTerm ((x^3)^5)",
6.153 - "differentiateFor x", "derivative f_'_"],
6.154 + "differentiateFor x", "derivative f_f'"],
6.155 ("Isac", ["derivative_of","function"],
6.156 ["diff","after_simplification"]))];
6.157 Iterator 1;
6.158 @@ -644,7 +644,7 @@
6.159 "----------- autoCalculate differentiate_equality ----------------";
6.160 states:=[];
6.161 CalcTree
6.162 -[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"],
6.163 +[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"],
6.164 ("Isac", ["named","derivative_of","function"],
6.165 ["diff","differentiate_equality"]))];
6.166 Iterator 1;
6.167 @@ -676,7 +676,7 @@
6.168 states:=[];
6.169 CalcTree
6.170 [(["functionTerm (x^2 + x + 1)",
6.171 - "differentiateFor x", "derivative f_'_"],
6.172 + "differentiateFor x", "derivative f_f'"],
6.173 ("Isac", ["derivative_of","function"],
6.174 ["diff","differentiate_on_R"]))];
6.175 Iterator 1;
7.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:17:29 2010 +0200
7.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:20:03 2010 +0200
7.3 @@ -45,7 +45,7 @@
7.4 map (the o (parseold thy)) fmz;
7.5 " -------------- [make,function] -------------- ";
7.6 val pbt =
7.7 - ["functionOf f_","boundVariable v_v","equalities eqs_",
7.8 + ["functionOf f_f","boundVariable v_v","equalities eqs",
7.9 "functionTerm f_0_"];
7.10 map (the o (parseold thy)) pbt;
7.11 val fmz12 =
7.12 @@ -89,7 +89,7 @@
7.13 map (the o (parseold thy)) fmz3;
7.14 " --------- [derivative_of,function] --------- ";
7.15 val pbt =
7.16 - ["functionTerm f_","boundVariable v_v","derivative f_'_"];
7.17 + ["functionTerm f_f","boundVariable v_v","derivative f_f'"];
7.18 map (the o (parseold thy)) pbt;
7.19 val fmz =
7.20 [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
7.21 @@ -99,7 +99,7 @@
7.22 map (the o (parseold thy)) fmz;
7.23 " --------- [find_values,tool] --------- ";
7.24 val pbt =
7.25 - ["maxArgument ma_","functionTerm f_","boundVariable v_v",
7.26 + ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
7.27 "valuesFor vls_","additionalRels rs_"];
7.28 map (the o (parseold thy)) pbt;
7.29 val fmz1 =
7.30 @@ -519,25 +519,25 @@
7.31 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
7.32 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
7.33 str2term
7.34 - "Script Make_fun_by_explicit (f_::real) (v_v::real) \
7.35 - \ (eqs_::bool list) = \
7.36 - \ (let h_ = (hd o (filterVar f_)) eqs_; \
7.37 - \ e_1 = hd (dropWhile (ident h_) eqs_); \
7.38 + "Script Make_fun_by_explicit (f_f::real) (v_v::real) \
7.39 + \ (eqs::bool list) = \
7.40 + \ (let h_ = (hd o (filterVar f_)) eqs; \
7.41 + \ e_1 = hd (dropWhile (ident h_) eqs); \
7.42 \ vs_ = dropWhile (ident f_) (Vars h_); \
7.43 \ v_1 = hd (dropWhile (ident v_v) vs_); \
7.44 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
7.45 \ [BOOL e_1, REAL v_1])\
7.46 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
7.47 -val f_ = (str2term "f_::real",
7.48 +val f_ = (str2term "f_f::real",
7.49 str2term "A");
7.50 val v_v = (str2term "v_v::real",
7.51 str2term "b");
7.52 -val eqs_=(str2term "eqs_::bool list",
7.53 +val eqs=(str2term "eqs::bool list",
7.54 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]");
7.55 -val env = [f_, v_v, eqs_];
7.56 +val env = [f_f, v_v, eqs];
7.57
7.58 (*--- 1.line in script ---*)
7.59 -val t = str2term "(hd o (filterVar v_v)) (eqs_::bool list)";
7.60 +val t = str2term "(hd o (filterVar v_v)) (eqs::bool list)";
7.61 val s = subst_atomic env t;
7.62 term2str s;
7.63 val t = str2term
7.64 @@ -548,7 +548,7 @@
7.65 val env = env @ [(str2term "h_::bool", str2term s')];
7.66
7.67 (*--- 2.line in script ---*)
7.68 -val t = str2term "hd (dropWhile (ident h_) (eqs_::bool list))";
7.69 +val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))";
7.70 val s = subst_atomic env t;
7.71 term2str s;
7.72 val t = str2term
7.73 @@ -610,10 +610,10 @@
7.74 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
7.75 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
7.76 str2term
7.77 - "Script Make_fun_by_new_variable (f_::real) (v_v::real) \
7.78 - \ (eqs_::bool list) = \
7.79 - \(let h_ = (hd o (filterVar f_)) eqs_; \
7.80 - \ es_ = dropWhile (ident h_) eqs_; \
7.81 + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \
7.82 + \ (eqs::bool list) = \
7.83 + \(let h_ = (hd o (filterVar f_)) eqs; \
7.84 + \ es_ = dropWhile (ident h_) eqs; \
7.85 \ vs_ = dropWhile (ident f_) (Vars h_); \
7.86 \ v_1 = nth_ 1 vs_; \
7.87 \ v_2 = nth_ 2 vs_; \
7.88 @@ -624,16 +624,16 @@
7.89 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
7.90 \ [BOOL e_2, REAL v_2])\
7.91 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
7.92 -val f_ = (str2term "f_::real",
7.93 +val f_ = (str2term "f_f::real",
7.94 str2term "A");
7.95 val v_v = (str2term "v_v::real",
7.96 str2term "alpha");
7.97 -val eqs_=(str2term "eqs_::bool list",
7.98 +val eqs=(str2term "eqs::bool list",
7.99 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");
7.100 -val env = [f_, v_v, eqs_];
7.101 +val env = [f_f, v_v, eqs];
7.102
7.103 (*--- 1.line in script ---*)
7.104 -val t = str2term "(hd o (filterVar (f_::real))) (eqs_::bool list)";
7.105 +val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";
7.106 val s = subst_atomic env t;
7.107 term2str s;
7.108 val t = str2term
7.109 @@ -646,7 +646,7 @@
7.110 val env = env @ [(str2term "h_::bool", str2term s')];
7.111
7.112 (*--- 2.line in script ---*)
7.113 -val t = str2term "dropWhile (ident (h_::bool)) (eqs_::bool list)";
7.114 +val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)";
7.115 val s = subst_atomic env t;
7.116 term2str s;
7.117 val t = str2term
7.118 @@ -659,7 +659,7 @@
7.119 val env = env @ [(str2term "es_::bool list", str2term s')];
7.120
7.121 (*--- 3.line in script ---*)
7.122 -val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))";
7.123 +val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))";
7.124 val s = subst_atomic env t;
7.125 term2str s;
7.126 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";
8.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 17:17:29 2010 +0200
8.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 17:20:03 2010 +0200
8.3 @@ -314,7 +314,7 @@
8.4 "----------- check probem type -----------------------------------";
8.5 "----------- check probem type -----------------------------------";
8.6 "----------- check probem type -----------------------------------";
8.7 -val model = {Given =["functionTerm f_", "integrateBy v_v"],
8.8 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
8.9 Where =[],
8.10 Find =["antiDerivative F_"],
8.11 With =[],
8.12 @@ -326,7 +326,7 @@
8.13 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
8.14 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
8.15
8.16 -val model = {Given =["functionTerm f_", "integrateBy v_v"],
8.17 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
8.18 Where =[],
8.19 Find =["antiDerivativeName F_"],
8.20 With =[],
8.21 @@ -362,14 +362,14 @@
8.22 "----------- check Scripts ---------------------------------------";
8.23 "----------- check Scripts ---------------------------------------";
8.24 val str =
8.25 -"Script IntegrationScript (f_::real) (v_v::real) = \
8.26 +"Script IntegrationScript (f_f::real) (v_v::real) = \
8.27 \ (let t_ = Take (Integral f_ D v_v) \
8.28 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
8.29 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
8.30 atomty sc;
8.31
8.32 val str =
8.33 -"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \
8.34 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \
8.35 \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \
8.36 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
8.37 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
8.38 @@ -479,17 +479,17 @@
8.39 store_met
8.40 (prep_met Integrate.thy "met_testint" [] e_metID
8.41 (["diff","integration","test"],
8.42 - [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
8.43 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
8.44 ("#Find" ,["antiDerivative F_"])
8.45 ],
8.46 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
8.47 srls = e_rls,
8.48 prls=e_rls,
8.49 crls = Atools_erls, nrls = e_rls},
8.50 -"Script IntegrationScript (f_::real) (v_v::real) = \
8.51 +"Script IntegrationScript (f_f::real) (v_v::real) = \
8.52 \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
8.53 \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
8.54 -\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))"
8.55 +\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"
8.56 ));
8.57
8.58 states:=[];