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^^^2 = (0::real)) ----------------------------------------";
20 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
21 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
22 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
23 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
24 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
25 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
26 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
27 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
28 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
29 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
30 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
31 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
32 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
33 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
34 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
35 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
36 "-----------------------------------------------------------------";
37 "------ polyeq-2.sml ---------------------------------------------";
38 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
39 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
40 "----------- (-147 + 3*x^^^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)^^^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 (* trace_rewrite:=true;
55 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
57 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
58 else error "polyeq.sml: diff.behav. in lhs";
60 val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
61 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
62 if (term2str t) = "True" then ()
63 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
65 val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
66 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
67 if (term2str t) = "False" then ()
68 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
70 val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
71 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
72 if (term2str t) = "True" then ()
73 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
75 val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
76 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
77 if (term2str t) = "True" then ()
78 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
81 val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
82 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
83 if (term2str t) = "True" then ()
84 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
86 val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
87 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
88 if (term2str t) = "True" then ()
89 else error "polyeq.sml: diff.behav. in has_degree_in_in";
91 val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
92 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
93 if (term2str t) = "False" then ()
94 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
96 val t4 = (Thm.term_of o the o (parse thy))
97 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
98 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
99 if (term2str t) = "False" then ()
100 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
102 val t5 = (Thm.term_of o the o (parse thy))
103 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
104 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
105 if (term2str t) = "True" then ()
106 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
108 "----------- test matching problems --------------------------0---";
109 "----------- test matching problems --------------------------0---";
110 "----------- test matching problems --------------------------0---";
111 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
112 if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
113 Matches' {Find = [Correct "solutions L"],
115 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
116 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
117 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
119 then () else error "match_pbl [expanded,univariate,equation]";
121 if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
122 Matches' {Find = [Correct "solutions L"],
124 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
125 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
126 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
127 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
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 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
133 (*##################################################################################
134 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
136 (*Aufgabe zum Einstieg in die Arbeit...*)
137 val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
138 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
139 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
141 "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
143 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
145 "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
146 (* bei Verwendung von "size_of-term" nach MG :*)
147 (*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
149 (*wir holen 'a' wieder aus der Klammerung heraus...*)
150 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
152 "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
153 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
156 rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
158 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
159 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
160 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
162 (*das rewriting l"asst sich beobachten mit
163 trace_rewrite := false;
166 "------15.11.02 --------------------------";
167 val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
168 val bdv = (Thm.term_of o the o (parse thy)) "bdv";
169 val a = (Thm.term_of o the o (parse thy)) "a";
171 trace_rewrite := false;
172 (* Anwenden einer Regelmenge aus Termorder.ML: *)
174 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
177 rewrite_set_ thy false discard_parentheses t;
181 val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
183 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
186 rewrite_set_ thy false discard_parentheses t;
188 "1 + (x + b * x) * a + a ^^^ 2";
190 val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
192 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
195 rewrite_set_ thy false discard_parentheses t;
197 "1 + b * a + (7 + x) * a ^^^ 2";
200 Prog_Expr.thy grundlegende Algebra
204 RootRat.thy Wurzen + Br"uche
205 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
207 get_thm Termorder.thy "bdv_n_collect";
208 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
210 val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
212 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
215 rewrite_set_ thy false discard_parentheses t;
219 val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
221 val t = (Thm.term_of o the o (parseold thy)) "7";
222 ##################################################################################*)
225 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
226 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
227 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
228 val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
229 val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
230 val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
232 val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
233 val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
234 val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
235 val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
237 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
238 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
240 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
241 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
243 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
244 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
246 val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
247 val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
248 ord_make_polynomial_in true thy substx (aa, bb);
251 val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
252 val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
253 ord_make_polynomial_in true thy substa (aa, bb);
254 false; (* => GREATER *)
256 (* und nach dem Re-engineering der Termorders in den 'rulesets'
257 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
258 val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";
259 val x = (Thm.term_of o the o (parse thy)) "x";
260 val a = (Thm.term_of o the o (parse thy)) "a";
261 val b = (Thm.term_of o the o (parse thy)) "b";
262 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
263 if term2str t' = "b + x + a" then ()
264 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
266 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
268 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
269 if term2str t' = "a + b + x" then ()
270 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
272 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
273 val ppp = (Thm.term_of o the o (parse thy)) ppp';
274 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
275 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
276 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
278 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
279 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
280 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
282 val ttt' = "(3*x + 5)/18";
283 val ttt = (Thm.term_of o the o (parse thy)) ttt';
284 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
285 if term2str uuu = "(5 + 3 * x) / 18" then ()
286 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
288 (*============ inhibit exn WN120316 ==============================================
289 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
290 if term2str uuu = "(5 + 3 * x) / 18" then ()
291 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
292 ============ inhibit exn WN120316 ==============================================*)
295 "----------- lin.eq degree_0 -------------------------------------";
296 "----------- lin.eq degree_0 -------------------------------------";
297 "----------- lin.eq degree_0 -------------------------------------";
298 "----- d0_false ------";
299 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
300 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
301 ["PolyEq","solve_d0_polyeq_equation"]);
302 (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
303 TODO: change to "equality (x + -1*x = (0::real))"
304 and search for an appropriate problem and method.
306 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
307 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
314 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
316 "----- d0_true ------";
317 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
318 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
319 ["PolyEq","solve_d0_polyeq_equation"]);
320 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
321 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
327 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
328 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
329 ============ inhibit exn WN110914 ============================================*)
331 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
332 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
333 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
334 "----- d2_pqformula1 ------!!!!";
335 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
337 ("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
338 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
345 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
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;
349 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
351 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
353 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
354 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
355 val Appl m = applicable_in p pt tac;
356 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
357 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
359 term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
360 terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
361 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
362 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
363 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
364 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
365 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
366 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
367 (*if*) Tactic.for_specify' m; (*false*)
368 (*loc_solve_ (mI,m) ptp;
369 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
370 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
372 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
373 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
374 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
375 val thy' = get_obj g_domID pt (par_pblobj pt p);
376 val (is, sc) = resume_prog thy' (p,p_) pt;
378 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
379 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
380 "~~~~~ fun locate_input_tactic, args:"; val () = ();
381 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
382 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
383 (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
384 ... Accept_Tac1 ... is correct*)
385 "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
386 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
387 1 < length l (*true*);
388 val up = drop_last l;
389 term2str (at_location up sc);
391 (*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
392 ... ???? ... is correct*)
393 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
394 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (at_location up sc));
395 val l = drop_last l; (*comes from e, goes to Abs*)
396 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location l sc;
397 val i = mk_Free (i, T);
398 val E = Env.update E (i, v);
399 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
400 val [(tac_, mout, ctree, pos', xxx)] = ss;
401 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
402 (*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body
403 ... Accept_Tac1 ... is correct*)
404 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
405 ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
406 val (Program.Tac stac, a') = check_leaf "locate" thy' sr (E, (a, v)) t
407 val ctxt = get_ctxt pt (p,p_)
408 val p' = lev_on p : pos;
409 (* WAS val Not_Associated = associate pt d (m, stac)
410 ... Associated ... is correct*)
411 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
412 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
415 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
416 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
417 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
419 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
420 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
421 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
422 "----- d2_pqformula1_neg ------";
423 val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
424 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
425 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
426 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
427 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
428 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
432 ([1],Res) False Or_to_List)*)
433 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
435 ([2],Res) [] Check_elementwise "Assumptions"*)
436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
437 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
438 val asm = Ctree.get_assumptions pt p;
439 if f2str f = "[]" andalso
440 terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
441 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
442 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
444 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
445 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
446 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
447 "----- d2_pqformula2 ------";
448 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
449 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
450 ["PolyEq","solve_d2_polyeq_pq_equation"]);
452 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
453 val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
454 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
456 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
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 FormKF "[x = 2, x = -1]" => ()
465 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
468 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
469 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
470 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
471 "----- d2_pqformula3 ------";
473 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
474 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
475 ["PolyEq","solve_d2_polyeq_pq_equation"]);
476 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
477 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;
483 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
484 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
485 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
486 case f of FormKF "[x = 1, x = -2]" => ()
487 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
490 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
491 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
492 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
493 "----- d2_pqformula3_neg ------";
494 val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
495 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
496 ["PolyEq","solve_d2_polyeq_pq_equation"]);
497 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
498 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
502 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
504 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
505 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
506 "TODO 2 + x + x^^^2 = 0";
507 "TODO 2 + x + x^^^2 = 0";
508 "TODO 2 + x + x^^^2 = 0";
510 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
511 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
512 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
513 "----- d2_pqformula4 ------";
514 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
515 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
516 ["PolyEq","solve_d2_polyeq_pq_equation"]);
517 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
518 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
522 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
523 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
526 case f of FormKF "[x = 1, x = -2]" => ()
527 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
529 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
530 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
531 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
532 "----- d2_pqformula5 ------";
533 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
534 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
535 ["PolyEq","solve_d2_polyeq_pq_equation"]);
536 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
537 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
541 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
542 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
543 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
544 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
545 case f of FormKF "[x = 0, x = -1]" => ()
546 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
548 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
549 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
550 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
551 "----- d2_pqformula6 ------";
552 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
553 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
554 ["PolyEq","solve_d2_polyeq_pq_equation"]);
555 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
556 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
560 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
561 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
562 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
563 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
564 case f of FormKF "[x = 0, x = -1]" => ()
565 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
567 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
568 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
569 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
570 "----- d2_pqformula7 ------";
572 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
573 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
574 ["PolyEq","solve_d2_polyeq_pq_equation"]);
575 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
576 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
577 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
578 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
579 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
580 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
581 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
582 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
583 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
584 case f of FormKF "[x = 0, x = -1]" => ()
585 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
587 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
588 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
589 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
590 "----- d2_pqformula8 ------";
591 val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
592 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
593 ["PolyEq","solve_d2_polyeq_pq_equation"]);
594 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
595 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
596 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
597 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
598 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
599 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
600 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
601 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
602 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
603 case f of FormKF "[x = 0, x = -1]" => ()
604 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
606 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
607 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
608 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
609 "----- d2_pqformula9 ------";
610 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
611 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
612 ["PolyEq","solve_d2_polyeq_pq_equation"]);
613 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
614 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
615 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
616 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
617 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
618 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
619 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
620 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
621 case f of FormKF "[x = 2, x = -2]" => ()
622 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
625 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
626 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
627 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
628 "----- d2_pqformula9_neg ------";
629 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
630 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
631 ["PolyEq","solve_d2_polyeq_pq_equation"]);
632 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
633 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
634 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
635 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
636 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
637 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
638 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
639 "TODO 4 + 1*x^^^2 = 0";
640 "TODO 4 + 1*x^^^2 = 0";
641 "TODO 4 + 1*x^^^2 = 0";
643 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
644 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
645 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
646 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
647 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
648 ["PolyEq","solve_d2_polyeq_abc_equation"]);
649 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
650 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
653 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
654 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
655 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
656 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
657 case f of FormKF "[x = 1, x = -1 / 2]" => ()
658 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
660 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
661 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
662 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
663 val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
664 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
665 ["PolyEq","solve_d2_polyeq_abc_equation"]);
666 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
667 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
671 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
672 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
673 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
674 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
675 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
676 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
679 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
680 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
681 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
683 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
684 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
685 ["PolyEq","solve_d2_polyeq_abc_equation"]);
686 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
687 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
688 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
690 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
691 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
692 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
696 case f of FormKF "[x = 1 / 2, x = -1]" => ()
697 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
700 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
701 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
702 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
703 val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
704 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
705 ["PolyEq","solve_d2_polyeq_abc_equation"]);
706 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
707 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;
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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
713 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
714 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
715 "TODO 1 + x + 2*x^^^2 = 0";
716 "TODO 1 + x + 2*x^^^2 = 0";
717 "TODO 1 + x + 2*x^^^2 = 0";
720 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
721 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
722 ["PolyEq","solve_d2_polyeq_abc_equation"]);
723 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
724 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
730 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
731 case f of FormKF "[x = 1, x = -2]" => ()
732 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
734 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
735 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
736 ["PolyEq","solve_d2_polyeq_abc_equation"]);
737 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
738 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
743 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
744 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
745 "TODO 2 + 1*x + x^^^2 = 0";
746 "TODO 2 + 1*x + x^^^2 = 0";
747 "TODO 2 + 1*x + x^^^2 = 0";
750 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
751 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
752 ["PolyEq","solve_d2_polyeq_abc_equation"]);
753 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
754 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
758 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
759 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
760 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
761 case f of FormKF "[x = 1, x = -2]" => ()
762 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
764 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
765 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
766 ["PolyEq","solve_d2_polyeq_abc_equation"]);
767 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
768 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
771 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
772 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
774 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
775 "TODO 2 + x + x^^^2 = 0";
776 "TODO 2 + x + x^^^2 = 0";
777 "TODO 2 + x + x^^^2 = 0";
780 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
781 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
782 ["PolyEq","solve_d2_polyeq_abc_equation"]);
783 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
784 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
787 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
788 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
789 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
790 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
791 case f of FormKF "[x = 2, x = -2]" => ()
792 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
794 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
795 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
796 ["PolyEq","solve_d2_polyeq_abc_equation"]);
797 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
798 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
801 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
802 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
803 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
804 "TODO 8+ 2*x^^^2 = 0";
805 "TODO 8+ 2*x^^^2 = 0";
806 "TODO 8+ 2*x^^^2 = 0";
809 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
810 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
811 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
812 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
816 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
817 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
818 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
819 case f of FormKF "[x = 2, x = -2]" => ()
820 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
823 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
824 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
825 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
826 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
831 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
837 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
838 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
839 ["PolyEq","solve_d2_polyeq_abc_equation"]);
840 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
841 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
842 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
843 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
844 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
845 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
846 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
847 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
848 case f of FormKF "[x = 0, x = -1]" => ()
849 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
851 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
852 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
853 ["PolyEq","solve_d2_polyeq_abc_equation"]);
854 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
855 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
857 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
858 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
859 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
860 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
861 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
862 case f of FormKF "[x = 0, x = -1]" => ()
863 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
866 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
867 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
868 ["PolyEq","solve_d2_polyeq_abc_equation"]);
869 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
870 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
871 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
874 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
875 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
876 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
877 case f of FormKF "[x = 0, x = -1 / 2]" => ()
878 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
881 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
882 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
883 ["PolyEq","solve_d2_polyeq_abc_equation"]);
884 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
885 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
886 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
887 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
888 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
889 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
890 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
891 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
892 case f of FormKF "[x = 0, x = -1]" => ()
893 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
896 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
897 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
898 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
899 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
900 see --- val rls = calculate_RootRat > calculate_Rational ---
901 calculate_RootRat was a TODO with 2002, requires re-design.
902 see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
904 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
905 "solveFor x","solutions L"];
907 ("PolyEq",["degree_2","expanded","univariate","equation"],
908 ["PolyEq","complete_square"]);
909 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
910 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
911 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
912 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
914 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
915 (*Apply_Method ("PolyEq","complete_square")*)
916 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
917 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
918 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
919 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
920 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
921 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
922 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
923 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
924 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
925 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
926 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
927 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
928 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
929 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
930 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
931 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
932 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
933 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
934 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
935 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
936 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
937 NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
938 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
939 (*"x = -2 | x = 4" nxt = Or_to_List*)
940 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
941 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
942 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
944 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
945 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
948 "[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
949 (*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
950 then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
953 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
954 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
955 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
956 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
957 see --- val rls = calculate_RootRat > calculate_Rational ---*)
958 val thy = @{theory PolyEq};
959 val ctxt = Proof_Context.init_global thy;
960 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
961 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
963 val rls = complete_square;
964 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
965 term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
967 val thm = num_str @{thm square_explicit1};
968 val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
969 term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
971 val thm = num_str @{thm root_plus_minus};
972 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
973 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
974 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
976 (*the thm bdv_explicit2* here required to be constrained to ::real*)
977 val thm = num_str @{thm bdv_explicit2};
978 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
979 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
980 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
982 val thm = num_str @{thm bdv_explicit3};
983 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
984 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
985 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
987 val thm = num_str @{thm bdv_explicit2};
988 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
989 term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
990 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
992 val rls = calculate_RootRat;
993 val SOME (t,asm) = rewrite_set_ thy true rls t;
995 "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
996 (*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
997 then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
998 (*SHOULD BE: term2str = "x = -2 | x = 4;*)
1001 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1002 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1003 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1004 "---- test the erls ----";
1005 val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
1006 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1007 val t' = term2str t;
1008 (*if t'= "HOL.True" then ()
1009 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1011 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1012 "solveFor x","solutions L"];
1014 ("PolyEq",["degree_2","expanded","univariate","equation"],
1015 ["PolyEq","complete_square"]);
1016 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1017 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1018 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1019 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1020 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1021 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1022 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1023 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1024 (*Apply_Method ("PolyEq","complete_square")*)
1025 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1027 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1028 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1029 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1030 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1031 "solveFor x","solutions L"];
1033 ("PolyEq",["degree_2","expanded","univariate","equation"],
1034 ["PolyEq","complete_square"]);
1035 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1036 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1037 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1038 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1039 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1040 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1041 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1042 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1043 (*Apply_Method ("PolyEq","complete_square")*)
1044 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1045 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1046 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1047 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1048 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1049 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1050 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1051 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1052 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1053 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1055 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1056 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";