1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.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 @@ -11,8 +11,8 @@
1.10 "-----------------------------------------------------------------";
1.11 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.12 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.13 -"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.14 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.15 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.16 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.17 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.18 "----------- rls make_polynomial_in ------------------------------";
1.19 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.20 @@ -53,7 +53,7 @@
1.21 Form'
1.22 (Test_Out.FormKF
1.23 (~1,EdUndef,0,Nundef,
1.24 - "[x = (a + b) / 2 + -1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]"))
1.25 + "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]"))
1.26 => ()
1.27 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";
1.28 this will be simplified [x = a, x = b] to by Factor.ML*)
1.29 @@ -81,15 +81,15 @@
1.30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.33 -(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1.34 +(*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]"
1.35 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1.36 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.37 *)
1.38
1.39 -"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.40 -"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.41 -"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.42 -val fmz = ["equality (-147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.43 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.44 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.45 +"----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.46 +val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.47 "solveFor x", "solutions L"];
1.48 val (dI',pI',mI') =
1.49 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.50 @@ -103,19 +103,19 @@
1.51 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.52 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.53 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.54 -(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1.55 +(*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]"
1.56 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1.57 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1.58 *)
1.59 -if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1.60 +if f2str f = "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" then ()
1.61 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1.62
1.63
1.64 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.65 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.66 -"----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.67 -(*EP-17 Schalk_I_p86_n5*)
1.68 -val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)", "solveFor x", "solutions L"];
1.69 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.70 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.71 +"----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
1.72 +(*EP- 17 Schalk_I_p86_n5*)
1.73 +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"];
1.74 (* Refine.refine fmz ["univariate", "equation"];
1.75 *)
1.76 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.77 @@ -206,8 +206,8 @@
1.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.81 -case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.82 - | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1.83 +case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
1.84 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]";
1.85
1.86 "----------- rls make_polynomial_in ------------------------------";
1.87 "----------- rls make_polynomial_in ------------------------------";
1.88 @@ -215,35 +215,35 @@
1.89 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1.90 (*WN.19.3.03 ---v-*)
1.91 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");
1.92 -val t = TermC.str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1.93 +val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0";
1.94 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.95 -if UnparseC.term t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()
1.96 -else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";
1.97 -"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1.98 +if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then ()
1.99 +else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)";
1.100 +"- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0";
1.101 (*WN.19.3.03 ---^-*)
1.102
1.103 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
1.104 -val t = TermC.str2term "y \<up> 2 + -2 * (x * p) = 0";
1.105 +val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";
1.106 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.107 -if UnparseC.term t' = "y \<up> 2 + -2 * x * p = 0" then ()
1.108 -else error "make_polynomial_in (y \<up> 2 + -2 * (x * p) = 0)";
1.109 +if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()
1.110 +else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";
1.111
1.112 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
1.113 val t = TermC.str2term
1.114 -"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
1.115 +"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1 * (x1 * (y2 * (1 / 2))) + - 1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + - 1 * (y3 * (1 / 2 * x2)) = 0";
1.116 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.117 if UnparseC.term t' =
1.118 -"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) +\n-1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n-1 * y3 * (1 / 2) * x2 =\n0"
1.119 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0"
1.120 then ()
1.121 -else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
1.122 +else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
1.123 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
1.124
1.125 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1.126 if UnparseC.term t' =
1.127 -"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 + -1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n-1 * y3 * x2 / 2 =\n0"
1.128 +"A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0"
1.129 then ()
1.130 -else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";
1.131 -"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
1.132 +else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1...";
1.133 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) + - 1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - 1 * y3 * (1 / 2)) * x2 = 0";
1.134
1.135 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
1.136 val t = TermC.str2term
1.137 @@ -262,7 +262,7 @@
1.138 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.139 reset_states ();
1.140 CalcTree
1.141 -[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)", "solveFor x", "solutions L"],
1.142 +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"],
1.143 ("PolyEq",["univariate", "equation"],["no_met"]))];
1.144 Iterator 1;
1.145 moveActiveRoot 1;