1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -30,16 +30,16 @@
1.4 "-------- fun is_polyexp -----------------------------------------------------------------------";
1.5 "-------- fun is_polyexp -----------------------------------------------------------------------";
1.6 "-------- fun is_polyexp -----------------------------------------------------------------------";
1.7 -val t = TermC.str2term "x / x";
1.8 +val t = TermC.parse_test @{context} "x / x";
1.9 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
1.10
1.11 -val t = TermC.str2term "- 1 * A * 3";
1.12 +val t = TermC.parse_test @{context} "- 1 * A * 3";
1.13 if is_polyexp t then () else error "is_polyexp (- 1 * A * 3)";
1.14
1.15 -val t = TermC.str2term "- 1 * AA * 3";
1.16 +val t = TermC.parse_test @{context} "- 1 * AA * 3";
1.17 if is_polyexp t then () else error "is_polyexp (- 1 * AA * 3)";
1.18
1.19 -val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
1.20 +val t = TermC.parse_test @{context} "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
1.21 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
1.22
1.23 "-------- fun has_degree_in --------------------------------------------------------------------";
1.24 @@ -264,7 +264,7 @@
1.25 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.26 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.27 val ctxt = Proof_Context.init_global @{theory}
1.28 -val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.29 +val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.30 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.31 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.32 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1.33 @@ -280,9 +280,9 @@
1.34 ####### calc. to: False (*isa*)
1.35 True (*isa2*)
1.36 ( **)
1.37 - if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
1.38 + if is_addUnordered (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
1.39 else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
1.40 -"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
1.41 +"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
1.42 ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
1.43
1.44 (*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.45 @@ -412,32 +412,32 @@
1.46 "-------- check make_polynomial with simple terms ----------------------------------------------";
1.47 "-------- check make_polynomial with simple terms ----------------------------------------------";
1.48 "----- check 1 ---";
1.49 -val t = TermC.str2term "2*3*a";
1.50 +val t = TermC.parse_test @{context} "2*3*a";
1.51 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.52 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
1.53
1.54 "----- check 2 ---";
1.55 -val t = TermC.str2term "2*a + 3*a";
1.56 +val t = TermC.parse_test @{context} "2*a + 3*a";
1.57 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.58 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
1.59
1.60 "----- check 3 ---";
1.61 -val t = TermC.str2term "2*a + 3*a + 3*a";
1.62 +val t = TermC.parse_test @{context} "2*a + 3*a + 3*a";
1.63 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.64 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
1.65
1.66 "----- check 4 ---";
1.67 -val t = TermC.str2term "3*a - 2*a";
1.68 +val t = TermC.parse_test @{context} "3*a - 2*a";
1.69 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.70 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
1.71
1.72 "----- check 5 ---";
1.73 -val t = TermC.str2term "4*(3*a - 2*a)";
1.74 +val t = TermC.parse_test @{context} "4*(3*a - 2*a)";
1.75 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.76 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
1.77
1.78 "----- check 6 ---";
1.79 -val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
1.80 +val t = TermC.parse_test @{context} "4*(3*a \<up> 2 - 2*a \<up> 2)";
1.81 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
1.82 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
1.83
1.84 @@ -446,7 +446,7 @@
1.85 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.86 val thy = @{theory "Isac_Knowledge"};
1.87 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
1.88 -val t = TermC.str2term "x \<up> 2 * x";
1.89 +val t = TermC.parse_test @{context} "x \<up> 2 * x";
1.90 val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
1.91 if UnparseC.term t' = "x * x \<up> 2" then ()
1.92 else error "poly.sml Poly.is_multUnordered doesn't work";
1.93 @@ -458,7 +458,7 @@
1.94 ####### try calc: Poly.is_multUnordered'
1.95 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
1.96 *)
1.97 -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.98 +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))";
1.99
1.100 "----- is_multUnordered ---";
1.101 val tsort = sort_variables t;
1.102 @@ -469,7 +469,7 @@
1.103 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
1.104
1.105 "----- eval_is_multUnordered ---";
1.106 -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.107 +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";
1.108 case eval_is_multUnordered "testid" "" tm @{context} of
1.109 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
1.110 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
1.111 @@ -486,7 +486,7 @@
1.112 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.113 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.114 val thy = @{theory "Isac_Knowledge"};
1.115 -val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
1.116 +val t as (_ $ arg) = TermC.parse_test @{context} "(3 * a + - 2 * a) is_multUnordered";
1.117
1.118 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
1.119 (*+*) andalso not (is_multUnordered arg)
1.120 @@ -501,7 +501,7 @@
1.121 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.122
1.123 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
1.124 -val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
1.125 +val t as (_ $ arg) = TermC.parse_test @{context} "(- 2 * a) is_multUnordered";
1.126
1.127 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
1.128 (*+*) andalso not (is_multUnordered arg)
1.129 @@ -515,7 +515,7 @@
1.130 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.131
1.132 "----- is_multUnordered --- (a) is_multUnordered = False";
1.133 -val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
1.134 +val t as (_ $ arg) = TermC.parse_test @{context} "(a) is_multUnordered";
1.135
1.136 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
1.137 (*+*) andalso not (is_multUnordered arg)
1.138 @@ -529,7 +529,7 @@
1.139 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
1.140
1.141 "----- is_multUnordered --- (- 2) is_multUnordered = False";
1.142 -val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
1.143 +val t as (_ $ arg) = TermC.parse_test @{context} "(- 2) is_multUnordered";
1.144
1.145 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
1.146 (*+*) andalso not (is_multUnordered arg)
1.147 @@ -567,7 +567,7 @@
1.148 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.149 -------------------------------------------------------------------------------------------------<>
1.150 *)
1.151 -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.152 +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";
1.153 (*
1.154 "~~~~~ fun is_multUnordered
1.155 "~~~~~~~ fun sort_variables
1.156 @@ -636,7 +636,7 @@
1.157 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.158 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.159 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.160 -val t = TermC.str2term "b * a * a";
1.161 +val t = TermC.parse_test @{context} "b * a * a";
1.162 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.163 if UnparseC.term t = "a \<up> 2 * b" then ()
1.164 else error "poly.sml: diff.behav. in make_polynomial 21";
1.165 @@ -659,7 +659,7 @@
1.166 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.167 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.168 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.169 -val t = TermC.str2term "2*3*a";
1.170 +val t = TermC.parse_test @{context} "2*3*a";
1.171 val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
1.172 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
1.173 (*
1.174 @@ -673,7 +673,7 @@
1.175 ####### calc. to: True (*isa*)
1.176 False (*isa2*)
1.177 *)
1.178 -val t = TermC.str2term "(6 * a) is_multUnordered";
1.179 +val t = TermC.parse_test @{context} "(6 * a) is_multUnordered";
1.180 val SOME
1.181 (_, t') =
1.182 eval_is_multUnordered "xxx" () t @{context};
1.183 @@ -702,7 +702,7 @@
1.184 val ctxt = Proof_Context.init_global thy;
1.185
1.186 val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
1.187 -(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.188 +(TermC.parse_test @{context} "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.189 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
1.190 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
1.191 else error "norm_Poly changed behavior";
1.192 @@ -720,7 +720,7 @@
1.193 ### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
1.194 *)
1.195 "~~~~~ fun sort_monoms , args:"; val (t) =
1.196 - (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
1.197 + (TermC.parse_test @{context} "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
1.198 (*+*)val t' =
1.199 sort_monoms t;
1.200 (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
1.201 @@ -729,37 +729,37 @@
1.202 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.203 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.204 "-------- complex examples from textbook Schalk I ----------------------------------------------";
1.205 -val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.206 +val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
1.207 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.208 if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
1.209 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.210
1.211 "-----SPB Schalk I p.64 No.296a ---";
1.212 -val t = TermC.str2term "(x - a) \<up> 3";
1.213 +val t = TermC.parse_test @{context} "(x - a) \<up> 3";
1.214 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.215 if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1.216 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.217
1.218 "-----SPB Schalk I p.64 No.296c ---";
1.219 -val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1.220 +val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
1.221 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.222 if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1.223 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.224
1.225 "-----SPB Schalk I p.62 No.242c ---";
1.226 -val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.227 +val t = TermC.parse_test @{context} "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
1.228 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.229 if (UnparseC.term t) = "1"
1.230 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.231
1.232 "-----SPB Schalk I p.60 No.209a ---";
1.233 -val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
1.234 +val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
1.235 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.236 if UnparseC.term t = "a \<up> 7"
1.237 then () else error "poly.sml: diff.behav. in make_polynomial 13";
1.238
1.239 "-----SPB Schalk I p.60 No.209d ---";
1.240 -val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.241 +val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.242 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.243 if UnparseC.term t = "d \<up> 3"
1.244 then () else error "poly.sml: diff.behav. in make_polynomial 14";
1.245 @@ -769,23 +769,23 @@
1.246 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.247 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.248 "-----SPO ---";
1.249 -val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.250 +val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
1.251 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.252 if UnparseC.term t = "1" then ()
1.253 else error "poly.sml: diff.behav. in make_polynomial 15";
1.254
1.255 "-----SPO ---";
1.256 -val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
1.257 +val t = TermC.parse_test @{context} "a \<up> 2*b*b \<up> (- 1)";
1.258 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.259 if UnparseC.term t = "a \<up> 2" then ()
1.260 else error "poly.sml: diff.behav. in make_polynomial 18";
1.261 "-----SPO ---";
1.262 -val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
1.263 +val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
1.264 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.265 if (UnparseC.term t) = "1" then ()
1.266 else error "poly.sml: diff.behav. in make_polynomial 19";
1.267 "-----SPO ---";
1.268 -val t = TermC.str2term "b + a - b";
1.269 +val t = TermC.parse_test @{context} "b + a - b";
1.270 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
1.271 if (UnparseC.term t) = "a" then ()
1.272 else error "poly.sml: diff.behav. in make_polynomial 20";