1.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -9,11 +9,11 @@
1.4 "-----------------------------------------------------------------";
1.5 "table of contents -----------------------------------------------";
1.6 "-----------------------------------------------------------------";
1.7 -"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.8 -"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.9 -"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.10 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.11 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.12 +"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.13 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.14 -"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.15 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.16 "----------- rls make_polynomial_in ------------------------------";
1.17 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.18 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.19 @@ -21,10 +21,10 @@
1.20 "-----------------------------------------------------------------";
1.21
1.22
1.23 -"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.24 -"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.25 -"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.26 - val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
1.27 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.28 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.29 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.30 + val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",
1.31 "solveFor x", "solutions L"];
1.32 val (dI',pI',mI') =
1.33 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.34 @@ -53,16 +53,16 @@
1.35 Form'
1.36 (Test_Out.FormKF
1.37 (~1,EdUndef,0,Nundef,
1.38 - "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
1.39 + "[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.40 => ()
1.41 - | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
1.42 + | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0";
1.43 this will be simplified [x = a, x = b] to by Factor.ML*)
1.44
1.45
1.46 -"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.47 -"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.48 -"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.49 - val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.50 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.51 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.52 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.53 + val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.54 "solveFor x", "solutions L"];
1.55 val (dI',pI',mI') =
1.56 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.57 @@ -86,10 +86,10 @@
1.58 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.59 *)
1.60
1.61 -"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.62 -"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.63 -"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.64 -val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.65 +"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.66 +"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.67 +"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.68 +val fmz = ["equality (-147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.69 "solveFor x", "solutions L"];
1.70 val (dI',pI',mI') =
1.71 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.72 @@ -150,11 +150,11 @@
1.73 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1.74
1.75
1.76 -"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.77 -"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.78 -"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.79 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.80 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.81 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.82 (*is in rlang.sml, too*)
1.83 -val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1.84 +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",
1.85 "solveFor x", "solutions L"];
1.86 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.87 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.88 @@ -190,11 +190,11 @@
1.89 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1.90
1.91
1.92 -" -4 + x^^^2 =0 ";
1.93 -" -4 + x^^^2 =0 ";
1.94 -" -4 + x^^^2 =0 ";
1.95 -val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x", "solutions L"];
1.96 -(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x", "solutions L"];*)
1.97 +" -4 + x \<up> 2 =0 ";
1.98 +" -4 + x \<up> 2 =0 ";
1.99 +" -4 + x \<up> 2 =0 ";
1.100 +val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];
1.101 +(* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)
1.102 (*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*)
1.103 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]);
1.104 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.105 @@ -223,10 +223,10 @@
1.106 (*WN.19.3.03 ---^-*)
1.107
1.108 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");
1.109 -val t = TermC.str2term "y ^^^ 2 + -2 * (x * p) = 0";
1.110 +val t = TermC.str2term "y \<up> 2 + -2 * (x * p) = 0";
1.111 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.112 -if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()
1.113 -else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";
1.114 +if UnparseC.term t' = "y \<up> 2 + -2 * x * p = 0" then ()
1.115 +else error "make_polynomial_in (y \<up> 2 + -2 * (x * p) = 0)";
1.116
1.117 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");
1.118 val t = TermC.str2term
1.119 @@ -247,11 +247,11 @@
1.120
1.121 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");
1.122 val t = TermC.str2term
1.123 -"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1.124 +"A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";
1.125 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1.126 (* the invisible parentheses are as expected *)
1.127
1.128 -val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1.129 +val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";
1.130 Rewrite.trace_on:=(*true*)false;
1.131 rewrite_set_ thy false expand_binoms t;
1.132 Rewrite.trace_on:=false;
1.133 @@ -276,7 +276,7 @@
1.134 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.135 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.136 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.137 -val t = TermC.str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";
1.138 +val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";
1.139 val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];
1.140 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;
1.141 (* steps in rls d2_polyeq_bdv_only_simplify:*)