analysed error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))
this error is caused in test/../polyminus
by wrong input data to me, autoCalculate, and NOT by bugs in me,
because me work in test/../integrate.sml and test/../diff.sml,
the latter checked in this changeset.
the error probably occurs in all expls with simplify.
1.1 --- a/src/Tools/isac/Test_Isac.thy Wed Dec 29 20:07:52 2010 +0100
1.2 +++ b/src/Tools/isac/Test_Isac.thy Thu Dec 30 14:24:43 2010 +0100
1.3 @@ -77,7 +77,7 @@
1.4 *)
1.5 ML{* writeln "**** run tests on math-engine complete ******************" *};
1.6 (*
1.7 -cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
1.8 +cd"smltest/IsacKnowledge"; ---below the order as in theory Isac---
1.9 use"atools.sml";
1.10 use"termorder.sml";
1.11 *)
2.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Dec 29 20:07:52 2010 +0100
2.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Dec 30 14:24:43 2010 +0100
2.3 @@ -4,44 +4,45 @@
2.4 use"diff.sml";
2.5 *)
2.6
2.7 -"-----------------------------------------------------------------";
2.8 -"table of contents -----------------------------------------------";
2.9 -"-----------------------------------------------------------------";
2.10 -" _________________ problemtype _________________ ";
2.11 -"----------- for correction of diff_const ------------------------";
2.12 -" _________________ for correction of diff_quot _________________ ";
2.13 -" _________________ differentiate by rewrite _________________ ";
2.14 -" ______________ differentiate: me (*+ tacs input*) ______________ ";
2.15 -" ________________ differentiate stdin: student active________________ ";
2.16 -" _________________ differentiate stdin: tutor active_________________ ";
2.17 -"---------------------1.5.02 me from script ---------------------";
2.18 -"----------- primed id -------------------------------------------";
2.19 -"----------- diff_conv, sym_diff_conv ----------------------------";
2.20 -"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
2.21 -"----------- autoCalculate diff after_simplification -------------";
2.22 -"----------- autoCalculate differentiate_equality ----------------";
2.23 -"----------- tests for examples ----------------------------------";
2.24 -"------------inform for x^2+x+1 ----------------------------------";
2.25 -"-----------------------------------------------------------------";
2.26 -"-----------------------------------------------------------------";
2.27 -"-----------------------------------------------------------------";
2.28 +"--------------------------------------------------------";
2.29 +"--------------------------------------------------------";
2.30 +"table of contents --------------------------------------";
2.31 +"--------------------------------------------------------";
2.32 +"----------- problemtype --------------------------------";
2.33 +"----------- for correction of diff_const ---------------";
2.34 +"----------- for correction of diff_quot ----------------";
2.35 +"----------- differentiate by rewrite -------------------";
2.36 +"----------- differentiate: me (*+ tacs input*) ---------";
2.37 +"----------- differentiate stdin: student active --------";(*was outcom.101230*)
2.38 +"----------- differentiate stdin: tutor active ----------";(*was outcom.101230*)
2.39 +"----------- 1.5.02 me from script ----------------------";
2.40 +"----------- primed id ----------------------------------";
2.41 +"----------- diff_conv, sym_diff_conv -------------------";
2.42 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
2.43 +"----------- autoCalculate diff after_simplification ----";
2.44 +"----------- autoCalculate differentiate_equality -------";
2.45 +"----------- tests for examples -------------------------";
2.46 +"------------inform for x^2+x+1 -------------------------";
2.47 +"--------------------------------------------------------";
2.48 +"--------------------------------------------------------";
2.49 +"--------------------------------------------------------";
2.50
2.51
2.52 -val thy = Diff.thy;
2.53 +val thy = theory "Diff";
2.54
2.55 -" _________________ problemtype _________________ ";
2.56 -" _________________ problemtype _________________ ";
2.57 -" _________________ problemtype _________________ ";
2.58 +"----------- problemtype --------------------------------";
2.59 +"----------- problemtype --------------------------------";
2.60 +"----------- problemtype --------------------------------";
2.61 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
2.62 Where =[],
2.63 Find =["derivative f_f'"],
2.64 With =[],
2.65 Relate=[]}:string ppc;
2.66 -val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
2.67 +val chkpbt = ((map (the o (parse thy))) o ppc2list) pbt;
2.68
2.69 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
2.70 "differentiateFor x","derivative f_f'"];
2.71 -val chkorg = map (the o (parse Diff.thy)) org;
2.72 +val chkorg = map (the o (parse thy)) org;
2.73
2.74 get_pbt ["derivative_of","function"];
2.75 get_met ["diff","differentiate_on_R"];
2.76 @@ -54,7 +55,7 @@
2.77 Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),
2.78 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
2.79 rules = [Thm ("refl",num_str @{thm refl}),
2.80 - Thm ("real_le_refl",num_str @{thm real_le_refl}}),
2.81 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
2.82 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
2.83 Thm ("not_true",num_str @{thm not_true}),
2.84 Thm ("not_false",num_str @{thm not_false}),
2.85 @@ -62,8 +63,8 @@
2.86 Thm ("and_false",num_str @{thm and_false}),
2.87 Thm ("or_true",num_str @{thm or_true}),
2.88 Thm ("or_false",num_str @{thm or_false}),
2.89 - Thm ("and_commute",num_str @{and_commute}),
2.90 - Thm ("or_commute",num_str @{or_commute}),
2.91 + Thm ("and_commute",num_str @{thm and_commute}),
2.92 + Thm ("or_commute",num_str @{thm or_commute}),
2.93
2.94 Calc ("Atools.is'_const",eval_const "#is_const_"),
2.95 Calc ("Atools.occurs'_in", eval_occurs_in ""),
2.96 @@ -82,9 +83,9 @@
2.97 }:rls
2.98 )]);
2.99
2.100 -"----------- for correction of diff_const ------------------------";
2.101 -"----------- for correction of diff_const ------------------------";
2.102 -"----------- for correction of diff_const ------------------------";
2.103 +"----------- for correction of diff_const ---------------";
2.104 +"----------- for correction of diff_const ---------------";
2.105 +"----------- for correction of diff_const ---------------";
2.106 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
2.107 val thy' = "Diff";
2.108 val ct = "Not (x =!= a)";
2.109 @@ -124,9 +125,9 @@
2.110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
2.111
2.112
2.113 -" _________________ for correction of diff_quot _________________ ";
2.114 -" _________________ for correction of diff_quot _________________ ";
2.115 -" _________________ for correction of diff_quot _________________ ";
2.116 +"----------- for correction of diff_quot ----------------";
2.117 +"----------- for correction of diff_quot ----------------";
2.118 +"----------- for correction of diff_quot ----------------";
2.119 val thy' = "Diff";
2.120 val ct = "Not (x = 0)";
2.121 rewrite_set thy' false "erls" ct;
2.122 @@ -137,14 +138,9 @@
2.123 (rewrite_inst thy' "tless_true" "erls" true [("bdv","x")] thm ct);
2.124
2.125
2.126 -
2.127 -
2.128 -
2.129 -
2.130 -
2.131 -" _________________ differentiate by rewrite _________________ ";
2.132 -" _________________ differentiate by rewrite _________________ ";
2.133 -" _________________ differentiate by rewrite _________________ ";
2.134 +"----------- differentiate by rewrite -------------------";
2.135 +"----------- differentiate by rewrite -------------------";
2.136 +"----------- differentiate by rewrite -------------------";
2.137 val thy' = "Diff";
2.138 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
2.139 "--- 1 ---";
2.140 @@ -191,9 +187,9 @@
2.141 *)
2.142
2.143
2.144 -" ______________ differentiate: me (*+ tacs input*) ______________ ";
2.145 -" ______________ differentiate: me (*+ tacs input*) ______________ ";
2.146 -" ______________ differentiate: me (*+ tacs input*) ______________ ";
2.147 +"----------- differentiate: me (*+ tacs input*) ---------";
2.148 +"----------- differentiate: me (*+ tacs input*) ---------";
2.149 +"----------- differentiate: me (*+ tacs input*) ---------";
2.150 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
2.151 "differentiateFor x","derivative f_f'"];
2.152 val (dI',pI',mI') =
2.153 @@ -304,7 +300,7 @@
2.154 " _________________ script-eval corrected _________________ ";
2.155 " _________________ script-eval corrected _________________ ";
2.156 val scr = Script (((inst_abs (assoc_thy "Test")) o
2.157 - term_of o the o (parse Diff.thy))
2.158 + term_of o the o (parse thy))
2.159 "Script Differentiate (f_f::real) (v_v::real) = \
2.160 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
2.161 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
2.162 @@ -342,7 +338,7 @@
2.163 val p = ([1],Frm):pos';
2.164
2.165
2.166 -val parseee = (term_of o the o (parse Diff.thy));
2.167 +val parseee = (term_of o the o (parse thy));
2.168 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
2.169 val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];
2.170 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
2.171 @@ -399,11 +395,9 @@
2.172 ---------------- 1.5.02 -----------------------------------------*)
2.173
2.174
2.175 -
2.176 -
2.177 -" ________________ differentiate stdin: student active________________ ";
2.178 -" ________________ differentiate stdin: student active________________ ";
2.179 -" ________________ differentiate stdin: student active________________ ";
2.180 +"----------- differentiate stdin: student active --------";
2.181 +"----------- differentiate stdin: student active --------";
2.182 +"----------- differentiate stdin: student active --------";
2.183 (*
2.184 proofs:= []; dials:=([],[],[]);
2.185 StdinSML 0 0 0 0 New_User;
2.186 @@ -417,9 +411,9 @@
2.187 *)
2.188
2.189
2.190 -" _________________ differentiate stdin: tutor active_________________ ";
2.191 -" _________________ differentiate stdin: tutor active_________________ ";
2.192 -" _________________ differentiate stdin: tutor active_________________ ";
2.193 +"----------- differentiate stdin: tutor active ----------";
2.194 +"----------- differentiate stdin: tutor active ----------";
2.195 +"----------- differentiate stdin: tutor active ----------";
2.196 (*proofs:= []; dials:=([],[],[]);
2.197 StdinSML 0 0 0 0 New_User;
2.198 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
2.199 @@ -432,9 +426,9 @@
2.200 *)
2.201
2.202
2.203 -"---------------------1.5.02 me from script ---------------------";
2.204 -"---------------------1.5.02 me from script ---------------------";
2.205 -"---------------------1.5.02 me from script ---------------------";
2.206 +"----------- 1.5.02 me from script ----------------------";
2.207 +"----------- 1.5.02 me from script ----------------------";
2.208 +"----------- 1.5.02 me from script ----------------------";
2.209 (*exp_Diff_No-1.xml*)
2.210 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
2.211 "differentiateFor x","derivative f_f'"];
2.212 @@ -466,18 +460,18 @@
2.213 if nxt = ("End_Proof'",End_Proof') then ()
2.214 else error "new behaviour in tests/differentiate, 1.5.02 me from script";
2.215
2.216 -"----------- primed id -------------------------------------------";
2.217 -"----------- primed id -------------------------------------------";
2.218 -"----------- primed id -------------------------------------------";
2.219
2.220 +"----------- primed id ----------------------------------";
2.221 +"----------- primed id ----------------------------------";
2.222 +"----------- primed id ----------------------------------";
2.223 val f_ = str2term "f_f::bool";
2.224 val f = str2term "A = s * (a - s)";
2.225 -val v_v = str2term "v_";
2.226 +val v_ = str2term "v_v";
2.227 val v = str2term "s";
2.228 -val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))";
2.229 +val screxp0 = str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
2.230 atomty screxp0;
2.231
2.232 -val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0;
2.233 +val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
2.234 term2str screxp1;
2.235 atomty screxp1;
2.236
2.237 @@ -487,7 +481,7 @@
2.238 atomty f'_;
2.239
2.240 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
2.241 -\ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
2.242 +\ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
2.243 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
2.244 \ (Try (Repeat (Rewrite root_conv False))) @@ \
2.245 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
2.246 @@ -517,9 +511,9 @@
2.247 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.248
2.249
2.250 -"----------- diff_conv, sym_diff_conv ----------------------------";
2.251 -"----------- diff_conv, sym_diff_conv ----------------------------";
2.252 -"----------- diff_conv, sym_diff_conv ----------------------------";
2.253 +"----------- diff_conv, sym_diff_conv -------------------";
2.254 +"----------- diff_conv, sym_diff_conv -------------------";
2.255 +"----------- diff_conv, sym_diff_conv -------------------";
2.256 val subs = [(str2term "bdv", str2term "x")];
2.257 val rls = diff_conv;
2.258
2.259 @@ -559,10 +553,9 @@
2.260 *)
2.261 (*@@@@*)
2.262
2.263 -
2.264 -"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
2.265 -"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
2.266 -"----------- autoCalculate differentiate_on_R 2/x^2 --------------";
2.267 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
2.268 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
2.269 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
2.270 states:=[];
2.271 CalcTree
2.272 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
2.273 @@ -578,7 +571,7 @@
2.274 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
2.275 else error "diff.sml: differentiate_on_R 2/x^2 changed";
2.276
2.277 -"-----------------------------------------------------------------";
2.278 +"---------------------------------------------------------";
2.279 states:=[];
2.280 CalcTree
2.281 [(["functionTerm (x^3 * x^5)",
2.282 @@ -601,9 +594,9 @@
2.283 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
2.284
2.285
2.286 -"----------- autoCalculate diff after_simplification -------------";
2.287 -"----------- autoCalculate diff after_simplification -------------";
2.288 -"----------- autoCalculate diff after_simplification -------------";
2.289 +"----------- autoCalculate diff after_simplification ----";
2.290 +"----------- autoCalculate diff after_simplification ----";
2.291 +"----------- autoCalculate diff after_simplification ----";
2.292 states:=[];
2.293 CalcTree
2.294 [(["functionTerm (x^3 * x^5)",
2.295 @@ -623,7 +616,7 @@
2.296 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
2.297 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
2.298
2.299 -"-----------------------------------------------------------------";
2.300 +"--------------------------------------------------------";
2.301 states:=[];
2.302 CalcTree
2.303 [(["functionTerm ((x^3)^5)",
2.304 @@ -638,10 +631,9 @@
2.305 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
2.306
2.307
2.308 -
2.309 -"----------- autoCalculate differentiate_equality ----------------";
2.310 -"----------- autoCalculate differentiate_equality ----------------";
2.311 -"----------- autoCalculate differentiate_equality ----------------";
2.312 +"----------- autoCalculate differentiate_equality -------";
2.313 +"----------- autoCalculate differentiate_equality -------";
2.314 +"----------- autoCalculate differentiate_equality -------";
2.315 states:=[];
2.316 CalcTree
2.317 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"],
2.318 @@ -653,26 +645,27 @@
2.319 val ((pt,p),_) = get_calc 1; show_pt pt;
2.320
2.321
2.322 -"----------- tests for examples ----------------------------------";
2.323 -"----------- tests for examples ----------------------------------";
2.324 -"----------- tests for examples ----------------------------------";
2.325 +"----------- tests for examples -------------------------";
2.326 +"----------- tests for examples -------------------------";
2.327 +"----------- tests for examples -------------------------";
2.328 "----- parse errors";
2.329 -(*str2term "F = sqrt( y^2 - O) * (z + O^2)";
2.330 -str2term "O";*)
2.331 -str2term "OO";
2.332 +(*str2term "F = sqrt( y^^^2 - O) * (z + O^^^2)";
2.333 +str2term "O";
2.334 +str2term "OO"; ---errors*)
2.335 +str2term "OOO";
2.336
2.337 "----- thm 'diff_prod_const'";
2.338 val subs = [(str2term "bdv", str2term "l")];
2.339 -val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))";
2.340 +val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))";
2.341 (*
2.342 trace_rewrite := true;
2.343 rewrite_inst_ (theory "Isac") tless_true erls_diff true subs diff_prod_const f;
2.344 trace_rewrite := false;
2.345 *)
2.346
2.347 -"------------inform for x^2+x+1 ----------------------------------";
2.348 -"------------inform for x^2+x+1 ----------------------------------";
2.349 -"------------inform for x^2+x+1 ----------------------------------";
2.350 +"------------inform for x^2+x+1 -------------------------";
2.351 +"------------inform for x^2+x+1 -------------------------";
2.352 +"------------inform for x^2+x+1 -------------------------";
2.353 states:=[];
2.354 CalcTree
2.355 [(["functionTerm (x^2 + x + 1)",
2.356 @@ -690,3 +683,4 @@
2.357 val ((pt,p),_) = get_calc 1; show_pt pt;
2.358 if existpt' ([3], Res) pt then ()
2.359 else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";
2.360 +