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

equal deleted inserted replaced

-:90ea835c07b3
+:f92963a33fe3
 "-------- fun is_polyexp -----------------------------------------------------------------------";
 "-------- fun is_polyexp -----------------------------------------------------------------------";
 "-------- fun is_polyexp -----------------------------------------------------------------------";
-val t = TermC.str2term "x / x";
+val t = TermC.parse_test @{context} "x / x";
 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
-val t = TermC.str2term "- 1 * A * 3";
+val t = TermC.parse_test @{context} "- 1 * A * 3";
 if is_polyexp t then () else error "is_polyexp (- 1 * A * 3)";
-val t = TermC.str2term "- 1 * AA * 3";
+val t = TermC.parse_test @{context} "- 1 * AA * 3";
 if is_polyexp t then () else error "is_polyexp (- 1 * AA * 3)";
-val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
+val t = TermC.parse_test @{context} "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
 "-------- fun has_degree_in --------------------------------------------------------------------";
 "-------- fun has_degree_in --------------------------------------------------------------------";
 "-------- fun has_degree_in --------------------------------------------------------------------";
 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 val ctxt = Proof_Context.init_global @{theory}
-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_ ctxt false make_polynomial t; UnparseC.term t;
 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
 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";
 ########  eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False"  (*isa*)
 True"   (*isa2*)
 #######  calc. to: False  (*isa*)
 True   (*isa2*)
 ( **)
-if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
+if is_addUnordered (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
 else error"is_addUnordered  x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
-"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
+"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
 ((is_polyexp t) andalso not (t = sort_monoms t)) = false;  (*isa == isa2*)
 (*+*) if is_polyexp t = true then () else error "is_polyexp  x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
 (*+*) if                           t = sort_monoms t = false then () else error "sort_monoms 123";
 "-------- check make_polynomial with simple terms ----------------------------------------------";
 "-------- check make_polynomial with simple terms ----------------------------------------------";
 "-------- check make_polynomial with simple terms ----------------------------------------------";
 "----- check 1 ---";
-val t = TermC.str2term "2*3*a";
+val t = TermC.parse_test @{context} "2*3*a";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
 "----- check 2 ---";
-val t = TermC.str2term "2*a + 3*a";
+val t = TermC.parse_test @{context} "2*a + 3*a";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
 "----- check 3 ---";
-val t = TermC.str2term "2*a + 3*a + 3*a";
+val t = TermC.parse_test @{context} "2*a + 3*a + 3*a";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
 "----- check 4 ---";
-val t = TermC.str2term "3*a - 2*a";
+val t = TermC.parse_test @{context} "3*a - 2*a";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
 "----- check 5 ---";
-val t = TermC.str2term "4*(3*a - 2*a)";
+val t = TermC.parse_test @{context} "4*(3*a - 2*a)";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
 "----- check 6 ---";
-val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
+val t = TermC.parse_test @{context} "4*(3*a \<up> 2 - 2*a \<up> 2)";
 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 val thy = @{theory "Isac_Knowledge"};
 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
-val t = TermC.str2term "x \<up> 2 * x";
+val t = TermC.parse_test @{context} "x \<up> 2 * x";
 val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
 if UnparseC.term t' = "x * x \<up> 2" then ()
 else error "poly.sml Poly.is_multUnordered doesn't work";
 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
 (-48 * x \<up> 4 + 8))
 ######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
 #######  try calc: Poly.is_multUnordered'
 =======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
 *)
-val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))";
+val t = TermC.parse_test @{context} "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))";
 "----- is_multUnordered ---";
 val tsort = sort_variables t;
 UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n- 1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n- 1 * (- 1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";
 is_polyexp t;
 tsort = t;
 is_polyexp t andalso not (t = sort_variables t);
 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
 "----- eval_is_multUnordered ---";
-val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";
+val tm = TermC.parse_test @{context} "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";
 case eval_is_multUnordered "testid" "" tm @{context} of
 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
 Const (\<^const_name>\<open>True\<close>, _))) => ()
 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 val thy = @{theory "Isac_Knowledge"};
-val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
+val t as (_ $ arg) = TermC.parse_test @{context} "(3 * a + - 2 * a) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";
 Const (\<^const_name>\<open>False\<close>, _))) => ()
 (*      Const (\<^const_name>\<open>True\<close>, _))) => ()   <<<<<--------------------------- this is false*)
 | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
-val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
+val t as (_ $ arg) = TermC.parse_test @{context} "(- 2 * a) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  - 2 * a   CHANGED";
 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
 Const (\<^const_name>\<open>False\<close>, _))) => ()
 | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "----- is_multUnordered --- (a) is_multUnordered = False";
-val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
+val t as (_ $ arg) = TermC.parse_test @{context} "(a) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   a   CHANGED";
 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
 Const (\<^const_name>\<open>False\<close>, _))) => ()
 | _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "----- is_multUnordered --- (- 2) is_multUnordered = False";
-val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
+val t as (_ $ arg) = TermC.parse_test @{context} "(- 2) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   - 2   CHANGED";
 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2))  +  3 * (a \<up> 2 * (x * (- 1) \<up> 2))  +  a \<up> 3 * (- 1) \<up> 3
 --------+--------------------------+---------------------------------+---------------------------<>
 O:x \<up> 3 + - 1  * (3 * (a * x \<up> 2))  +  - 1 \<up> 2 * (3 * (a \<up> 2 * x))     +  - 1 \<up> 3 * a \<up> 3
 -------------------------------------------------------------------------------------------------<>
 *)
-val t = TermC.str2term "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3";
+val t = TermC.parse_test @{context} "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3";
 (*
 "~~~~~ fun is_multUnordered
 "~~~~~~~ fun sort_variables
 "~~~~~~~~~ val sort_varList
 *)
 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
-val t = TermC.str2term "b * a * a";
+val t = TermC.parse_test @{context} "b * a * a";
 val SOME (t,_) = rewrite_set_ ctxt 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";
 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
-val t = TermC.str2term "2*3*a";
+val t = TermC.parse_test @{context} "2*3*a";
 val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
 (*
 ##  try calc: "Groups.times_class.times"
 ##  rls: order_mult_rls_ on: 6 * a
 ########  eval asms: "6 * a is_multUnordered = True"    (*isa*)
 = False"   (*isa2*)
 #######  calc. to: True  (*isa*)
 False (*isa2*)
 *)
-val t = TermC.str2term "(6 * a) is_multUnordered";
+val t = TermC.parse_test @{context} "(6 * a) is_multUnordered";
 val SOME
 (_, t') =
 eval_is_multUnordered "xxx" () t @{context};
 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
 (*+*)else error "6 * a is_multUnordered = False CHANGED";
 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
 val thy = @{theory AlgEin};
 val ctxt = Proof_Context.init_global thy;
 val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
-(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
+(TermC.parse_test @{context} "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
 else error "norm_Poly changed behavior";
 (* isa:
 ##  rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
 #######  try calc: "Poly.is_addUnordered"
 #######  try calc: "Poly.is_addUnordered"
 ###  rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
 *)
 "~~~~~ fun sort_monoms , args:"; val (t) =
-(TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
+(TermC.parse_test @{context} "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
 (*+*)val t' =
 sort_monoms t;
 (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 "-------- complex examples from textbook Schalk I ----------------------------------------------";
-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_ ctxt 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_ ctxt false make_polynomial t; UnparseC.term t;
 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_ ctxt 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_ ctxt 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_ ctxt 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_ ctxt 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";
 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 "-----SPO ---";
-val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
+val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "1" then ()
 else error "poly.sml: diff.behav. in make_polynomial 15";
 "-----SPO ---";
-val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
+val t = TermC.parse_test @{context} "a \<up> 2*b*b \<up> (- 1)";
 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 if UnparseC.term t = "a \<up> 2" then ()
 else error "poly.sml: diff.behav. in make_polynomial 18";
 "-----SPO ---";
-val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
+val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 if (UnparseC.term t) = "1" then ()
 else error "poly.sml: diff.behav. in make_polynomial 19";
 "-----SPO ---";
-val t = TermC.str2term "b + a - b";
+val t = TermC.parse_test @{context} "b + a - b";
 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 if (UnparseC.term t) = "a" then ()
 else error "poly.sml: diff.behav. in make_polynomial 20";
 "-----SPO ---";

changeset 60565	f92963a33fe3
parent 60509	2e0b7ca391dc
child 60660	c4b24621077e