1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: Knowledge/polyeq-1.sml
1.5 +(* Title: Knowledge/polyeq- 1.sml
1.6 testexamples for PolyEq, poynomial equations and equational systems
1.7 Author: Richard Lang 2003
1.8 (c) due to copyright terms
1.9 @@ -9,36 +9,36 @@
1.10 "-----------------------------------------------------------------";
1.11 "table of contents -----------------------------------------------";
1.12 "-----------------------------------------------------------------";
1.13 -"------ polyeq-1.sml ---------------------------------------------";
1.14 +"------ polyeq- 1.sml ---------------------------------------------";
1.15 "----------- tests on predicates in problems ---------------------";
1.16 "----------- test matching problems ------------------------------";
1.17 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.18 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.19 "----------- lin.eq degree_0 -------------------------------------";
1.20 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.21 -"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.22 -"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.23 -"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.24 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.25 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.26 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.27 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.28 -"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.29 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.30 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.31 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.32 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.33 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.34 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.35 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.36 -"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.37 -"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.38 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.39 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.40 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.41 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.42 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.43 -"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.44 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.45 "-----------------------------------------------------------------";
1.46 -"------ polyeq-2.sml ---------------------------------------------";
1.47 +"------ polyeq- 2.sml ---------------------------------------------";
1.48 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.49 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.50 -"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.51 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.52 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.53 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.54 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.55 "----------- rls make_polynomial_in ------------------------------";
1.56 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.57 @@ -49,9 +49,8 @@
1.58 "----------- tests on predicates in problems ---------------------";
1.59 "----------- tests on predicates in problems ---------------------";
1.60 "----------- tests on predicates in problems ---------------------";
1.61 -(* Rewrite.trace_on:=true;
1.62 - Rewrite.trace_on:=false;
1.63 -*)
1.64 +Rewrite.trace_on:=true; (*true false*)
1.65 +
1.66 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.67 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.68 if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
1.69 @@ -67,12 +66,12 @@
1.70 if (UnparseC.term t) = "False" then ()
1.71 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.72
1.73 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x \<up> 2) is_poly_in x";
1.74 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
1.75 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.76 if (UnparseC.term t) = "True" then ()
1.77 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.78
1.79 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
1.80 + val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
1.81 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.82 if (UnparseC.term t) = "True" then ()
1.83 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.84 @@ -131,44 +130,44 @@
1.85 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.86 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.87 (*##################################################################################
1.88 ------------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.89 +----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.90
1.91 (*Aufgabe zum Einstieg in die Arbeit...*)
1.92 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
1.93 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.94 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.95 UnparseC.term t;
1.96 - "a * b + (-1 * (a * x) + (-1 * (b * x) + x \<up> 2)) = 0";
1.97 + "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
1.98 val SOME (t,_) =
1.99 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.100 UnparseC.term t;
1.101 - "x \<up> 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.102 + "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
1.103 (* bei Verwendung von "size_of-term" nach MG :*)
1.104 -(*"x \<up> 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
1.105 +(*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
1.106
1.107 (*wir holen 'a' wieder aus der Klammerung heraus...*)
1.108 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
1.109 UnparseC.term t;
1.110 - "x \<up> 2 + -1 * b * x + -1 * x * a + b * a = 0";
1.111 -(* "x \<up> 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.112 + "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
1.113 +(* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
1.114
1.115 val SOME (t,_) =
1.116 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.117 UnparseC.term t;
1.118 - "x \<up> 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.119 + "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
1.120 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.121 - "x \<up> 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.122 + "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
1.123
1.124 (*das rewriting l"asst sich beobachten mit
1.125 -Rewrite.trace_on := false;
1.126 +Rewrite.trace_on := false; (*true false*)
1.127 *)
1.128
1.129 -"------15.11.02 --------------------------";
1.130 +"------ 15.11.02 --------------------------";
1.131 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
1.132 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
1.133 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
1.134
1.135 -Rewrite.trace_on := false;
1.136 +Rewrite.trace_on := false; (*true false*)
1.137 (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.138 val SOME (t,_) =
1.139 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.140 @@ -243,12 +242,12 @@
1.141 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
1.142 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.143
1.144 - val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.145 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.146 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.147 ord_make_polynomial_in true thy substx (aa, bb);
1.148 true; (* => LESS *)
1.149
1.150 - val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.151 + val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
1.152 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.153 ord_make_polynomial_in true thy substa (aa, bb);
1.154 false; (* => GREATER *)
1.155 @@ -269,14 +268,14 @@
1.156 if UnparseC.term t' = "a + b + x" then ()
1.157 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.158
1.159 - val ppp' = "-6 + -5*x + x \<up> 3 + -1*x \<up> 2 + -1*x \<up> 3 + -14*x \<up> 2";
1.160 + val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
1.161 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.162 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.163 -if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
1.164 +if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.165 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.166
1.167 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.168 -if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
1.169 +if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.170 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.171
1.172 val ttt' = "(3*x + 5)/18";
1.173 @@ -300,7 +299,7 @@
1.174 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
1.175 ["PolyEq", "solve_d0_polyeq_equation"]);
1.176 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
1.177 -TODO: change to "equality (x + -1*x = (0::real))"
1.178 +TODO: change to "equality (x + - 1*x = (0::real))"
1.179 and search for an appropriate problem and method.
1.180
1.181 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.182 @@ -332,7 +331,7 @@
1.183 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.184 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.185 "----- d2_pqformula1 ------!!!!";
1.186 -val fmz = ["equality (-1/8 + (-1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
1.187 +val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
1.188 val (dI',pI',mI') =
1.189 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
1.190 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.191 @@ -348,21 +347,21 @@
1.192 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.193 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.194
1.195 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.196 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.197 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.198 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.199 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.200
1.201 if p = ([], Res) andalso
1.202 - f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]" then
1.203 - case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
1.204 -else error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
1.205 + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
1.206 + case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
1.207 +else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
1.208
1.209 -"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.210 -"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.211 -"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.212 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.213 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.214 +"----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.215 "----- d2_pqformula1_neg ------";
1.216 -val fmz = ["equality (2 +(-1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
1.217 +val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
1.218 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.219 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.220 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.221 @@ -379,15 +378,15 @@
1.222 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.223 val asm = Ctree.get_assumptions pt p;
1.224 if f2str f = "[]" andalso
1.225 - UnparseC.terms asm = "[\"lhs (2 + -1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
1.226 - "\"lhs (2 + -1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
1.227 -else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x \<up> 2 = 0";
1.228 + UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
1.229 + "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
1.230 +else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
1.231
1.232 -"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.233 -"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.234 -"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.235 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.236 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.237 +"----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.238 "----- d2_pqformula2 ------";
1.239 -val fmz = ["equality (-2 +(-1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.240 +val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.241 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.242 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.243 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.244 @@ -400,16 +399,16 @@
1.245 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.246 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.247 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.248 -case f of Test_Out.FormKF "[x = 2, x = -1]" => ()
1.249 - | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.250 +case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
1.251 + | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
1.252
1.253
1.254 -"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.255 -"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.256 -"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.257 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.258 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.259 +"----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.260 "----- d2_pqformula3 ------";
1.261 (*EP-9*)
1.262 -val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.263 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.264 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.265 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.267 @@ -422,8 +421,8 @@
1.268 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.269 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.270 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.271 -case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.272 - | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.273 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.274 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
1.275
1.276
1.277 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.278 @@ -446,11 +445,11 @@
1.279 "TODO 2 + x + x \<up> 2 = 0";
1.280 "TODO 2 + x + x \<up> 2 = 0";
1.281
1.282 -"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.283 -"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.284 -"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.285 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.286 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.287 +"----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.288 "----- d2_pqformula4 ------";
1.289 -val fmz = ["equality (-2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.290 +val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.291 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.292 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.293 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.294 @@ -462,8 +461,8 @@
1.295 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.296 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.297 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.298 -case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.299 - | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = -2]";
1.300 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.301 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
1.302
1.303 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.304 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.305 @@ -481,8 +480,8 @@
1.306 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.307 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.309 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.310 - | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.311 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.312 + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
1.313
1.314 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.315 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.316 @@ -500,14 +499,14 @@
1.317 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.318 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.319 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.320 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.321 - | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.322 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.323 + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
1.324
1.325 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.326 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.327 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.328 "----- d2_pqformula7 ------";
1.329 -(*EP-10*)
1.330 +(*EP- 10*)
1.331 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.332 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.333 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.334 @@ -520,8 +519,8 @@
1.335 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.336 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.337 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.338 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.339 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.340 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.341 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.342
1.343 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.344 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.345 @@ -539,8 +538,8 @@
1.346 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.347 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.348 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.349 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.350 - | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.351 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.352 + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
1.353
1.354 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.355 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.356 @@ -557,8 +556,8 @@
1.357 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.358 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.359 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.360 -case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.361 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.362 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.363 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
1.364
1.365
1.366 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.367 @@ -582,7 +581,7 @@
1.368 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.369 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.370 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.371 -val fmz = ["equality (-1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.372 +val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.373 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.374 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.375 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.376 @@ -593,13 +592,13 @@
1.377 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.378 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.379 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.380 -case f of Test_Out.FormKF "[x = 1, x = -1 / 2]" => ()
1.381 - | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.382 +case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
1.383 + | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
1.384
1.385 -"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.386 -"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.387 -"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.388 -val fmz = ["equality (1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.389 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.390 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.391 +"----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.392 +val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.393 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.394 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.395 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.396 @@ -610,16 +609,16 @@
1.397 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.398 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.399 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.400 -"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.401 -"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.402 -"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.403 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.404 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.405 +"TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
1.406
1.407
1.408 -"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.409 -"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.410 -"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.411 -(*EP-11*)
1.412 -val fmz = ["equality (-1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.413 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.414 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.415 +"----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.416 +(*EP- 11*)
1.417 +val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.418 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.419 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.420 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.421 @@ -632,8 +631,8 @@
1.422 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.423
1.424 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.425 -case f of Test_Out.FormKF "[x = 1 / 2, x = -1]" => ()
1.426 - | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.427 +case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
1.428 + | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
1.429
1.430
1.431 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.432 @@ -656,7 +655,7 @@
1.433 "TODO 1 + x + 2*x \<up> 2 = 0";
1.434
1.435
1.436 -val fmz = ["equality (-2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.437 +val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.438 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.439 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.440 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.441 @@ -667,8 +666,8 @@
1.442 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.443 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.444 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.445 -case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.446 - | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.447 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.448 + | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
1.449
1.450 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.451 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.452 @@ -685,8 +684,8 @@
1.453 "TODO 2 + 1*x + x \<up> 2 = 0";
1.454 "TODO 2 + 1*x + x \<up> 2 = 0";
1.455
1.456 -(*EP-12*)
1.457 -val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.458 +(*EP- 12*)
1.459 +val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.460 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.461 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.462 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.463 @@ -697,8 +696,8 @@
1.464 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.465 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.466 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.467 -case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.468 - | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.469 +case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
1.470 + | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
1.471
1.472 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.473 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.474 @@ -715,7 +714,7 @@
1.475 "TODO 2 + x + x \<up> 2 = 0";
1.476 "TODO 2 + x + x \<up> 2 = 0";
1.477
1.478 -(*EP-13*)
1.479 +(*EP- 13*)
1.480 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.481 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.482 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.483 @@ -727,8 +726,8 @@
1.484 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.485 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.486 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.487 -case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.488 - | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.489 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.490 + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
1.491
1.492 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.493 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.494 @@ -744,7 +743,7 @@
1.495 "TODO 8+ 2*x \<up> 2 = 0";
1.496 "TODO 8+ 2*x \<up> 2 = 0";
1.497
1.498 -(*EP-14*)
1.499 +(*EP- 14*)
1.500 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.501 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.503 @@ -755,8 +754,8 @@
1.504 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.505 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.506 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.507 -case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.508 - | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.509 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.510 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
1.511
1.512
1.513 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.514 @@ -772,7 +771,7 @@
1.515 "TODO 4+ x \<up> 2 = 0";
1.516 "TODO 4+ x \<up> 2 = 0";
1.517
1.518 -(*EP-15*)
1.519 +(*EP- 15*)
1.520 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.521 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.522 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.523 @@ -784,8 +783,8 @@
1.524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.526 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.527 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.528 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.529 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.530 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.531
1.532 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.533 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.534 @@ -798,10 +797,10 @@
1.535 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.536 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.537 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.538 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.539 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.540 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.541 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.542
1.543 -(*EP-16*)
1.544 +(*EP- 16*)
1.545 val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.546 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.547 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.548 @@ -813,8 +812,8 @@
1.549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.550 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.551 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.552 -case f of Test_Out.FormKF "[x = 0, x = -1 / 2]" => ()
1.553 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.554 +case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
1.555 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
1.556
1.557 (*EP-//*)
1.558 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.559 @@ -828,8 +827,8 @@
1.560 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.561 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.562 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.563 -case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.564 - | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.565 +case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
1.566 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
1.567
1.568
1.569 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.570 @@ -863,30 +862,30 @@
1.571 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.572 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.573 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1.574 - -1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.575 + - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.576 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.577 -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.578 - -1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
1.579 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.580 + - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
1.581 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.582 -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.583 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
1.584 +(*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.585 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
1.586 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.587 -(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
1.588 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
1.589 +(*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
1.590 + x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
1.591 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
1.592 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.593 -(*"x = -2 | x = 4" nxt = Or_to_List*)
1.594 +(*"x = - 2 | x = 4" nxt = Or_to_List*)
1.595 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.596 -(*"[x = -2, x = 4]" nxt = Check_Postcond*)
1.597 +(*"[x = - 2, x = 4]" nxt = Check_Postcond*)
1.598 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.599 (* FIXXXME
1.600 - case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
1.601 - | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.602 + case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
1.603 + | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1.604 *)
1.605 if f2str f =
1.606 -"[x = -1 * -1 + -1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))]"
1.607 -(*"[x = -1 * -1 + -1 * sqrt (1 \<up> 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 \<up> 2 - -8))]"*)
1.608 -then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.609 +"[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))]"
1.610 +(*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1.611 +then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1.612
1.613
1.614 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.615 @@ -910,31 +909,31 @@
1.616 val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1.617 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.618 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.619 - "\n2 / 2 - x = -1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.620 + "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.621
1.622 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.623 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.624 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.625 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.626 - "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.627 + "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.628
1.629 val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1.630 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.631 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.632 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.633 + "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.634
1.635 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.636 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.637 -UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1.638 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.639 +UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1.640 + "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.641
1.642 val rls = calculate_RootRat;
1.643 val SOME (t,asm) = rewrite_set_ thy true rls t;
1.644 if UnparseC.term t =
1.645 - "-1 * x = -1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"
1.646 -(*"-1 * x = -1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
1.647 + "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"
1.648 +(*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
1.649 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.650 -(*SHOULD BE: UnparseC.term = "x = -2 | x = 4;*)
1.651 +(*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
1.652
1.653
1.654 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.655 @@ -963,10 +962,10 @@
1.656 (*Apply_Method ("PolyEq", "complete_square")*)
1.657 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.658
1.659 -"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.660 -"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.661 -"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.662 - val fmz = ["equality (-16 + 4*x + 2*x \<up> 2 = 0)",
1.663 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.664 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.665 +"----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.666 + val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
1.667 "solveFor x", "solutions L"];
1.668 val (dI',pI',mI') =
1.669 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],