166 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
127 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
167 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
128 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
168 "-----------------------------------------------------------------"; |
129 "-----------------------------------------------------------------"; |
169 "-----------------------------------------------------------------"; |
130 "-----------------------------------------------------------------"; |
170 |
131 |
171 "----------- tests on predicates in problems ---------------------"; |
132 |
172 "----------- tests on predicates in problems ---------------------"; |
133 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
173 "----------- tests on predicates in problems ---------------------"; |
134 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
174 val thy = @{theory}; |
135 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)"; |
175 Rewrite.trace_on:=false; (*true false*) |
136 val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)", |
176 |
|
177 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)"; |
|
178 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; |
|
179 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then () |
|
180 else error "polyeq.sml: diff.behav. in lhs"; |
|
181 |
|
182 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x"; |
|
183 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; |
|
184 if (UnparseC.term t) = "True" then () |
|
185 else error "polyeq.sml: diff.behav. 1 in is_expended_in"; |
|
186 |
|
187 val t0 = (Thm.term_of o the o (TermC.parse thy)) "(sqrt(x)) is_poly_in x"; |
|
188 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; |
|
189 if (UnparseC.term t) = "False" then () |
|
190 else error "polyeq.sml: diff.behav. 2 in is_poly_in"; |
|
191 |
|
192 val t3 = (Thm.term_of o the o (TermC.parse thy)) "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x"; |
|
193 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
|
194 if (UnparseC.term t) = "True" then () |
|
195 else error "polyeq.sml: diff.behav. 3 in is_poly_in"; |
|
196 |
|
197 val t4 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x"; |
|
198 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; |
|
199 if (UnparseC.term t) = "True" then () |
|
200 else error "polyeq.sml: diff.behav. 4 in is_expended_in"; |
|
201 |
|
202 val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x"; |
|
203 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; |
|
204 if (UnparseC.term t) = "True" then () |
|
205 else error "polyeq.sml: diff.behav. 5 in is_expended_in"; |
|
206 |
|
207 val t3 = (Thm.term_of o the o (TermC.parse thy))"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
|
208 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
|
209 if (UnparseC.term t) = "True" then () |
|
210 else error "polyeq.sml: diff.behav. in has_degree_in_in"; |
|
211 |
|
212 val t3 = (Thm.term_of o the o (TermC.parse thy)) "((sqrt(x)) has_degree_in x) = 2"; |
|
213 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
|
214 if (UnparseC.term t) = "False" then () |
|
215 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; |
|
216 |
|
217 val t4 = (Thm.term_of o the o (TermC.parse thy)) |
|
218 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1"; |
|
219 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; |
|
220 if (UnparseC.term t) = "False" then () |
|
221 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; |
|
222 |
|
223 val t5 = (Thm.term_of o the o (TermC.parse thy)) |
|
224 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
|
225 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; |
|
226 if (UnparseC.term t) = "True" then () |
|
227 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; |
|
228 |
|
229 \<close> ML \<open> |
|
230 "----------- test matching problems --------------------------0---"; |
|
231 "----------- test matching problems --------------------------0---"; |
|
232 "----------- test matching problems --------------------------0---"; |
|
233 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
234 if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) = |
|
235 M_Match.Matches' {Find = [Correct "solutions L"], |
|
236 With = [], |
|
237 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], |
|
238 Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)", |
|
239 Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], |
|
240 Relate = []} |
|
241 then () else error "M_Match.match_pbl [expanded,univariate,equation]"; |
|
242 |
|
243 if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) = |
|
244 M_Match.Matches' {Find = [Correct "solutions L"], |
|
245 With = [], |
|
246 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], |
|
247 Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], |
|
248 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*) |
|
249 then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]"; |
|
250 |
|
251 |
|
252 \<close> ML \<open> |
|
253 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; |
|
254 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; |
|
255 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----"; |
|
256 (*################################################################################## |
|
257 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy |
|
258 |
|
259 (*Aufgabe zum Einstieg in die Arbeit...*) |
|
260 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b - (a+b)*x + x \<up> 2 = 0"; |
|
261 (*ein 'ruleset' aus Poly.ML wird angewandt...*) |
|
262 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; |
|
263 UnparseC.term t; |
|
264 "a * b + (- 1 * (a * x) + (- 1 * (b * x) + x \<up> 2)) = 0"; |
|
265 val SOME (t,_) = |
|
266 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; |
|
267 UnparseC.term t; |
|
268 "x \<up> 2 + (- 1 * (b * x) + (- 1 * (x * a) + b * a)) = 0"; |
|
269 (* bei Verwendung von "size_of-term" nach MG :*) |
|
270 (*"x \<up> 2 + (- 1 * (b * x) + (b * a + - 1 * (x * a))) = 0" !!! *) |
|
271 |
|
272 (*wir holen 'a' wieder aus der Klammerung heraus...*) |
|
273 val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t; |
|
274 UnparseC.term t; |
|
275 "x \<up> 2 + - 1 * b * x + - 1 * x * a + b * a = 0"; |
|
276 (* "x \<up> 2 + - 1 * b * x + b * a + - 1 * x * a = 0" !!! *) |
|
277 |
|
278 val SOME (t,_) = |
|
279 rewrite_set_inst_ thy Poly_erls false [("bdv", "a")] make_polynomial_in t; |
|
280 UnparseC.term t; |
|
281 "x \<up> 2 + (- 1 * (b * x) + a * (b + - 1 * x)) = 0"; |
|
282 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
|
283 "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*) |
|
284 |
|
285 (*das rewriting l"asst sich beobachten mit |
|
286 Rewrite.trace_on := false; (*true false*) |
|
287 *) |
|
288 |
|
289 "------ 15.11.02 --------------------------"; |
|
290 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * x + b * x"; |
|
291 val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv"; |
|
292 val a = (Thm.term_of o the o (TermC.parse thy)) "a"; |
|
293 |
|
294 Rewrite.trace_on := false; (*true false*) |
|
295 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
|
296 val SOME (t,_) = |
|
297 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
298 UnparseC.term t; |
|
299 val SOME (t,_) = |
|
300 rewrite_set_ thy false discard_parentheses t; |
|
301 UnparseC.term t; |
|
302 "1 + b * x + x * a"; |
|
303 |
|
304 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a * (x + b * x) + a \<up> 2"; |
|
305 val SOME (t,_) = |
|
306 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
307 UnparseC.term t; |
|
308 val SOME (t,_) = |
|
309 rewrite_set_ thy false discard_parentheses t; |
|
310 UnparseC.term t; |
|
311 "1 + (x + b * x) * a + a \<up> 2"; |
|
312 |
|
313 val t = (Thm.term_of o the o (TermC.parse thy)) "1 + a \<up> 2 * x + b * a + 7*a \<up> 2"; |
|
314 val SOME (t,_) = |
|
315 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
316 UnparseC.term t; |
|
317 val SOME (t,_) = |
|
318 rewrite_set_ thy false discard_parentheses t; |
|
319 UnparseC.term t; |
|
320 "1 + b * a + (7 + x) * a \<up> 2"; |
|
321 |
|
322 (* MG2003 |
|
323 Prog_Expr.thy grundlegende Algebra |
|
324 Poly.thy Polynome |
|
325 Rational.thy Br"uche |
|
326 Root.thy Wurzeln |
|
327 RootRat.thy Wurzen + Br"uche |
|
328 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03) |
|
329 |
|
330 get_thm Termorder.thy "bdv_n_collect"; |
|
331 get_thm (theory "Isac_Knowledge") "bdv_n_collect"; |
|
332 *) |
|
333 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * x + 7 * a \<up> 2"; |
|
334 val SOME (t,_) = |
|
335 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
|
336 UnparseC.term t; |
|
337 val SOME (t,_) = |
|
338 rewrite_set_ thy false discard_parentheses t; |
|
339 UnparseC.term t; |
|
340 "(7 + x) * a \<up> 2"; |
|
341 |
|
342 val t = (Thm.term_of o the o (TermC.parse Termorder.thy)) "Pi"; |
|
343 |
|
344 val t = (Thm.term_of o the o (parseold thy)) "7"; |
|
345 ##################################################################################*) |
|
346 |
|
347 |
|
348 \<close> ML \<open> |
|
349 "----------- open local of fun ord_make_polynomial_in ------------------------------------------"; |
|
350 "----------- open local of fun ord_make_polynomial_in ------------------------------------------"; |
|
351 "----------- open local of fun ord_make_polynomial_in ------------------------------------------"; |
|
352 (* termorder hacked by MG, adapted later by WN *) |
|
353 (** )local ( *. for make_polynomial_in .*) |
|
354 |
|
355 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
356 |
|
357 fun pr_ord EQUAL = "EQUAL" |
|
358 | pr_ord LESS = "LESS" |
|
359 | pr_ord GREATER = "GREATER"; |
|
360 |
|
361 fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0) |
|
362 | dest_hd' x (t as Free (a, T)) = |
|
363 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*) |
|
364 else (((a, 0), T), 1) |
|
365 | dest_hd' _ (Var v) = (v, 2) |
|
366 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3) |
|
367 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4) |
|
368 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def."; |
|
369 |
|
370 fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $ |
|
371 Free (var, _) $ Free (pot, _)) = |
|
372 (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else (); |
|
373 case x of (*WN*) |
|
374 (Free (xstr, _)) => |
|
375 if xstr = var |
|
376 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else (); |
|
377 1000 * (the (TermC.int_opt_of_string pot))) |
|
378 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3) |
|
379 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) |
|
380 | size_of_term' i pr x (t as Abs (_, _, body)) = |
|
381 (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else (); |
|
382 1 + size_of_term' (i + 1) pr x body) |
|
383 | size_of_term' i pr x (f $ t) = |
|
384 let |
|
385 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else (); |
|
386 val s1 = size_of_term' (i + 1) pr x f |
|
387 val s2 = size_of_term' (i + 1) pr x t |
|
388 val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else (); |
|
389 in (s1 + s2) end |
|
390 | size_of_term' i pr x t = |
|
391 (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else (); |
|
392 case t of |
|
393 Free (subst, _) => |
|
394 (case x of |
|
395 Free (xstr, _) => |
|
396 if xstr = subst |
|
397 then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000) |
|
398 else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1) |
|
399 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) |
|
400 | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1)); |
|
401 |
|
402 fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) |
|
403 let |
|
404 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else (); |
|
405 val ord = |
|
406 case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord |
|
407 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else () |
|
408 in ord end |
|
409 | term_ord' i pr x _ (t, u) = |
|
410 let |
|
411 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else (); |
|
412 val ord = |
|
413 case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of |
|
414 EQUAL => |
|
415 let val (f, ts) = strip_comb t and (g, us) = strip_comb u |
|
416 in |
|
417 (case hd_ord (i + 1) pr x (f, g) of |
|
418 EQUAL => (terms_ord x (i + 1) pr) (ts, us) |
|
419 | ord => ord) |
|
420 end |
|
421 | ord => ord |
|
422 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else () |
|
423 in ord end |
|
424 and hd_ord i pr x (f, g) = (* ~ term.ML *) |
|
425 let |
|
426 val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else (); |
|
427 val ord = prod_ord |
|
428 (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord |
|
429 (dest_hd' x f, dest_hd' x g) |
|
430 val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else (); |
|
431 in ord end |
|
432 and terms_ord x i pr (ts, us) = |
|
433 let |
|
434 val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else (); |
|
435 val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us); |
|
436 val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else (); |
|
437 in ord end |
|
438 |
|
439 (** )in( *local*) |
|
440 |
|
441 fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) = |
|
442 ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **) |
|
443 case subst of |
|
444 (_, x) :: _ => |
|
445 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS |
|
446 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) |
|
447 |
|
448 (** )end;( *local*) |
|
449 |
|
450 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
|
451 if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?"; |
|
452 |
|
453 val x = TermC.str2term "x ::real"; |
|
454 |
|
455 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real"); |
|
456 if 2006 = size_of_term' 1 true x t1 |
|
457 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)"; |
|
458 |
|
459 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real"); |
|
460 if 3004 = size_of_term' 1 true x t2 |
|
461 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED"; |
|
462 |
|
463 |
|
464 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; |
|
465 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; |
|
466 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; |
|
467 val substa = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "a")]; |
|
468 val substb = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "b")]; |
|
469 val substx = [(TermC.empty, (Thm.term_of o the o (TermC.parse thy)) "x")]; |
|
470 |
|
471 val x1 = (Thm.term_of o the o (TermC.parse thy)) "a + b + x"; |
|
472 val x2 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; |
|
473 val x3 = (Thm.term_of o the o (TermC.parse thy)) "a + x + b"; |
|
474 val x4 = (Thm.term_of o the o (TermC.parse thy)) "x + a + b"; |
|
475 |
|
476 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () |
|
477 else error "termorder.sml diff.behav ord_make_polynomial_in #1"; |
|
478 |
|
479 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then () |
|
480 else error "termorder.sml diff.behav ord_make_polynomial_in #2"; |
|
481 |
|
482 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () |
|
483 else error "termorder.sml diff.behav ord_make_polynomial_in #3"; |
|
484 |
|
485 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; |
|
486 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3"; |
|
487 ord_make_polynomial_in true thy substx (aa, bb); |
|
488 true; (* => LESS *) |
|
489 |
|
490 val aa = (Thm.term_of o the o (TermC.parse thy)) "- 1 * a * x"; |
|
491 val bb = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 3"; |
|
492 ord_make_polynomial_in true thy substa (aa, bb); |
|
493 false; (* => GREATER *) |
|
494 |
|
495 (* und nach dem Re-engineering der Termorders in den 'rulesets' |
|
496 kannst Du die 'gr"osste' Variable frei w"ahlen: *) |
|
497 val bdv= TermC.str2term "bdv ::real"; |
|
498 val x = TermC.str2term "x ::real"; |
|
499 val a = TermC.str2term "a ::real"; |
|
500 val b = TermC.str2term "b ::real"; |
|
501 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; |
|
502 if UnparseC.term t' = "b + x + a" then () |
|
503 else error "termorder.sml diff.behav ord_make_polynomial_in #11"; |
|
504 |
|
505 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; |
|
506 |
|
507 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; |
|
508 if UnparseC.term t' = "a + b + x" then () |
|
509 else error "termorder.sml diff.behav ord_make_polynomial_in #13"; |
|
510 |
|
511 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2"; |
|
512 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp'; |
|
513 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; |
|
514 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then () |
|
515 else error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
|
516 |
|
517 val ttt' = "(3*x + 5)/18 ::real"; |
|
518 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt'; |
|
519 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; |
|
520 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
|
521 else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; |
|
522 |
|
523 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt; |
|
524 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
|
525 else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; |
|
526 |
|
527 "----------- lin.eq degree_0 -------------------------------------"; |
|
528 "----------- lin.eq degree_0 -------------------------------------"; |
|
529 "----------- lin.eq degree_0 -------------------------------------"; |
|
530 "----- d0_false ------"; |
|
531 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"]; |
|
532 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], |
|
533 ["PolyEq", "solve_d0_polyeq_equation"]); |
|
534 (*=== inhibit exn WN110914: declare_constraints doesnt work with ThmC.numerals_to_Free ======== |
|
535 TODO: change to "equality (x + - 1*x = (0::real))" |
|
536 and search for an appropriate problem and method. |
|
537 |
|
538 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
539 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
540 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
541 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
542 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
543 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
544 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
545 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[]")) => () |
|
546 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []"; |
|
547 |
|
548 "----- d0_true ------"; |
|
549 val fmz = ["equality (0 = (0::real))", "solveFor x", "solutions L"]; |
|
550 val (dI',pI',mI') = ("PolyEq",["degree_0", "polynomial", "univariate", "equation"], |
|
551 ["PolyEq", "solve_d0_polyeq_equation"]); |
|
552 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
553 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
554 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
555 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
556 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
557 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
558 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
559 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => () |
|
560 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList"; |
|
561 ============ inhibit exn WN110914 ============================================*) |
|
562 |
|
563 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
564 "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; |
|
565 "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; |
|
566 "----------- test thm's d2_pq_formulsxx[_neg]---------------------"; |
|
567 "----- d2_pqformula1 ------!!!!"; |
|
568 val fmz = ["equality (- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real))", "solveFor z", "solutions L"]; |
|
569 val (dI',pI',mI') = |
|
570 ("Isac_Knowledge", ["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["no_met"]); |
|
571 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
572 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
573 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
574 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
575 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
576 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
577 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
578 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*) |
|
579 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
580 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
581 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
582 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
583 |
|
584 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2] TODO sqrt*) |
|
585 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) |
|
586 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
587 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
588 |
|
589 if p = ([], Res) andalso |
|
590 f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + - 1 * sqrt (9 / 16) / 2]" then |
|
591 case nxt of End_Proof' => () | _ => error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 1" |
|
592 else error "(- 1/8 + (- 1/4)*z + z \<up> 2 = (0::real)) CHANGED 2"; |
|
593 |
|
594 \<close> ML \<open> |
|
595 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------"; |
|
596 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------"; |
|
597 "----------- equality (2 +(- 1)*x + x \<up> 2 = (0::real)) ----------------------------------------"; |
|
598 "----- d2_pqformula1_neg ------"; |
|
599 val fmz = ["equality (2 +(- 1)*x + x \<up> 2 = (0::real))", "solveFor x", "solutions L"]; |
|
600 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
601 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
602 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
603 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
604 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
605 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
606 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
607 (*### or2list False |
|
608 ([1],Res) False Or_to_List)*) |
|
609 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
610 (*### or2list False |
|
611 ([2],Res) [] Check_elementwise "Assumptions"*) |
|
612 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
613 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
614 val asm = Ctree.get_assumptions pt p; |
|
615 if f2str f = "[]" andalso |
|
616 UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^ |
|
617 "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then () |
|
618 else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0"; |
|
619 |
|
620 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
621 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------"; |
|
622 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------"; |
|
623 "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------"; |
|
624 "----- d2_pqformula2 ------"; |
|
625 val fmz = ["equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
626 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
627 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
628 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
629 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
630 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
631 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
632 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
633 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
634 |
|
635 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
636 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
637 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
638 case f of Test_Out.FormKF "[x = 2, x = - 1]" => () |
|
639 | _ => error "polyeq.sml: diff.behav. in - 2 + (- 1)*x + x^2 = 0 -> [x = 2, x = - 1]"; |
|
640 |
|
641 |
|
642 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
643 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------"; |
|
644 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------"; |
|
645 "----------- equality (- 2 + x + x \<up> 2 = 0) ---------------------------------------------------"; |
|
646 "----- d2_pqformula3 ------"; |
|
647 (*EP-9*) |
|
648 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
649 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
650 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
651 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
652 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
653 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
654 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
655 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
656 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
657 |
|
658 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
659 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
660 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
661 case f of Test_Out.FormKF "[x = 1, x = - 2]" => () |
|
662 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0-> [x = 1, x = - 2]"; |
|
663 |
|
664 |
|
665 \<close> ML \<open> |
|
666 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
667 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
668 "----------- equality (2 + x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
669 "----- d2_pqformula3_neg ------"; |
|
670 val fmz = ["equality (2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
671 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
672 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
673 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
674 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
675 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
676 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
677 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
678 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
679 |
|
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; |
|
682 "TODO 2 + x + x \<up> 2 = 0"; |
|
683 "TODO 2 + x + x \<up> 2 = 0"; |
|
684 "TODO 2 + x + x \<up> 2 = 0"; |
|
685 |
|
686 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
687 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------"; |
|
688 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------"; |
|
689 "----------- equality (- 2 + x + 1*x \<up> 2 = 0)) ------------------------------------------------"; |
|
690 "----- d2_pqformula4 ------"; |
|
691 val fmz = ["equality (- 2 + x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
692 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
693 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
694 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
695 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
696 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
697 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
698 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
699 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
700 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
701 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; |
|
703 case f of Test_Out.FormKF "[x = 1, x = - 2]" => () |
|
704 | _ => error "polyeq.sml: diff.behav. in - 2 + x + 1*x \<up> 2 = 0 -> [x = 1, x = - 2]"; |
|
705 |
|
706 \<close> ML \<open> |
|
707 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
708 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
709 "----------- equality (1*x + x \<up> 2 = 0) ----------------------------------------------------"; |
|
710 "----- d2_pqformula5 ------"; |
|
711 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
712 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
713 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
722 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
723 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
724 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = - 1]"; |
|
725 |
|
726 \<close> ML \<open> |
|
727 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------"; |
|
728 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------"; |
|
729 "----------- equality (1*x + 1*x \<up> 2 = 0) ----------------------------------------------------"; |
|
730 "----- d2_pqformula6 ------"; |
|
731 val fmz = ["equality (1*x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
732 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
733 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
734 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
735 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 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
741 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
742 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
743 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
744 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = - 1]"; |
|
745 |
|
746 \<close> ML \<open> |
|
747 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------"; |
|
748 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------"; |
|
749 "----------- equality (x + x \<up> 2 = 0) ------------------------------------------------------"; |
|
750 "----- d2_pqformula7 ------"; |
|
751 (*EP- 10*) |
|
752 val fmz = ["equality ( x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
753 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
754 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
755 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
756 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
757 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
758 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
759 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
760 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
761 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
762 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
763 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
764 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
765 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; |
|
766 |
|
767 \<close> ML \<open> |
|
768 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------"; |
|
769 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------"; |
|
770 "----------- equality (x + 1*x \<up> 2 = 0) ------------------------------------------------------"; |
|
771 "----- d2_pqformula8 ------"; |
|
772 val fmz = ["equality (x + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
773 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
774 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
775 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
776 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
777 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
778 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
779 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
780 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
781 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
782 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
783 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
784 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
785 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = - 1]"; |
|
786 |
|
787 \<close> ML \<open> |
|
788 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------"; |
|
789 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------"; |
|
790 "----------- equality (-4 + x \<up> 2 = 0) -------------------------------------------------------"; |
|
791 "----- d2_pqformula9 ------"; |
|
792 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
793 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
794 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
795 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
796 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
797 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
798 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
799 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
800 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
801 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
802 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
803 case f of Test_Out.FormKF "[x = 2, x = - 2]" => () |
|
804 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; |
|
805 |
|
806 |
|
807 \<close> ML \<open> |
|
808 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------"; |
|
809 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------"; |
|
810 "----------- equality (4 + 1*x \<up> 2 = 0) -------------------------------------------------------"; |
|
811 "----- d2_pqformula9_neg ------"; |
|
812 val fmz = ["equality (4 + 1*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
813 val (dI',pI',mI') = ("PolyEq",["pqFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
814 ["PolyEq", "solve_d2_polyeq_pq_equation"]); |
|
815 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
816 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
817 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
818 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
819 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
820 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
821 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
822 "TODO 4 + 1*x \<up> 2 = 0"; |
|
823 "TODO 4 + 1*x \<up> 2 = 0"; |
|
824 "TODO 4 + 1*x \<up> 2 = 0"; |
|
825 |
|
826 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
827 "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; |
|
828 "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; |
|
829 "-------------------- test thm's d2_abc_formulsxx[_neg]-----"; |
|
830 val fmz = ["equality (- 1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
831 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
832 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
833 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
834 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
835 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
836 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
837 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
838 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
839 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
840 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
841 case f of Test_Out.FormKF "[x = 1, x = - 1 / 2]" => () |
|
842 | _ => error "polyeq.sml: diff.behav. in - 1 + (- 1)*x + 2*x^2 = 0 -> [x = 1, x = - 1/2]"; |
|
843 |
|
844 \<close> ML \<open> |
|
845 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------"; |
|
846 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------"; |
|
847 "----------- equality (1 +(- 1)*x + 2*x \<up> 2 = 0) ----------------------------------------------"; |
|
848 val fmz = ["equality (1 +(- 1)*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
849 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
850 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
851 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
852 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
853 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
854 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
855 |
|
856 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
857 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
858 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
859 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0"; |
|
860 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0"; |
|
861 "TODO 1 +(- 1)*x + 2*x \<up> 2 = 0"; |
|
862 |
|
863 |
|
864 \<close> ML \<open> |
|
865 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------"; |
|
866 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------"; |
|
867 "----------- equality (- 1 + x + 2*x \<up> 2 = 0) -------------------------------------------------"; |
|
868 (*EP- 11*) |
|
869 val fmz = ["equality (- 1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
870 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
871 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
872 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
873 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
874 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
875 |
|
876 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
877 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
878 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
879 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
880 |
|
881 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
882 case f of Test_Out.FormKF "[x = 1 / 2, x = - 1]" => () |
|
883 | _ => error "polyeq.sml: diff.behav. in - 1 + x + 2*x^2 = 0 -> [x = 1/2, x = - 1]"; |
|
884 |
|
885 |
|
886 \<close> ML \<open> |
|
887 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------"; |
|
888 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------"; |
|
889 "----------- equality (1 + x + 2*x \<up> 2 = 0) --------------------------------------------------"; |
|
890 val fmz = ["equality (1 + x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
891 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
892 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
893 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
894 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
895 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
896 |
|
897 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
898 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
899 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
900 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
901 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
902 "TODO 1 + x + 2*x \<up> 2 = 0"; |
|
903 "TODO 1 + x + 2*x \<up> 2 = 0"; |
|
904 "TODO 1 + x + 2*x \<up> 2 = 0"; |
|
905 |
|
906 |
|
907 val fmz = ["equality (- 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
908 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
909 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
910 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
911 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
912 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
913 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
914 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
915 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
916 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
917 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
918 case f of Test_Out.FormKF "[x = 1, x = - 2]" => () |
|
919 | _ => error "polyeq.sml: diff.behav. in - 2 + 1*x + x^2 = 0 -> [x = 1, x = - 2]"; |
|
920 |
|
921 val fmz = ["equality ( 2 + 1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
922 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
923 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
924 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
925 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
926 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
927 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
928 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
929 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
930 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
931 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
932 "TODO 2 + 1*x + x \<up> 2 = 0"; |
|
933 "TODO 2 + 1*x + x \<up> 2 = 0"; |
|
934 "TODO 2 + 1*x + x \<up> 2 = 0"; |
|
935 |
|
936 \<close> ML \<open> |
|
937 (*EP- 12*) |
|
938 val fmz = ["equality (- 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
939 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
940 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
941 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
942 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
943 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
944 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
945 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
946 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
947 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
948 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
949 case f of Test_Out.FormKF "[x = 1, x = - 2]" => () |
|
950 | _ => error "polyeq.sml: diff.behav. in - 2 + x + x^2 = 0 -> [x = 1, x = - 2]"; |
|
951 |
|
952 val fmz = ["equality ( 2 + x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
953 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
954 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
955 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
956 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
957 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
958 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
959 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
960 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
961 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
962 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
963 "TODO 2 + x + x \<up> 2 = 0"; |
|
964 "TODO 2 + x + x \<up> 2 = 0"; |
|
965 "TODO 2 + x + x \<up> 2 = 0"; |
|
966 |
|
967 \<close> ML \<open> |
|
968 (*EP- 13*) |
|
969 val fmz = ["equality (-8 + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
970 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
971 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
972 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
973 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
974 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
975 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
976 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
977 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
978 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
979 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
980 case f of Test_Out.FormKF "[x = 2, x = - 2]" => () |
|
981 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = - 2]"; |
|
982 |
|
983 val fmz = ["equality ( 8+ 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
984 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
985 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
986 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
987 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
988 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
989 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
990 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
991 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
992 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
993 "TODO 8+ 2*x \<up> 2 = 0"; |
|
994 "TODO 8+ 2*x \<up> 2 = 0"; |
|
995 "TODO 8+ 2*x \<up> 2 = 0"; |
|
996 |
|
997 \<close> ML \<open> |
|
998 (*EP- 14*) |
|
999 val fmz = ["equality (-4 + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
1000 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1001 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1002 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1003 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1004 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1005 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1006 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1007 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1008 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1009 case f of Test_Out.FormKF "[x = 2, x = - 2]" => () |
|
1010 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = - 2]"; |
|
1011 |
|
1012 |
|
1013 \<close> ML \<open> |
|
1014 val fmz = ["equality ( 4+ x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
1015 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1016 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1017 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1018 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1019 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1020 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1021 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1022 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1023 "TODO 4+ x \<up> 2 = 0"; |
|
1024 "TODO 4+ x \<up> 2 = 0"; |
|
1025 "TODO 4+ x \<up> 2 = 0"; |
|
1026 |
|
1027 \<close> ML \<open> |
|
1028 (*EP- 15*) |
|
1029 val fmz = ["equality (2*x + 2*x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
1030 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
1031 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1032 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1033 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1034 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1035 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1036 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1037 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1038 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1039 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1040 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
1041 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; |
|
1042 |
|
1043 \<close> ML \<open> |
|
1044 val fmz = ["equality (1*x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
1045 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
1046 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1047 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1048 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1049 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1050 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1051 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1052 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1053 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1054 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1055 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
1056 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; |
|
1057 |
|
1058 \<close> text \<open> (*rewrite_set_, rewrite_ ..= NONE*) |
|
1059 \<close> ML \<open> |
|
1060 (*EP- 16*) |
|
1061 val fmz = ["equality (x + 2 * x \<up> 2 = (0::real))", "solveFor (x::real)", "solutions L"]; |
|
1062 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
1063 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1064 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1065 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1066 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1067 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1068 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1069 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1070 \<close> ML \<open> |
|
1071 (*+*)val Test_Out.FormKF "x + 2 * x \<up> 2 = 0" = f; |
|
1072 (*+*)val Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_abcFormula_simplify") = nxt |
|
1073 \<close> ML \<open> |
|
1074 Rewrite.trace_on := false; (*false true*) |
|
1075 \<close> text \<open> (* *) |
|
1076 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*"x + 2 * x \<up> 2 = 0", d2_polyeq_abcFormula_simplify*) |
|
1077 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*) |
|
1078 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt); |
|
1079 \<close> ML \<open> |
|
1080 val (pt, p) = |
|
1081 (*Step.by_tactic is here for testing by me; do_next would suffice in me*) |
|
1082 case Step.by_tactic tac (pt, p) of |
|
1083 ("ok", (_, _, ptp)) => ptp |
|
1084 | ("unsafe-ok", (_, _, ptp)) => ptp |
|
1085 | ("not-applicable",_) => (pt, p) |
|
1086 | ("end-of-calculation", (_, _, ptp)) => ptp |
|
1087 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic" |
|
1088 | _ => raise ERROR "me: uncovered case Step.by_tactic" |
|
1089 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1090 (*case*) |
|
1091 Step.do_next p ((pt, Pos.e_pos'), []) (*of*); |
|
1092 \<close> ML \<open> |
|
1093 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); |
|
1094 \<close> ML \<open> |
|
1095 (*if*) Pos.on_calc_end ip (*else*); |
|
1096 \<close> ML \<open> |
|
1097 val (_, probl_id, _) = Calc.references (pt, p); |
|
1098 \<close> ML \<open> |
|
1099 val _ = |
|
1100 (*case*) tacis (*of*); |
|
1101 \<close> ML \<open> |
|
1102 (*if*) probl_id = Problem.id_empty (*else*); |
|
1103 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1104 switch_specify_solve p_ (pt, ip); |
|
1105 \<close> ML \<open> |
|
1106 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); |
|
1107 \<close> ML \<open> |
|
1108 (*if*) Pos.on_specification ([], state_pos) (*else*); |
|
1109 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1110 LI.do_next (pt, input_pos) |
|
1111 \<close> ML \<open> |
|
1112 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); |
|
1113 \<close> ML \<open> |
|
1114 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
|
1115 \<close> ML \<open> |
|
1116 val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
1117 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; |
|
1118 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1119 (*case*) |
|
1120 LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
|
1121 \<close> ML \<open> |
|
1122 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) = |
|
1123 (sc, (pt, pos), ist, ctxt); |
|
1124 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1125 (*case*) |
|
1126 LI.scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) |
|
1127 \<close> ML \<open> |
|
1128 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) = |
|
1129 ((prog, (ptp, ctxt)), (Pstate ist)); |
|
1130 \<close> ML \<open> |
|
1131 (*if*) path = [] (*else*); |
|
1132 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1133 go_scan_up (prog, cc) (trans_scan_up ist) |
|
1134 \<close> ML \<open> |
|
1135 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) = |
|
1136 ((prog, cc), (trans_scan_up ist)); |
|
1137 \<close> ML \<open> |
|
1138 (*if*) path = [R] (*else*); |
|
1139 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1140 scan_up pcc (ist |> path_up) (go_up path sc) |
|
1141 \<close> ML \<open> |
|
1142 "~~~~~ and scan_up , args:"; val (pcc, ist,(Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ )) = |
|
1143 (pcc, (ist |> path_up), (go_up path sc)); |
|
1144 \<close> text \<open> (*rewrite_set_, rewrite_ "- 1 / 2 = - 1 / 2" x = - 0 \<or> x = - 1 / 2 = NONE*) |
|
1145 go_scan_up pcc ist |
|
1146 \<close> ML \<open> |
|
1147 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) = |
|
1148 (pcc, ist); |
|
1149 \<close> ML \<open> |
|
1150 (*if*) path = [R] (*else*); |
|
1151 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1152 scan_up pcc (ist |> path_up) (go_up path sc) |
|
1153 \<close> ML \<open> |
|
1154 "~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _)) = |
|
1155 (pcc, (ist |> path_up), (go_up path sc)); |
|
1156 \<close> ML \<open> |
|
1157 val e2 = check_Seq_up ist sc; |
|
1158 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1159 (*case*) |
|
1160 scan_dn cc (ist |> path_up_down [R]) e2 (*of*); |
|
1161 \<close> ML \<open> |
|
1162 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2)) = |
|
1163 (cc, (ist |> path_up_down [R]), e2); |
|
1164 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1165 (*case*) |
|
1166 scan_dn cc (ist |> path_down [L, R]) e1 (*of*); |
|
1167 \<close> ML \<open> |
|
1168 "~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e)) = |
|
1169 (cc, (ist |> path_down [L, R]), e1); |
|
1170 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1171 (*case*) |
|
1172 scan_dn cc (ist |> path_down [R]) e (*of*); |
|
1173 \<close> ML \<open> |
|
1174 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) = |
|
1175 (cc, (ist |> path_down [R]), e); |
|
1176 \<close> ML \<open> |
|
1177 (*if*) Tactical.contained_in t (*else*); |
|
1178 \<close> ML \<open> |
|
1179 val (Program.Tac prog_tac, form_arg) = (*case*) |
|
1180 LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); |
|
1181 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1182 check_tac cc ist (prog_tac, form_arg) |
|
1183 \<close> ML \<open> |
|
1184 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) = |
|
1185 (cc, ist, (prog_tac, form_arg)); |
|
1186 \<close> ML \<open> |
|
1187 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac |
|
1188 \<close> ML \<open> |
|
1189 val _ = (*case*) m (*of*); |
|
1190 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1191 (*case*) |
|
1192 Solve_Step.check m (pt, p) (*of*); |
|
1193 \<close> ML \<open> |
|
1194 "~~~~~ fun check , args:"; val ((Tactic.Rewrite_Set rls), (cs as (pt, (p, _)))) = |
|
1195 (m, (pt, p)); |
|
1196 \<close> ML \<open> |
|
1197 val pp = Ctree.par_pblobj pt p; |
|
1198 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
1199 val f = Calc.current_formula cs; |
|
1200 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1201 (*case*) |
|
1202 Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f (*of*); |
|
1203 \<close> ML \<open> |
|
1204 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = |
|
1205 ((ThyC.get_theory thy'), false, (assoc_rls rls), f); |
|
1206 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1207 rewrite__set_ thy 1 bool [] rls term; |
|
1208 \<close> ML \<open> |
|
1209 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) = |
|
1210 (thy, 1, bool, [], rls, term); |
|
1211 \<close> ML \<open> |
|
1212 \<close> ML \<open> (* \<longrightarrow> src/../rewrite.sml *) |
|
1213 (*//-------------------------------- cp fromewrite.sml-----------------------------------------\\*) |
|
1214 \<close> ML \<open> |
|
1215 fun msg call thy op_ thmC t = |
|
1216 call ^ ": \n" ^ |
|
1217 "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^ |
|
1218 "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE"; |
|
1219 \<close> ML \<open> |
|
1220 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*) |
|
1221 datatype switch = Appl | Noap; |
|
1222 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *) |
|
1223 | rew_once ruls asm ct Appl [] = |
|
1224 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls |
|
1225 | Rule_Set.Sequence _ => (ct, asm) |
|
1226 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\"")) |
|
1227 | rew_once ruls asm ct apno (rul :: thms) = |
|
1228 case rul of |
|
1229 Rule.Thm (thmid, thm) => |
|
1230 (trace_in1 i "try thm" thmid; |
|
1231 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1232 ((#erls o Rule_Set.rep) rls) put_asm thm ct of |
|
1233 NONE => rew_once ruls asm ct apno thms |
|
1234 | SOME (ct', asm') => |
|
1235 (trace_in2 i "rewrites to" thy ct'; |
|
1236 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) |
|
1237 (* once again try the same rule, e.g. associativity against "()"*) |
|
1238 | Rule.Eval (cc as (op_, _)) => |
|
1239 let val _ = trace_in1 i "try calc" op_; |
|
1240 in case Eval.adhoc_thm thy cc ct of |
|
1241 NONE => rew_once ruls asm ct apno thms |
|
1242 | SOME (_, thm') => |
|
1243 let |
|
1244 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1245 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
|
1246 val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" thy op_ thm' ct) |
|
1247 val _ = trace_in3 i "calc. to" thy pairopt; |
|
1248 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end |
|
1249 end |
|
1250 | Rule.Cal1 (cc as (op_, _)) => |
|
1251 let val _ = trace_in1 i "try cal1" op_; |
|
1252 in case Eval.adhoc_thm1_ thy cc ct of |
|
1253 NONE => (ct, asm) |
|
1254 | SOME (_, thm') => |
|
1255 let |
|
1256 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1257 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
|
1258 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^ |
|
1259 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE") |
|
1260 val _ = trace_in3 i "cal1. to" thy pairopt; |
|
1261 in the pairopt end |
|
1262 end |
|
1263 | Rule.Rls_ rls' => |
|
1264 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of |
|
1265 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms |
|
1266 | NONE => rew_once ruls asm ct apno thms) |
|
1267 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\""); |
|
1268 (*\\------------------------------- cp from rewrite.sml---------------------------------------//*) |
|
1269 \<close> ML \<open> |
|
1270 val ruls = (#rules o Rule_Set.rep) rls; |
|
1271 \<close> text \<open> (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1272 Rewrite.trace_on := false; (*false rew_once-3-isa.txt true*) |
|
1273 val (ct', asm') = |
|
1274 rew_once ruls [] ct Noap ruls; |
|
1275 \<close> ML \<open> |
|
1276 (*+*)UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"; |
|
1277 \<close> ML \<open> |
|
1278 (*+*)rls;(*val it = |
|
1279 Repeat |
|
1280 {calc = |
|
1281 [("PLUS", ("Groups.plus_class.plus", fn)), ("MINUS", ("Groups.minus_class.minus", fn)), ("TIMES", ("Groups.times_class.times", fn)), |
|
1282 ("DIVIDE", ("Rings.divide_class.divide", fn)), ("SQRT", ("NthRoot.sqrt", fn)), ("POWER", ("Transcendental.powr", fn))], |
|
1283 ======^^^^^^====== |
|
1284 erls = ------------------------------ id = "calc_rat_erls" ------------------------------------------------------vvvvvvvvvvvvvvvvvvvv |
|
1285 Repeat |
|
1286 {calc = [("DIVIDE", ("Rings.divide_class.divide", fn))], erls = |
|
1287 ======^^^^^^====== |
|
1288 Repeat |
|
1289 {calc = [("matches", ("Prog_Expr.matches", fn)), ("equal", ("HOL.eq", fn)), ("is_num", ("Prog_Expr.is_num", fn))], erls = Empty, errpatts = [], id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", fn), |
|
1290 rules = [Eval ("Prog_Expr.matches", fn), Eval ("HOL.eq", fn), Eval ("Prog_Expr.is_num", fn), Thm ("not_true", "(\<not> True) = False"), Thm ("not_false", "(\<not> False) = True")], scr = Empty_Prog, srls = Empty}, |
|
1291 errpatts = [], id = "PolyEq_erls", <<<------------------------------------- "PolyEq_erls" |
|
1292 preconds = [], rew_ord = ("dummy_ord", fn), rules = |
|
1293 [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Eval ("Transcendental.powr", fn), Eval ("Groups.times_class.times", fn), Eval ("Groups.minus_class.minus", fn), Eval ("Groups.plus_class.plus", fn), |
|
1294 Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Eval ("Prog_Expr.matches", fn), Eval ("Prog_Expr.occurs_in", fn), Eval ("Prog_Expr.is_num", fn), Eval ("Prog_Expr.ident", fn), |
|
1295 Eval ("Orderings.ord_class.less_eq", fn), Eval ("Orderings.ord_class.less", fn), Thm ("radd_left_cancel_le", "(?k + ?m \<le> ?k + ?n) = (?m \<le> ?n)"), Thm ("order_refl", "?x \<le> ?x"), Thm ("refl", "?t = ?t"), |
|
1296 Thm ("or_false", "(?a \<or> False) = ?a"), Thm ("or_true", "(?a \<or> True) = True"), Thm ("and_false", "(?a \<and> False) = False"), Thm ("and_true", "(?a \<and> True) = ?a"), Thm ("not_false", "(\<not> False) = True"), |
|
1297 Thm ("not_true", "(\<not> True) = False"), Thm ("mult_cross2", "?d \<noteq> 0 \<Longrightarrow> (?a = ?c / ?d) = (?a * ?d = ?c)"), Thm ("mult_cross1", "?b \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c) = (?a = ?b * ?c)"), |
|
1298 Thm ("mult_cross", "?b \<noteq> 0 \<Longrightarrow> ?d \<noteq> 0 \<Longrightarrow> (?a / ?b = ?c / ?d) = (?a * ?d = ?b * ?c)"), Thm ("rat_power", "(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"), Thm ("divide_divide_eq_left", "?a / ?b / ?c = ?a / (?b * ?c)"), |
|
1299 Thm ("real_divide_divide1", "?y \<noteq> 0 \<Longrightarrow> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"), Thm ("times_divide_eq_left", "?b / ?c * ?a = ?b * ?a / ?c"), |
|
1300 Thm ("times_divide_eq_right", "?a * (?b / ?c) = ?a * ?b / ?c"), Thm ("rat_mult", "?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"), |
|
1301 Thm ("rat_add3", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a + ?b / ?c = (?a * ?c + ?b) / ?c"), Thm ("rat_add2", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"), |
|
1302 Thm ("rat_add1", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?a / ?c + ?b / ?c = (?a + ?b) / ?c"), |
|
1303 Thm ("rat_add", "?a is_num \<Longrightarrow> ?b is_num \<Longrightarrow> ?c is_num \<Longrightarrow> ?d is_num \<Longrightarrow> ?a / ?c + ?b / ?d = (?a * ?d + ?b * ?c) / (?c * ?d)"), Thm ("sym_minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"), |
|
1304 Eval ("Rings.divide_class.divide", fn), Eval ("HOL.eq", fn), Thm ("plus_leq", "(0 \<le> ?a + ?b) = (- 1 * ?b \<le> ?a)"), Thm ("minus_leq", "(0 \<le> ?a - ?b) = (?b \<le> ?a)"), |
|
1305 ======^^^^^^====== |
|
1306 Thm ("rat_leq1", "0 \<noteq> ?b \<Longrightarrow> 0 \<noteq> ?d \<Longrightarrow> (?a / ?b \<le> ?c / ?d) = (?a * ?d \<le> ?b * ?c)"), Thm ("rat_leq2", "0 \<noteq> ?d \<Longrightarrow> (?a \<le> ?c / ?d) = (?a * ?d \<le> ?c)"), |
|
1307 Thm ("rat_leq3", "0 \<noteq> ?b \<Longrightarrow> (?a / ?b \<le> ?c) = (?a \<le> ?b * ?c)")], |
|
1308 scr = Empty_Prog, srls = Empty}, |
|
1309 errpatts = [], id = "polyeq_simplify", <<<------------------------------- "polyeq_simplify" |
|
1310 preconds = [], rew_ord = ("termlessI", fn), rules = |
|
1311 [Thm ("real_assoc_1", "?a + (?b + ?c) = ?a + ?b + ?c"), Thm ("real_assoc_2", "?a * (?b * ?c) = ?a * ?b * ?c"), Thm ("real_diff_minus", "?a - ?b = ?a + - 1 * ?b"), |
|
1312 Thm ("real_unari_minus", "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"), Thm ("realpow_multI", "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"), Eval ("Groups.plus_class.plus", fn), Eval ("Groups.minus_class.minus", fn), |
|
1313 Eval ("Groups.times_class.times", fn), Eval ("Rings.divide_class.divide", fn), Eval ("NthRoot.sqrt", fn), Eval ("Transcendental.powr", fn), |
|
1314 ======^^^^^^====== |
|
1315 Rls_ |
|
1316 ( |
|
1317 Repeat |
|
1318 {calc = [], erls = |
|
1319 Repeat ---------vvvvvvvvvvvvvvvvvvvvvvvvv------------------ |
|
1320 {calc = [], erls = Empty, errpatts = [], id = "erls_in_reduce_012", preconds = [], rew_ord = ("dummy_ord", fn), rules = |
|
1321 [Eval ("Prog_Expr.is_num", fn), Thm ("not_false", "(\<not> False) = True"), Thm ("not_true", "(\<not> True) = False")], scr = Empty_Prog, srls = Empty}, |
|
1322 errpatts = [], id = "reduce_012", <<<---------------------------------- "reduce_012" |
|
1323 preconds = [], rew_ord = ("dummy_ord", fn), rules = |
|
1324 [Thm ("mult_1_left", "1 * ?a = ?a"), Thm ("real_minus_mult_left", "\<not> (?a is_num) \<Longrightarrow> - ?a * ?b = - (?a * ?b)"), Thm ("mult_zero_left", "0 * ?a = 0"), Thm ("add_0_left", "0 + ?a = ?a"), |
|
1325 Thm ("add_0_right", "?a + 0 = ?a"), Thm ("right_minus", "?a + - ?a = 0"), Thm ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1"), Thm ("real_mult_2_assoc", "?z1.0 + (?z1.0 + ?k) = 2 * ?z1.0 + ?k")], |
|
1326 scr = Empty_Prog, srls = Empty} |
|
1327 )], |
|
1328 scr = Empty_Prog, srls = Empty}: id = |
|
1329 Rule_Def.rule_set*) |
|
1330 \<close> ML \<open> |
|
1331 "~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) = |
|
1332 (ruls, [], ct, Noap, ruls); |
|
1333 \<close> ML \<open> |
|
1334 val Rule.Thm (thmid, thm) = |
|
1335 (*case*) rul (*of*); |
|
1336 \<close> ML \<open> |
|
1337 val NONE = (*case*) rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1338 ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*); |
|
1339 \<close> ML \<open> |
|
1340 (* GOON: find a way to find out, why test -- fun adhoc_thm + fun eval_cancel -- gives |
|
1341 Eval.adhoc_thm \<longrightarrow> NONE and above we have ERROR |
|
1342 (*rew_once: Eval.get_pair for "Rings.divide_class.divide" \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2") but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE*) |
|
1343 |
|
1344 *) |
|
1345 \<close> ML \<open> |
|
1346 \<close> ML \<open> |
|
1347 \<close> ML \<open> |
|
1348 \<close> ML \<open> |
|
1349 \<close> ML \<open> |
|
1350 \<close> ML \<open> |
|
1351 \<close> ML \<open> |
|
1352 \<close> ML \<open> |
|
1353 \<close> ML \<open> |
|
1354 \<close> ML \<open> |
|
1355 \<close> ML \<open> |
|
1356 \<close> ML \<open> |
|
1357 \<close> ML \<open> |
|
1358 \<close> ML \<open> |
|
1359 \<close> ML \<open> |
|
1360 \<close> ML \<open> |
|
1361 \<close> ML \<open> |
|
1362 \<close> ML \<open> |
|
1363 \<close> ML \<open> |
|
1364 \<close> ML \<open> |
|
1365 \<close> ML \<open> |
|
1366 \<close> ML \<open> |
|
1367 \<close> ML \<open> |
|
1368 \<close> ML \<open> |
|
1369 \<close> ML \<open> |
|
1370 \<close> ML \<open> |
|
1371 \<close> ML \<open> |
|
1372 (*/------------------------------- fun rew_once ITERATED BY HAND -----------------------------\*) |
|
1373 \<close> ML \<open> |
|
1374 UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or> x = (- 1 - sqrt (1 - 0)) / (2 * 2)"; |
|
1375 \<close> ML \<open> |
|
1376 val thm = Rule.thm (nth 1 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*) |
|
1377 \<close> ML \<open> |
|
1378 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1379 ((#erls o Rule_Set.rep) rls) put_asm thm ct (*of*); |
|
1380 \<close> ML \<open> |
|
1381 val thm = Rule.thm (nth 2 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c" |
|
1382 ATTENTION "real_assoc_1" == "real_assoc_2"*) |
|
1383 \<close> ML \<open> |
|
1384 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1385 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1386 \<close> ML \<open> |
|
1387 val thm = Rule.thm (nth 3 ruls); (* = "?a + (?b + ?c) = ?a + ?b + ?c"*) |
|
1388 \<close> ML \<open> |
|
1389 val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1390 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1391 \<close> ML \<open> |
|
1392 UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 - 0)) / (2 * 2)" |
|
1393 \<close> ML \<open> |
|
1394 val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1395 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1396 \<close> ML \<open> |
|
1397 UnparseC.term ct = "x = (- 1 + sqrt (1 - 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)" |
|
1398 \<close> ML \<open> |
|
1399 val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1400 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1401 \<close> ML \<open> |
|
1402 UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)" |
|
1403 \<close> ML \<open> |
|
1404 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1405 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1406 \<close> ML \<open> |
|
1407 val thm = Rule.thm (nth 4 ruls); (* = "\<not> (?a is_num) \<Longrightarrow> - ?a = - 1 * ?a"*) |
|
1408 \<close> ML \<open> |
|
1409 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1410 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1411 \<close> ML \<open> |
|
1412 val thm = Rule.thm (nth 5 ruls); (* = "(?r * ?s) \<up> ?n = ?r \<up> ?n * ?s \<up> ?n"*) |
|
1413 \<close> ML \<open> |
|
1414 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1415 ((#erls o Rule_Set.rep) rls) put_asm thm ct |
|
1416 \<close> ML \<open> (* \<longrightarrow> Rule.*) |
|
1417 \<close> ML \<open> |
|
1418 val (cc as (op_, _)) = Rule.eval (nth 6 ruls); (* = "Groups.plus_class.plus"*) |
|
1419 \<close> ML \<open> |
|
1420 val NONE = Eval.adhoc_thm thy cc ct |
|
1421 \<close> ML \<open> |
|
1422 val (cc as (op_, _)) = Rule.eval (nth 7 ruls); (* = "Groups.minus_class.minus"*) |
|
1423 \<close> ML \<open> |
|
1424 val NONE = Eval.adhoc_thm thy cc ct |
|
1425 \<close> ML \<open> |
|
1426 val (cc as (op_, _)) = Rule.eval (nth 8 ruls); (* = "Groups.times_class.times"*) |
|
1427 \<close> ML \<open> |
|
1428 val SOME (_, thm') = Eval.adhoc_thm thy cc ct |
|
1429 \<close> ML \<open> |
|
1430 val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1431 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
|
1432 \<close> ML \<open> |
|
1433 "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + - 1 * 0)) / (2 * 2)"; |
|
1434 UnparseC.term ct = "x = (- 1 + sqrt (1 + - 1 * 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)" |
|
1435 \<close> ML \<open> |
|
1436 val SOME (ct, []) = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1437 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
|
1438 \<close> ML \<open> |
|
1439 UnparseC.term ct = "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)" |
|
1440 \<close> ML \<open> |
|
1441 val NONE = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
|
1442 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
|
1443 \<close> ML \<open> |
|
1444 val (cc as (op_, _)) = Rule.eval (nth 9 ruls); (* = "Rings.divide_class.divide"*) |
|
1445 \<close> ML \<open> |
|
1446 val NONE = Eval.adhoc_thm thy cc ct |
|
1447 \<close> ML \<open> |
|
1448 val (cc as (op_, _)) = Rule.eval (nth 10 ruls); (* = "NthRoot.sqrt"*) |
|
1449 \<close> ML \<open> |
|
1450 val NONE = Eval.adhoc_thm thy cc ct |
|
1451 \<close> ML \<open> |
|
1452 val (cc as (op_, _)) = Rule.eval (nth 11 ruls); (* = "Transcendental.powr"*) |
|
1453 \<close> ML \<open> |
|
1454 val NONE = Eval.adhoc_thm thy cc ct |
|
1455 \<close> ML \<open> |
|
1456 val rls' = Rule.rls (nth 12 ruls); (* = "reduce_012"*) |
|
1457 \<close> ML \<open> |
|
1458 val SOME (ct, []) = rewrite__set_ thy (i + 1) put_asm bdv rls' ct |
|
1459 \<close> ML \<open> |
|
1460 "x = (- 1 + sqrt (1 + 0)) / (2 * 2) \<or>\nx = (- 1 + - 1 * sqrt (1 + 0)) / (2 * 2)"; |
|
1461 UnparseC.term ct = "x = (- 1 + sqrt 1) / (2 * 2) \<or> x = (- 1 + - 1 * sqrt 1) / (2 * 2)" |
|
1462 \<close> ML \<open> |
|
1463 length ruls = 12; |
|
1464 (*========== now are further iterations to come, and there is the strange error ===============*) |
|
1465 \<close> ML \<open> |
|
1466 \<close> ML \<open> |
|
1467 \<close> ML \<open> |
|
1468 \<close> ML \<open> |
|
1469 \<close> ML \<open> |
|
1470 \<close> ML \<open> |
|
1471 \<close> ML \<open> |
|
1472 \<close> ML \<open> |
|
1473 \<close> ML \<open> |
|
1474 \<close> ML \<open> |
|
1475 \<close> ML \<open> |
|
1476 \<close> ML \<open> |
|
1477 \<close> ML \<open> |
|
1478 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*) |
|
1479 \<close> text \<open> |
|
1480 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1481 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1482 case f of Test_Out.FormKF "[x = 0, x = - 1 / 2]" => () |
|
1483 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1 / 2]"; |
|
1484 |
|
1485 \<close> ML \<open> |
|
1486 (*EP-//*) |
|
1487 val fmz = ["equality (x + x \<up> 2 = 0)", "solveFor x", "solutions L"]; |
|
1488 val (dI',pI',mI') = ("PolyEq",["abcFormula", "degree_2", "polynomial", "univariate", "equation"], |
|
1489 ["PolyEq", "solve_d2_polyeq_abc_equation"]); |
|
1490 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
1491 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1492 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1493 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1494 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1495 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1496 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1497 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1498 case f of Test_Out.FormKF "[x = 0, x = - 1]" => () |
|
1499 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = - 1]"; |
|
1500 |
|
1501 |
|
1502 \<close> ML \<open> |
|
1503 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
|
1504 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
|
1505 "----------- (-8 - 2*x + x \<up> 2 = 0), (*Schalk 2, S.67 Nr.31.b----"; |
|
1506 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat |
|
1507 see --- val rls = calculate_RootRat > calculate_Rational --- |
|
1508 calculate_RootRat was a TODO with 2002, requires re-design. |
|
1509 see also --- (-8 - 2*x + x \<up> 2 = 0), by rewriting --- below |
|
1510 *) |
|
1511 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", (*Schalk 2, S.67 Nr.31.b*) |
|
1512 "solveFor x", "solutions L"]; |
137 "solveFor x", "solutions L"]; |
1513 val (dI',pI',mI') = |
138 val (dI',pI',mI') = |
1514 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
139 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
1515 ["PolyEq", "complete_square"]); |
140 ["PolyEq", "complete_square"]); |
1516 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
141 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
1517 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
142 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1518 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
143 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1519 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
144 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1520 |
145 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1521 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
146 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1522 (*Apply_Method ("PolyEq", "complete_square")*) |
147 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1523 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
148 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1524 (*"-8 - 2 * x + x \<up> 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*) |
149 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1525 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1526 (*"-8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2", nxt = Rewrite("square_explicit1"*) |
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1527 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1528 (*"(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - -8" nxt = Rewrite("root_plus_minus*) |
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1529 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1530 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) | |
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1531 2 / 2 - x = - sqrt ((2 / 2) \<up> 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*) |
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1532 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1533 (*"2 / 2 - x = sqrt ((2 / 2) \<up> 2 - -8) | |
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1534 - 1*x = - (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8)"nxt = R_Inst("bdv_explt2"*) |
|
1535 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1536 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) | |
|
1537 - 1 * x = (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = bdv_explicit3*) |
|
1538 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1539 (*"- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) | |
|
1540 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))" nxt = bdv_explicit3*) |
|
1541 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1542 (*"x = - 1 * (- (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8)) | |
|
1543 x = - 1 * (- (2 / 2) + - sqrt ((2 / 2) \<up> 2 - -8))"nxt = calculate_Rational |
|
1544 NOT IMPLEMENTED SINCE 2002 ------------------------------ \<up> \<up> \<up> \<up> \<up> \<up> *) |
|
1545 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1546 (*"x = - 2 | x = 4" nxt = Or_to_List*) |
|
1547 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1548 (*"[x = - 2, x = 4]" nxt = Check_Postcond*) |
|
1549 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
1550 (* FIXXXME |
160 (*WN.2.5.03 TODO FIXME Matthias ? |
1551 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 2, x = 4]")) => () TODO |
161 case f of |
1552 | _ => error "polyeq.sml: diff.behav. in [x = - 2, x = 4]"; |
162 Form' |
1553 *) |
163 (Test_Out.FormKF |
1554 if f2str f = |
164 (~1,EdUndef,0,Nundef, |
1555 "[x = - 1 * - 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))]" |
165 "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]")) |
1556 (*"[x = - 1 * - 1 + - 1 * sqrt (1 \<up> 2 - -8),\n x = - 1 * - 1 + - 1 * (- 1 * sqrt (1 \<up> 2 - -8))]"*) |
166 => () |
1557 then () else error "polyeq.sml corrected?behav. in [x = - 2, x = 4]"; |
167 | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x \<up> 2 = 0"; |
1558 |
168 this will be simplified [x = a, x = b] to by Factor.ML*) |
1559 |
169 |
1560 \<close> ML \<open> |
170 |
1561 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------"; |
171 \<close> ML \<open> |
1562 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------"; |
172 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
1563 "----------- (-8 - 2*x + x \<up> 2 = 0), by rewriting ---------------"; |
173 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
1564 (*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat |
174 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)"; |
1565 see --- val rls = calculate_RootRat > calculate_Rational ---*) |
175 val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*) |
1566 val thy = @{theory PolyEq}; |
|
1567 val ctxt = Proof_Context.init_global thy; |
|
1568 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")]; |
|
1569 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)"; |
|
1570 |
|
1571 \<close> ML \<open> |
|
1572 val rls = complete_square; |
|
1573 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; |
|
1574 \<close> ML \<open> |
|
1575 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2" |
|
1576 then () else error "rls complete_square CHANGED"; |
|
1577 |
|
1578 \<close> ML \<open> |
|
1579 val thm = @{thm square_explicit1}; |
|
1580 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; |
|
1581 \<close> ML \<open> |
|
1582 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8" |
|
1583 then () else error "thm square_explicit1 CHANGED"; |
|
1584 |
|
1585 \<close> ML \<open> |
|
1586 val thm = @{thm root_plus_minus}; |
|
1587 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; |
|
1588 \<close> ML \<open> |
|
1589 if UnparseC.term t = |
|
1590 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
|
1591 then () else error "thm root_plus_minus CHANGED"; |
|
1592 |
|
1593 \<close> ML \<open> |
|
1594 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
|
1595 val thm = @{thm bdv_explicit2}; |
|
1596 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
|
1597 \<close> ML \<open> |
|
1598 if UnparseC.term t = |
|
1599 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
|
1600 then () else error "thm bdv_explicit2 CHANGED"; |
|
1601 |
|
1602 \<close> ML \<open> |
|
1603 val thm = @{thm bdv_explicit3}; |
|
1604 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
|
1605 \<close> ML \<open> |
|
1606 if UnparseC.term t = |
|
1607 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
|
1608 then () else error "thm bdv_explicit3 CHANGED"; |
|
1609 |
|
1610 \<close> ML \<open> |
|
1611 val thm = @{thm bdv_explicit2}; |
|
1612 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
|
1613 \<close> ML \<open> |
|
1614 if UnparseC.term t = |
|
1615 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
|
1616 then () else error "thm bdv_explicit2 CHANGED"; |
|
1617 |
|
1618 \<close> ML \<open> |
|
1619 val rls = calculate_RootRat; |
|
1620 val SOME (t,asm) = rewrite_set_ thy true rls t; |
|
1621 \<close> ML \<open> |
|
1622 if UnparseC.term t = |
|
1623 "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))" |
|
1624 (*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*) |
|
1625 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; |
|
1626 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) |
|
1627 |
|
1628 |
|
1629 \<close> ML \<open> |
|
1630 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
|
1631 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
|
1632 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
|
1633 "---- test the erls ----"; |
|
1634 val t1 = (Thm.term_of o the o (TermC.parse thy)) "0 <= (10/3/2) \<up> 2 - 1"; |
|
1635 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; |
|
1636 val t' = UnparseC.term t; |
|
1637 (*if t'= \<^const_name>\<open>True\<close> then () |
|
1638 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) |
|
1639 (* *) |
|
1640 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)", |
|
1641 "solveFor x", "solutions L"]; |
176 "solveFor x", "solutions L"]; |
1642 val (dI',pI',mI') = |
177 val (dI',pI',mI') = |
1643 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
178 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
1644 ["PolyEq", "complete_square"]); |
179 ["PolyEq", "complete_square"]); |
1645 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
180 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
1646 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
181 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1647 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
182 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1648 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
183 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1649 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
184 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1650 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
185 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1651 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
186 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1652 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
187 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1653 (*Apply_Method ("PolyEq", "complete_square")*) |
188 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1654 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
189 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1655 |
190 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1656 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------"; |
191 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1657 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------"; |
192 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1658 "----------- (- 16 + 4*x + 2*x \<up> 2 = 0), --------------------------"; |
193 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f; |
1659 val fmz = ["equality (- 16 + 4*x + 2*x \<up> 2 = 0)", |
194 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = - 1 * sqrt (0 - -64)]" |
|
195 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => () |
|
196 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]"; |
|
197 *) |
|
198 |
|
199 \<close> ML \<open> |
|
200 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
201 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
202 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)"; |
|
203 val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*) |
1660 "solveFor x", "solutions L"]; |
204 "solveFor x", "solutions L"]; |
1661 val (dI',pI',mI') = |
205 val (dI',pI',mI') = |
1662 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
206 ("PolyEq",["degree_2", "expanded", "univariate", "equation"], |
1663 ["PolyEq", "complete_square"]); |
207 ["PolyEq", "complete_square"]); |
1664 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
208 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
1665 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1666 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
210 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1667 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
211 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1668 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
212 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1669 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
213 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1670 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
214 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1671 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1672 (*Apply_Method ("PolyEq", "complete_square")*) |
216 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
1673 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
217 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = - 1 * sqrt (0 - -49)]" |
1674 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
218 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => () |
1675 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
219 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]"; |
1676 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1677 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1678 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1679 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1680 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1681 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1682 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
1683 (* FIXXXXME n1., |
|
1684 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO |
|
1685 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]"; |
|
1686 *) |
220 *) |
1687 |
221 if f2str f = "[x = sqrt (0 - - 49), x = - 1 * sqrt (0 - - 49)]" then () |
1688 \<close> ML \<open> |
222 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]"; |
1689 \<close> |
223 |
1690 |
224 |
1691 section \<open>===================================================================================\<close> |
225 \<close> ML \<open> |
1692 ML \<open> |
226 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; |
1693 \<close> ML \<open> |
227 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; |
|
228 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = - 11),(*Schalk Is86Bsp5"; |
|
229 (*EP- 17 Schalk_I_p86_n5*) |
|
230 val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"]; |
|
231 (* Refine.refine fmz ["univariate", "equation"]; |
|
232 *) |
|
233 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); |
|
234 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
235 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
236 (* val nxt = |
|
237 ("Model_Problem", |
|
238 Model_Problem ["normalise", "polynomial", "univariate", "equation"]) |
|
239 : string * tac*) |
|
240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
241 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
242 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
244 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
245 (* val nxt = |
|
246 ("Subproblem", |
|
247 Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) |
|
248 : string * tac *) |
|
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
250 (*val nxt = |
|
251 ("Model_Problem", |
|
252 Model_Problem ["degree_1", "polynomial", "univariate", "equation"]) |
|
253 : string * tac *) |
|
254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
257 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
260 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
261 case f of Test_Out.FormKF "[x = 2]" => () |
|
262 | _ => error "polyeq.sml: diff.behav. in [x = 2]"; |
|
263 |
|
264 |
|
265 \<close> ML \<open> |
|
266 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37"; |
|
267 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37"; |
|
268 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37"; |
|
269 (*is in rlang.sml, too*) |
|
270 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))", |
|
271 "solveFor x", "solutions L"]; |
|
272 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); |
|
273 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
274 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate", "equation"])*) |
|
275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
276 (* val nxt = |
|
277 ("Model_Problem", |
|
278 Model_Problem ["normalise", "polynomial", "univariate", "equation"]) |
|
279 : string * tac *) |
|
280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
284 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
286 (* val nxt = |
|
287 ("Subproblem", |
|
288 Subproblem ("PolyEq",["polynomial", "univariate", "equation"])) |
|
289 : string * tac*) |
|
290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
291 (*val nxt = |
|
292 ("Model_Problem", |
|
293 Model_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]) |
|
294 : string * tac*) |
|
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
296 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
299 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
300 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
301 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
302 case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => () |
|
303 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]"; |
|
304 |
|
305 |
|
306 " -4 + x \<up> 2 =0 "; |
|
307 " -4 + x \<up> 2 =0 "; |
|
308 " -4 + x \<up> 2 =0 "; |
|
309 val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"]; |
|
310 (* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*) |
|
311 (*val fmz = ["equality (0 =0)", "solveFor x", "solutions L"];*) |
|
312 val (dI',pI',mI') = ("PolyEq",["univariate", "equation"],["no_met"]); |
|
313 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
314 |
|
315 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
316 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
318 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
321 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
322 case f of Test_Out.FormKF "[x = 2, x = - 2]" => () |
|
323 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = - 2]"; |
|
324 |
|
325 \<close> ML \<open> |
|
326 "----------- rls make_polynomial_in ------------------------------"; |
|
327 "----------- rls make_polynomial_in ------------------------------"; |
|
328 "----------- rls make_polynomial_in ------------------------------"; |
|
329 val thy = @{theory}; |
|
330 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*) |
|
331 (*WN.19.3.03 ---v-*) |
|
332 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1"); |
|
333 val t = TermC.str2term "- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0"; |
|
334 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
335 if UnparseC.term t' = "- 1 * R * R2 + R2 * R1 + - 1 * R * R1 = 0" then () |
|
336 else error "make_polynomial_in (- 1 * (R * R2) + R2 * R1 + - 1 * (R * R1) = 0)"; |
|
337 "- 1 * R * R2 + (R2 + - 1 * R) * R1 = 0"; |
|
338 (*WN.19.3.03 ---^-*) |
|
339 |
|
340 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p"); |
|
341 val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0"; |
|
342 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
343 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then () |
|
344 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)"; |
|
345 |
|
346 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2"); |
|
347 val t = TermC.str2term |
|
348 "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"; |
|
349 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
350 if UnparseC.term t' = |
|
351 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - 1 * x1 * y2 * (1 / 2) +\n- 1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n- 1 * y3 * (1 / 2) * x2 =\n0" |
|
352 then () |
|
353 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1..."; |
|
354 "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"; |
|
355 |
|
356 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t; |
|
357 if UnparseC.term t' = |
|
358 "A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + - 1 * x1 * y2 / 2 + - 1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n- 1 * y3 * x2 / 2 =\n0" |
|
359 then () |
|
360 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + - 1..."; |
|
361 "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"; |
|
362 |
|
363 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a"); |
|
364 val t = TermC.str2term |
|
365 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0"; |
|
366 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t; |
|
367 (* the invisible parentheses are as expected *) |
|
368 |
|
369 val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0"; |
|
370 Rewrite.trace_on:= false; (*true false*) |
|
371 rewrite_set_ thy false expand_binoms t; |
|
372 Rewrite.trace_on:=false; (*true false*) |
|
373 |
|
374 |
|
375 \<close> ML \<open> |
|
376 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
377 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
378 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------"; |
|
379 reset_states (); |
|
380 CalcTree |
|
381 [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"], |
|
382 ("PolyEq",["univariate", "equation"],["no_met"]))]; |
|
383 Iterator 1; |
|
384 moveActiveRoot 1; |
|
385 |
|
386 autoCalculate 1 CompleteCalc; |
|
387 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
|
388 interSteps 1 ([1],Res) |
|
389 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*); |
|
390 |
|
391 |
|
392 \<close> ML \<open> |
|
393 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
394 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
395 "----------- rls d2_polyeq_bdv_only_simplify ---------------------"; |
|
396 val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)"; |
|
397 val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")]; |
|
398 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t; |
|
399 (* steps in rls d2_polyeq_bdv_only_simplify:*) |
|
400 |
|
401 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1", "")) --> x * (-6 + 5 * x) = 0*) |
|
402 t |> UnparseC.term; t |> TermC.atomty; |
|
403 val thm = @{thm d2_prescind1}; |
|
404 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; |
|
405 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t'; |
|
406 |
|
407 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", "")) |
|
408 --> x = 0 | -6 + 5 * x = 0*) |
|
409 t' |> UnparseC.term; t' |> TermC.atomty; |
|
410 val thm = @{thm d2_reduce_equation1}; |
|
411 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty; |
|
412 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t''; |
|
413 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" |
|
414 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" |
|
415 *) |
|
416 if UnparseC.term t'' = "x = 0 \<or> - 6 + 5 * x = 0" then () |
|
417 else error "rls d2_polyeq_bdv_only_simplify broken"; |
1694 \<close> ML \<open> |
418 \<close> ML \<open> |
1695 \<close> ML \<open> |
419 \<close> ML \<open> |
1696 \<close> |
420 \<close> |
1697 |
421 |
1698 section \<open>===================================================================================\<close> |
422 section \<open>===================================================================================\<close> |