wneuper/isa: comparison test/Tools/isac/Knowledge/poly-2.sml

equal deleted inserted replaced

-:90ea835c07b3
+:f92963a33fe3
 "~~~~~~~~~ fun sort_varList
 "~~~~~~~~~~~ fun var_ord
 "~~~~~~~~~~~~~ fun get_basStr               used twice --^^
 "~~~~~~~~~~~~~ fun get_potStr               used twice --^^
 *)
-val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
+val t = TermC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
 eval_is_addUnordered "xxx" "yyy" t @{context};
 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
 		       (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
 ("xxx", "yyy", t, @{context});
 "-------- examples from textbook Schalk I ------------------------------------------------------";
 "-------- examples from textbook Schalk I ------------------------------------------------------";
 "-------- examples from textbook Schalk I ------------------------------------------------------";
 "-----SPB Schalk I p.63 No.267b ---";
-val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
+val t = TermC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
 then () else error "poly.sml: diff.behav. in make_polynomial 1";
 "-----SPB Schalk I p.63 No.275b ---";
-val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
+val t = TermC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t =
 "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"
 then () else error "poly.sml: diff.behav. in make_polynomial 2";
 "-----SPB Schalk I p.63 No.279b ---";
-val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
+val t = TermC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t =
 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
 "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
 "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
 " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
 then () else error "poly.sml: diff.behav. in make_polynomial 3";
 (*associate poly*)
 "-----SPB Schalk I p.63 No.291 ---";
-val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
+val t = TermC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
 then () else error "poly.sml: diff.behav. in make_polynomial 4";
 "-----SPB Schalk I p.64 No.295c ---";
-val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
+val t = TermC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t =
 "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"
 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
 "-----SPB Schalk I p.64 No.299a ---";
-val t = TermC.str2term "(x - y)*(x + y)";
+val t = TermC.parse_test @{context} "(x - y)*(x + y)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
 then () else error "poly.sml: diff.behav. in make_polynomial 6";
 "-----SPB Schalk I p.64 No.300c ---";
-val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
+val t = TermC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
 then () else error "poly.sml: diff.behav. in make_polynomial 7";
 "-----SPB Schalk I p.64 No.302 ---";
-val t = TermC.str2term
+val t = TermC.parse_test @{context}
 "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
 if UnparseC.term t = "0"
 then () else error "poly.sml: diff.behav. in make_polynomial 8";
 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
 "-----SPB Schalk I p.64 No.306a ---";
-val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
+val t = TermC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";
 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
 the above resulted in the term below ... but reduces from then correctly*)
-val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
+val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
 "-----SPB Schalk I p.64 No.296a ---";
-val t = TermC.str2term "(x - a) \<up> 3";
+val t = TermC.parse_test @{context} "(x - a) \<up> 3";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
-val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc";
+val NONE = eval_is_even "aaa" "bbb" (TermC.parse_test @{context} "3::real") "ccc";
 if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
 then () else error "poly.sml: diff.behav. in make_polynomial 10";
 "-----SPB Schalk I p.64 No.296c ---";
-val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
+val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
 then () else error "poly.sml: diff.behav. in make_polynomial 11";
 "-----SPB Schalk I p.62 No.242c ---";
-val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
+val t = TermC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "1"
 then () else error "poly.sml: diff.behav. in make_polynomial 12";
 "-----SPB Schalk I p.60 No.209a ---";
-val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
+val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "a \<up> 7"
 then () else error "poly.sml: diff.behav. in make_polynomial 13";
 "-----SPB Schalk I p.60 No.209d ---";
-val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
+val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "d \<up> 3"
 then () else error "poly.sml: diff.behav. in make_polynomial 14";
 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
 "-----Schalk I p.64 No.303 ---";
-val t = TermC.str2term "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
+val t = TermC.parse_test @{context} "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
 (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "1280 * b \<up> 4"
 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
 "-----SPO ---";
-val t = TermC.str2term "a + a + a";
+val t = TermC.parse_test @{context} "a + a + a";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "3 * a" then ()
 else error "poly.sml: diff.behav. in make_polynomial 16";
 "-----SPO ---";
-val t = TermC.str2term "a + b + b + b";
+val t = TermC.parse_test @{context} "a + b + b + b";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "a + 3 * b" then ()
 else error "poly.sml: diff.behav. in make_polynomial 17";
 "-----SPO ---";
-val t = TermC.str2term "b * a * a";
+val t = TermC.parse_test @{context} "b * a * a";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "a \<up> 2 * b" then ()
 else error "poly.sml: diff.behav. in make_polynomial 21";
 "-----SPO ---";
-val t = TermC.str2term "(a \<up> 2) \<up> 3";
+val t = TermC.parse_test @{context} "(a \<up> 2) \<up> 3";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "a \<up> 6" then ()
 else error "poly.sml: diff.behav. in make_polynomial 22";
 "-----SPO ---";
-val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
+val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
 else error "poly.sml: diff.behav. in make_polynomial 23";
 "-----SPO ---";
-val t = TermC.str2term "a * b * b \<up> (- 1) + a";
+val t = TermC.parse_test @{context} "a * b * b \<up> (- 1) + a";
 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "2 * a" then ()
 else error "poly.sml: diff.behav. in make_polynomial 25";
 "-----SPO ---";
-val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
+val t = TermC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
 then () else error "poly.sml: diff.behav. in make_polynomial 26";
 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
 "-----SPO ---";
-val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
+val t = TermC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
-val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
+val t = TermC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
 then () else error "poly.sml: diff.behav. in make_polynomial 28";
 "-------- check pbl  'polynomial simplification' -----------------------------------------------";
 "-----3 ---";
 (*default_print_depth 7;*)
 val prls = (#prls o Problem.from_store @{context}) ["polynomial", "simplification"];
 (*default_print_depth 3;*)
-val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
+val t = TermC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
 val SOME (t',_) = rewrite_set_ thy false prls t;
 if t' = @{term True} then ()
 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
 (*... if this works, but -- 1-- does still NOT work, check types:*)
 ============ inhibit exn WN120316 ==============================================*)
 "-------- ord_make_polynomial ------------------------------------------------------------------";
 "-------- ord_make_polynomial ------------------------------------------------------------------";
 "-------- ord_make_polynomial ------------------------------------------------------------------";
-val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
+val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
-val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
+val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
 if ord_make_polynomial true @{theory} [] (t1, t2) then ()
 else error "poly.sml: diff.behav. in ord_make_polynomial";
 (*SO: WHY IS THERE NO REWRITING ...*)
-val term = TermC.str2term "2*b + (3*a + 3*b)";
+val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)";
 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
 (*
 WHY IS THERE NO REWRITING ?!?
 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
 while order_add_mult uses isac's rewriter -- and this is used rarely!

changeset 60565	f92963a33fe3
parent 60559	aba19e46dd84
child 60571	19a172de0bb5