1 (* testexamples for PolyEq, poynomial equations and equational systems
2 author: Richard Lang 2003
3 (c) due to copyright terms
4 WN030609: some expls dont work due to unfinished handling of 'expanded terms';
5 others marked with TODO have to be checked, too.
8 "-----------------------------------------------------------------";
9 "table of contents -----------------------------------------------";
10 (*WN060608 some ----- are not in this table*)
11 "-----------------------------------------------------------------";
12 "----------- tests on predicates in problems ---------------------";
13 "----------- test matching problems --------------------------0---";
14 "----------- lin.eq degree_0 -------------------------------------";
15 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
16 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
17 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
18 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
19 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
20 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
21 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
22 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
23 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
24 "-----------------------------------------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
28 "----------- tests on predicates in problems ---------------------";
29 "----------- tests on predicates in problems ---------------------";
30 "----------- tests on predicates in problems ---------------------";
35 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
36 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
37 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
38 else error "polyeq.sml: diff.behav. in lhs";
40 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
41 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
42 if (term2str t) = "True" then ()
43 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
45 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
46 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
47 if (term2str t) = "False" then ()
48 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
50 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
51 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
52 if (term2str t) = "True" then ()
53 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
55 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
57 if (term2str t) = "True" then ()
58 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
61 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
62 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
63 if (term2str t) = "True" then ()
64 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
66 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
67 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
68 if (term2str t) = "True" then ()
69 else error "polyeq.sml: diff.behav. in has_degree_in_in";
71 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
72 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
73 if (term2str t) = "False" then ()
74 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
76 val t4 = (term_of o the o (parse thy))
77 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
78 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
79 if (term2str t) = "False" then ()
80 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
82 val t5 = (term_of o the o (parse thy))
83 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
84 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
85 if (term2str t) = "True" then ()
86 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
88 "----------- test matching problems --------------------------0---";
89 "----------- test matching problems --------------------------0---";
90 "----------- test matching problems --------------------------0---";
91 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
92 if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
93 Matches' {Find = [Correct "solutions L"],
95 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
96 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
97 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
99 then () else error "match_pbl [expanded,univariate,equation]";
101 if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
102 Matches' {Find = [Correct "solutions L"],
104 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
105 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
106 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
107 then () else error "match_pbl [degree_2,expanded,univariate,equation]";
109 "----------- lin.eq degree_0 -------------------------------------";
110 "----------- lin.eq degree_0 -------------------------------------";
111 "----------- lin.eq degree_0 -------------------------------------";
112 "----- d0_false ------";
113 (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
114 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
115 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
116 ["PolyEq","solve_d0_polyeq_equation"]);
117 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
118 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
120 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
124 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
125 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
127 "----- d0_true ------";
128 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
129 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
130 ["PolyEq","solve_d0_polyeq_equation"]);
131 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
132 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
135 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
136 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
137 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
138 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
139 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
140 ============ inhibit exn WN110914 ============================================*)
142 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
143 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
144 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
145 "----- d2_pqformula1 ------!!!!";
146 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
148 ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
149 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
161 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
162 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
163 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
164 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
165 val (mI,m) = mk_tac'_ tac;
166 val Appl m = applicable_in p pt m;
167 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
168 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
170 term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
171 terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
172 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
173 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
174 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
175 "\"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\","^
176 "\"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\"]";
177 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
178 member op = specsteps mI (*false*);
179 (*loc_solve_ (mI,m) ptp;
180 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
181 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
183 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
184 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
185 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
186 val thy' = get_obj g_domID pt (par_pblobj pt p);
187 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
189 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
190 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
191 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
192 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
193 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
194 val thy = assoc_thy thy';
195 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
196 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
197 ... Assoc ... is correct*)
198 "~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
199 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
200 1 < length l (*true*);
201 val up = drop_last l;
204 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
205 ... ???? ... is correct*)
206 "~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
207 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
208 val l = drop_last l; (*comes from e, goes to Abs*)
209 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
210 val i = mk_Free (i, T);
211 val E = upd_env E (i, v);
212 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
213 val [(tac_, mout, ptree, pos', xxx)] = ss;
214 val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
215 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
216 ... Assoc ... is correct*)
217 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
218 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
219 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
220 val ctxt = get_ctxt pt (p,p_)
221 val p' = lev_on p : pos;
222 (* WAS val NotAss = assod pt d m stac
223 ... Ass ... is correct*)
224 "~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
225 (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
228 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
229 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
235 "----- d2_pqformula1_neg ------";
236 val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
237 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
238 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
239 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
240 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
241 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
242 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
245 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
247 ([1],Res) False Or_to_List)*)
248 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
250 ([2],Res) [] Check_elementwise "Assumptions"*)
251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
252 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
253 val asm = get_assumptions_ pt p;
254 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
255 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
259 "----- d2_pqformula2 ------";
260 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
261 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
262 ["PolyEq","solve_d2_polyeq_pq_equation"]);
264 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
265 val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
267 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
268 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
269 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
270 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
271 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
272 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
273 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
274 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
276 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
279 "----- d2_pqformula2_neg ------";
280 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
281 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
282 ["PolyEq","solve_d2_polyeq_pq_equation"]);
283 (*val p = e_pos'; val c = [];
284 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
285 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
286 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
287 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
288 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
289 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
294 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
295 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
296 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
299 "----- d2_pqformula3 ------";
301 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
302 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
303 ["PolyEq","solve_d2_polyeq_pq_equation"]);
304 (*val p = e_pos'; val c = [];
305 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
306 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
307 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 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;
316 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
317 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
319 "----- d2_pqformula3_neg ------";
320 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
321 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
322 ["PolyEq","solve_d2_polyeq_pq_equation"]);
323 (*val p = e_pos'; val c = [];
324 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
325 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
326 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
327 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
331 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
332 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
334 "TODO 2 + x + x^^^2 = 0";
335 "TODO 2 + x + x^^^2 = 0";
336 "TODO 2 + x + x^^^2 = 0";
339 "----- d2_pqformula4 ------";
340 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
341 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
342 ["PolyEq","solve_d2_polyeq_pq_equation"]);
343 (*val p = e_pos'; val c = [];
344 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
345 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
346 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
348 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
349 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
350 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
351 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
352 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
355 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
356 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
358 "----- d2_pqformula4_neg ------";
359 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
360 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
361 ["PolyEq","solve_d2_polyeq_pq_equation"]);
362 (*val p = e_pos'; val c = [];
363 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
364 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
365 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
366 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
367 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
368 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
372 "TODO 2 + x + 1*x^^^2 = 0";
373 "TODO 2 + x + 1*x^^^2 = 0";
374 "TODO 2 + x + 1*x^^^2 = 0";
376 "----- d2_pqformula5 ------";
377 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
378 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
379 ["PolyEq","solve_d2_polyeq_pq_equation"]);
380 (*val p = e_pos'; val c = [];
381 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
382 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
383 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
384 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
385 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
386 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
387 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
388 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
389 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
392 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
393 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
395 "----- d2_pqformula6 ------";
396 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
397 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
398 ["PolyEq","solve_d2_polyeq_pq_equation"]);
399 (*val p = e_pos'; val c = [];
400 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
401 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
402 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
403 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
404 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
405 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
406 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
407 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
408 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
409 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
410 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
411 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
412 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
414 "----- d2_pqformula7 ------";
416 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
417 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
418 ["PolyEq","solve_d2_polyeq_pq_equation"]);
419 (*val p = e_pos'; val c = [];
420 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
421 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
422 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
423 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
431 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
432 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
434 "----- d2_pqformula8 ------";
435 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
436 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
437 ["PolyEq","solve_d2_polyeq_pq_equation"]);
438 (*val p = e_pos'; val c = [];
439 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
440 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
443 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
444 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
445 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
446 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
447 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
448 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
451 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
452 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
454 "----- d2_pqformula9 ------";
455 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
456 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
457 ["PolyEq","solve_d2_polyeq_pq_equation"]);
458 (*val p = e_pos'; val c = [];
459 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
460 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
462 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
464 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
465 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
466 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
467 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
471 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
474 "----- d2_pqformula10_neg ------";
475 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
476 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
477 ["PolyEq","solve_d2_polyeq_pq_equation"]);
478 (*val p = e_pos'; val c = [];
479 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
480 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
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;
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;
490 "TODO 4 + x^^^2 = 0";
491 "TODO 4 + x^^^2 = 0";
492 "TODO 4 + x^^^2 = 0";
494 "----- d2_pqformula10 ------";
495 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
496 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
497 ["PolyEq","solve_d2_polyeq_pq_equation"]);
498 (*val p = e_pos'; val c = [];
499 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
500 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
503 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
504 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
505 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
506 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
507 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
508 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
509 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
511 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
513 "----- d2_pqformula9_neg ------";
514 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
515 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
516 ["PolyEq","solve_d2_polyeq_pq_equation"]);
517 (*val p = e_pos'; val c = [];
518 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
519 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
521 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
522 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
523 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
524 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
528 "TODO 4 + 1*x^^^2 = 0";
529 "TODO 4 + 1*x^^^2 = 0";
530 "TODO 4 + 1*x^^^2 = 0";
532 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
533 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
534 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
536 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
537 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
538 ["PolyEq","solve_d2_polyeq_abc_equation"]);
539 (*val p = e_pos'; val c = [];
540 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
541 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
543 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
544 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
550 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
551 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
552 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
554 val fmz = ["equality ( 1 +(-1)*x + 2*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 = e_pos'; val c = [];
558 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
559 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
561 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
562 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
566 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
567 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
568 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
569 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
570 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
573 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
574 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
575 ["PolyEq","solve_d2_polyeq_abc_equation"]);
576 (*val p = e_pos'; val c = [];
577 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
578 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
580 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
581 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
582 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
583 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
584 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
585 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
586 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
587 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
588 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
589 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
591 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
592 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
593 ["PolyEq","solve_d2_polyeq_abc_equation"]);
594 (*val p = e_pos'; val c = [];
595 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
596 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
598 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
599 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
600 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
601 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
602 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
606 "TODO 1 + x + 2*x^^^2 = 0";
607 "TODO 1 + x + 2*x^^^2 = 0";
608 "TODO 1 + x + 2*x^^^2 = 0";
610 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
611 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
612 ["PolyEq","solve_d2_polyeq_abc_equation"]);
613 (*val p = e_pos'; val c = [];
614 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
615 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
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 Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
626 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
628 val fmz = ["equality ( 2 + 1*x + 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 = e_pos'; val c = [];
632 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
633 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
635 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
636 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
637 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
638 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
639 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
640 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
641 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
642 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
643 "TODO 2 + 1*x + x^^^2 = 0";
644 "TODO 2 + 1*x + x^^^2 = 0";
645 "TODO 2 + 1*x + x^^^2 = 0";
648 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
649 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
650 ["PolyEq","solve_d2_polyeq_abc_equation"]);
651 (*val p = e_pos'; val c = [];
652 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
653 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
655 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
656 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
657 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
658 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
659 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
660 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
664 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
666 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
667 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
668 ["PolyEq","solve_d2_polyeq_abc_equation"]);
669 (*val p = e_pos'; val c = [];
670 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
671 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
673 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
674 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
675 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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;
681 "TODO 2 + x + x^^^2 = 0";
682 "TODO 2 + x + x^^^2 = 0";
683 "TODO 2 + x + x^^^2 = 0";
686 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
687 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
688 ["PolyEq","solve_d2_polyeq_abc_equation"]);
689 (*val p = e_pos'; val c = [];
690 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
691 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
693 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
694 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
696 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
697 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
698 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
699 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
700 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
701 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
702 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
704 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
705 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
706 ["PolyEq","solve_d2_polyeq_abc_equation"]);
707 (*val p = e_pos'; val c = [];
708 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
709 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
711 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
712 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
713 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
714 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
715 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
716 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
717 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
718 "TODO 8+ 2*x^^^2 = 0";
719 "TODO 8+ 2*x^^^2 = 0";
720 "TODO 8+ 2*x^^^2 = 0";
723 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
724 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
725 (*val p = e_pos'; val c = [];
726 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
727 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
729 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
730 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
731 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
732 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
733 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
734 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
735 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
736 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
737 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
738 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
741 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
742 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
743 (*val p = e_pos'; val c = [];
744 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
745 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
747 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
748 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
751 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
752 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
753 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
759 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
760 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
761 ["PolyEq","solve_d2_polyeq_abc_equation"]);
762 (*val p = e_pos'; val c = [];
763 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
764 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
766 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
767 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
768 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
769 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
770 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
771 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
772 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
774 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
775 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
777 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
778 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
779 ["PolyEq","solve_d2_polyeq_abc_equation"]);
780 (*val p = e_pos'; val c = [];
781 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
782 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
784 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
785 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
786 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
787 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
788 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
789 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
790 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
791 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
792 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
793 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
796 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
797 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
798 ["PolyEq","solve_d2_polyeq_abc_equation"]);
799 (*val p = e_pos'; val c = [];
800 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
801 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
803 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
804 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
805 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
806 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
807 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
808 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
809 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 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
812 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
815 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
816 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
817 ["PolyEq","solve_d2_polyeq_abc_equation"]);
818 (*val p = e_pos'; val c = [];
819 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
820 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
822 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
823 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
824 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
825 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
826 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
827 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
828 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
829 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
830 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
831 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
833 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
834 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
835 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
836 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
837 "solveFor x","solutions L"];
839 ("PolyEq",["degree_2","expanded","univariate","equation"],
840 ["PolyEq","complete_square"]);
841 (* val p = e_pos'; val c = [];
842 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
843 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
845 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
846 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
847 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
848 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
849 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
850 (*Apply_Method ("PolyEq","complete_square")*)
851 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
853 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
854 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
855 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
856 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
857 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
858 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
859 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
860 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
861 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
862 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
863 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
864 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
865 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
866 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
867 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
868 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
869 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
870 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
871 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 (*"x = -2 | x = 4" nxt = Or_to_List*)
874 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
875 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
876 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
878 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
879 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
881 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
882 else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
885 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
886 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
887 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
888 "---- test the erls ----";
889 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
890 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
892 (*if t'= "HOL.True" then ()
893 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
895 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
896 "solveFor x","solutions L"];
898 ("PolyEq",["degree_2","expanded","univariate","equation"],
899 ["PolyEq","complete_square"]);
900 (* val p = e_pos'; val c = [];
901 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
902 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
904 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
905 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
906 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
907 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
908 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
909 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
910 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
911 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
912 (*Apply_Method ("PolyEq","complete_square")*)
913 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
915 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
916 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
917 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
918 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
919 "solveFor x","solutions L"];
921 ("PolyEq",["degree_2","expanded","univariate","equation"],
922 ["PolyEq","complete_square"]);
923 (* val p = e_pos'; val c = [];
924 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
925 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
927 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
928 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
929 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
930 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
931 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
932 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
933 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
934 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
935 (*Apply_Method ("PolyEq","complete_square")*)
936 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
937 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
938 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
939 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
940 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
941 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
942 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
943 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
944 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
945 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
947 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
948 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
951 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
952 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
953 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
954 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
955 "solveFor x","solutions L"];
957 ("PolyEq",["degree_2","expanded","univariate","equation"],
958 ["PolyEq","complete_square"]);
959 (* val p = e_pos'; val c = [];
960 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
961 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
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;
966 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
967 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
968 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
969 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
970 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
971 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
972 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
973 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
975 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
976 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
977 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
978 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
979 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
980 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
981 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
982 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
983 (*WN.2.5.03 TODO FIXME Matthias ?
987 (~1,EdUndef,0,Nundef,
988 "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
990 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
991 this will be simplified [x = a, x = b] to by Factor.ML*)
994 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
995 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
996 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
997 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
998 "solveFor x","solutions L"];
1000 ("PolyEq",["degree_2","expanded","univariate","equation"],
1001 ["PolyEq","complete_square"]);
1002 (* val p = e_pos'; val c = [];
1003 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1004 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1006 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1007 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1008 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1009 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1010 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1011 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1012 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1013 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1014 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1015 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1016 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1017 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1018 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1019 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1020 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1021 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1022 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1025 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1026 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1027 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1028 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1029 "solveFor x","solutions L"];
1031 ("PolyEq",["degree_2","expanded","univariate","equation"],
1032 ["PolyEq","complete_square"]);
1033 (* val p = e_pos'; val c = [];
1034 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1035 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1037 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1038 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1039 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1040 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1041 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1042 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1043 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1044 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1045 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1046 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1047 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1048 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1050 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1051 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1054 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1055 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1056 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1057 (*EP-17 Schalk_I_p86_n5*)
1058 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1059 (* refine fmz ["univariate","equation"];
1061 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1064 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1065 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1067 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1068 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1071 Model_Problem ["normalize","polynomial","univariate","equation"])
1073 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1074 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1075 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1076 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1077 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1080 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1082 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1085 Model_Problem ["degree_1","polynomial","univariate","equation"])
1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1088 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1090 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1091 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1092 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1093 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1094 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1095 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1096 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1099 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1100 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1101 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1102 (*is in rlang.sml, too*)
1103 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1104 "solveFor x","solutions L"];
1105 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1107 (*val p = e_pos'; val c = [];
1108 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1109 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1111 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1112 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1116 Model_Problem ["normalize","polynomial","univariate","equation"])
1118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1126 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1131 Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
1133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1140 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1141 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1147 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1148 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1149 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1150 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1153 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1154 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1155 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1164 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1165 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1167 "----------------- polyeq.sml end ------------------";
1169 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1170 (*WN.19.3.03 ---v-*)
1171 (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1172 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1173 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1175 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1176 (*WN.19.3.03 ---^-*)
1178 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1179 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1180 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1182 "y ^^^ 2 + -2 * x * p = 0";
1184 (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1186 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
1187 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1189 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
1190 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1192 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
1194 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1196 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1197 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1198 (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1201 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1202 trace_rewrite:=true;
1203 rewrite_set_ thy false expand_binoms t;
1204 trace_rewrite:=false;
1207 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1208 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1209 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1212 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1213 ("PolyEq",["univariate","equation"],["no_met"]))];
1216 autoCalculate 1 CompleteCalc;
1217 val ((pt,p),_) = get_calc 1; show_pt pt;
1219 interSteps 1 ([1],Res) (*no Rewrite_Set...*);
1221 ============ inhibit exn WN110906 ==============================================*)