1 (* testexamples for PolyEq, poynomial equations and equational systems
4 (c) due to copyright terms
6 use"../smltest/IsacKnowledge/polyeq.sml";
9 WN030609: some expls dont work due to unfinished handling of 'expanded terms';
10 others marked with TODO have to be checked, too.
13 "-----------------------------------------------------------------";
14 "table of contents -----------------------------------------------";
15 (*WN060608 some ----- are not in this table*)
16 "-----------------------------------------------------------------";
17 "----------- tests on predicates in problems ---------------------";
18 "----------- test matching problems --------------------------0---";
19 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
20 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
21 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
22 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
23 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
24 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
25 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
26 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
27 "-----------------------------------------------------------------";
28 "-----------------------------------------------------------------";
29 "-----------------------------------------------------------------";
33 "----------- tests on predicates in problems ---------------------";
34 "----------- tests on predicates in problems ---------------------";
35 "----------- tests on predicates in problems ---------------------";
37 Compiler.Control.Print.printDepth:=5; (*4 default*)
41 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
42 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
43 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
44 else error "polyeq.sml: diff.behav. in lhs";
47 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
48 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
49 if (term2str t) = "True" then ()
50 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
52 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
53 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
54 if (term2str t) = "False" then ()
55 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
58 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
59 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
60 if (term2str t) = "True" then ()
61 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
64 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
65 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
66 if (term2str t) = "True" then ()
67 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
70 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
71 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
72 if (term2str t) = "True" then ()
73 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
75 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
76 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
77 if (term2str t) = "True" then ()
78 else error "polyeq.sml: diff.behav. in has_degree_in_in";
81 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
82 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
83 if (term2str t) = "False" then ()
84 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
86 val t4 = (term_of o the o (parse thy))
87 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
88 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
89 if (term2str t) = "False" then ()
90 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
93 val t5 = (term_of o the o (parse thy))
94 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
95 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
96 if (term2str t) = "True" then ()
97 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
100 "----------- test matching problems --------------------------0---";
101 "----------- test matching problems --------------------------0---";
102 "----------- test matching problems --------------------------0---";
103 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
104 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
105 get_pbt ["expanded","univariate","equation"];
107 match_pbl fmz (get_pbt ["expanded","univariate","equation"]);
109 {Find=[Correct "solutions L"],
110 Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
111 Correct "solveFor x"],Relate=[],
112 Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
113 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],With=[]}
115 match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]);
117 {Find=[Correct "solutions L"],
118 Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
119 Correct "solveFor x"],Relate=[],
120 Where=[Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x =!= 2"],
123 "-------------------- test thm's degree_0 --------------------------------------";
124 "-------------------- test thm's degree_0 --------------------------------------";
125 "----- d0_false ------";
127 val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
128 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
129 ["PolyEq","solve_d0_polyeq_equation"]);
131 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
132 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
133 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
134 val (p,_,f,nxt,_,pt) = me nxt p c pt;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
139 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
140 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
141 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
143 "----- d0_true ------";
145 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
146 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
147 ["PolyEq","solve_d0_polyeq_equation"]);
148 (*val p = e_pos'; val c = [];
149 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
150 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
151 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
152 val (p,_,f,nxt,_,pt) = me nxt p c pt;
153 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
158 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
159 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
161 "-------------------- test thm's degree_2 ------------------------------------------";
162 "-------------------- test thm's degree_2 ------------------------------------------";
164 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
165 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
166 "-------------------- test thm's d2_pq_formulsxx[_neg]-----";
168 "----- d2_pqformula1 ------!!!!";
169 val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
170 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
171 (*val p = e_pos'; val c = [];
172 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
173 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
174 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
175 val (p,_,f,nxt,_,pt) = me nxt p c pt;
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
178 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
182 ([3],Res) "x = 2 | x = -1" Or_to_List*)
183 val (p,_,f,nxt,_,pt) = me nxt p c pt;
185 ### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
186 ([4],Res) "[x = 2, x = -1]" Check_elementwise "Assumptions"*)
187 val (p,_,f,nxt,_,pt) = me nxt p c pt;
188 (*### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
189 ([5],Res) "[x = 2, x = -1]" Check_Postcond*)
190 val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
192 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
194 "----- d2_pqformula1_neg ------";
196 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
197 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
198 (*val p = e_pos'; val c = [];
199 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
200 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
201 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
204 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
205 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
208 ([1],Res) False Or_to_List)*)
209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
211 ([2],Res) [] Check_elementwise "Assumptions"*)
212 val (p,_,f,nxt,_,pt) = me nxt p c pt;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 val asm = get_assumptions_ pt p;
215 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
216 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
218 "----- d2_pqformula2 ------";
219 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
220 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
221 ["PolyEq","solve_d2_polyeq_pq_equation"]);
222 (*val p = e_pos'; val c = [];
223 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
224 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
225 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
226 val (p,_,f,nxt,_,pt) = me nxt p c pt;
227 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
228 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
233 val (p,_,f,nxt,_,pt) = me nxt p c pt;
234 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
235 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
238 "----- d2_pqformula2_neg ------";
239 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
240 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
241 ["PolyEq","solve_d2_polyeq_pq_equation"]);
242 (*val p = e_pos'; val c = [];
243 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
244 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
245 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
246 val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
248 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
249 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
254 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
255 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
258 "----- d2_pqformula3 ------";
260 val fmz = ["equality (-2 + x + 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"]);
263 (*val p = e_pos'; val c = [];
264 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
265 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
266 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
267 val (p,_,f,nxt,_,pt) = me nxt p c pt;
268 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
269 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
271 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
272 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
274 val (p,_,f,nxt,_,pt) = me nxt p c pt;
275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
276 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
278 "----- d2_pqformula3_neg ------";
279 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
280 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
281 ["PolyEq","solve_d2_polyeq_pq_equation"]);
282 (*val p = e_pos'; val c = [];
283 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
284 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
285 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
286 val (p,_,f,nxt,_,pt) = me nxt p c pt;
287 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
290 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
291 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
292 val (p,_,f,nxt,_,pt) = me nxt p c pt;
293 "TODO 2 + x + x^^^2 = 0";
294 "TODO 2 + x + x^^^2 = 0";
295 "TODO 2 + x + x^^^2 = 0";
298 "----- d2_pqformula4 ------";
299 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
300 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
301 ["PolyEq","solve_d2_polyeq_pq_equation"]);
302 (*val p = e_pos'; val c = [];
303 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
304 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
305 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
306 val (p,_,f,nxt,_,pt) = me nxt p c pt;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
308 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
309 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
310 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
311 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
312 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
313 val (p,_,f,nxt,_,pt) = me nxt p c pt;
314 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
315 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
317 "----- d2_pqformula4_neg ------";
318 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
319 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
320 ["PolyEq","solve_d2_polyeq_pq_equation"]);
321 (*val p = e_pos'; val c = [];
322 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
323 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
324 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
325 val (p,_,f,nxt,_,pt) = me nxt p c pt;
326 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
327 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
328 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
329 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
330 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
331 "TODO 2 + x + 1*x^^^2 = 0";
332 "TODO 2 + x + 1*x^^^2 = 0";
333 "TODO 2 + x + 1*x^^^2 = 0";
335 "----- d2_pqformula5 ------";
336 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
337 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
338 ["PolyEq","solve_d2_polyeq_pq_equation"]);
339 (*val p = e_pos'; val c = [];
340 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
341 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
342 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
343 val (p,_,f,nxt,_,pt) = me nxt p c pt;
344 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
345 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
346 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
347 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
348 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
349 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
350 val (p,_,f,nxt,_,pt) = me nxt p c pt;
351 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
352 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
354 "----- d2_pqformula6 ------";
355 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
356 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
357 ["PolyEq","solve_d2_polyeq_pq_equation"]);
358 (*val p = e_pos'; val c = [];
359 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
360 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
361 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
363 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
364 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
365 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
366 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
367 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
368 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
369 val (p,_,f,nxt,_,pt) = me nxt p c pt;
370 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
371 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
373 "----- d2_pqformula7 ------";
375 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
376 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
377 ["PolyEq","solve_d2_polyeq_pq_equation"]);
378 (*val p = e_pos'; val c = [];
379 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
380 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
381 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
382 val (p,_,f,nxt,_,pt) = me nxt p c pt;
383 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
385 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
386 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
387 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
388 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
389 val (p,_,f,nxt,_,pt) = me nxt p c pt;
390 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
391 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
393 "----- d2_pqformula8 ------";
394 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
395 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
396 ["PolyEq","solve_d2_polyeq_pq_equation"]);
397 (*val p = e_pos'; val c = [];
398 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
399 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
401 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
403 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
404 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
405 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
406 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 val (p,_,f,nxt,_,pt) = me nxt p c pt;
410 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
411 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
413 "----- d2_pqformula9 ------";
414 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
415 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
416 ["PolyEq","solve_d2_polyeq_pq_equation"]);
417 (*val p = e_pos'; val c = [];
418 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
419 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
421 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
422 val (p,_,f,nxt,_,pt) = me nxt p c pt;
423 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
424 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
425 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
426 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
427 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
428 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
429 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
430 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
433 "----- d2_pqformula10_neg ------";
434 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
435 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
436 ["PolyEq","solve_d2_polyeq_pq_equation"]);
437 (*val p = e_pos'; val c = [];
438 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
439 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
441 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
442 val (p,_,f,nxt,_,pt) = me nxt p c pt;
443 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
444 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
445 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
446 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
448 val (p,_,f,nxt,_,pt) = me nxt p c pt;
449 "TODO 4 + x^^^2 = 0";
450 "TODO 4 + x^^^2 = 0";
451 "TODO 4 + x^^^2 = 0";
453 "----- d2_pqformula10 ------";
454 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
455 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
456 ["PolyEq","solve_d2_polyeq_pq_equation"]);
457 (*val p = e_pos'; val c = [];
458 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
461 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
466 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
468 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
469 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
470 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
472 "----- d2_pqformula9_neg ------";
473 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
474 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
475 ["PolyEq","solve_d2_polyeq_pq_equation"]);
476 (*val p = e_pos'; val c = [];
477 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
478 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
480 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
481 val (p,_,f,nxt,_,pt) = me nxt p c pt;
482 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
483 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
484 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
485 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
486 val (p,_,f,nxt,_,pt) = me nxt p c pt;
487 "TODO 4 + 1*x^^^2 = 0";
488 "TODO 4 + 1*x^^^2 = 0";
489 "TODO 4 + 1*x^^^2 = 0";
491 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
492 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
493 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
495 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
496 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
497 ["PolyEq","solve_d2_polyeq_abc_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 c pt;
504 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
505 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
506 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
507 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
508 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
509 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
510 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
511 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
513 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
514 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
515 ["PolyEq","solve_d2_polyeq_abc_equation"]);
516 (*val p = e_pos'; val c = [];
517 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
518 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
520 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
522 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
524 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
526 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
527 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
528 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
529 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
532 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
533 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
534 ["PolyEq","solve_d2_polyeq_abc_equation"]);
535 (*val p = e_pos'; val c = [];
536 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
537 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
539 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
540 val (p,_,f,nxt,_,pt) = me nxt p c pt;
541 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
542 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
543 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
544 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
547 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
548 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
550 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
551 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
552 ["PolyEq","solve_d2_polyeq_abc_equation"]);
553 (*val p = e_pos'; val c = [];
554 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
555 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
557 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;
559 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
560 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
561 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
562 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
563 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
564 val (p,_,f,nxt,_,pt) = me nxt p c pt;
565 "TODO 1 + x + 2*x^^^2 = 0";
566 "TODO 1 + x + 2*x^^^2 = 0";
567 "TODO 1 + x + 2*x^^^2 = 0";
569 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
570 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
571 ["PolyEq","solve_d2_polyeq_abc_equation"]);
572 (*val p = e_pos'; val c = [];
573 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
574 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
576 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
577 val (p,_,f,nxt,_,pt) = me nxt p c pt;
578 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
579 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
580 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
581 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
582 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
583 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
584 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
585 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
587 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
588 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
589 ["PolyEq","solve_d2_polyeq_abc_equation"]);
590 (*val p = e_pos'; val c = [];
591 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
592 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
594 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
595 val (p,_,f,nxt,_,pt) = me nxt p c pt;
596 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
597 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
598 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
599 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
600 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
601 val (p,_,f,nxt,_,pt) = me nxt p c pt;
602 "TODO 2 + 1*x + x^^^2 = 0";
603 "TODO 2 + 1*x + x^^^2 = 0";
604 "TODO 2 + 1*x + x^^^2 = 0";
607 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
608 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
609 ["PolyEq","solve_d2_polyeq_abc_equation"]);
610 (*val p = e_pos'; val c = [];
611 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
612 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
614 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
615 val (p,_,f,nxt,_,pt) = me nxt p c pt;
616 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
617 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
620 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
621 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
622 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
623 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
625 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
626 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
627 ["PolyEq","solve_d2_polyeq_abc_equation"]);
628 (*val p = e_pos'; val c = [];
629 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
630 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
632 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
633 val (p,_,f,nxt,_,pt) = me nxt p c pt;
634 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
635 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
636 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
637 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
638 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
639 val (p,_,f,nxt,_,pt) = me nxt p c pt;
640 "TODO 2 + x + x^^^2 = 0";
641 "TODO 2 + x + x^^^2 = 0";
642 "TODO 2 + x + x^^^2 = 0";
645 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
646 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
647 ["PolyEq","solve_d2_polyeq_abc_equation"]);
648 (*val p = e_pos'; val c = [];
649 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
650 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
652 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
653 val (p,_,f,nxt,_,pt) = me nxt p c pt;
654 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
655 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
656 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
657 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
658 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
659 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
660 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
661 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
663 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
664 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
665 ["PolyEq","solve_d2_polyeq_abc_equation"]);
666 (*val p = e_pos'; val c = [];
667 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
668 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
670 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
671 val (p,_,f,nxt,_,pt) = me nxt p c pt;
672 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
673 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
674 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
675 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
676 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
677 "TODO 8+ 2*x^^^2 = 0";
678 "TODO 8+ 2*x^^^2 = 0";
679 "TODO 8+ 2*x^^^2 = 0";
682 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
683 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
684 (*val p = e_pos'; val c = [];
685 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
686 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
689 val (p,_,f,nxt,_,pt) = me nxt p c pt;
690 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
691 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
692 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
693 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
695 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
696 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
697 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
700 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
701 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
702 (*val p = e_pos'; val c = [];
703 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
704 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
706 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
707 val (p,_,f,nxt,_,pt) = me nxt p c pt;
708 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
709 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
710 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
711 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
712 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
718 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
719 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
720 ["PolyEq","solve_d2_polyeq_abc_equation"]);
721 (*val p = e_pos'; val c = [];
722 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
723 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
725 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
726 val (p,_,f,nxt,_,pt) = me nxt p c pt;
727 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
728 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
729 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
730 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
731 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
732 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
733 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
734 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
736 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
737 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
738 ["PolyEq","solve_d2_polyeq_abc_equation"]);
739 (*val p = e_pos'; val c = [];
740 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
741 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
743 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
744 val (p,_,f,nxt,_,pt) = me nxt p c pt;
745 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
746 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
747 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
748 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
749 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
750 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
751 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
752 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
755 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
756 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
757 ["PolyEq","solve_d2_polyeq_abc_equation"]);
758 (*val p = e_pos'; val c = [];
759 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
760 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
762 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
763 val (p,_,f,nxt,_,pt) = me nxt p c pt;
764 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
765 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
766 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
767 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
768 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
769 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
770 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
771 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
774 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
775 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
776 ["PolyEq","solve_d2_polyeq_abc_equation"]);
777 (*val p = e_pos'; val c = [];
778 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
779 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
781 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
782 val (p,_,f,nxt,_,pt) = me nxt p c pt;
783 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
784 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
785 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
786 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
787 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
788 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
789 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
790 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
792 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
793 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
794 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
795 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
796 "solveFor x","solutions L"];
798 ("PolyEq",["degree_2","expanded","univariate","equation"],
799 ["PolyEq","complete_square"]);
800 (* val p = e_pos'; val c = [];
801 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
802 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
804 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
805 val (p,_,f,nxt,_,pt) = me nxt p c pt;
806 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
807 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
808 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
809 (*Apply_Method ("PolyEq","complete_square")*)
810 val (p,_,f,nxt,_,pt) = me nxt p c pt;
811 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
812 val (p,_,f,nxt,_,pt) = me nxt p c pt;
813 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
814 val (p,_,f,nxt,_,pt) = me nxt p c pt;
815 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
816 val (p,_,f,nxt,_,pt) = me nxt p c pt;
817 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
818 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
819 val (p,_,f,nxt,_,pt) = me nxt p c pt;
820 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
821 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
822 val (p,_,f,nxt,_,pt) = me nxt p c pt;
823 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
824 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
825 val (p,_,f,nxt,_,pt) = me nxt p c pt;
826 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
827 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
828 val (p,_,f,nxt,_,pt) = me nxt p c pt;
829 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
830 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
831 val (p,_,f,nxt,_,pt) = me nxt p c pt;
832 (*"x = -2 | x = 4" nxt = Or_to_List*)
833 val (p,_,f,nxt,_,pt) = me nxt p c pt;
834 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
835 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
837 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
838 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
840 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
841 else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
844 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
845 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
846 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
847 "---- test the erls ----";
848 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
849 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
851 (*if t'= "True" then ()
852 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
854 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
855 "solveFor x","solutions L"];
857 ("PolyEq",["degree_2","expanded","univariate","equation"],
858 ["PolyEq","complete_square"]);
859 (* val p = e_pos'; val c = [];
860 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
861 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
863 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
864 val (p,_,f,nxt,_,pt) = me nxt p c pt;
865 val (p,_,f,nxt,_,pt) = me nxt p c pt;
866 val (p,_,f,nxt,_,pt) = me nxt p c pt;
867 val (p,_,f,nxt,_,pt) = me nxt p c pt;
868 val (p,_,f,nxt,_,pt) = me nxt p c pt;
869 val (p,_,f,nxt,_,pt) = me nxt p c pt;
870 val (p,_,f,nxt,_,pt) = me nxt p c pt;
871 (*Apply_Method ("PolyEq","complete_square")*)
872 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
874 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
875 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
876 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
877 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
878 "solveFor x","solutions L"];
880 ("PolyEq",["degree_2","expanded","univariate","equation"],
881 ["PolyEq","complete_square"]);
882 (* val p = e_pos'; val c = [];
883 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
884 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
886 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
887 val (p,_,f,nxt,_,pt) = me nxt p c pt;
888 val (p,_,f,nxt,_,pt) = me nxt p c pt;
889 val (p,_,f,nxt,_,pt) = me nxt p c pt;
890 val (p,_,f,nxt,_,pt) = me nxt p c pt;
891 val (p,_,f,nxt,_,pt) = me nxt p c pt;
892 val (p,_,f,nxt,_,pt) = me nxt p c pt;
893 val (p,_,f,nxt,_,pt) = me nxt p c pt;
894 (*Apply_Method ("PolyEq","complete_square")*)
895 val (p,_,f,nxt,_,pt) = me nxt p c pt;
896 val (p,_,f,nxt,_,pt) = me nxt p c pt;
897 val (p,_,f,nxt,_,pt) = me nxt p c pt;
898 val (p,_,f,nxt,_,pt) = me nxt p c pt;
899 val (p,_,f,nxt,_,pt) = me nxt p c pt;
900 val (p,_,f,nxt,_,pt) = me nxt p c pt;
901 val (p,_,f,nxt,_,pt) = me nxt p c pt;
902 val (p,_,f,nxt,_,pt) = me nxt p c pt;
903 val (p,_,f,nxt,_,pt) = me nxt p c pt;
904 val (p,_,f,nxt,_,pt) = me nxt p c pt;
906 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
907 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
910 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
911 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
912 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
913 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
914 "solveFor x","solutions L"];
916 ("PolyEq",["degree_2","expanded","univariate","equation"],
917 ["PolyEq","complete_square"]);
918 (* val p = e_pos'; val c = [];
919 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
920 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
922 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
923 val (p,_,f,nxt,_,pt) = me nxt p c pt;
924 val (p,_,f,nxt,_,pt) = me nxt p c pt;
925 val (p,_,f,nxt,_,pt) = me nxt p c pt;
926 val (p,_,f,nxt,_,pt) = me nxt p c pt;
927 val (p,_,f,nxt,_,pt) = me nxt p c pt;
928 val (p,_,f,nxt,_,pt) = me nxt p c pt;
929 val (p,_,f,nxt,_,pt) = me nxt p c pt;
930 val (p,_,f,nxt,_,pt) = me nxt p c pt;
931 val (p,_,f,nxt,_,pt) = me nxt p c pt;
932 val (p,_,f,nxt,_,pt) = me nxt p c pt;
934 val (p,_,f,nxt,_,pt) = me nxt p c pt;
935 val (p,_,f,nxt,_,pt) = me nxt p c pt;
936 val (p,_,f,nxt,_,pt) = me nxt p c pt;
937 val (p,_,f,nxt,_,pt) = me nxt p c pt;
938 val (p,_,f,nxt,_,pt) = me nxt p c pt;
939 val (p,_,f,nxt,_,pt) = me nxt p c pt;
940 val (p,_,f,nxt,_,pt) = me nxt p c pt;
941 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
942 (*WN.2.5.03 TODO FIXME Matthias ?
946 (~1,EdUndef,0,Nundef,
947 "[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)]"))
949 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
950 this will be simplified [x = a, x = b] to by Factor.ML*)
953 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
954 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
955 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
956 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
957 "solveFor x","solutions L"];
959 ("PolyEq",["degree_2","expanded","univariate","equation"],
960 ["PolyEq","complete_square"]);
961 (* val p = e_pos'; val c = [];
962 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
963 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
965 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
966 val (p,_,f,nxt,_,pt) = me nxt p c pt;
967 val (p,_,f,nxt,_,pt) = me nxt p c pt;
968 val (p,_,f,nxt,_,pt) = me nxt p c pt;
969 val (p,_,f,nxt,_,pt) = me nxt p c pt;
970 val (p,_,f,nxt,_,pt) = me nxt p c pt;
971 val (p,_,f,nxt,_,pt) = me nxt p c pt;
972 val (p,_,f,nxt,_,pt) = me nxt p c pt;
973 val (p,_,f,nxt,_,pt) = me nxt p c pt;
974 val (p,_,f,nxt,_,pt) = me nxt p c pt;
975 val (p,_,f,nxt,_,pt) = me nxt p c pt;
976 val (p,_,f,nxt,_,pt) = me nxt p c pt;
977 val (p,_,f,nxt,_,pt) = me nxt p c pt;
978 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
979 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
980 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
981 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
984 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
985 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
986 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
987 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
988 "solveFor x","solutions L"];
990 ("PolyEq",["degree_2","expanded","univariate","equation"],
991 ["PolyEq","complete_square"]);
992 (* val p = e_pos'; val c = [];
993 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
994 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
996 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
997 val (p,_,f,nxt,_,pt) = me nxt p c pt;
998 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
999 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1000 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1001 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1002 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1003 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1004 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1005 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1006 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1007 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1009 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1010 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1013 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1014 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1015 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1016 (*EP-17 Schalk_I_p86_n5*)
1017 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1018 (* refine fmz ["univariate","equation"];
1020 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1023 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1024 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1026 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1027 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1030 Model_Problem ["normalize","polynomial","univariate","equation"])
1032 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1033 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1034 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1035 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1036 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1039 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1041 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1044 Model_Problem ["degree_1","polynomial","univariate","equation"])
1046 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1047 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1049 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1050 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1051 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1052 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1053 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1054 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1055 | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1058 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1059 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1060 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1061 (*is in rlang.sml, too*)
1062 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1063 "solveFor x","solutions L"];
1064 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1066 (*val p = e_pos'; val c = [];
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 nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
1072 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1075 Model_Problem ["normalize","polynomial","univariate","equation"])
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;
1081 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1082 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1085 Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1087 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1090 Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
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 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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1099 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1100 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1106 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1107 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1108 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1109 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1112 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1113 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1124 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1126 "----------------- polyeq.sml end ------------------";
1128 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
1129 (*WN.19.3.03 ---v-*)
1130 (*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
1131 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
1132 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1134 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
1135 (*WN.19.3.03 ---^-*)
1137 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
1138 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
1139 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1141 "y ^^^ 2 + -2 * x * p = 0";
1143 (*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
1145 "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";
1146 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1148 "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";
1149 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
1151 "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";
1153 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
1155 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
1156 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
1157 (*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
1160 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
1161 trace_rewrite:=true;
1162 rewrite_set_ thy false expand_binoms t;
1163 trace_rewrite:=false;
1166 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1167 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1168 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
1171 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1172 ("PolyEq",["univariate","equation"],["no_met"]))];
1175 autoCalculate 1 CompleteCalc;
1176 val ((pt,p),_) = get_calc 1; show_pt pt;
1178 interSteps 1 ([1],Res) (*no Rewrite_Set...*);