191 val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x / 5"; |
191 val t = (Thm.term_of o the o (TermC.parse thy)) "3 * x / 5"; |
192 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true |
192 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true |
193 [ (bdv, v) ] make_ratpoly_in t; |
193 [ (bdv, v) ] make_ratpoly_in t; |
194 if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1"; |
194 if UnparseC.term t' = "3 / 5 * x" then () else error "rlang.sml: 1"; |
195 |
195 |
196 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; |
196 val t = TermC.parse_test @{context} "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; |
197 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
197 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
198 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
198 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
199 if UnparseC.term t' = "1 / 18 = 0" then () else error "rlang.sml: 2"; |
199 if UnparseC.term t' = "1 / 18 = 0" then () else error "rlang.sml: 2"; |
200 (*WN---^ *) |
200 (*WN---^ *) |
201 |
201 |
202 (*----------------- Schalk I s.87 Bsp 36b ------------------------*) |
202 (*----------------- Schalk I s.87 Bsp 36b ------------------------*) |
224 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 237 / 65]")) => () |
224 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = - 237 / 65]")) => () |
225 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = - 237 / 65]"; |
225 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = - 237 / 65]"; |
226 |
226 |
227 |
227 |
228 (*WN---v *) |
228 (*WN---v *) |
229 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0"; |
229 val t = TermC.parse_test @{context} "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0"; |
230 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
230 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
231 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
231 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
232 UnparseC.term t'; |
232 UnparseC.term t'; |
233 if UnparseC.term t' = "79 / 12 + 65 / 36 * x = 0" then () |
233 if UnparseC.term t' = "79 / 12 + 65 / 36 * x = 0" then () |
234 else error "rlang.sml: 3"; |
234 else error "rlang.sml: 3"; |
235 (*WN---^ *) |
235 (*WN---^ *) |
336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
337 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => () |
337 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => () |
338 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]"; |
338 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]"; |
339 |
339 |
340 (*WN---v *) |
340 (*WN---v *) |
341 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29"; |
341 val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29"; |
342 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
342 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
343 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
343 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
344 if UnparseC.term t' = "23 + 35 * x + -72 * x \<up> 2" then () |
344 if UnparseC.term t' = "23 + 35 * x + -72 * x \<up> 2" then () |
345 else error "rlang.sml: 4"; |
345 else error "rlang.sml: 4"; |
346 |
346 |
347 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 + (6*x) \<up> 2 - 29"; |
347 val t = TermC.parse_test @{context} "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 + (6*x) \<up> 2 - 29"; |
348 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
348 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
349 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
349 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
350 if UnparseC.term t' = "-35 + 35 * x" then () |
350 if UnparseC.term t' = "-35 + 35 * x" then () |
351 else error "rlang.sml: 4.1"; |
351 else error "rlang.sml: 4.1"; |
352 (*WN---^ *) |
352 (*WN---^ *) |
353 |
353 |
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
485 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
485 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
486 "[v = (u * v0 + v0 * w + - 1 * f * w) / f]")) => () |
486 "[v = (u * v0 + v0 * w + - 1 * f * w) / f]")) => () |
487 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]"; |
487 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]"; |
488 if Ctree.get_assumptions pt p = |
488 if Ctree.get_assumptions pt p = |
489 [TermC.str2term"(u * v0 + v0 * w + - 1 * f * w) / f + w ~= 0"] then () |
489 [TermC.parse_test @{context}"(u * v0 + v0 * w + - 1 * f * w) / f + w ~= 0"] then () |
490 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm"; |
490 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm"; |
491 |
491 |
492 |
492 |
493 (*----------------- Schalk I s.89 Bsp 90a(2) ------------------------*) |
493 (*----------------- Schalk I s.89 Bsp 90a(2) ------------------------*) |
494 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)"; |
494 "Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)"; |
528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
528 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
529 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
529 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
530 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + - 1 * f * v) / (f + - 1 * v0)]")) => () |
530 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + - 1 * f * v) / (f + - 1 * v0)]")) => () |
531 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)"; |
531 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)"; |
532 if Ctree.get_assumptions pt p = |
532 if Ctree.get_assumptions pt p = |
533 [TermC.str2term"v + (u * v0 + - 1 * f * v) / (f + - 1 * v0) ~= 0", |
533 [TermC.parse_test @{context}"v + (u * v0 + - 1 * f * v) / (f + - 1 * v0) ~= 0", |
534 TermC.str2term"f + - 1 * v0 ~= 0"] |
534 TermC.parse_test @{context}"f + - 1 * v0 ~= 0"] |
535 then writeln "asm should be simplified ???" |
535 then writeln "asm should be simplified ???" |
536 else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm"; |
536 else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm"; |
537 |
537 |
538 (*----------------- Schalk I s.89 Bsp 98a(1) ------------------------*) |
538 (*----------------- Schalk I s.89 Bsp 98a(1) ------------------------*) |
539 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)"; |
539 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)"; |
569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
569 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
570 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
571 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
572 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + - 1 * R)]")) => () |
572 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + - 1 * R)]")) => () |
573 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]"; |
573 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]"; |
574 if Ctree.get_assumptions pt p = [TermC.str2term"R * R2 * R2 ~= (R2 + - 1 * R) * 0", |
574 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"R * R2 * R2 ~= (R2 + - 1 * R) * 0", |
575 TermC.str2term"R2 + - 1 * R ~= 0", |
575 TermC.parse_test @{context}"R2 + - 1 * R ~= 0", |
576 TermC.str2term"R2 + - 1 * R ~= 0"] |
576 TermC.parse_test @{context}"R2 + - 1 * R ~= 0"] |
577 then writeln "asm should be simplified" |
577 then writeln "asm should be simplified" |
578 else error "rlang.sml: diff.behav. in 98a(1) asm"; |
578 else error "rlang.sml: diff.behav. in 98a(1) asm"; |
579 |
579 |
580 (*----------------- Schalk I s.89 Bsp 104a(1) ------------------------*) |
580 (*----------------- Schalk I s.89 Bsp 104a(1) ------------------------*) |
581 "Schalk I s.89 Bsp 104a (1) (y \<up> 2=2*p*x)"; |
581 "Schalk I s.89 Bsp 104a (1) (y \<up> 2=2*p*x)"; |
600 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
600 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
601 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
601 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
603 case f of Form' (Test_Out.FormKF (_,_,0,_,"[p = y \<up> 2 / (2 * x)]")) => () |
603 case f of Form' (Test_Out.FormKF (_,_,0,_,"[p = y \<up> 2 / (2 * x)]")) => () |
604 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]"; |
604 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]"; |
605 if Ctree.get_assumptions pt p = [TermC.str2term"- 2 * x ~= 0"] |
605 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"- 2 * x ~= 0"] |
606 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n" |
606 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n" |
607 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm"; |
607 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm"; |
608 |
608 |
609 |
609 |
610 (*----------------- Schalk I s.89 Bsp 104a(2) ------------------------*) |
610 (*----------------- Schalk I s.89 Bsp 104a(2) ------------------------*) |
630 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
630 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
631 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
631 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
632 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
632 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
633 case f of Form' (Test_Out.FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = - 1 * sqrt (2 * p * x)]")) => () |
633 case f of Form' (Test_Out.FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = - 1 * sqrt (2 * p * x)]")) => () |
634 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]"; |
634 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]"; |
635 if Ctree.get_assumptions pt p = [TermC.str2term"0 <= - 1 * (- 2 * p * x)", |
635 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)", |
636 TermC.str2term"0 <= - 1 * (- 2 * p * x)"] |
636 TermC.parse_test @{context}"0 <= - 1 * (- 2 * p * x)"] |
637 then writeln "asm should be simplified\nshould be simplified" |
637 then writeln "asm should be simplified\nshould be simplified" |
638 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm"; |
638 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm"; |
639 |
639 |
640 |
640 |
641 (*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*) |
641 (*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*) |
676 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p; |
676 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p; |
677 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2),\n x = - 1 * sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2)]")) => writeln"should be simplified MG" |
677 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2),\n x = - 1 * sqrt ((a \<up> 2 * b \<up> 2 + - 1 * a \<up> 2 * y \<up> 2) / b \<up> 2)]")) => writeln"should be simplified MG" |
678 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]"; |
678 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]"; |
679 val asms = Ctree.get_assumptions pt p; |
679 val asms = Ctree.get_assumptions pt p; |
680 if asms = |
680 if asms = |
681 [TermC.str2term"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)", |
681 [TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)", |
682 TermC.str2term"b \<up> 2 ~= 0", |
682 TermC.parse_test @{context}"b \<up> 2 ~= 0", |
683 TermC.str2term"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)", |
683 TermC.parse_test @{context}"0 * b \<up> 2 <= - 1 * (a \<up> 2 * y \<up> 2 + - 1 * a \<up> 2 * b \<up> 2)", |
684 TermC.str2term"b \<up> 2 ~= 0"] then writeln"should be simplified MG" |
684 TermC.parse_test @{context}"b \<up> 2 ~= 0"] then writeln"should be simplified MG" |
685 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms"; |
685 else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms"; |
686 |
686 |
687 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*) |
687 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*) |
688 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))"; |
688 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))"; |
689 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))"; |
689 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))"; |
707 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
707 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
708 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
708 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
709 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
709 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
710 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (- 2 * A + x1 * y2 + x3 * y1 + - 1 * x1 * y3 + - 1 * x3 * y2) /\n (y1 + - 1 * y3)]")) => () |
710 case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (- 2 * A + x1 * y2 + x3 * y1 + - 1 * x1 * y3 + - 1 * x3 * y2) /\n (y1 + - 1 * y3)]")) => () |
711 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]"; |
711 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]"; |
712 if Ctree.get_assumptions pt p = [TermC.str2term"y1 / 2 + - 1 * y3 / 2 ~= 0"] then () |
712 if Ctree.get_assumptions pt p = [TermC.parse_test @{context}"y1 / 2 + - 1 * y3 / 2 ~= 0"] then () |
713 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm"; |
713 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm"; |
714 |
714 |
715 (*-------------------- Schalk II ----------------------------*) |
715 (*-------------------- Schalk II ----------------------------*) |
716 (*-------------------- Schalk II ----------------------------*) |
716 (*-------------------- Schalk II ----------------------------*) |
717 (*-------------------- Schalk II ----------------------------*) |
717 (*-------------------- Schalk II ----------------------------*) |
822 \0 <= 1 / 9,\ |
822 \0 <= 1 / 9,\ |
823 \0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56,\ |
823 \0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56,\ |
824 \0 <= 1 / 9]" |
824 \0 <= 1 / 9]" |
825 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..' |
825 (*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..' |
826 thus: maybe the rls for the asms is Rule_Set.Empty ??: |
826 thus: maybe the rls for the asms is Rule_Set.Empty ??: |
827 [(TermC.str2term"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", []), |
827 [(TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", []), |
828 (TermC.str2term"9 ~= 0", []), |
828 (TermC.parse_test @{context}"9 ~= 0", []), |
829 (TermC.str2term"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []), |
829 (TermC.parse_test @{context}"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []), |
830 (TermC.str2term"9 ~= 0", []), |
830 (TermC.parse_test @{context}"9 ~= 0", []), |
831 (TermC.str2term"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", [])]*) |
831 (TermC.parse_test @{context}"0 <= (25 * (1 / 9) + - 1 * (16 + 49 * (1 / 9))) * -56", [])]*) |
832 then "should get True * False!!!" |
832 then "should get True * False!!!" |
833 else error "rlang.sml: diff.behav. in II 68a asms"; |
833 else error "rlang.sml: diff.behav. in II 68a asms"; |
834 |
834 |
835 (*----------------- Schalk II s.56 Bsp 73b ------------------------*) |
835 (*----------------- Schalk II s.56 Bsp 73b ------------------------*) |
836 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))"; |
836 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))"; |
1327 val nxt = ("Rewrite_Set",Rewrite_Set "make_ratpoly") : string * tac |
1327 val nxt = ("Rewrite_Set",Rewrite_Set "make_ratpoly") : string * tac |
1328 "(a + b * x) / (a + - 1 * b * x) + (- 1 * a + b * x) / (a + b * x) =\n4 * |
1328 "(a + b * x) / (a + - 1 * b * x) + (- 1 * a + b * x) / (a + b * x) =\n4 * |
1329 a * b / (a \<up> 2 + - 1 * b \<up> 2)" |
1329 a * b / (a \<up> 2 + - 1 * b \<up> 2)" |
1330 |
1330 |
1331 |
1331 |
1332 val t = TermC.str2term"(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)"; |
1332 val t = TermC.parse_test @{context}"(a + b * x) / (a + - 1 * (b * x)) + - 1 * (a + - 1 * (b * x)) / (a + b * x) =\n4 * a * b / (a \<up> 2 + - 1 * b \<up> 2)"; |
1333 Rewrite.trace_on := false; (*true false*) |
1333 Rewrite.trace_on := false; (*true false*) |
1334 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t; |
1334 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t; |
1335 UnparseC.term t'; |
1335 UnparseC.term t'; |
1336 Rewrite.trace_on:=false; (*true false*) |
1336 Rewrite.trace_on:=false; (*true false*) |
1337 |
1337 |
1494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*) |
1494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*) |
1495 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
1495 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
1496 "[x = (- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4,\n x =\n (- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4]")) then writeln "simplify MG" |
1496 "[x = (- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4,\n x =\n (- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4]")) then writeln "simplify MG" |
1497 else error "rlang.sml: diff.behav. in II 62b [x=...]"; |
1497 else error "rlang.sml: diff.behav. in II 62b [x=...]"; |
1498 val asms = Ctree.get_assumptions pt p; |
1498 val asms = Ctree.get_assumptions pt p; |
1499 if asms = [TermC.str2term"0 <= ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2", |
1499 if asms = [TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2", |
1500 TermC.str2term"0 <= a + 2 * b", |
1500 TermC.parse_test @{context}"0 <= a + 2 * b", |
1501 TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1501 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1502 TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1502 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1503 TermC.str2term"0 <= ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2", |
1503 TermC.parse_test @{context}"0 <= ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 + a) \<up> 2 + ((- 2 * a + 4 * b + - 1 * sqrt (16 * a * b + 16 * b \<up> 2 + 4 * a \<up> 2)) / 4 - 2 * b) \<up> 2", |
1504 TermC.str2term"0 <= a + 2 * b", |
1504 TermC.parse_test @{context}"0 <= a + 2 * b", |
1505 TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1505 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2", |
1506 TermC.str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2"] |
1506 TermC.parse_test @{context}"8 * (-4 * a * b) <= (-4 * b + 2 * a) \<up> 2"] |
1507 then writeln "should be simplified MG" |
1507 then writeln "should be simplified MG" |
1508 else error "rlang.sml: diff.behav. in II 62b asms"; |
1508 else error "rlang.sml: diff.behav. in II 62b asms"; |
1509 |
1509 |
1510 "------ WN.TEST---------------------------------"; |
1510 "------ WN.TEST---------------------------------"; |
1511 "------ WN.TEST---------------------------------"; |
1511 "------ WN.TEST---------------------------------"; |
1521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1522 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1522 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1523 (* |
1523 (* |
1524 val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x \<up> 2 = 0")) |
1524 val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x \<up> 2 = 0")) |
1525 normiert nicht ... korr.WN: |
1525 normiert nicht ... korr.WN: |
1526 val t = TermC.str2term "(2*x+1)*x \<up> 2 = 0"; |
1526 val t = TermC.parse_test @{context} "(2*x+1)*x \<up> 2 = 0"; |
1527 val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; |
1527 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]; |
1528 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
1528 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t; |
1529 if UnparseC.term t' = "x \<up> 2 + 2 * x \<up> 3 = 0" then () |
1529 if UnparseC.term t' = "x \<up> 2 + 2 * x \<up> 3 = 0" then () |
1530 else error "rlang.sml: 7"; |
1530 else error "rlang.sml: 7"; |
1531 *) |
1531 *) |
1532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1532 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
1545 |
1545 |
1546 "------ rlang.sml end---------------------------------"; |
1546 "------ rlang.sml end---------------------------------"; |
1547 |
1547 |
1548 (*------------------------------vvv-Rewrite_Set "rat_eliminate"--------- |
1548 (*------------------------------vvv-Rewrite_Set "rat_eliminate"--------- |
1549 > Rewrite.trace_on:=true; (*true false*) |
1549 > Rewrite.trace_on:=true; (*true false*) |
1550 > val t = TermC.str2term |
1550 > val t = TermC.parse_test @{context} |
1551 "(3 + - 1 * x + 1 * x \<up> 2) / (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3) = 1 / x"; |
1551 "(3 + - 1 * x + 1 * x \<up> 2) / (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3) = 1 / x"; |
1552 > val SOME (t',asm) = |
1552 > val SOME (t',asm) = |
1553 rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t; |
1553 rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t; |
1554 > UnparseC.term t'; UnparseC.terms asm; |
1554 > UnparseC.term t'; UnparseC.terms asm; |
1555 "(3 + - 1 * x + 1 * x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3)" |
1555 "(3 + - 1 * x + 1 * x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + 1 * x \<up> 3)" |
1593 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
1593 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef, |
1594 "[a = sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1),\n a = - 1 * sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof') |
1594 "[a = sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1),\n a = - 1 * sqrt ((- 1 * b \<up> 2 + 4 * r \<up> 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof') |
1595 then writeln"simplify result\nsimplify result\nsimplify result" |
1595 then writeln"simplify result\nsimplify result\nsimplify result" |
1596 else error "rlang.sml: diff.behav. in Pythagoras"; |
1596 else error "rlang.sml: diff.behav. in Pythagoras"; |
1597 val asms = Ctree.get_assumptions pt p; |
1597 val asms = Ctree.get_assumptions pt p; |
1598 (*if asms = [TermC.str2term"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)", |
1598 (*if asms = [TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)", |
1599 TermC.str2term"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)"]*) |
1599 TermC.parse_test @{context}"0 <= -4 * (b \<up> 2 / 4 + -4 * r \<up> 2 / 4)"]*) |
1600 if UnparseC.terms (*WN1104changed*) asms = |
1600 if UnparseC.terms (*WN1104changed*) asms = |
1601 "[0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1),\ |
1601 "[0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1),\ |
1602 \0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1)]" |
1602 \0 <= -4 * (b \<up> 2 / 4 + - 1 * r \<up> 2 / 1)]" |
1603 then writeln"simplify result\nsimplify result\nsimplify result" |
1603 then writeln"simplify result\nsimplify result\nsimplify result" |
1604 else error "rlang.sml: diff.behav. in Pythagoras asms"; |
1604 else error "rlang.sml: diff.behav. in Pythagoras asms"; |