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 "----------- 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 ---------------------";
53 Rewrite.trace_on:=false; (*true false*)
55 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
57 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
58 else error "polyeq.sml: diff.behav. in lhs";
60 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
61 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
62 if (UnparseC.term t) = "True" then ()
63 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
65 val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x";
66 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
67 if (UnparseC.term t) = "False" then ()
68 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
70 val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
71 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
72 if (UnparseC.term t) = "True" then ()
73 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
75 val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
76 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
77 if (UnparseC.term t) = "True" then ()
78 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
81 val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
82 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
83 if (UnparseC.term t) = "True" then ()
84 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
86 val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
87 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
88 if (UnparseC.term t) = "True" then ()
89 else error "polyeq.sml: diff.behav. in has_degree_in_in";
91 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2";
92 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
93 if (UnparseC.term 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 (TermC.parse thy))
97 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
98 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
99 if (UnparseC.term 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 (TermC.parse thy))
103 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
104 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
105 if (UnparseC.term 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 \<up> 2 = 0)", "solveFor x", "solutions L"];
112 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
113 M_Match.Matches' {Find = [Correct "solutions L"],
115 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
116 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)",
117 Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"],
119 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
121 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
122 M_Match.Matches' {Find = [Correct "solutions L"],
124 Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
125 Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"],
126 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
127 then () else error "M_Match.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 (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 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 \<up> 2)) = 0";
143 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t;
145 "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0";
146 (* bei Verwendung von "size_of-term" nach MG :*)
147 (*"x \<up> 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 \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0";
153 (* "x \<up> 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 \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0";
159 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
160 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
162 (*das rewriting l"asst sich beobachten mit
163 Rewrite.trace_on := false; (*true false*)
166 "------ 15.11.02 --------------------------";
167 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x";
168 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
169 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
171 Rewrite.trace_on := false; (*true 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 (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 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 \<up> 2";
190 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 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 \<up> 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 (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2";
212 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
215 rewrite_set_ thy false discard_parentheses t;
217 "(7 + x) * a \<up> 2";
219 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi";
221 val t = (Thm.term_of o the o (parseold thy)) "7";
222 ##################################################################################*)
225 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
226 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
227 "----------- open local of fun ord_make_polynomial_in ------------------------------------------";
228 (* termorder hacked by MG, adapted later by WN *)
229 (** )local ( *. for make_polynomial_in .*)
231 open Term; (* for type order = EQUAL | LESS | GREATER *)
233 fun pr_ord EQUAL = "EQUAL"
234 | pr_ord LESS = "LESS"
235 | pr_ord GREATER = "GREATER";
237 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
238 | dest_hd' x (t as Free (a, T)) =
239 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
240 else (((a, 0), T), 1)
241 | dest_hd' _ (Var v) = (v, 2)
242 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
243 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
244 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
246 fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
247 Free (var, _) $ Free (pot, _)) =
248 (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
252 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
253 1000 * (the (TermC.int_opt_of_string pot)))
254 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
255 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
256 | size_of_term' i pr x (t as Abs (_, _, body)) =
257 (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
258 1 + size_of_term' (i + 1) pr x body)
259 | size_of_term' i pr x (f $ t) =
261 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
262 val s1 = size_of_term' (i + 1) pr x f
263 val s2 = size_of_term' (i + 1) pr x t
264 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
266 | size_of_term' i pr x t =
267 (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
273 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
274 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
275 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
276 | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
278 fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
280 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
282 case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
283 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
285 | term_ord' i pr x _ (t, u) =
287 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
289 case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
291 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
293 (case hd_ord (i + 1) pr x (f, g) of
294 EQUAL => (terms_ord x (i + 1) pr) (ts, us)
298 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
300 and hd_ord i pr x (f, g) = (* ~ term.ML *)
302 val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
304 (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
305 (dest_hd' x f, dest_hd' x g)
306 val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
308 and terms_ord x i pr (ts, us) =
310 val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
311 val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
312 val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
317 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
318 ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
321 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
322 | _ => 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 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 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 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, (Thm.term_of o the o (TermC.parse thy)) "a")];
345 val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")];
346 val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")];
348 val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x";
349 val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
350 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b";
351 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b";
353 if ord_make_polynomial_in 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 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 true thy substb (x1,x2) = false(*GREATER*) then ()
360 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
362 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
363 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
364 ord_make_polynomial_in true thy substx (aa, bb);
367 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x";
368 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3";
369 ord_make_polynomial_in true thy substa (aa, bb);
370 false; (* => GREATER *)
372 (* und nach dem Re-engineering der Termorders in den 'rulesets'
373 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
374 val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
375 val x = (Thm.term_of o the o (TermC.parse thy)) "x";
376 val a = (Thm.term_of o the o (TermC.parse thy)) "a";
377 val b = (Thm.term_of o the o (TermC.parse thy)) "b";
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 = (Thm.term_of o the o (TermC.parse thy)) 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 + 0" then ()
392 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
394 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
395 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
396 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
398 val ttt' = "(3*x + 5)/18 ::real";
399 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
400 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
401 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
402 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
404 (*============ inhibit exn WN120316 ==============================================
405 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
406 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
407 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
410 "----------- lin.eq degree_0 -------------------------------------";
411 "----------- lin.eq degree_0 -------------------------------------";
412 "----------- lin.eq degree_0 -------------------------------------";
413 "----- d0_false ------";
414 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
415 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
416 ["PolyEq", "solve_d0_polyeq_equation"]);
417 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ========
418 TODO: change to "equality (x + - 1*x = (0::real))"
419 and search for an appropriate problem and method.
421 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
423 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
424 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
425 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
426 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
429 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
431 "----- d0_true ------";
432 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"];
433 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"],
434 ["PolyEq", "solve_d0_polyeq_equation"]);
435 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
436 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
437 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
438 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
439 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
440 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
441 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
442 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
443 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
444 ============ inhibit exn WN110914 ============================================*)
446 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
447 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
448 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
449 "----- d2_pqformula1 ------!!!!";
450 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"];
452 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]);
453 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
454 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
459 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
460 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
461 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
462 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
464 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
466 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*)
467 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
471 if p = ([], Res) andalso
472 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then
473 case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1"
474 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2";
476 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
477 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
478 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------";
479 "----- d2_pqformula1_neg ------";
480 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"];
481 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]);
482 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
483 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
486 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
487 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
489 ([1],Res) False Or_to_List)*)
490 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
492 ([2],Res) [] Check_elementwise "Assumptions"*)
493 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
494 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
495 val asm = Ctree.get_assumptions pt p;
496 if f2str f = "[]" andalso
497 UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
498 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
499 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
501 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
502 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
503 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";
504 "----- d2_pqformula2 ------";
505 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
506 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
507 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
508 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
509 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
512 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
513 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
515 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
516 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
517 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
518 case f of Test_Out.FormKF "[x = 2, x = - 1]" => ()
519 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]";
522 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
523 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
524 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------";
525 "----- d2_pqformula3 ------";
527 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
528 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
529 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
530 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
531 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
534 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
535 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
537 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
538 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
539 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
540 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
541 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]";
544 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
545 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
546 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------";
547 "----- d2_pqformula3_neg ------";
548 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
549 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
550 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
551 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
552 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
554 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
555 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
556 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
560 "TODO 2 + x + x \<up> 2 = 0";
561 "TODO 2 + x + x \<up> 2 = 0";
562 "TODO 2 + x + x \<up> 2 = 0";
564 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
565 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
566 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------";
567 "----- d2_pqformula4 ------";
568 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
569 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
570 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
571 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
572 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
573 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
574 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
575 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
576 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
580 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
581 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]";
583 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
584 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
585 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------";
586 "----- d2_pqformula5 ------";
587 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
588 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
589 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
590 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
591 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
592 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
593 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
594 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
595 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
599 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
600 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]";
602 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
603 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
604 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------";
605 "----- d2_pqformula6 ------";
606 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
607 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
608 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
609 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
610 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
611 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
612 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
613 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
614 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
618 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
619 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]";
621 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
622 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
623 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------";
624 "----- d2_pqformula7 ------";
626 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
627 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
628 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
629 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
630 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
631 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
632 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
633 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
634 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;
638 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
639 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
641 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
642 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
643 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------";
644 "----- d2_pqformula8 ------";
645 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
646 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
647 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
648 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
649 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
650 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
651 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
652 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
657 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
658 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]";
660 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
661 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
662 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------";
663 "----- d2_pqformula9 ------";
664 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
665 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
666 ["PolyEq", "solve_d2_polyeq_pq_equation"]);
667 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
668 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;
670 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
675 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
676 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
679 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
680 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
681 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------";
682 "----- d2_pqformula9_neg ------";
683 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"];
684 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
685 ["PolyEq", "solve_d2_polyeq_pq_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;
689 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;
693 "TODO 4 + 1*x \<up> 2 = 0";
694 "TODO 4 + 1*x \<up> 2 = 0";
695 "TODO 4 + 1*x \<up> 2 = 0";
697 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
698 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
699 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
700 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
701 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
702 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
703 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
704 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
705 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
706 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
707 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
708 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
709 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
710 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
711 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => ()
712 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]";
714 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
715 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
716 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------";
717 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
718 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
719 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
720 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
721 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
722 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
723 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
729 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
730 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0";
733 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
734 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
735 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------";
737 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
738 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
739 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
740 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
741 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;
744 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
745 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
746 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
747 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
749 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
750 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => ()
751 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]";
754 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
755 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
756 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------";
757 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
758 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
759 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
760 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
761 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
762 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
764 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
765 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
766 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
767 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
769 "TODO 1 + x + 2*x \<up> 2 = 0";
770 "TODO 1 + x + 2*x \<up> 2 = 0";
771 "TODO 1 + x + 2*x \<up> 2 = 0";
774 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
775 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
776 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
777 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
778 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
779 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
780 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
781 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
782 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
783 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
784 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
785 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
786 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]";
788 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
789 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
790 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
791 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
792 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
793 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
794 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
795 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
796 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
797 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
798 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
799 "TODO 2 + 1*x + x \<up> 2 = 0";
800 "TODO 2 + 1*x + x \<up> 2 = 0";
801 "TODO 2 + 1*x + x \<up> 2 = 0";
804 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
805 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
806 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
807 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
808 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
809 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
810 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
811 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
812 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
813 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
814 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
815 case f of Test_Out.FormKF "[x = 1, x = - 2]" => ()
816 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]";
818 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
819 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
820 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
821 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
822 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
823 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
824 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
825 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
826 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
827 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
828 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
829 "TODO 2 + x + x \<up> 2 = 0";
830 "TODO 2 + x + x \<up> 2 = 0";
831 "TODO 2 + x + x \<up> 2 = 0";
834 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
835 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
836 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
837 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
838 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
839 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
840 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
841 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
846 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]";
848 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
849 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
850 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
851 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
853 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
855 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 "TODO 8+ 2*x \<up> 2 = 0";
859 "TODO 8+ 2*x \<up> 2 = 0";
860 "TODO 8+ 2*x \<up> 2 = 0";
863 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"];
864 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
865 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
866 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
867 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
868 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
869 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
870 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Test_Out.FormKF "[x = 2, x = - 2]" => ()
874 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]";
877 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"];
878 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]);
879 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
880 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
881 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
882 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
883 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
884 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
885 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
886 "TODO 4+ x \<up> 2 = 0";
887 "TODO 4+ x \<up> 2 = 0";
888 "TODO 4+ x \<up> 2 = 0";
891 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
892 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
893 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
894 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
895 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
896 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
897 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
898 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
899 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
900 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
901 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
902 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
903 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
905 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
906 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
907 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
908 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
909 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
910 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
913 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
916 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
917 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
920 val fmz = ["equality (x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"];
921 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
922 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
923 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
924 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
925 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
926 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
927 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
931 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => ()
932 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]";
935 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
936 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
937 ["PolyEq", "solve_d2_polyeq_abc_equation"]);
938 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
939 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
946 case f of Test_Out.FormKF "[x = 0, x = - 1]" => ()
947 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]";
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 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----";
953 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
954 see --- val rls = calculate_RootRat > calculate_Rational ---
955 calculate_RootRat was a TODO with 2002, requires re-design.
956 see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below
958 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
959 "solveFor x", "solutions L"];
961 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
962 ["PolyEq", "complete_square"]);
963 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
964 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;
966 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
968 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
969 (*Apply_Method ("PolyEq", "complete_square")*)
970 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
971 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
972 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
973 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*)
974 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
975 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*)
976 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
977 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
978 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
979 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
980 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |
981 - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*)
982 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
983 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
984 - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*)
985 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
986 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |
987 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*)
988 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
989 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) |
990 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational
991 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *)
992 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
993 (*"x = - 2 | x = 4" nxt = Or_to_List*)
994 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
995 (*"[x = - 2, x = 4]" nxt = Check_Postcond*)
996 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
998 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO
999 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]";
1002 "[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))]"
1003 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*)
1004 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]";
1007 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1008 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1009 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------";
1010 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
1011 see --- val rls = calculate_RootRat > calculate_Rational ---*)
1012 val thy = @{theory PolyEq};
1013 val ctxt = Proof_Context.init_global thy;
1014 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
1015 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1017 val rls = complete_square;
1018 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1019 UnparseC.term t = "-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2";
1021 val thm = ThmC.numerals_to_Free @{thm square_explicit1};
1022 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1023 UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8";
1025 val thm = ThmC.numerals_to_Free @{thm root_plus_minus};
1026 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1027 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1028 "\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1030 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1031 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1032 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1033 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1034 "\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8)";
1036 val thm = ThmC.numerals_to_Free @{thm bdv_explicit3};
1037 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1038 UnparseC.term t = "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) |"^
1039 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1041 val thm = ThmC.numerals_to_Free @{thm bdv_explicit2};
1042 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1043 UnparseC.term t = "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) |"^
1044 "\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))";
1046 val rls = calculate_RootRat;
1047 val SOME (t,asm) = rewrite_set_ thy true rls t;
1048 if UnparseC.term t =
1049 "- 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))"
1050 (*"- 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*)
1051 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
1052 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*)
1055 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1056 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1057 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1058 "---- test the erls ----";
1059 val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1";
1060 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1061 val t' = UnparseC.term t;
1062 (*if t'= \<^const_name>\<open>True\<close> then ()
1063 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1065 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)",
1066 "solveFor x", "solutions L"];
1068 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1069 ["PolyEq", "complete_square"]);
1070 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1071 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1072 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1073 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1074 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1075 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1076 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1077 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1078 (*Apply_Method ("PolyEq", "complete_square")*)
1079 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1081 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1082 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1083 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------";
1084 val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)",
1085 "solveFor x", "solutions L"];
1087 ("PolyEq",["degree_2", "expanded", "univariate", "equation"],
1088 ["PolyEq", "complete_square"]);
1089 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1090 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1091 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1092 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1093 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1094 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1095 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1096 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1097 (*Apply_Method ("PolyEq", "complete_square")*)
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
1109 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1110 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";