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