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

equal deleted inserted replaced

-:cc02d2cc2e24
+:0c10aeff57d7
 "-------- fun is_polyexp -----------------------------------------------------------------------";
 "-------- fun is_polyexp -----------------------------------------------------------------------";
 val t = TermC.str2term "x / x";
 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
-val t = TermC.str2term "-1 * A * 3";
+val t = TermC.str2term "- 1 * A * 3";
-if is_polyexp t then () else error "is_polyexp (-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.str2term "- 1 * AA * 3";
-if is_polyexp t then () else error "is_polyexp (-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";
 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
 "-------- fun has_degree_in --------------------------------------------------------------------";
 val SOME (t', _) = rewrite_set_ thy 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:
-###  rls: order_mult_ on: 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) +
+###  rls: order_mult_ on: 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))
 ######  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.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 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";
+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.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";
 case eval_is_multUnordered "testid" "" tm thy of
 SOME (_, Const ("HOL.Trueprop", _) $
 (Const ("HOL.eq", _) $
 (Const ("Poly.is_multUnordered", _) $ _) $
 Const ("HOL.True", _))) => ()
 SOME
 ("xxx 3 * a + - 2 * a_",
 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
 Const ("HOL.False", _))) => ()
 (*      Const ("HOL.True", _))) => ()   <<<<<--------------------------- this is false*)
-| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";
+| _ => 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";
 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
 case eval_is_multUnordered "xxx " "yyy " t thy of
 SOME
 ("xxx - 2 * a_",
 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
 Const ("HOL.False", _))) => ()
-| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";
+| _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "----- is_multUnordered --- (a) is_multUnordered = False";
 val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
 case eval_is_multUnordered "xxx " "yyy " t thy of
 SOME
 ("xxx a_",
 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
 Const ("HOL.False", _))) => ()
-| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";
+| _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "----- is_multUnordered --- (- 2) is_multUnordered = False";
 val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
 case eval_is_multUnordered "xxx " "yyy " t thy of
 SOME
 ("xxx - 2_",
 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
 Const ("HOL.False", _))) => ()
-| _ => error "eval_is_multUnordered  3 * a + -2 * a  CHANGED";
+| _ => error "eval_is_multUnordered  3 * a + - 2 * a  CHANGED";
 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered
 #######  try calc: "Poly.is_multUnordered"
 ########  eval asms:
 N:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered = True"
 -------------------------------------------------------------------------------------------------==
-O:x \<up> 3 + 3 * x \<up> 2 * (-1 * a)  + 3 * x * (-1    \<up> 2 * a \<up> 2) + -1    \<up> 3 * a \<up> 3 is_multUnordered = True"
+O:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a)  + 3 * x * (- 1    \<up> 2 * a \<up> 2) + - 1    \<up> 3 * a \<up> 3 is_multUnordered = True"
 #######  calc. to: True
 #######  try calc: "Poly.is_multUnordered"
 #######  try calc: "Poly.is_multUnordered"
 ###  rls: order_mult_ on:
 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
+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";
 (*
 "~~~~~ fun is_multUnordered
 "-------- 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.str2term "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"
+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 SOME (t,_) = rewrite_set_ thy 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"
+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 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"
+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.str2term "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 ---";
 "-------- 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.str2term "a \<up> 2*a \<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 15";
 "-----SPO ---";
-val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
+val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
 val SOME (t,_) = rewrite_set_ thy 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.str2term "a \<up> 2*a \<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 19";
 "-----SPO ---";
 val t = TermC.str2term "b + a - b";

changeset 60329	0c10aeff57d7
parent 60328	cc02d2cc2e24
child 60330	e5e9a6c45597