1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Sat Jul 17 14:05:28 2021 +0200
1.3 @@ -33,11 +33,11 @@
1.4 val t = TermC.str2term "x / x";
1.5 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
1.6
1.7 -val t = TermC.str2term "-1 * A * 3";
1.8 -if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
1.9 +val t = TermC.str2term "- 1 * A * 3";
1.10 +if is_polyexp t then () else error "is_polyexp (- 1 * A * 3)";
1.11
1.12 -val t = TermC.str2term "-1 * AA * 3";
1.13 -if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
1.14 +val t = TermC.str2term "- 1 * AA * 3";
1.15 +if is_polyexp t then () else error "is_polyexp (- 1 * AA * 3)";
1.16
1.17 val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
1.18 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
1.19 @@ -449,24 +449,24 @@
1.20 else error "poly.sml Poly.is_multUnordered doesn't work";
1.21
1.22 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
1.23 -### 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) +
1.24 +### 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) +
1.25 (-48 * x \<up> 4 + 8))
1.26 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
1.27 ####### try calc: Poly.is_multUnordered'
1.28 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
1.29 *)
1.30 -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))";
1.31 +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))";
1.32
1.33 "----- is_multUnordered ---";
1.34 val tsort = sort_variables t;
1.35 -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";
1.36 +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";
1.37 is_polyexp t;
1.38 tsort = t;
1.39 is_polyexp t andalso not (t = sort_variables t);
1.40 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
1.41
1.42 "----- eval_is_multUnordered ---";
1.43 -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";
1.44 +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";
1.45 case eval_is_multUnordered "testid" "" tm thy of
1.46 SOME (_, Const ("HOL.Trueprop", _) $
1.47 (Const ("HOL.eq", _) $
1.48 @@ -495,7 +495,7 @@
1.49 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.50 Const ("HOL.False", _))) => ()
1.51 (* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
1.52 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.53 +| _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.54
1.55 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
1.56 val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
1.57 @@ -509,7 +509,7 @@
1.58 ("xxx - 2 * a_",
1.59 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.60 Const ("HOL.False", _))) => ()
1.61 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.62 +| _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.63
1.64 "----- is_multUnordered --- (a) is_multUnordered = False";
1.65 val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
1.66 @@ -523,7 +523,7 @@
1.67 ("xxx a_",
1.68 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.69 Const ("HOL.False", _))) => ()
1.70 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.71 +| _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.72
1.73 "----- is_multUnordered --- (- 2) is_multUnordered = False";
1.74 val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
1.75 @@ -537,7 +537,7 @@
1.76 ("xxx - 2_",
1.77 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.78 Const ("HOL.False", _))) => ()
1.79 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.80 +| _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.81
1.82
1.83 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.84 @@ -554,14 +554,14 @@
1.85 ######## eval asms:
1.86 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"
1.87 -------------------------------------------------------------------------------------------------==
1.88 -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"
1.89 +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"
1.90 ####### calc. to: True
1.91 ####### try calc: "Poly.is_multUnordered"
1.92 ####### try calc: "Poly.is_multUnordered"
1.93 ### rls: order_mult_ on:
1.94 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3
1.95 --------+--------------------------+---------------------------------+---------------------------<>
1.96 -O:x \<up> 3 + -1 * (3 * (a * x \<up> 2)) + -1 \<up> 2 * (3 * (a \<up> 2 * x)) + -1 \<up> 3 * a \<up> 3
1.97 +O:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + - 1 \<up> 2 * (3 * (a \<up> 2 * x)) + - 1 \<up> 3 * a \<up> 3
1.98 -------------------------------------------------------------------------------------------------<>
1.99 *)
1.100 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";
1.101 @@ -725,25 +725,25 @@
1.102 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.103 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.104 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.105 -val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
1.106 +val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.107 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.108 -if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"
1.109 +if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
1.110 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.111
1.112 "-----SPB Schalk I p.64 No.296a ---";
1.113 val t = TermC.str2term "(x - a) \<up> 3";
1.114 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.115 -if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"
1.116 +if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1.117 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.118
1.119 "-----SPB Schalk I p.64 No.296c ---";
1.120 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1.121 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.122 -if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
1.123 +if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1.124 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.125
1.126 "-----SPB Schalk I p.62 No.242c ---";
1.127 -val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
1.128 +val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.129 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.130 if (UnparseC.term t) = "1"
1.131 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.132 @@ -765,18 +765,18 @@
1.133 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.134 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.135 "-----SPO ---";
1.136 -val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1.137 +val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.138 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.139 if UnparseC.term t = "1" then ()
1.140 else error "poly.sml: diff.behav. in make_polynomial 15";
1.141
1.142 "-----SPO ---";
1.143 -val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
1.144 +val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
1.145 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.146 if UnparseC.term t = "a \<up> 2" then ()
1.147 else error "poly.sml: diff.behav. in make_polynomial 18";
1.148 "-----SPO ---";
1.149 -val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1.150 +val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.151 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.152 if (UnparseC.term t) = "1" then ()
1.153 else error "poly.sml: diff.behav. in make_polynomial 19";