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
6 Separation into polyeq-1.sml and polyeq-1a.sml due to
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 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
17 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
18 "----------- lin.eq degree_0 -------------------------------------";
19 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
20 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
21 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
22 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
23 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
24 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
25 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
26 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
27 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
28 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
29 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
30 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
31 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
32 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
33 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
34 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
35 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
36 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
37 "-----------------------------------------------------------------";
38 "------ polyeq-2.sml ---------------------------------------------";
39 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";
40 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
41 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
42 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5";
43 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";
44 "----------- rls make_polynomial_in ------------------------------";
45 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
46 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
47 "-----------------------------------------------------------------";
48 "-----------------------------------------------------------------";
50 "----------- tests on predicates in problems ---------------------";
51 "----------- tests on predicates in problems ---------------------";
52 "----------- tests on predicates in problems ---------------------";
54 val ctxt = Proof_Context.init_global thy;
55 Rewrite.trace_on:=false; (*true false*)
57 val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";
58 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
59 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
60 else error "polyeq.sml: diff.behav. in lhs";
62 val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";
63 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
64 if (UnparseC.term t) = "True" then ()
65 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
67 val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x";
68 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
69 if (UnparseC.term t) = "False" then ()
70 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
72 val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
73 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
74 if (UnparseC.term t) = "True" then ()
75 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
77 val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
78 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
79 if (UnparseC.term t) = "True" then ()
80 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
82 val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
83 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
84 if (UnparseC.term t) = "True" then ()
85 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
87 val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
88 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
89 if (UnparseC.term t) = "True" then ()
90 else error "polyeq.sml: diff.behav. in has_degree_in_in";
92 val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2";
93 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
94 if (UnparseC.term t) = "False" then ()
95 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
97 val t4 = TermC.parseNEW' ctxt
98 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
99 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
100 if (UnparseC.term t) = "False" then ()
101 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
103 val t5 = TermC.parseNEW' ctxt
104 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
105 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
106 if (UnparseC.term t) = "True" then ()
107 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
109 "----------- test matching problems --------------------------0---";
110 "----------- test matching problems --------------------------0---";
111 "----------- test matching problems --------------------------0---";
112 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
113 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
114 M_Match.Matches' {Find = [Correct "solutions L"],
116 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
117 Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)",
118 Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
120 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
122 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
123 M_Match.Matches' {Find = [Correct "solutions L"],
125 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
126 Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
127 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
128 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
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 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
134 (*##################################################################################
135 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
137 (*Aufgabe zum Einstieg in die Arbeit...*)
138 val t = TermC.parseNEW' ctxt "a*b - (a+b)*x + x \<up> 2 = 0";
139 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
140 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
142 "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0";
144 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
146 "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
147 (* bei Verwendung von "size_of-term" nach MG :*)
148 (*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *)
150 (*wir holen 'a' wieder aus der Klammerung heraus...*)
151 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
153 "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
154 (* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *)
157 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
159 "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
160 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
161 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
163 (*das rewriting l"asst sich beobachten mit
164 Rewrite.trace_on := false; (*true false*)
167 "------ 15.11.02 --------------------------";
168 val t = TermC.parseNEW' ctxt "1 + a * x + b * x";
169 val bdv = TermC.parseNEW' ctxt "bdv";
170 val a = TermC.parseNEW' ctxt "a";
172 Rewrite.trace_on := false; (*true false*)
173 (* Anwenden einer Regelmenge aus Termorder.ML: *)
175 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
178 rewrite_set_ thy false discard_parentheses t;
182 val t = TermC.parseNEW' ctxt "1 + a * (x + b * x) + a \<up> 2";
184 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
187 rewrite_set_ thy false discard_parentheses t;
189 "1 + (x + b * x) * a + a \<up> 2";
191 val t = TermC.parseNEW' ctxt "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
193 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
196 rewrite_set_ thy false discard_parentheses t;
198 "1 + b * a + (7 + x) * a \<up> 2";
201 Prog_Expr.thy grundlegende Algebra
205 RootRat.thy Wurzen + Br"uche
206 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
208 get_thm Termorder.thy "bdv_n_collect";
209 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
211 val t = TermC.parseNEW' ctxt "a \<up> 2 * x + 7 * a \<up> 2";
213 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
216 rewrite_set_ thy false discard_parentheses t;
218 "(7 + x) * a \<up> 2";
220 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
222 val t = (Thm.term_of o the o (parseold thy)) "7";
223 ##################################################################################*)
226 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
227 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
228 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
229 (* termorder hacked by MG, adapted later by WN *)
230 (** )local ( *. for make_polynomial_in .*)
232 open Term; (* for type order = EQUAL | LESS | GREATER *)
234 fun pr_ord EQUAL = "EQUAL"
235 | pr_ord LESS = "LESS"
236 | pr_ord GREATER = "GREATER";
238 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
239 | dest_hd' x (t as Free (a, T)) =
240 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
241 else (((a, 0), T), 1)
242 | dest_hd' _ (Var v) = (v, 2)
243 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
244 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
245 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
247 fun size_of_term' i pr x (t as Const (\<^const_name>\<open>realpow\<close>, _) $
248 Free (var, _) $ Free (pot, _)) =
249 (if pr then tracing (idt "#" i ^ "size_of_term' realpow: " ^ UnparseC.term t) else ();
253 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
254 1000 * (the (TermC.int_opt_of_string pot)))
255 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
256 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
257 | size_of_term' i pr x (t as Abs (_, _, body)) =
258 (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
259 1 + size_of_term' (i + 1) pr x body)
260 | size_of_term' i pr x (f $ t) =
262 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
263 val s1 = size_of_term' (i + 1) pr x f
264 val s2 = size_of_term' (i + 1) pr x t
265 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
267 | size_of_term' i pr x t =
268 (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
274 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
275 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
276 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
277 | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
279 fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
281 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
283 case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
284 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
286 | term_ord' i pr x _ (t, u) =
288 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
290 case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
292 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
294 (case hd_ord (i + 1) pr x (f, g) of
295 EQUAL => (terms_ord x (i + 1) pr) (ts, us)
299 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
301 and hd_ord i pr x (f, g) = (* ~ term.ML *)
303 val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
305 (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
306 (dest_hd' x f, dest_hd' x g)
307 val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
309 and terms_ord x i pr (ts, us) =
311 val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
312 val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
313 val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
318 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
319 ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
322 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
323 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
327 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
328 if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?";
330 val x = TermC.str2term "x ::real";
332 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
333 if 2006 = size_of_term' 1 false(*true*) x t1
334 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
336 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
337 if 3004 = size_of_term' 1 false(*true*) x t2
338 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
341 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
342 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
343 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
344 val substa = [(TermC.empty, TermC.parseNEW' ctxt "a::real")];
345 val substb = [(TermC.empty, TermC.parseNEW' ctxt "b::real")];
346 val substx = [(TermC.empty, TermC.parseNEW' ctxt "x::real")];
348 val x1 = TermC.parseNEW' ctxt "a + b + x::real";
349 val x2 = TermC.parseNEW' ctxt "a + x + b::real";
350 val x3 = TermC.parseNEW' ctxt "a + x + b::real";
351 val x4 = TermC.parseNEW' ctxt "x + a + b::real";
353 if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
354 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
356 if ord_make_polynomial_in false(*true*) thy substa (x1,x2) = true(*LESS *) then ()
357 else error "termorder.sml diff.behav ord_make_polynomial_in #2";
359 if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
360 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
362 val aa = TermC.parseNEW' ctxt "- 1 * a * x::real";
363 val bb = TermC.parseNEW' ctxt "x \<up> 3::real";
364 if ord_make_polynomial_in false(*true*) thy substx (aa, bb) = true(*LESS *) then ()
365 else error "termorder.sml diff.behav ord_make_polynomial_in #4";
367 val aa = TermC.parseNEW' ctxt "- 1 * a * x";
368 val bb = TermC.parseNEW' ctxt "x \<up> 3";
369 if ord_make_polynomial_in false(*true*) thy substa (aa, bb) = false(*GREATER*) then ()
370 else error "termorder.sml diff.behav ord_make_polynomial_in #5";
372 (* und nach dem Re-engineering der Termorders in den 'rulesets'
373 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
374 val bdv= TermC.parseNEW' ctxt "bdv ::real";
375 val x = TermC.parseNEW' ctxt "x ::real";
376 val a = TermC.parseNEW' ctxt "a ::real";
377 val b = TermC.parseNEW' ctxt "b ::real";
378 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
379 if UnparseC.term t' = "b + x + a" then ()
380 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
382 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
384 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
385 if UnparseC.term t' = "a + b + x" then ()
386 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
388 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
389 val ppp = TermC.parseNEW' ctxt ppp';
390 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
391 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
392 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
394 val ttt' = "(3*x + 5)/18 ::real";
395 val ttt = TermC.parseNEW' ctxt ttt';
396 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
397 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
398 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
400 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
401 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
402 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
404 "----------- lin.eq degree_0 -------------------------------------";
405 "----------- lin.eq degree_0 -------------------------------------";
406 "----------- lin.eq degree_0 -------------------------------------";
407 "----- d0_false ------";
408 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
409 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
410 ["PolyEq", "solve_d0_polyeq_equation"]);
411 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
412 TODO: change to "equality (x + - 1*x = (0::real))"
413 and search for an appropriate problem and method.
415 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
416 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;
420 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 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
423 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
425 "----- d0_true ------";
426 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
427 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
428 ["PolyEq", "solve_d0_polyeq_equation"]);
429 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
431 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
432 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
433 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
434 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
435 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
436 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
437 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
438 ============ inhibit exn WN110914 ============================================*)
440 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
441 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
442 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
443 "----- d2_pqformula1 ------!!!!";
444 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
446 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
447 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
448 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
449 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
450 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
451 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
452 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
453 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
454 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
455 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
456 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
457 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
458 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
460 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
461 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
462 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
465 if p = ([], Res) andalso
466 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
467 case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
468 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
470 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
471 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
472 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
473 "----- d2_pqformula1_neg ------";
474 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
475 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["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 ([1],Res) False Or_to_List)*)
484 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
486 ([2],Res) [] Check_elementwise "Assumptions"*)
487 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
488 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
489 val asm = Ctree.get_assumptions pt p;
490 if f2str f = "[]" andalso
491 UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
492 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
493 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
495 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
496 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
497 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
498 "----- d2_pqformula2 ------";
499 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
500 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
501 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
503 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
506 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
507 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
509 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
510 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
511 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
512 case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
513 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
516 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
517 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
518 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
519 "----- d2_pqformula3 ------";
521 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
522 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
523 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
524 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
527 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
529 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
531 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
532 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
533 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
534 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
535 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
538 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
539 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
540 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
541 "----- d2_pqformula3_neg ------";
542 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
543 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
544 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
545 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
546 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
547 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
548 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
550 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
552 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
554 "TODO 2 + x + x \<up> 2 = 0";
555 "TODO 2 + x + x \<up> 2 = 0";
556 "TODO 2 + x + x \<up> 2 = 0";
558 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
559 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
560 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
561 "----- d2_pqformula4 ------";
562 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
563 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
564 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
565 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
566 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
567 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
568 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
571 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
574 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
575 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
577 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
578 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
579 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
580 "----- d2_pqformula5 ------";
581 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
582 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
583 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
584 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
585 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
586 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
587 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
588 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
593 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
594 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
596 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
597 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
598 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
599 "----- d2_pqformula6 ------";
600 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
601 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
602 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
603 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
604 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
605 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
608 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;
612 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
613 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
615 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
616 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
617 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
618 "----- d2_pqformula7 ------";
620 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
621 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
622 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
623 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
624 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
625 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
627 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;
632 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
633 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
635 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
636 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
637 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
638 "----- d2_pqformula8 ------";
639 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
640 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
641 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
642 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
643 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
644 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
645 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
647 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;
651 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
652 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
654 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
655 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
656 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
657 "----- d2_pqformula9 ------";
658 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
659 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
660 ["PolyEq", "solve_d2_polyeq_pq_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 = 2, x = - 2]" => ()
670 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
673 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
674 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
675 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
676 "----- d2_pqformula9_neg ------";
677 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
678 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
679 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
680 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
681 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
682 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
683 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
684 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
685 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
686 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
687 "TODO 4 + 1*x \<up> 2 = 0";
688 "TODO 4 + 1*x \<up> 2 = 0";
689 "TODO 4 + 1*x \<up> 2 = 0";
691 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
692 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
693 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
694 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
695 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
696 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
697 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
698 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
699 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
700 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
701 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
702 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
703 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
704 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
705 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
706 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
708 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
709 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
710 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
711 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
712 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
713 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
714 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
715 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
716 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
717 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
719 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
720 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
721 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
722 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
723 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
724 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
727 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
728 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
729 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
731 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
732 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
733 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
734 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
735 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
736 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;
743 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
744 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
745 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
748 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
749 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
750 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
751 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
752 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
753 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
754 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
755 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;
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
762 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
763 "TODO 1 + x + 2*x \<up> 2 = 0";
764 "TODO 1 + x + 2*x \<up> 2 = 0";
765 "TODO 1 + x + 2*x \<up> 2 = 0";
768 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
769 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
770 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
771 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
772 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
775 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
776 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
777 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
778 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
779 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
780 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
782 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
783 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
784 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
785 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
786 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
792 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
793 "TODO 2 + 1*x + x \<up> 2 = 0";
794 "TODO 2 + 1*x + x \<up> 2 = 0";
795 "TODO 2 + 1*x + x \<up> 2 = 0";
798 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
799 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
800 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
801 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
802 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
805 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
806 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
807 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
808 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
809 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
810 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
812 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
813 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
814 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
815 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
816 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
820 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
821 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
822 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
823 "TODO 2 + x + x \<up> 2 = 0";
824 "TODO 2 + x + x \<up> 2 = 0";
825 "TODO 2 + x + x \<up> 2 = 0";
828 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
829 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
830 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
831 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
832 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
833 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
834 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
835 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
836 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
837 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
838 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
839 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
840 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
842 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
843 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
844 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
845 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
846 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
851 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 "TODO 8+ 2*x \<up> 2 = 0";
853 "TODO 8+ 2*x \<up> 2 = 0";
854 "TODO 8+ 2*x \<up> 2 = 0";
857 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
858 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
859 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
860 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
863 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
864 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
865 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
866 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
867 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
868 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
871 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
872 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
873 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
874 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
878 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
879 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
880 "TODO 4+ x \<up> 2 = 0";
881 "TODO 4+ x \<up> 2 = 0";
882 "TODO 4+ x \<up> 2 = 0";
885 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
886 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
887 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
888 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
889 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
893 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
894 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
895 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
896 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
897 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
899 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
900 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
901 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
902 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
903 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
904 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
905 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
906 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
907 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
908 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
909 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
910 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
911 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
914 val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"];
915 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
916 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
917 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
918 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
919 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
920 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
921 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
922 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
924 (*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f;
925 (*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt
927 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*)
928 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
929 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
930 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
931 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
934 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
935 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
936 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
937 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
938 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
939 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
940 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
941 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
942 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
943 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
944 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
945 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
946 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
949 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
950 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
951 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
952 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
953 see --- val rls = calculate_RootRat > calculate_Rational ---
954 calculate_RootRat was a TODO with 2002, requires re-design.
955 see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
957 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
958 "solveFor x", "solutions L"];
960 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
961 ["PolyEq", "complete_square"]);
962 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
963 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
964 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
965 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
967 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
968 (*Apply_Method ("PolyEq", "complete_square")*)
969 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
970 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
971 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
972 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
973 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
974 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
975 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
976 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
977 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
978 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
979 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
980 - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
981 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
982 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
983 - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
984 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
985 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
986 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
987 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
988 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
989 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
990 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
991 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
992 (*"x = - 2 | x = 4" nxt = Or_to_List*)
993 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
994 (*"[x = - 2, x = 4]" nxt = Check_Postcond*)
995 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
997 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
998 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1001 "[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))]"
1002 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1003 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1006 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1007 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1008 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1009 (*stopped due to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1010 see --- val rls = calculate_RootRat > calculate_Rational ---*)
1011 val thy = @{theory PolyEq};
1012 val ctxt = Proof_Context.init_global thy;
1013 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1014 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1016 val rls = complete_square;
1017 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1018 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
1019 then () else error "rls complete_square CHANGED";
1021 val thm = @{thm square_explicit1};
1022 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1023 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
1024 then () else error "thm square_explicit1 CHANGED";
1026 val thm = @{thm root_plus_minus};
1027 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1028 if UnparseC.term t =
1029 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1030 then () else error "thm root_plus_minus CHANGED";
1032 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1033 val thm = @{thm bdv_explicit2};
1034 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1035 if UnparseC.term t =
1036 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1037 then () else error "thm bdv_explicit2 CHANGED";
1039 val thm = @{thm bdv_explicit3};
1040 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1041 if UnparseC.term t =
1042 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1043 then () else error "thm bdv_explicit3 CHANGED";
1045 val thm = @{thm bdv_explicit2};
1046 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1047 if UnparseC.term t =
1048 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1049 then () else error "thm bdv_explicit2 CHANGED";
1051 val rls = calculate_RootRat;
1052 val SOME (t,asm) = rewrite_set_ thy true rls t;
1053 if UnparseC.term t =
1054 "- 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))"
1055 (*"- 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*)
1056 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1057 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
1060 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1061 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1062 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1063 "---- test the erls ----";
1064 val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1";
1065 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1066 val t' = UnparseC.term t;
1067 (*if t'= \<^const_name>\<open>True\<close> then ()
1068 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1070 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
1071 "solveFor x", "solutions L"];
1073 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1074 ["PolyEq", "complete_square"]);
1075 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1076 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1077 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1078 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1079 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1080 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1081 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1082 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1083 (*Apply_Method ("PolyEq", "complete_square")*)
1084 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1086 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1087 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1088 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1089 val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
1090 "solveFor x", "solutions L"];
1092 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1093 ["PolyEq", "complete_square"]);
1094 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1095 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1096 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1097 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1098 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1099 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1102 (*Apply_Method ("PolyEq", "complete_square")*)
1103 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1104 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1106 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1107 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1108 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1109 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1110 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1111 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1112 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1114 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1115 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";