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 "----------- lin.eq degree_0 -------------------------------------";
16 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
17 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
18 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
19 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
20 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
21 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
22 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
23 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
24 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
25 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
26 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
27 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
28 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
29 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
30 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
31 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
32 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
33 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
34 "-----------------------------------------------------------------";
35 "------ polyeq-2.sml ---------------------------------------------";
36 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
37 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
38 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
39 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
40 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
41 "----------- rls make_polynomial_in ------------------------------";
42 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
43 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";
44 "-----------------------------------------------------------------";
45 "-----------------------------------------------------------------";
47 "----------- tests on predicates in problems ---------------------";
48 "----------- tests on predicates in problems ---------------------";
49 "----------- tests on predicates in problems ---------------------";
50 (* trace_rewrite:=true;
53 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
54 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
55 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
56 else error "polyeq.sml: diff.behav. in lhs";
58 val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
59 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
60 if (term2str t) = "True" then ()
61 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
63 val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
64 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
65 if (term2str t) = "False" then ()
66 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
68 val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
69 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
70 if (term2str t) = "True" then ()
71 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
73 val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
74 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
75 if (term2str t) = "True" then ()
76 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
79 val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
80 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
81 if (term2str t) = "True" then ()
82 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
84 val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
85 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
86 if (term2str t) = "True" then ()
87 else error "polyeq.sml: diff.behav. in has_degree_in_in";
89 val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
90 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
91 if (term2str t) = "False" then ()
92 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
94 val t4 = (Thm.term_of o the o (parse thy))
95 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
96 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
97 if (term2str t) = "False" then ()
98 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
100 val t5 = (Thm.term_of o the o (parse thy))
101 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
102 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
103 if (term2str t) = "True" then ()
104 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
106 "----------- test matching problems --------------------------0---";
107 "----------- test matching problems --------------------------0---";
108 "----------- test matching problems --------------------------0---";
109 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
110 if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
111 Matches' {Find = [Correct "solutions L"],
113 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
114 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
115 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
117 then () else error "match_pbl [expanded,univariate,equation]";
119 if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
120 Matches' {Find = [Correct "solutions L"],
122 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
123 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
124 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
125 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
127 "----------- lin.eq degree_0 -------------------------------------";
128 "----------- lin.eq degree_0 -------------------------------------";
129 "----------- lin.eq degree_0 -------------------------------------";
130 "----- d0_false ------";
131 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
132 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
133 ["PolyEq","solve_d0_polyeq_equation"]);
134 (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
135 TODO: change to "equality (x + -1*x = (0::real))"
136 and search for an appropriate problem and method.
138 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
139 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
141 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
145 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
146 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
148 "----- d0_true ------";
149 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
150 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
151 ["PolyEq","solve_d0_polyeq_equation"]);
152 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
159 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
160 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
161 ============ inhibit exn WN110914 ============================================*)
163 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
164 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
165 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
166 "----- d2_pqformula1 ------!!!!";
167 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
169 ("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
170 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
171 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
172 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
173 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
174 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
175 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
176 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
177 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
178 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
179 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
180 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
181 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
183 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
184 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
185 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
186 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
187 val (mI,m) = mk_tac'_ tac;
188 val Appl m = applicable_in p pt m;
189 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
190 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
192 term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
193 terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
194 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
195 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
196 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
197 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
198 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
199 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
200 member op = specsteps mI (*false*);
201 (*loc_solve_ (mI,m) ptp;
202 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
203 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
205 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
206 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
207 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
208 val thy' = get_obj g_domID pt (par_pblobj pt p);
209 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
211 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
212 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
213 "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'),
214 (scr as Prog (h $ body),d), (Pstate (E,l,a,v,S,b), ctxt)) =
215 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
216 val thy = assoc_thy thy';
217 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
218 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
219 ... Assoc ... is correct*)
220 "~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
221 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
222 1 < length l (*true*);
223 val up = drop_last l;
226 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
227 ... ???? ... is correct*)
228 "~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
229 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
230 val l = drop_last l; (*comes from e, goes to Abs*)
231 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
232 val i = mk_Free (i, T);
233 val E = Env.upd_env E (i, v);
234 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
235 val [(tac_, mout, ctree, pos', xxx)] = ss;
236 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
237 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
238 ... Assoc ... is correct*)
239 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
240 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
241 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
242 val ctxt = get_ctxt pt (p,p_)
243 val p' = lev_on p : pos;
244 (* WAS val NotAss = associate pt d (m, stac)
245 ... Ass ... is correct*)
246 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
247 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
250 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
251 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
253 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
254 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
255 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
256 "----- d2_pqformula1_neg ------";
257 val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
258 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
259 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
260 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
261 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
264 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
266 ([1],Res) False Or_to_List)*)
267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
269 ([2],Res) [] Check_elementwise "Assumptions"*)
270 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
271 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
272 val asm = get_assumptions_ pt p;
273 if f2str f = "[]" andalso
274 terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
275 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
276 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
278 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
279 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
280 "----------- equality (-2 +(-1)*x + 1*x^^^2 = 0) ---------------------------------------------";
281 "----- d2_pqformula2 ------";
282 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
283 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
284 ["PolyEq","solve_d2_polyeq_pq_equation"]);
286 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
287 val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
288 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
289 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
290 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
291 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
295 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
296 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
297 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
298 case f of FormKF "[x = 2, x = -1]" => ()
299 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
302 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
303 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
304 "----------- equality (-2 + x + x^^^2 = 0) ---------------------------------------------------";
305 "----- d2_pqformula3 ------";
307 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
308 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
309 ["PolyEq","solve_d2_polyeq_pq_equation"]);
310 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
314 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
315 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
319 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
320 case f of FormKF "[x = 1, x = -2]" => ()
321 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
324 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
325 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
326 "----------- equality (2 + x + x^^^2 = 0) ----------------------------------------------------";
327 "----- d2_pqformula3_neg ------";
328 val fmz = ["equality (2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
329 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
330 ["PolyEq","solve_d2_polyeq_pq_equation"]);
331 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
332 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
334 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
335 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
336 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
338 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
339 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
340 "TODO 2 + x + x^^^2 = 0";
341 "TODO 2 + x + x^^^2 = 0";
342 "TODO 2 + x + x^^^2 = 0";
344 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
345 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
346 "----------- equality (-2 + x + 1*x^^^2 = 0)) ------------------------------------------------";
347 "----- d2_pqformula4 ------";
348 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
349 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
350 ["PolyEq","solve_d2_polyeq_pq_equation"]);
351 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
353 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
354 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
355 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
356 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
357 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
358 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
359 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
360 case f of FormKF "[x = 1, x = -2]" => ()
361 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
363 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
364 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
365 "----------- equality (1*x + x^^^2 = 0) ----------------------------------------------------";
366 "----- d2_pqformula5 ------";
367 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
368 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
369 ["PolyEq","solve_d2_polyeq_pq_equation"]);
370 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
372 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
373 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
374 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
375 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
376 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
377 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
378 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
379 case f of FormKF "[x = 0, x = -1]" => ()
380 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
382 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
383 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
384 "----------- equality (1*x + 1*x^^^2 = 0) ----------------------------------------------------";
385 "----- d2_pqformula6 ------";
386 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
387 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
388 ["PolyEq","solve_d2_polyeq_pq_equation"]);
389 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
390 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
392 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
398 case f of FormKF "[x = 0, x = -1]" => ()
399 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
401 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
402 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
403 "----------- equality (x + x^^^2 = 0) ------------------------------------------------------";
404 "----- d2_pqformula7 ------";
406 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
407 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
408 ["PolyEq","solve_d2_polyeq_pq_equation"]);
409 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
410 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
411 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
412 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
413 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
414 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
415 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
416 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
417 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
418 case f of FormKF "[x = 0, x = -1]" => ()
419 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
421 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
422 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
423 "----------- equality (x + 1*x^^^2 = 0) ------------------------------------------------------";
424 "----- d2_pqformula8 ------";
425 val fmz = ["equality (x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
426 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
427 ["PolyEq","solve_d2_polyeq_pq_equation"]);
428 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
437 case f of FormKF "[x = 0, x = -1]" => ()
438 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
440 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
441 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
442 "----------- equality (-4 + x^^^2 = 0) -------------------------------------------------------";
443 "----- d2_pqformula9 ------";
444 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
445 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
446 ["PolyEq","solve_d2_polyeq_pq_equation"]);
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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
450 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
451 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
452 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
453 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
454 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
455 case f of FormKF "[x = 2, x = -2]" => ()
456 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
459 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
460 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
461 "----------- equality (4 + 1*x^^^2 = 0) -------------------------------------------------------";
462 "----- d2_pqformula9_neg ------";
463 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
464 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
465 ["PolyEq","solve_d2_polyeq_pq_equation"]);
466 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
467 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
468 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
471 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
472 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
473 "TODO 4 + 1*x^^^2 = 0";
474 "TODO 4 + 1*x^^^2 = 0";
475 "TODO 4 + 1*x^^^2 = 0";
477 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
478 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
479 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
480 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
481 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
482 ["PolyEq","solve_d2_polyeq_abc_equation"]);
483 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
484 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;
488 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
489 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
490 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
491 case f of FormKF "[x = 1, x = -1 / 2]" => ()
492 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
494 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
495 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
496 "----------- equality (1 +(-1)*x + 2*x^^^2 = 0) ----------------------------------------------";
497 val fmz = ["equality (1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
498 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
499 ["PolyEq","solve_d2_polyeq_abc_equation"]);
500 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
501 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
502 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
503 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;
508 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
509 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
510 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
513 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
514 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
515 "----------- equality (-1 + x + 2*x^^^2 = 0) -------------------------------------------------";
517 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
518 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
519 ["PolyEq","solve_d2_polyeq_abc_equation"]);
520 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
521 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
522 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
529 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
530 case f of FormKF "[x = 1 / 2, x = -1]" => ()
531 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
534 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
535 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
536 "----------- equality (1 + x + 2*x^^^2 = 0) --------------------------------------------------";
537 val fmz = ["equality (1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
538 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
539 ["PolyEq","solve_d2_polyeq_abc_equation"]);
540 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
541 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
542 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
544 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
545 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
546 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
549 "TODO 1 + x + 2*x^^^2 = 0";
550 "TODO 1 + x + 2*x^^^2 = 0";
551 "TODO 1 + x + 2*x^^^2 = 0";
554 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
555 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
556 ["PolyEq","solve_d2_polyeq_abc_equation"]);
557 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
558 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
559 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
560 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
561 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
562 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
563 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
564 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
565 case f of FormKF "[x = 1, x = -2]" => ()
566 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
568 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
569 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
570 ["PolyEq","solve_d2_polyeq_abc_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;
579 "TODO 2 + 1*x + x^^^2 = 0";
580 "TODO 2 + 1*x + x^^^2 = 0";
581 "TODO 2 + 1*x + x^^^2 = 0";
584 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
585 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
586 ["PolyEq","solve_d2_polyeq_abc_equation"]);
587 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
588 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
589 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
590 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
591 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
592 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
593 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
594 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
595 case f of FormKF "[x = 1, x = -2]" => ()
596 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
598 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
599 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
600 ["PolyEq","solve_d2_polyeq_abc_equation"]);
601 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
602 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
603 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
604 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
609 "TODO 2 + x + x^^^2 = 0";
610 "TODO 2 + x + x^^^2 = 0";
611 "TODO 2 + x + x^^^2 = 0";
614 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
615 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
616 ["PolyEq","solve_d2_polyeq_abc_equation"]);
617 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
618 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
619 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
620 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
621 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
622 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
623 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
624 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
625 case f of FormKF "[x = 2, x = -2]" => ()
626 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
628 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
629 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
630 ["PolyEq","solve_d2_polyeq_abc_equation"]);
631 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
632 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
638 "TODO 8+ 2*x^^^2 = 0";
639 "TODO 8+ 2*x^^^2 = 0";
640 "TODO 8+ 2*x^^^2 = 0";
643 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
644 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
645 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
646 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; 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 case f of FormKF "[x = 2, x = -2]" => ()
654 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
657 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
658 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
659 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
660 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
661 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
662 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
671 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
672 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
673 ["PolyEq","solve_d2_polyeq_abc_equation"]);
674 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
675 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
676 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
677 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
678 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
679 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
680 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
681 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
682 case f of FormKF "[x = 0, x = -1]" => ()
683 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
685 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
686 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
687 ["PolyEq","solve_d2_polyeq_abc_equation"]);
688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
689 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
690 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
691 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
692 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
693 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
694 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
696 case f of FormKF "[x = 0, x = -1]" => ()
697 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
700 val fmz = ["equality (x + 2*x^^^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 FormKF "[x = 0, x = -1 / 2]" => ()
712 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
715 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
716 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
717 ["PolyEq","solve_d2_polyeq_abc_equation"]);
718 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
719 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 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;
724 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
725 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
726 case f of FormKF "[x = 0, x = -1]" => ()
727 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
730 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
731 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
732 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
733 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
734 see --- val rls = calculate_RootRat > calculate_Rational ---
735 calculate_RootRat was a TODO with 2002, requires re-design.
736 see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
738 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
739 "solveFor x","solutions L"];
741 ("PolyEq",["degree_2","expanded","univariate","equation"],
742 ["PolyEq","complete_square"]);
743 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
744 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;
748 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
749 (*Apply_Method ("PolyEq","complete_square")*)
750 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
751 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
752 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
753 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
754 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
755 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
756 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
757 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
758 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
759 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
760 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
761 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
762 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
763 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
764 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
765 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
766 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
767 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
768 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
769 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
770 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
771 NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
772 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
773 (*"x = -2 | x = 4" nxt = Or_to_List*)
774 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
775 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
776 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
778 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
779 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
782 "[x = -1 * -1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))]"
783 (*"[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]"*)
784 then () else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
787 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
788 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
789 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
790 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
791 see --- val rls = calculate_RootRat > calculate_Rational ---*)
792 val thy = @{theory PolyEq};
793 val ctxt = Proof_Context.init_global thy;
794 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
795 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
797 val rls = complete_square;
798 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
799 term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
801 val thm = num_str @{thm square_explicit1};
802 val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
803 term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
805 val thm = num_str @{thm root_plus_minus};
806 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
807 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
808 "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
810 (*the thm bdv_explicit2* here required to be constrained to ::real*)
811 val thm = num_str @{thm bdv_explicit2};
812 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
813 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
814 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
816 val thm = num_str @{thm bdv_explicit3};
817 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
818 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
819 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
821 val thm = num_str @{thm bdv_explicit2};
822 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
823 term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
824 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
826 val rls = calculate_RootRat;
827 val SOME (t,asm) = rewrite_set_ thy true rls t;
829 "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
830 (*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
831 then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
832 (*SHOULD BE: term2str = "x = -2 | x = 4;*)
835 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
836 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
837 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
838 "---- test the erls ----";
839 val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
840 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
842 (*if t'= "HOL.True" then ()
843 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
845 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
846 "solveFor x","solutions L"];
848 ("PolyEq",["degree_2","expanded","univariate","equation"],
849 ["PolyEq","complete_square"]);
850 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
851 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
853 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
855 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
857 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
858 (*Apply_Method ("PolyEq","complete_square")*)
859 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
861 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
862 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
863 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
864 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
865 "solveFor x","solutions L"];
867 ("PolyEq",["degree_2","expanded","univariate","equation"],
868 ["PolyEq","complete_square"]);
869 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
870 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
871 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
874 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
875 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
876 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
877 (*Apply_Method ("PolyEq","complete_square")*)
878 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
879 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
880 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
881 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
882 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
883 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
884 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
885 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
886 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
887 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
889 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
890 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";