1 (* Title: Knowledge/polyeq- 1.sml
2 testexamples for PolyEq, poynomial equations and equational systems
3 Author: Richard Lang 2003
4 (c) due to copyright terms
5 WN030609: some expls dont work due to unfinished handling of 'expanded terms';
6 others marked with TODO have to be checked, too.
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "------ polyeq- 1.sml ---------------------------------------------";
13 "----------- tests on predicates in problems ---------------------";
14 "----------- test matching problems ------------------------------";
15 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
16 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
17 "----------- lin.eq degree_0 -------------------------------------";
18 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
19 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
20 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
21 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
22 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
23 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
24 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
25 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
26 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
27 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
28 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
29 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
30 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
31 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
32 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
33 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
34 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
35 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
36 "-----------------------------------------------------------------";
37 "------ polyeq- 2.sml ---------------------------------------------";
38 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
39 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
40 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
41 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
42 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
43 "----------- rls make_polynomial_in ------------------------------";
44 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
45 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
46 "-----------------------------------------------------------------";
47 "-----------------------------------------------------------------";
49 "----------- tests on predicates in problems ---------------------";
50 "----------- tests on predicates in problems ---------------------";
51 "----------- tests on predicates in problems ---------------------";
52 Rewrite.trace_on:=true; (*true false*)
54 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
55 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
56 if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
57 else error "polyeq.sml: diff.behav. in lhs";
59 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
60 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
61 if (UnparseC.term t) = "True" then ()
62 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
64 val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
65 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
66 if (UnparseC.term t) = "False" then ()
67 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
69 val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
70 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
71 if (UnparseC.term t) = "True" then ()
72 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
74 val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
75 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
76 if (UnparseC.term t) = "True" then ()
77 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
80 val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
81 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
82 if (UnparseC.term t) = "True" then ()
83 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
85 val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
86 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
87 if (UnparseC.term t) = "True" then ()
88 else error "polyeq.sml: diff.behav. in has_degree_in_in";
90 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
91 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
92 if (UnparseC.term t) = "False" then ()
93 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
95 val t4 = (Thm.term_of o the o (TermC.parse thy))
96 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
97 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
98 if (UnparseC.term t) = "False" then ()
99 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
101 val t5 = (Thm.term_of o the o (TermC.parse thy))
102 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
103 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
104 if (UnparseC.term t) = "True" then ()
105 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
107 "----------- test matching problems --------------------------0---";
108 "----------- test matching problems --------------------------0---";
109 "----------- test matching problems --------------------------0---";
110 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
111 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
112 M_Match.Matches' {Find = [Correct "solutions L"],
114 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
115 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
116 Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
118 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
120 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
121 M_Match.Matches' {Find = [Correct "solutions L"],
123 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
124 Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
125 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
126 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
129 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
130 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
131 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
132 (*##################################################################################
133 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
135 (*Aufgabe zum Einstieg in die Arbeit...*)
136 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0";
137 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
138 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
140 "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
142 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
144 "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
145 (* bei Verwendung von "size_of-term" nach MG :*)
146 (*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
148 (*wir holen 'a' wieder aus der Klammerung heraus...*)
149 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
151 "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
152 (* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
155 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
157 "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
158 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
159 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
161 (*das rewriting l"asst sich beobachten mit
162 Rewrite.trace_on := false; (*true false*)
165 "------ 15.11.02 --------------------------";
166 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
167 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
168 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
170 Rewrite.trace_on := false; (*true false*)
171 (* Anwenden einer Regelmenge aus Termorder.ML: *)
173 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
176 rewrite_set_ thy false discard_parentheses t;
180 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2";
182 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
185 rewrite_set_ thy false discard_parentheses t;
187 "1 + (x + b * x) * a + a \<up> 2";
189 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
191 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
194 rewrite_set_ thy false discard_parentheses t;
196 "1 + b * a + (7 + x) * a \<up> 2";
199 Prog_Expr.thy grundlegende Algebra
203 RootRat.thy Wurzen + Br"uche
204 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
206 get_thm Termorder.thy "bdv_n_collect";
207 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
209 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
211 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
214 rewrite_set_ thy false discard_parentheses t;
216 "(7 + x) * a \<up> 2";
218 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
220 val t = (Thm.term_of o the o (parseold thy)) "7";
221 ##################################################################################*)
224 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
225 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
226 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
227 val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")];
228 val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
229 val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
231 val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
232 val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
233 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
234 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
236 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
237 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
239 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
240 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
242 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
243 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
245 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
246 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
247 ord_make_polynomial_in true thy substx (aa, bb);
250 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
251 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
252 ord_make_polynomial_in true thy substa (aa, bb);
253 false; (* => GREATER *)
255 (* und nach dem Re-engineering der Termorders in den 'rulesets'
256 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
257 val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
258 val x = (Thm.term_of o the o (TermC.parse thy)) "x";
259 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
260 val b = (Thm.term_of o the o (TermC.parse thy)) "b";
261 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
262 if UnparseC.term t' = "b + x + a" then ()
263 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
265 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
267 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
268 if UnparseC.term t' = "a + b + x" then ()
269 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
271 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
272 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
273 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
274 if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
275 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
277 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
278 if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
279 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
281 val ttt' = "(3*x + 5)/18";
282 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
283 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
284 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
285 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
287 (*============ inhibit exn WN120316 ==============================================
288 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
289 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
290 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
291 ============ inhibit exn WN120316 ==============================================*)
294 "----------- lin.eq degree_0 -------------------------------------";
295 "----------- lin.eq degree_0 -------------------------------------";
296 "----------- lin.eq degree_0 -------------------------------------";
297 "----- d0_false ------";
298 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
299 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
300 ["PolyEq", "solve_d0_polyeq_equation"]);
301 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
302 TODO: change to "equality (x + - 1*x = (0::real))"
303 and search for an appropriate problem and method.
305 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
306 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
307 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
308 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
313 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
315 "----- d0_true ------";
316 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
317 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
318 ["PolyEq", "solve_d0_polyeq_equation"]);
319 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
320 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
321 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
322 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
323 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
324 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
325 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
326 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
327 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
328 ============ inhibit exn WN110914 ============================================*)
330 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
331 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
332 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
333 "----- d2_pqformula1 ------!!!!";
334 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
336 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
337 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
338 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
339 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
340 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
342 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
343 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
344 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
346 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
348 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
350 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
351 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
353 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
355 if p = ([], Res) andalso
356 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
357 case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
358 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
360 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
361 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
362 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
363 "----- d2_pqformula1_neg ------";
364 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
365 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
366 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
367 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
368 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
373 ([1],Res) False Or_to_List)*)
374 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
376 ([2],Res) [] Check_elementwise "Assumptions"*)
377 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
378 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
379 val asm = Ctree.get_assumptions pt p;
380 if f2str f = "[]" andalso
381 UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
382 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
383 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
385 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
386 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
387 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
388 "----- d2_pqformula2 ------";
389 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
390 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
391 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
392 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
393 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
400 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
401 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
402 case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
403 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
406 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
407 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
408 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
409 "----- d2_pqformula3 ------";
411 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
412 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
413 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
414 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
415 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
416 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
417 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
418 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
419 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
421 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
422 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
423 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
424 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
425 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
428 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
429 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
430 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
431 "----- d2_pqformula3_neg ------";
432 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
433 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
434 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
435 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
437 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
438 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
439 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
440 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
442 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
444 "TODO 2 + x + x \<up> 2 = 0";
445 "TODO 2 + x + x \<up> 2 = 0";
446 "TODO 2 + x + x \<up> 2 = 0";
448 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
449 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
450 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
451 "----- d2_pqformula4 ------";
452 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
453 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
454 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
455 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
456 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
457 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
458 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
459 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
460 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
461 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
462 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
464 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
465 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
467 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
468 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
469 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
470 "----- d2_pqformula5 ------";
471 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
472 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
473 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
474 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
475 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
476 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
477 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
478 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
479 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
480 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
481 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
482 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
483 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
484 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
486 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
487 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
488 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
489 "----- d2_pqformula6 ------";
490 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
491 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
492 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
493 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
494 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
499 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
500 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
501 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
502 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
503 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
505 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
506 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
507 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
508 "----- d2_pqformula7 ------";
510 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
511 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
512 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
513 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
514 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
515 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
516 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
517 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
518 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
519 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
520 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
521 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
522 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
523 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
525 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
526 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
527 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
528 "----- d2_pqformula8 ------";
529 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
530 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
531 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
532 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
533 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
534 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
535 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
536 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
537 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
538 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
539 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
540 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
541 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
542 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
544 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
545 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
546 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
547 "----- d2_pqformula9 ------";
548 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
549 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
550 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
551 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
552 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
554 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
555 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
556 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
557 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
558 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
559 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
560 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
563 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
564 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
565 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
566 "----- d2_pqformula9_neg ------";
567 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
568 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
569 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
570 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
571 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
572 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
573 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
574 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
575 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
576 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
577 "TODO 4 + 1*x \<up> 2 = 0";
578 "TODO 4 + 1*x \<up> 2 = 0";
579 "TODO 4 + 1*x \<up> 2 = 0";
581 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
582 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
583 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
584 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
585 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
586 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
587 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
588 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
589 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
590 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
591 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
592 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
593 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
594 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
595 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
596 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
598 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
599 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
600 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
601 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
602 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
603 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
604 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
605 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
606 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
607 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
609 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
610 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
611 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
612 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
613 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
614 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
617 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
618 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
619 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
621 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
622 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
623 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
624 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
625 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
626 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
628 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
629 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
630 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
631 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
633 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
634 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
635 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
638 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
639 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
640 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
641 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
642 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
643 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
644 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
645 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
646 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
648 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
649 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
650 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
651 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
652 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
653 "TODO 1 + x + 2*x \<up> 2 = 0";
654 "TODO 1 + x + 2*x \<up> 2 = 0";
655 "TODO 1 + x + 2*x \<up> 2 = 0";
658 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
659 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
660 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
661 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
662 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
663 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
664 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
665 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
666 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
667 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
668 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
669 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
670 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
672 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
673 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
674 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
675 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
676 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
677 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
678 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
679 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
680 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
681 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
682 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
683 "TODO 2 + 1*x + x \<up> 2 = 0";
684 "TODO 2 + 1*x + x \<up> 2 = 0";
685 "TODO 2 + 1*x + x \<up> 2 = 0";
688 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
689 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
690 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
691 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
692 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
693 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
694 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
696 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
697 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
698 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
699 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
700 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
702 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
703 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
704 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
705 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
706 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
707 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
708 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
709 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
710 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
711 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
712 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
713 "TODO 2 + x + x \<up> 2 = 0";
714 "TODO 2 + x + x \<up> 2 = 0";
715 "TODO 2 + x + x \<up> 2 = 0";
718 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
719 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
720 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
721 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
722 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
723 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
724 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
725 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
726 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
727 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
728 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
729 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
730 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
732 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
733 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
734 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
735 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
736 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
737 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
738 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
739 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
740 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
741 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
742 "TODO 8+ 2*x \<up> 2 = 0";
743 "TODO 8+ 2*x \<up> 2 = 0";
744 "TODO 8+ 2*x \<up> 2 = 0";
747 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
748 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
749 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
750 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
751 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
752 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
753 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
754 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
755 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
756 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
757 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
758 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
761 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
762 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
763 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
764 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
765 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
766 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
767 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
769 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
770 "TODO 4+ x \<up> 2 = 0";
771 "TODO 4+ x \<up> 2 = 0";
772 "TODO 4+ x \<up> 2 = 0";
775 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
776 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
777 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
778 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
779 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
780 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
781 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
782 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
783 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
784 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
785 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
786 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
787 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
789 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
790 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
791 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
792 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
793 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
794 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
795 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
796 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
797 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
798 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
799 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
800 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
801 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
804 val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
805 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
806 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
807 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
808 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
809 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
810 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
811 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
812 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
813 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
814 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
815 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
816 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
819 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
820 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
821 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
822 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
823 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
824 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
825 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
826 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
827 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
828 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
829 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
830 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
831 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
834 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
835 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
836 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
837 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
838 see --- val rls = calculate_RootRat > calculate_Rational ---
839 calculate_RootRat was a TODO with 2002, requires re-design.
840 see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
842 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
843 "solveFor x", "solutions L"];
845 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
846 ["PolyEq", "complete_square"]);
847 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
848 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
849 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
850 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
853 (*Apply_Method ("PolyEq", "complete_square")*)
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
855 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
857 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
858 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
859 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
860 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
861 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
862 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
863 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
864 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
865 - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
866 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
867 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
868 - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
869 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
870 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
871 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
874 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
875 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
876 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
877 (*"x = - 2 | x = 4" nxt = Or_to_List*)
878 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
879 (*"[x = - 2, x = 4]" nxt = Check_Postcond*)
880 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
882 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
883 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
886 "[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))]"
887 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
888 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
891 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
892 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
893 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
894 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
895 see --- val rls = calculate_RootRat > calculate_Rational ---*)
896 val thy = @{theory PolyEq};
897 val ctxt = Proof_Context.init_global thy;
898 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
899 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
901 val rls = complete_square;
902 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
903 UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
905 val thm = ThmC.numerals_to_Free @{thm square_explicit1};
906 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
907 UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
909 val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
910 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
911 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
912 "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
914 (*the thm bdv_explicit2* here required to be constrained to ::real*)
915 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
916 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
917 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
918 "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
920 val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
921 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
922 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
923 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
925 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
926 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
927 UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
928 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
930 val rls = calculate_RootRat;
931 val SOME (t,asm) = rewrite_set_ thy true rls t;
933 "- 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))"
934 (*"- 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*)
935 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
936 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
939 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
940 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
941 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
942 "---- test the erls ----";
943 val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
944 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
945 val t' = UnparseC.term t;
946 (*if t'= \<^const_name>\<open>True\<close> then ()
947 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
949 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
950 "solveFor x", "solutions L"];
952 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
953 ["PolyEq", "complete_square"]);
954 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
955 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
956 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
957 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
958 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
959 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
960 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
961 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
962 (*Apply_Method ("PolyEq", "complete_square")*)
963 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
965 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
966 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
967 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
968 val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
969 "solveFor x", "solutions L"];
971 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
972 ["PolyEq", "complete_square"]);
973 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
974 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
975 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
976 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
977 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
978 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
979 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
980 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
981 (*Apply_Method ("PolyEq", "complete_square")*)
982 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
983 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
984 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
985 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
986 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
987 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
988 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
989 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
990 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
991 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
993 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
994 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";