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 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
114 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
115 ["PolyEq","solve_d0_polyeq_equation"]);
116 (*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
117 TODO: change to "equality (x + -1*x = (0::real))"
118 and search for an appropriate problem and method.
120 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
121 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
125 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
126 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
127 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
128 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
130 "----- d0_true ------";
131 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
132 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
133 ["PolyEq","solve_d0_polyeq_equation"]);
134 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
135 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
139 val (p,_,f,nxt,_,pt) = me nxt p [] pt; 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 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
142 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
143 ============ inhibit exn WN110914 ============================================*)
145 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
146 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
147 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
148 "----- d2_pqformula1 ------!!!!";
149 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
151 ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
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;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
161 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
162 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
163 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
164 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
165 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
166 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
167 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
168 val (mI,m) = mk_tac'_ tac;
169 val Appl m = applicable_in p pt m;
170 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
171 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
173 term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
174 terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
175 " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
176 "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
177 "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
178 "\"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\","^
179 "\"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\"]";
180 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
181 member op = specsteps mI (*false*);
182 (*loc_solve_ (mI,m) ptp;
183 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
184 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
186 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
187 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
188 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
189 val thy' = get_obj g_domID pt (par_pblobj pt p);
190 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
192 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
193 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
194 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
195 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
196 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
197 val thy = assoc_thy thy';
198 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
199 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
200 ... Assoc ... is correct*)
201 "~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
202 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
203 1 < length l (*true*);
204 val up = drop_last l;
207 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
208 ... ???? ... is correct*)
209 "~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
210 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
211 val l = drop_last l; (*comes from e, goes to Abs*)
212 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
213 val i = mk_Free (i, T);
214 val E = upd_env E (i, v);
215 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
216 val [(tac_, mout, ptree, pos', xxx)] = ss;
217 val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
218 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
219 ... Assoc ... is correct*)
220 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
221 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
222 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
223 val ctxt = get_ctxt pt (p,p_)
224 val p' = lev_on p : pos;
225 (* WAS val NotAss = assod pt d m stac
226 ... Ass ... is correct*)
227 "~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
228 (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
231 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
232 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
238 "----- d2_pqformula1_neg ------";
239 val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
240 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
241 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
242 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
243 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
244 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;
248 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
250 ([1],Res) False Or_to_List)*)
251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
253 ([2],Res) [] Check_elementwise "Assumptions"*)
254 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
256 val asm = get_assumptions_ pt p;
257 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
258 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
262 "----- d2_pqformula2 ------";
263 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
264 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
265 ["PolyEq","solve_d2_polyeq_pq_equation"]);
267 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
268 val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
269 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
270 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
275 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
276 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
277 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
278 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
279 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
282 "----- d2_pqformula2_neg ------";
283 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
284 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
285 ["PolyEq","solve_d2_polyeq_pq_equation"]);
286 (*val p = e_pos'; val c = [];
287 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
288 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
289 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
290 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;
294 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;
297 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
298 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
299 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
302 "----- d2_pqformula3 ------";
304 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
305 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
306 ["PolyEq","solve_d2_polyeq_pq_equation"]);
307 (*val p = e_pos'; val c = [];
308 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
309 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
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;
316 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;
319 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
320 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
322 "----- d2_pqformula3_neg ------";
323 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
324 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
325 ["PolyEq","solve_d2_polyeq_pq_equation"]);
326 (*val p = e_pos'; val c = [];
327 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
328 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
329 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
330 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; 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;
337 "TODO 2 + x + x^^^2 = 0";
338 "TODO 2 + x + x^^^2 = 0";
339 "TODO 2 + x + x^^^2 = 0";
342 "----- d2_pqformula4 ------";
343 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
344 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
345 ["PolyEq","solve_d2_polyeq_pq_equation"]);
346 (*val p = e_pos'; val c = [];
347 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
348 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
349 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
350 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; 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;
358 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
359 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
361 "----- d2_pqformula4_neg ------";
362 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
363 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
364 ["PolyEq","solve_d2_polyeq_pq_equation"]);
365 (*val p = e_pos'; val c = [];
366 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
367 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
368 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
369 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 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 "TODO 2 + x + 1*x^^^2 = 0";
376 "TODO 2 + x + 1*x^^^2 = 0";
377 "TODO 2 + x + 1*x^^^2 = 0";
379 "----- d2_pqformula5 ------";
380 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
381 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
382 ["PolyEq","solve_d2_polyeq_pq_equation"]);
383 (*val p = e_pos'; val c = [];
384 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
385 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
386 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
387 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; 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;
395 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
396 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
398 "----- d2_pqformula6 ------";
399 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
400 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
401 ["PolyEq","solve_d2_polyeq_pq_equation"]);
402 (*val p = e_pos'; val c = [];
403 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
404 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
405 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
406 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; 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;
414 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
415 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
417 "----- d2_pqformula7 ------";
419 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
420 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
421 ["PolyEq","solve_d2_polyeq_pq_equation"]);
422 (*val p = e_pos'; val c = [];
423 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
424 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
425 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
426 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
427 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
428 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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;
434 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
435 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
437 "----- d2_pqformula8 ------";
438 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
439 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
440 ["PolyEq","solve_d2_polyeq_pq_equation"]);
441 (*val p = e_pos'; val c = [];
442 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
443 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
445 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
446 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; 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;
454 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
455 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
457 "----- d2_pqformula9 ------";
458 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
459 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
460 ["PolyEq","solve_d2_polyeq_pq_equation"]);
461 (*val p = e_pos'; val c = [];
462 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
463 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
465 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
466 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 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
473 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
474 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
477 "----- d2_pqformula10_neg ------";
478 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
479 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
480 ["PolyEq","solve_d2_polyeq_pq_equation"]);
481 (*val p = e_pos'; val c = [];
482 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
483 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
485 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
486 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
492 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
493 "TODO 4 + x^^^2 = 0";
494 "TODO 4 + x^^^2 = 0";
495 "TODO 4 + x^^^2 = 0";
497 "----- d2_pqformula10 ------";
498 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
499 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
500 ["PolyEq","solve_d2_polyeq_pq_equation"]);
501 (*val p = e_pos'; val c = [];
502 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
503 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
505 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
506 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
511 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
512 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
513 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
514 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
516 "----- d2_pqformula9_neg ------";
517 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
518 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
519 ["PolyEq","solve_d2_polyeq_pq_equation"]);
520 (*val p = e_pos'; val c = [];
521 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
522 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
524 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
525 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
526 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
527 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
528 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
529 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
530 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
531 "TODO 4 + 1*x^^^2 = 0";
532 "TODO 4 + 1*x^^^2 = 0";
533 "TODO 4 + 1*x^^^2 = 0";
535 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
536 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
537 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
539 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
540 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
541 ["PolyEq","solve_d2_polyeq_abc_equation"]);
542 (*val p = e_pos'; val c = [];
543 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
544 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
546 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
547 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
552 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
554 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
555 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
557 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
558 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
559 ["PolyEq","solve_d2_polyeq_abc_equation"]);
560 (*val p = e_pos'; val c = [];
561 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
562 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
564 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
565 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
569 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
570 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
571 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
572 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
573 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
576 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
577 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
578 ["PolyEq","solve_d2_polyeq_abc_equation"]);
579 (*val p = e_pos'; val c = [];
580 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
581 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
583 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
584 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
589 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
590 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
591 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
592 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
594 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
595 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
596 ["PolyEq","solve_d2_polyeq_abc_equation"]);
597 (*val p = e_pos'; val c = [];
598 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
599 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
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 1 + x + 2*x^^^2 = 0";
610 "TODO 1 + x + 2*x^^^2 = 0";
611 "TODO 1 + x + 2*x^^^2 = 0";
613 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
614 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
615 ["PolyEq","solve_d2_polyeq_abc_equation"]);
616 (*val p = e_pos'; val c = [];
617 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
618 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
620 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
621 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
626 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
627 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
628 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
629 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
631 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
632 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
633 ["PolyEq","solve_d2_polyeq_abc_equation"]);
634 (*val p = e_pos'; val c = [];
635 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
636 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
638 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
639 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
643 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
644 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
645 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
646 "TODO 2 + 1*x + x^^^2 = 0";
647 "TODO 2 + 1*x + x^^^2 = 0";
648 "TODO 2 + 1*x + x^^^2 = 0";
651 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
652 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
653 ["PolyEq","solve_d2_polyeq_abc_equation"]);
654 (*val p = e_pos'; val c = [];
655 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
656 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
658 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
659 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
664 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
665 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
666 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
667 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
669 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
670 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
671 ["PolyEq","solve_d2_polyeq_abc_equation"]);
672 (*val p = e_pos'; val c = [];
673 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
674 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
676 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
677 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
683 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
684 "TODO 2 + x + x^^^2 = 0";
685 "TODO 2 + x + x^^^2 = 0";
686 "TODO 2 + x + x^^^2 = 0";
689 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
690 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
691 ["PolyEq","solve_d2_polyeq_abc_equation"]);
692 (*val p = e_pos'; val c = [];
693 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
694 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
696 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
697 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
702 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
703 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
704 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
705 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
707 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
708 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
709 ["PolyEq","solve_d2_polyeq_abc_equation"]);
710 (*val p = e_pos'; val c = [];
711 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
712 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
714 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
715 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
716 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
717 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
718 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
719 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
720 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
721 "TODO 8+ 2*x^^^2 = 0";
722 "TODO 8+ 2*x^^^2 = 0";
723 "TODO 8+ 2*x^^^2 = 0";
726 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
727 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
728 (*val p = e_pos'; val c = [];
729 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
730 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
732 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
733 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
738 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
739 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
740 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
741 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
744 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
745 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
746 (*val p = e_pos'; val c = [];
747 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
748 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
750 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
751 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;
754 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
755 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
756 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
762 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
763 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
764 ["PolyEq","solve_d2_polyeq_abc_equation"]);
765 (*val p = e_pos'; val c = [];
766 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
767 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
769 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
770 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
771 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
772 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
773 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
774 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
775 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
776 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
777 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
778 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
780 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
781 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
782 ["PolyEq","solve_d2_polyeq_abc_equation"]);
783 (*val p = e_pos'; val c = [];
784 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
785 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
787 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
788 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
789 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
790 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
791 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
792 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
793 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
794 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
795 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
796 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
799 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
800 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
801 ["PolyEq","solve_d2_polyeq_abc_equation"]);
802 (*val p = e_pos'; val c = [];
803 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
804 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
806 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
807 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
812 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
813 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
814 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
815 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
818 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
819 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
820 ["PolyEq","solve_d2_polyeq_abc_equation"]);
821 (*val p = e_pos'; val c = [];
822 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
823 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
825 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
826 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
827 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
828 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
829 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
830 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
831 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
832 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
833 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
834 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
836 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
837 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
838 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
839 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
840 "solveFor x","solutions L"];
842 ("PolyEq",["degree_2","expanded","univariate","equation"],
843 ["PolyEq","complete_square"]);
844 (* val p = e_pos'; val c = [];
845 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
846 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
848 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
849 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
850 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
851 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
853 (*Apply_Method ("PolyEq","complete_square")*)
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
855 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
857 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
858 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
859 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
860 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
861 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
862 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
863 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
864 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
865 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
866 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
867 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
868 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
869 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
870 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
871 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
872 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
873 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
874 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
875 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
876 (*"x = -2 | x = 4" nxt = Or_to_List*)
877 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
878 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
879 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
881 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
882 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
884 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
885 else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
888 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
889 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
890 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
891 "---- test the erls ----";
892 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
893 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
895 (*if t'= "HOL.True" then ()
896 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
898 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
899 "solveFor x","solutions L"];
901 ("PolyEq",["degree_2","expanded","univariate","equation"],
902 ["PolyEq","complete_square"]);
903 (* val p = e_pos'; val c = [];
904 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
905 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
907 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
913 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
914 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
915 (*Apply_Method ("PolyEq","complete_square")*)
916 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
918 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
919 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
920 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
921 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
922 "solveFor x","solutions L"];
924 ("PolyEq",["degree_2","expanded","univariate","equation"],
925 ["PolyEq","complete_square"]);
926 (* val p = e_pos'; val c = [];
927 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
928 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
930 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
936 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
937 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
938 (*Apply_Method ("PolyEq","complete_square")*)
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;
946 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
947 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
948 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
950 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
951 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
954 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
955 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
956 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
957 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
958 "solveFor x","solutions L"];
960 ("PolyEq",["degree_2","expanded","univariate","equation"],
961 ["PolyEq","complete_square"]);
962 (* val p = e_pos'; val c = [];
963 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
964 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
966 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
974 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;
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;
983 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
984 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
985 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
986 (*WN.2.5.03 TODO FIXME Matthias ?
990 (~1,EdUndef,0,Nundef,
991 "[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)]"))
993 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
994 this will be simplified [x = a, x = b] to by Factor.ML*)
997 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
998 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
999 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
1000 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1001 "solveFor x","solutions L"];
1003 ("PolyEq",["degree_2","expanded","univariate","equation"],
1004 ["PolyEq","complete_square"]);
1005 (* val p = e_pos'; val c = [];
1006 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1007 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1009 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
1020 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1021 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1022 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1023 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1024 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1025 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1028 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1029 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1030 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1031 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1032 "solveFor x","solutions L"];
1034 ("PolyEq",["degree_2","expanded","univariate","equation"],
1035 ["PolyEq","complete_square"]);
1036 (* val p = e_pos'; val c = [];
1037 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1038 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1040 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1041 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1046 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1047 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1048 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1049 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1050 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1051 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1053 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1054 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1057 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1058 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1059 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1060 (*EP-17 Schalk_I_p86_n5*)
1061 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1062 (* refine fmz ["univariate","equation"];
1064 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1067 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1068 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1070 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1071 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1074 Model_Problem ["normalize","polynomial","univariate","equation"])
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;
1078 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1079 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1080 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1083 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1085 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1088 Model_Problem ["degree_1","polynomial","univariate","equation"])
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;
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1096 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1097 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1098 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1099 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1102 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1103 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1104 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1105 (*is in rlang.sml, too*)
1106 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1107 "solveFor x","solutions L"];
1108 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1110 (*val p = e_pos'; val c = [];
1111 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1112 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1115 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1119 Model_Problem ["normalize","polynomial","univariate","equation"])
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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1129 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1134 Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1143 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1144 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1150 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1151 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1152 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1153 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1156 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1157 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1158 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1167 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1168 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1170 "----------------- polyeq.sml end ------------------";
1172 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1173 (*WN.19.3.03 ---v-*)
1174 (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1175 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1176 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1178 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1179 (*WN.19.3.03 ---^-*)
1181 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1182 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1183 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1185 "y ^^^ 2 + -2 * x * p = 0";
1187 (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1189 "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";
1190 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1192 "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";
1193 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1195 "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";
1197 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1199 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1200 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1201 (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1204 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1205 trace_rewrite:=true;
1206 rewrite_set_ thy false expand_binoms t;
1207 trace_rewrite:=false;
1210 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1211 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1212 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1215 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1216 ("PolyEq",["univariate","equation"],["no_met"]))];
1219 autoCalculate 1 CompleteCalc;
1220 val ((pt,p),_) = get_calc 1; show_pt pt;
1222 interSteps 1 ([1],Res) (*no Rewrite_Set...*);
1224 ============ inhibit exn WN110906 ==============================================*)