1.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:17:29 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:20:03 2010 +0200
1.3 @@ -32,15 +32,15 @@
1.4 " _________________ problemtype _________________ ";
1.5 " _________________ problemtype _________________ ";
1.6 " _________________ problemtype _________________ ";
1.7 -val pbt = {Given =["functionTerm f_", "differentiateFor v_v"],
1.8 +val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
1.9 Where =[],
1.10 - Find =["derivative f_'_"],
1.11 + Find =["derivative f_f'"],
1.12 With =[],
1.13 Relate=[]}:string ppc;
1.14 val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
1.15
1.16 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.17 - "differentiateFor x","derivative f_'_"];
1.18 + "differentiateFor x","derivative f_f'"];
1.19 val chkorg = map (the o (parse Diff.thy)) org;
1.20
1.21 get_pbt ["derivative_of","function"];
1.22 @@ -195,7 +195,7 @@
1.23 " ______________ differentiate: me (*+ tacs input*) ______________ ";
1.24 " ______________ differentiate: me (*+ tacs input*) ______________ ";
1.25 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.26 - "differentiateFor x","derivative f_'_"];
1.27 + "differentiateFor x","derivative f_f'"];
1.28 val (dI',pI',mI') =
1.29 ("Diff",["derivative_of","function"],
1.30 ["diff","diff_simpl"]);
1.31 @@ -211,7 +211,7 @@
1.32 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
1.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.34 "--- s4 ---";
1.35 -(*val nxt = ("Add_Find",Add_Find "derivative f_'_");*)
1.36 +(*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
1.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.38 "--- s5 ---";
1.39 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
1.40 @@ -305,7 +305,7 @@
1.41 " _________________ script-eval corrected _________________ ";
1.42 val scr = Script (((inst_abs (assoc_thy "Test")) o
1.43 term_of o the o (parse Diff.thy))
1.44 - "Script Differentiate (f_::real) (v_v::real) = \
1.45 + "Script Differentiate (f_f::real) (v_v::real) = \
1.46 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
1.47 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
1.48 \ f_ = Repeat \
1.49 @@ -344,7 +344,7 @@
1.50
1.51 val parseee = (term_of o the o (parse Diff.thy));
1.52 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
1.53 -val envvv = [(parseee"f_",parseee ct),(parseee"v_",parseee"x")];
1.54 +val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];
1.55 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
1.56 ([],(User', [], [], empty, empty,Sundef))]:ets;
1.57 val l0 = [];
1.58 @@ -410,7 +410,7 @@
1.59 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
1.60 StdinSML 1 0 0 0 New_Proof;
1.61 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.62 - "differentiateFor x","derivative f_'_"];
1.63 + "differentiateFor x","derivative f_f'"];
1.64 val (dI',pI',mI') =
1.65 ("Diff",["derivative_of","function"],
1.66 ["diff","differentiate_on_R"]);
1.67 @@ -425,7 +425,7 @@
1.68 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
1.69 StdinSML 1 0 0 0 New_Proof;
1.70 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.71 - "differentiateFor x","derivative f_'_"];
1.72 + "differentiateFor x","derivative f_f'"];
1.73 val (dI',pI',mI') =
1.74 ("Diff",["derivative_of","function"],
1.75 ["diff","differentiate_on_R"]);
1.76 @@ -437,7 +437,7 @@
1.77 "---------------------1.5.02 me from script ---------------------";
1.78 (*exp_Diff_No-1.xml*)
1.79 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.80 - "differentiateFor x","derivative f_'_"];
1.81 + "differentiateFor x","derivative f_f'"];
1.82 val (dI',pI',mI') =
1.83 ("Diff",["derivative_of","function"],
1.84 ["diff","diff_simpl"]);
1.85 @@ -470,14 +470,14 @@
1.86 "----------- primed id -------------------------------------------";
1.87 "----------- primed id -------------------------------------------";
1.88
1.89 -val f_ = str2term "f_::bool";
1.90 +val f_ = str2term "f_f::bool";
1.91 val f = str2term "A = s * (a - s)";
1.92 val v_v = str2term "v_";
1.93 val v = str2term "s";
1.94 val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))";
1.95 atomty screxp0;
1.96
1.97 -val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
1.98 +val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0;
1.99 term2str screxp1;
1.100 atomty screxp1;
1.101
1.102 @@ -486,8 +486,8 @@
1.103 else raise error "diff.sml: diff.behav. in 'primed'";
1.104 atomty f'_;
1.105
1.106 -val str = "Script DiffEqScr (f_::bool) (v_v::real) = \
1.107 -\ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
1.108 +val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
1.109 +\ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
1.110 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
1.111 \ (Try (Repeat (Rewrite root_conv False))) @@ \
1.112 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
1.113 @@ -512,7 +512,7 @@
1.114 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
1.115 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
1.116 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
1.117 - \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)"
1.118 + \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
1.119 ;
1.120 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.121
1.122 @@ -567,7 +567,7 @@
1.123 CalcTree
1.124 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
1.125 (*"functionTerm ((x^3)^5)",*)
1.126 - "differentiateFor x", "derivative f_'_"],
1.127 + "differentiateFor x", "derivative f_f'"],
1.128 ("Isac", ["derivative_of","function"],
1.129 ["diff","differentiate_on_R"]))];
1.130 Iterator 1;
1.131 @@ -582,7 +582,7 @@
1.132 states:=[];
1.133 CalcTree
1.134 [(["functionTerm (x^3 * x^5)",
1.135 - "differentiateFor x", "derivative f_'_"],
1.136 + "differentiateFor x", "derivative f_f'"],
1.137 ("Isac", ["derivative_of","function"],
1.138 ["diff","differentiate_on_R"]))];
1.139 Iterator 1;
1.140 @@ -607,7 +607,7 @@
1.141 states:=[];
1.142 CalcTree
1.143 [(["functionTerm (x^3 * x^5)",
1.144 - "differentiateFor x", "derivative f_'_"],
1.145 + "differentiateFor x", "derivative f_f'"],
1.146 ("Isac", ["derivative_of","function"],
1.147 ["diff","after_simplification"]))];
1.148 Iterator 1;
1.149 @@ -627,7 +627,7 @@
1.150 states:=[];
1.151 CalcTree
1.152 [(["functionTerm ((x^3)^5)",
1.153 - "differentiateFor x", "derivative f_'_"],
1.154 + "differentiateFor x", "derivative f_f'"],
1.155 ("Isac", ["derivative_of","function"],
1.156 ["diff","after_simplification"]))];
1.157 Iterator 1;
1.158 @@ -644,7 +644,7 @@
1.159 "----------- autoCalculate differentiate_equality ----------------";
1.160 states:=[];
1.161 CalcTree
1.162 -[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"],
1.163 +[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"],
1.164 ("Isac", ["named","derivative_of","function"],
1.165 ["diff","differentiate_equality"]))];
1.166 Iterator 1;
1.167 @@ -676,7 +676,7 @@
1.168 states:=[];
1.169 CalcTree
1.170 [(["functionTerm (x^2 + x + 1)",
1.171 - "differentiateFor x", "derivative f_'_"],
1.172 + "differentiateFor x", "derivative f_f'"],
1.173 ("Isac", ["derivative_of","function"],
1.174 ["diff","differentiate_on_R"]))];
1.175 Iterator 1;