1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -16,30 +16,30 @@
1.4 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.5 "----------- lin.eq degree_0 -------------------------------------";
1.6 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.7 -"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.8 -"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.9 -"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.10 -"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.11 -"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.12 -"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.13 -"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.14 -"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.15 -"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.16 -"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.17 -"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.18 -"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.19 -"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.20 -"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.21 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.22 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.23 -"----------- (-16 + 4*x + 2*x^^^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 (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.30 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.31 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.32 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.33 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.34 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.35 +"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.36 +"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.37 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.38 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.39 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.40 +"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.41 "-----------------------------------------------------------------";
1.42 "------ polyeq-2.sml ---------------------------------------------";
1.43 -"----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.44 -"----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.45 -"----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.46 +"----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.47 +"----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1.48 +"----------- (-147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.49 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.50 -"----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.51 +"----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
1.52 "----------- rls make_polynomial_in ------------------------------";
1.53 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1.54 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
1.55 @@ -52,12 +52,12 @@
1.56 (* Rewrite.trace_on:=true;
1.57 Rewrite.trace_on:=false;
1.58 *)
1.59 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.60 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.61 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.62 - if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then ()
1.63 + if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
1.64 else error "polyeq.sml: diff.behav. in lhs";
1.65
1.66 - val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.67 + val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.68 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.69 if (UnparseC.term t) = "True" then ()
1.70 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.71 @@ -67,23 +67,23 @@
1.72 if (UnparseC.term t) = "False" then ()
1.73 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.74
1.75 - val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.76 + val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (-1)*2*x + x \<up> 2) is_poly_in x";
1.77 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.78 if (UnparseC.term t) = "True" then ()
1.79 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.80
1.81 - val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.82 + 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.83 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.84 if (UnparseC.term t) = "True" then ()
1.85 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.86
1.87
1.88 - val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.89 + val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
1.90 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.91 if (UnparseC.term t) = "True" then ()
1.92 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.93
1.94 - val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.95 + val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.96 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.97 if (UnparseC.term t) = "True" then ()
1.98 else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.99 @@ -94,13 +94,13 @@
1.100 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.101
1.102 val t4 = (Thm.term_of o the o (TermC.parse thy))
1.103 - "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.104 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
1.105 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.106 if (UnparseC.term t) = "False" then ()
1.107 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.108
1.109 val t5 = (Thm.term_of o the o (TermC.parse thy))
1.110 - "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.111 + "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.112 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.113 if (UnparseC.term t) = "True" then ()
1.114 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.115 @@ -108,21 +108,21 @@
1.116 "----------- test matching problems --------------------------0---";
1.117 "----------- test matching problems --------------------------0---";
1.118 "----------- test matching problems --------------------------0---";
1.119 -val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.120 +val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.121 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
1.122 M_Match.Matches' {Find = [Correct "solutions L"],
1.123 With = [],
1.124 - Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.125 - Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
1.126 - Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
1.127 + Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
1.128 + Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
1.129 + Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
1.130 Relate = []}
1.131 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
1.132
1.133 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
1.134 M_Match.Matches' {Find = [Correct "solutions L"],
1.135 With = [],
1.136 - Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
1.137 - Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
1.138 + Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
1.139 + Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
1.140 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
1.141 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
1.142
1.143 @@ -134,30 +134,30 @@
1.144 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
1.145
1.146 (*Aufgabe zum Einstieg in die Arbeit...*)
1.147 - val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
1.148 + val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
1.149 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
1.150 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
1.151 UnparseC.term t;
1.152 - "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
1.153 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x \<up> 2)) = 0";
1.154 val SOME (t,_) =
1.155 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.156 UnparseC.term t;
1.157 - "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.158 + "x \<up> 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
1.159 (* bei Verwendung von "size_of-term" nach MG :*)
1.160 -(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
1.161 +(*"x \<up> 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
1.162
1.163 (*wir holen 'a' wieder aus der Klammerung heraus...*)
1.164 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
1.165 UnparseC.term t;
1.166 - "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
1.167 -(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.168 + "x \<up> 2 + -1 * b * x + -1 * x * a + b * a = 0";
1.169 +(* "x \<up> 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
1.170
1.171 val SOME (t,_) =
1.172 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
1.173 UnparseC.term t;
1.174 - "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.175 + "x \<up> 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
1.176 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
1.177 - "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.178 + "x \<up> 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.179
1.180 (*das rewriting l"asst sich beobachten mit
1.181 Rewrite.trace_on := false;
1.182 @@ -178,23 +178,23 @@
1.183 UnparseC.term t;
1.184 "1 + b * x + x * a";
1.185
1.186 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a^^^2";
1.187 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
1.188 val SOME (t,_) =
1.189 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.190 UnparseC.term t;
1.191 val SOME (t,_) =
1.192 rewrite_set_ thy false discard_parentheses t;
1.193 UnparseC.term t;
1.194 -"1 + (x + b * x) * a + a ^^^ 2";
1.195 +"1 + (x + b * x) * a + a \<up> 2";
1.196
1.197 - val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
1.198 + val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
1.199 val SOME (t,_) =
1.200 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.201 UnparseC.term t;
1.202 val SOME (t,_) =
1.203 rewrite_set_ thy false discard_parentheses t;
1.204 UnparseC.term t;
1.205 -"1 + b * a + (7 + x) * a ^^^ 2";
1.206 +"1 + b * a + (7 + x) * a \<up> 2";
1.207
1.208 (* MG2003
1.209 Prog_Expr.thy grundlegende Algebra
1.210 @@ -207,14 +207,14 @@
1.211 get_thm Termorder.thy "bdv_n_collect";
1.212 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
1.213 *)
1.214 - val t = (Thm.term_of o the o (TermC.parse thy)) "a ^^^2 * x + 7 * a^^^2";
1.215 + val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
1.216 val SOME (t,_) =
1.217 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
1.218 UnparseC.term t;
1.219 val SOME (t,_) =
1.220 rewrite_set_ thy false discard_parentheses t;
1.221 UnparseC.term t;
1.222 -"(7 + x) * a ^^^ 2";
1.223 +"(7 + x) * a \<up> 2";
1.224
1.225 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
1.226
1.227 @@ -244,12 +244,12 @@
1.228 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
1.229
1.230 val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.231 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
1.232 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.233 ord_make_polynomial_in true thy substx (aa, bb);
1.234 true; (* => LESS *)
1.235
1.236 val aa = (Thm.term_of o the o (TermC.parse thy)) "-1 * a * x";
1.237 - val bb = (Thm.term_of o the o (TermC.parse thy)) "x^^^3";
1.238 + val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
1.239 ord_make_polynomial_in true thy substa (aa, bb);
1.240 false; (* => GREATER *)
1.241
1.242 @@ -269,14 +269,14 @@
1.243 if UnparseC.term t' = "a + b + x" then ()
1.244 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.245
1.246 - val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
1.247 + val ppp' = "-6 + -5*x + x \<up> 3 + -1*x \<up> 2 + -1*x \<up> 3 + -14*x \<up> 2";
1.248 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.249 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.250 -if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.251 +if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
1.252 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.253
1.254 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.255 -if UnparseC.term t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
1.256 +if UnparseC.term t' = "-6 + -5 * x + -15 * x \<up> 2 + 0" then ()
1.257 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.258
1.259 val ttt' = "(3*x + 5)/18";
1.260 @@ -332,7 +332,7 @@
1.261 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.262 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.263 "----- d2_pqformula1 ------!!!!";
1.264 -val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z", "solutions L"];
1.265 +val fmz = ["equality (-1/8 + (-1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
1.266 val (dI',pI',mI') =
1.267 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
1.268 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.269 @@ -355,14 +355,14 @@
1.270
1.271 if p = ([], Res) andalso
1.272 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]" then
1.273 - case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z^^^2 = (0::real)) CHANGED 1"
1.274 -else error "(-1/8 + (-1/4)*z + z^^^2 = (0::real)) CHANGED 2";
1.275 + case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
1.276 +else error "(-1/8 + (-1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
1.277
1.278 -"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.279 -"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.280 -"----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.281 +"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.282 +"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.283 +"----------- equality (2 +(-1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
1.284 "----- d2_pqformula1_neg ------";
1.285 -val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x", "solutions L"];
1.286 +val fmz = ["equality (2 +(-1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
1.287 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.288 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.289 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.290 @@ -379,15 +379,15 @@
1.291 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.292 val asm = Ctree.get_assumptions pt p;
1.293 if f2str f = "[]" andalso
1.294 - UnparseC.terms asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\", " ^
1.295 - "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
1.296 -else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.297 + UnparseC.terms asm = "[\"lhs (2 + -1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
1.298 + "\"lhs (2 + -1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
1.299 +else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x \<up> 2 = 0";
1.300
1.301 -"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.302 -"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.303 -"----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
1.304 +"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.305 +"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.306 +"----------- equality (-2 +(-1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
1.307 "----- d2_pqformula2 ------";
1.308 -val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.309 +val fmz = ["equality (-2 +(-1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.310 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.311 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.312 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.313 @@ -404,12 +404,12 @@
1.314 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.315
1.316
1.317 -"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.318 -"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.319 -"----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
1.320 +"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.321 +"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.322 +"----------- equality (-2 + x + x \<up> 2 = 0) ---------------------------------------------------";
1.323 "----- d2_pqformula3 ------";
1.324 (*EP-9*)
1.325 -val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.326 +val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.327 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.328 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.329 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.330 @@ -426,11 +426,11 @@
1.331 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.332
1.333
1.334 -"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.335 -"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.336 -"----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
1.337 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.338 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.339 +"----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
1.340 "----- d2_pqformula3_neg ------";
1.341 -val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.342 +val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.343 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.344 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.345 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.346 @@ -442,15 +442,15 @@
1.347
1.348 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.349 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.350 -"TODO 2 + x + x^^^2 = 0";
1.351 -"TODO 2 + x + x^^^2 = 0";
1.352 -"TODO 2 + x + x^^^2 = 0";
1.353 +"TODO 2 + x + x \<up> 2 = 0";
1.354 +"TODO 2 + x + x \<up> 2 = 0";
1.355 +"TODO 2 + x + x \<up> 2 = 0";
1.356
1.357 -"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.358 -"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.359 -"----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
1.360 +"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.361 +"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.362 +"----------- equality (-2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
1.363 "----- d2_pqformula4 ------";
1.364 -val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.365 +val fmz = ["equality (-2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.366 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.367 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.368 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.369 @@ -463,13 +463,13 @@
1.370 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.371 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.372 case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.373 - | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
1.374 + | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = -2]";
1.375
1.376 -"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.377 -"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.378 -"----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
1.379 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.380 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.381 +"----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
1.382 "----- d2_pqformula5 ------";
1.383 -val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.384 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.385 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.386 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.387 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.388 @@ -484,11 +484,11 @@
1.389 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.390 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.391
1.392 -"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.393 -"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.394 -"----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
1.395 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.396 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.397 +"----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
1.398 "----- d2_pqformula6 ------";
1.399 -val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.400 +val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.401 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.402 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.403 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.404 @@ -503,12 +503,12 @@
1.405 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.406 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.407
1.408 -"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.409 -"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.410 -"----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
1.411 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.412 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.413 +"----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
1.414 "----- d2_pqformula7 ------";
1.415 (*EP-10*)
1.416 -val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.417 +val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.418 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.419 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.420 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.421 @@ -523,11 +523,11 @@
1.422 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.423 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.424
1.425 -"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.426 -"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.427 -"----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
1.428 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.429 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.430 +"----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
1.431 "----- d2_pqformula8 ------";
1.432 -val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.433 +val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.434 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.435 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.436 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.437 @@ -542,11 +542,11 @@
1.438 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.439 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.440
1.441 -"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.442 -"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.443 -"----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
1.444 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.445 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.446 +"----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
1.447 "----- d2_pqformula9 ------";
1.448 -val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x", "solutions L"];
1.449 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.450 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.451 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.452 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.453 @@ -561,11 +561,11 @@
1.454 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.455
1.456
1.457 -"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.458 -"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.459 -"----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
1.460 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.461 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.462 +"----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
1.463 "----- d2_pqformula9_neg ------";
1.464 -val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x", "solutions L"];
1.465 +val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.466 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.467 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
1.468 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.469 @@ -575,14 +575,14 @@
1.470 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.472 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.473 -"TODO 4 + 1*x^^^2 = 0";
1.474 -"TODO 4 + 1*x^^^2 = 0";
1.475 -"TODO 4 + 1*x^^^2 = 0";
1.476 +"TODO 4 + 1*x \<up> 2 = 0";
1.477 +"TODO 4 + 1*x \<up> 2 = 0";
1.478 +"TODO 4 + 1*x \<up> 2 = 0";
1.479
1.480 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.481 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.482 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.483 -val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.484 +val fmz = ["equality (-1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.485 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.486 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.487 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.488 @@ -596,10 +596,10 @@
1.489 case f of Test_Out.FormKF "[x = 1, x = -1 / 2]" => ()
1.490 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.491
1.492 -"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.493 -"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.494 -"----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
1.495 -val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.496 +"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.497 +"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.498 +"----------- equality (1 +(-1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
1.499 +val fmz = ["equality (1 +(-1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.500 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.501 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.503 @@ -610,16 +610,16 @@
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 -"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.508 -"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.509 -"TODO 1 +(-1)*x + 2*x^^^2 = 0";
1.510 +"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.511 +"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.512 +"TODO 1 +(-1)*x + 2*x \<up> 2 = 0";
1.513
1.514
1.515 -"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.516 -"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.517 -"----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
1.518 +"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.519 +"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.520 +"----------- equality (-1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
1.521 (*EP-11*)
1.522 -val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.523 +val fmz = ["equality (-1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.524 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.525 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.526 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.527 @@ -636,10 +636,10 @@
1.528 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.529
1.530
1.531 -"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.532 -"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.533 -"----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
1.534 -val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.535 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.536 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.537 +"----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
1.538 +val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.539 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.540 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.541 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.542 @@ -651,12 +651,12 @@
1.543 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.544 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.545 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.546 -"TODO 1 + x + 2*x^^^2 = 0";
1.547 -"TODO 1 + x + 2*x^^^2 = 0";
1.548 -"TODO 1 + x + 2*x^^^2 = 0";
1.549 +"TODO 1 + x + 2*x \<up> 2 = 0";
1.550 +"TODO 1 + x + 2*x \<up> 2 = 0";
1.551 +"TODO 1 + x + 2*x \<up> 2 = 0";
1.552
1.553
1.554 -val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.555 +val fmz = ["equality (-2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.556 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.557 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.558 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.559 @@ -670,7 +670,7 @@
1.560 case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.561 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.562
1.563 -val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.564 +val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.565 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.566 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.567 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.568 @@ -681,12 +681,12 @@
1.569 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.570 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.571 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.572 -"TODO 2 + 1*x + x^^^2 = 0";
1.573 -"TODO 2 + 1*x + x^^^2 = 0";
1.574 -"TODO 2 + 1*x + x^^^2 = 0";
1.575 +"TODO 2 + 1*x + x \<up> 2 = 0";
1.576 +"TODO 2 + 1*x + x \<up> 2 = 0";
1.577 +"TODO 2 + 1*x + x \<up> 2 = 0";
1.578
1.579 (*EP-12*)
1.580 -val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.581 +val fmz = ["equality (-2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.582 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.583 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.584 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.585 @@ -700,7 +700,7 @@
1.586 case f of Test_Out.FormKF "[x = 1, x = -2]" => ()
1.587 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.588
1.589 -val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.590 +val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.591 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.592 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.593 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.594 @@ -711,12 +711,12 @@
1.595 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.596 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.597 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.598 -"TODO 2 + x + x^^^2 = 0";
1.599 -"TODO 2 + x + x^^^2 = 0";
1.600 -"TODO 2 + x + x^^^2 = 0";
1.601 +"TODO 2 + x + x \<up> 2 = 0";
1.602 +"TODO 2 + x + x \<up> 2 = 0";
1.603 +"TODO 2 + x + x \<up> 2 = 0";
1.604
1.605 (*EP-13*)
1.606 -val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.607 +val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.608 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.609 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.610 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.611 @@ -730,7 +730,7 @@
1.612 case f of Test_Out.FormKF "[x = 2, x = -2]" => ()
1.613 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.614
1.615 -val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.616 +val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.617 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.618 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.619 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.620 @@ -740,12 +740,12 @@
1.621 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.622 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.623 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.624 -"TODO 8+ 2*x^^^2 = 0";
1.625 -"TODO 8+ 2*x^^^2 = 0";
1.626 -"TODO 8+ 2*x^^^2 = 0";
1.627 +"TODO 8+ 2*x \<up> 2 = 0";
1.628 +"TODO 8+ 2*x \<up> 2 = 0";
1.629 +"TODO 8+ 2*x \<up> 2 = 0";
1.630
1.631 (*EP-14*)
1.632 -val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x", "solutions L"];
1.633 +val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.634 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.635 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.636 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.637 @@ -759,7 +759,7 @@
1.638 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.639
1.640
1.641 -val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x", "solutions L"];
1.642 +val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.643 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.644 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.645 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.646 @@ -768,12 +768,12 @@
1.647 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.648 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.649 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.650 -"TODO 4+ x^^^2 = 0";
1.651 -"TODO 4+ x^^^2 = 0";
1.652 -"TODO 4+ x^^^2 = 0";
1.653 +"TODO 4+ x \<up> 2 = 0";
1.654 +"TODO 4+ x \<up> 2 = 0";
1.655 +"TODO 4+ x \<up> 2 = 0";
1.656
1.657 (*EP-15*)
1.658 -val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.659 +val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.660 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.661 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.662 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.663 @@ -787,7 +787,7 @@
1.664 case f of Test_Out.FormKF "[x = 0, x = -1]" => ()
1.665 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.666
1.667 -val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.668 +val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.669 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.670 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.671 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.672 @@ -802,7 +802,7 @@
1.673 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.674
1.675 (*EP-16*)
1.676 -val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x", "solutions L"];
1.677 +val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.678 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.679 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.680 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.681 @@ -817,7 +817,7 @@
1.682 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.683
1.684 (*EP-//*)
1.685 -val fmz = ["equality (x + x^^^2 = 0)", "solveFor x", "solutions L"];
1.686 +val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
1.687 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.688 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
1.689 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.690 @@ -832,15 +832,15 @@
1.691 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.692
1.693
1.694 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.695 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.696 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.697 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.698 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.699 +"----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.700 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.701 see --- val rls = calculate_RootRat > calculate_Rational ---
1.702 calculate_RootRat was a TODO with 2002, requires re-design.
1.703 -see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
1.704 +see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
1.705 *)
1.706 - val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.707 + val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.708 "solveFor x", "solutions L"];
1.709 val (dI',pI',mI') =
1.710 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.711 @@ -853,27 +853,27 @@
1.712 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.713 (*Apply_Method ("PolyEq", "complete_square")*)
1.714 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.715 -(*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.716 +(*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.717 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.718 -(*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
1.719 +(*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
1.720 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.721 -(*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
1.722 +(*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
1.723 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.724 -(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.725 - 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.726 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1.727 + 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
1.728 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.729 -(*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
1.730 - -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.731 +(*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
1.732 + -1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
1.733 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.734 -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.735 - -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
1.736 +(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.737 + -1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
1.738 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.739 -(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
1.740 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
1.741 +(*"-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
1.742 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
1.743 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.744 -(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
1.745 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
1.746 - NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
1.747 +(*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
1.748 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
1.749 + NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
1.750 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.751 (*"x = -2 | x = 4" nxt = Or_to_List*)
1.752 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.753 @@ -884,70 +884,70 @@
1.754 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.755 *)
1.756 if f2str f =
1.757 -"[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
1.758 -(*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
1.759 +"[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.760 +(*"[x = -1 * -1 + -1 * sqrt (1 \<up> 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 \<up> 2 - -8))]"*)
1.761 then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.762
1.763
1.764 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.765 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.766 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
1.767 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.768 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.769 +"----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1.770 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1.771 see --- val rls = calculate_RootRat > calculate_Rational ---*)
1.772 val thy = @{theory PolyEq};
1.773 val ctxt = Proof_Context.init_global thy;
1.774 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1.775 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
1.776 +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1.777
1.778 val rls = complete_square;
1.779 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.780 -UnparseC.term t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
1.781 +UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
1.782
1.783 val thm = ThmC.numerals_to_Free @{thm square_explicit1};
1.784 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.785 -UnparseC.term t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
1.786 +UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
1.787
1.788 val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1.789 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.790 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.791 - "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.792 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.793 + "\n2 / 2 - x = -1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.794
1.795 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.796 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.797 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.798 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.799 - "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
1.800 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.801 + "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8)";
1.802
1.803 val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1.804 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.805 -UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.806 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.807 +UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1.808 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.809
1.810 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1.811 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.812 -UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
1.813 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
1.814 +UnparseC.term t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1.815 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) \<up> 2 - -8))";
1.816
1.817 val rls = calculate_RootRat;
1.818 val SOME (t,asm) = rewrite_set_ thy true rls t;
1.819 if UnparseC.term t =
1.820 - "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
1.821 -(*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
1.822 -then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.823 + "-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.824 +(*"-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.825 +then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1.826 (*SHOULD BE: UnparseC.term = "x = -2 | x = 4;*)
1.827
1.828
1.829 -"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.830 -"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.831 -"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.832 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.833 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.834 +"-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.835 "---- test the erls ----";
1.836 - val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2)^^^2 - 1";
1.837 + val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
1.838 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.839 val t' = UnparseC.term t;
1.840 (*if t'= "HOL.True" then ()
1.841 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.842 (* *)
1.843 - val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.844 + val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
1.845 "solveFor x", "solutions L"];
1.846 val (dI',pI',mI') =
1.847 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1.848 @@ -963,10 +963,10 @@
1.849 (*Apply_Method ("PolyEq", "complete_square")*)
1.850 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.851
1.852 -"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.853 -"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.854 -"----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.855 - val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1.856 +"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.857 +"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.858 +"----------- (-16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1.859 + val fmz = ["equality (-16 + 4*x + 2*x \<up> 2 = 0)",
1.860 "solveFor x", "solutions L"];
1.861 val (dI',pI',mI') =
1.862 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],