1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -36,21 +36,21 @@
1.4 "----------- fun identifier --------------------------------------------------------------------";
1.5 "----------- fun identifier --------------------------------------------------------------------";
1.6 "----------- fun identifier --------------------------------------------------------------------";
1.7 -if identifier (TermC.str2term "12 ::real") = "12" then () else error "identifier 1";
1.8 -if identifier (TermC.str2term
1.9 +if identifier (TermC.parse_test @{context} "12 ::real") = "12" then () else error "identifier 1";
1.10 +if identifier (TermC.parse_test @{context}
1.11 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
1.12 then () else error "identifier 1a";
1.13
1.14 -if identifier (TermC.str2term "a ::real") = "a" then () else error "identifier 2";
1.15 -if identifier (TermC.str2term "3 * a ::real") = "a" then () else error "identifier 3";
1.16 +if identifier (TermC.parse_test @{context} "a ::real") = "a" then () else error "identifier 2";
1.17 +if identifier (TermC.parse_test @{context} "3 * a ::real") = "a" then () else error "identifier 3";
1.18
1.19 -if identifier (TermC.str2term "a \<up> 2 ::real") = "a" then () else error "identifier 4";
1.20 -if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
1.21 -if identifier (TermC.str2term "a * b ::real") = "b" then () else error "identifier 5b";
1.22 +if identifier (TermC.parse_test @{context} "a \<up> 2 ::real") = "a" then () else error "identifier 4";
1.23 +if identifier (TermC.parse_test @{context} "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
1.24 +if identifier (TermC.parse_test @{context} "a * b ::real") = "b" then () else error "identifier 5b";
1.25
1.26 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
1.27 -if identifier (TermC.str2term "a*b ::real") = "b" then () else error "identifier 6";
1.28 -if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
1.29 +if identifier (TermC.parse_test @{context} "a*b ::real") = "b" then () else error "identifier 6";
1.30 +if identifier (TermC.parse_test @{context} "(3*a*b) ::real") = "b" then () else error "identifier 7";
1.31
1.32
1.33 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
1.34 @@ -62,33 +62,33 @@
1.35 "12" < "3"; (*true !!!*)
1.36
1.37 " a kleiner b ==> (b + a) = (a + b)";
1.38 -TermC.str2term "aaa";
1.39 -TermC.str2term "222 * aaa";
1.40 +TermC.parse_test @{context} "aaa";
1.41 +TermC.parse_test @{context} "222 * aaa";
1.42
1.43 -case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
1.44 +case eval_kleiner 0 0 (TermC.parse_test @{context} "123 kleiner 32") 0 of
1.45 SOME ("123 kleiner 32 = False", _) => ()
1.46 | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.47 -case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
1.48 +case eval_kleiner 0 0 (TermC.parse_test @{context} "a kleiner b") 0 of
1.49 SOME ("a kleiner b = True", _) => ()
1.50 | _ => error "polyminus.sml: a kleiner b = True";
1.51 -case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
1.52 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(10*g) kleiner f") 0 of
1.53 SOME ("10 * g kleiner f = False", _) => ()
1.54 | _ => error "polyminus.sml: 10 * g kleiner f = False";
1.55 -case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
1.56 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(a \<up> 2) kleiner b") 0 of
1.57 SOME ("a \<up> 2 kleiner b = True", _) => ()
1.58 | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
1.59 -case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
1.60 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) kleiner b") 0 of
1.61 SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
1.62 | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
1.63 -case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
1.64 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(a*b) kleiner c") 0 of
1.65 SOME ("a * b kleiner c = True", _) => ()
1.66 | _ => error "polyminus.sml: a * b kleiner b = True";
1.67 -case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
1.68 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a*b) kleiner c") 0 of
1.69 SOME ("3 * a * b kleiner c = True", _) => ()
1.70 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.71
1.72
1.73 -val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
1.74 +val t = TermC.parse_test @{context} "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
1.75 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
1.76 eval_kleiner "aaa" "bbb" t "ccc";
1.77 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
1.78 @@ -106,61 +106,61 @@
1.79 "----------- fun ist_monom ---------------------------------------------------------------------";
1.80 "----------- fun ist_monom ---------------------------------------------------------------------";
1.81 "----------- fun ist_monom ---------------------------------------------------------------------";
1.82 -val t = TermC.str2term "0 ::real";
1.83 +val t = TermC.parse_test @{context} "0 ::real";
1.84 if ist_monom t then () else error "ist_monom 1";
1.85
1.86 -val t = TermC.str2term "a";
1.87 +val t = TermC.parse_test @{context} "a";
1.88 if ist_monom t then () else error "ist_monom 2";
1.89
1.90 -val t = TermC.str2term "2 * a";
1.91 +val t = TermC.parse_test @{context} "2 * a";
1.92 if ist_monom t then () else error "ist_monom 3";
1.93
1.94 -val t = TermC.str2term "2 * a * b";
1.95 +val t = TermC.parse_test @{context} "2 * a * b";
1.96 if ist_monom t then () else error "ist_monom 4";
1.97
1.98 -val t = TermC.str2term "a * b";
1.99 +val t = TermC.parse_test @{context} "a * b";
1.100 if ist_monom t then () else error "ist_monom 5";
1.101
1.102 (*not covered before NEW numerals*)
1.103 -val t = TermC.str2term "2 * a \<up> 2 * b";
1.104 +val t = TermC.parse_test @{context} "2 * a \<up> 2 * b";
1.105 if ist_monom t then () else error "ist_monom 6";
1.106
1.107 (*not covered before NEW numerals*)
1.108 -val t = TermC.str2term "a \<up> 2 * b \<up> 3";
1.109 +val t = TermC.parse_test @{context} "a \<up> 2 * b \<up> 3";
1.110 if ist_monom t then () else error "ist_monom 7";
1.111
1.112 -val t = TermC.str2term "a \<up> 2 * 4 * b \<up> 3 * 5";
1.113 +val t = TermC.parse_test @{context} "a \<up> 2 * 4 * b \<up> 3 * 5";
1.114 if ist_monom t then () else error "ist_monom 8";
1.115
1.116
1.117 "----------- fun eval_ist_monom ----------------------------------";
1.118 "----------- fun eval_ist_monom ----------------------------------";
1.119 "----------- fun eval_ist_monom ----------------------------------";
1.120 -case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
1.121 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "12 ist_monom") 0 of
1.122 SOME ("12 ist_monom = True", _) => ()
1.123 | _ => error "polyminus.sml: 12 ist_monom = True";
1.124
1.125 -case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of
1.126 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "a ist_monom") 0 of
1.127 SOME ("a ist_monom = True", _) => ()
1.128 | _ => error "polyminus.sml: a ist_monom = True";
1.129
1.130 -case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of
1.131 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a) ist_monom") 0 of
1.132 SOME ("3 * a ist_monom = True", _) => ()
1.133 | _ => error "polyminus.sml: 3 * a ist_monom = True";
1.134
1.135 -case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of
1.136 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "(a \<up> 2) ist_monom") 0 of
1.137 SOME ("a \<up> 2 ist_monom = True", _) => ()
1.138 | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
1.139
1.140 -case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of
1.141 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) ist_monom") 0 of
1.142 SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
1.143 | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
1.144
1.145 -case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
1.146 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "(a*b) ist_monom") 0 of
1.147 SOME ("a * b ist_monom = True", _) => ()
1.148 | _ => error "polyminus.sml: a*b ist_monom = True";
1.149
1.150 -case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of
1.151 +case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a*b) ist_monom") 0 of
1.152 SOME ("3 * a * b ist_monom = True", _) => ()
1.153 | _ => error "polyminus.sml: 3*a*b ist_monom = True";
1.154
1.155 @@ -170,14 +170,14 @@
1.156 "----------- watch order_add_mult -------------------------------";
1.157 "----- with these simple variables it works...";
1.158 val ctxt = @{context};
1.159 -val t = TermC.str2term "((a + d) + c) + b";
1.160 +val t = TermC.parse_test @{context} "((a + d) + c) + b";
1.161 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
1.162 if UnparseC.term t = "a + (b + (c + d))" then ()
1.163 else error "polyminus.sml 1 watch order_add_mult";
1.164
1.165 "----- the same stepwise...";
1.166 val od = ord_make_polynomial true (@{theory "Poly"});
1.167 -val t = TermC.str2term "((a + d) + c) + b";
1.168 +val t = TermC.parse_test @{context} "((a + d) + c) + b";
1.169 "((a + d) + c) + b";
1.170 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.171 "b + ((a + d) + c)";
1.172 @@ -191,7 +191,7 @@
1.173 else error "polyminus.sml 2 watch order_add_mult";
1.174
1.175 "----- if parentheses are right, left_commute is (almost) sufficient...";
1.176 -val t = TermC.str2term "a + (d + (c + b))";
1.177 +val t = TermC.parse_test @{context} "a + (d + (c + b))";
1.178 "a + (d + (c + b))";
1.179 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.180 "a + (c + (d + b))";
1.181 @@ -202,14 +202,14 @@
1.182
1.183 "----- but we do not want the parentheses at right; thus: cond.rew.";
1.184 "WN0712707 complicated monomials do not yet work ...";
1.185 -val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
1.186 +val t = TermC.parse_test @{context} "((5*a + 4*d) + 3*c) + 2*b";
1.187 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
1.188 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.189 else error "polyminus.sml: order_add_mult changed";
1.190
1.191 "----- here we see rew_sub going into subterm with ord.rew....";
1.192 val od = ord_make_polynomial false (@{theory "Poly"});
1.193 -val t = TermC.str2term "b + a + c + d";
1.194 +val t = TermC.parse_test @{context} "b + a + c + d";
1.195 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.196 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.197 (*@@@ rew_sub gosub: t = d + (b + a + c)
1.198 @@ -225,34 +225,34 @@
1.199 "12" < "3"; (*true !!!*)
1.200
1.201 " a kleiner b ==> (b + a) = (a + b)";
1.202 -TermC.str2term "aaa";
1.203 -TermC.str2term "222 * aaa";
1.204 +TermC.parse_test @{context} "aaa";
1.205 +TermC.parse_test @{context} "222 * aaa";
1.206
1.207 -case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
1.208 +case eval_kleiner 0 0 (TermC.parse_test @{context} "123 kleiner 32") 0 of
1.209 SOME ("123 kleiner 32 = False", _) => ()
1.210 | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.211
1.212 -case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
1.213 +case eval_kleiner 0 0 (TermC.parse_test @{context} "a kleiner b") 0 of
1.214 SOME ("a kleiner b = True", _) => ()
1.215 | _ => error "polyminus.sml: a kleiner b = True";
1.216
1.217 -case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
1.218 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(10*g) kleiner f") 0 of
1.219 SOME ("10 * g kleiner f = False", _) => ()
1.220 | _ => error "polyminus.sml: 10 * g kleiner f = False";
1.221
1.222 -case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
1.223 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(a \<up> 2) kleiner b") 0 of
1.224 SOME ("a \<up> 2 kleiner b = True", _) => ()
1.225 | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
1.226
1.227 -case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
1.228 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) kleiner b") 0 of
1.229 SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
1.230 | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
1.231
1.232 -case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
1.233 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(a*b) kleiner c") 0 of
1.234 SOME ("a * b kleiner c = True", _) => ()
1.235 | _ => error "polyminus.sml: a * b kleiner b = True";
1.236
1.237 -case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
1.238 +case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a*b) kleiner c") 0 of
1.239 SOME ("3 * a * b kleiner c = True", _) => ()
1.240 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.241
1.242 @@ -260,52 +260,52 @@
1.243 val od = Rewrite_Ord.function_empty;
1.244
1.245 val erls = erls_ordne_alphabetisch;
1.246 -val t = TermC.str2term "b + a";
1.247 +val t = TermC.parse_test @{context} "b + a";
1.248 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
1.249 if UnparseC.term t = "a + b" then ()
1.250 else error "polyminus.sml: ordne_alphabetisch1 b + a";
1.251
1.252 val erls = Atools_erls;
1.253 -val t = TermC.str2term "2*a + 3*a";
1.254 +val t = TermC.parse_test @{context} "2*a + 3*a";
1.255 val SOME (t,_) = rewrite_ ctxt od erls false @{thm real_num_collect} t; UnparseC.term t;
1.256
1.257 "======= test rewrite_, rewrite_set_";
1.258 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.259 val erls = erls_ordne_alphabetisch;
1.260 -val t = TermC.str2term "b + a";
1.261 +val t = TermC.parse_test @{context} "b + a";
1.262 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.263 if UnparseC.term t = "a + b" then ()
1.264 else error "polyminus.sml: ordne_alphabetisch a + b";
1.265
1.266 -val t = TermC.str2term "2*b + a";
1.267 +val t = TermC.parse_test @{context} "2*b + a";
1.268 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.269 if UnparseC.term t = "a + 2 * b" then ()
1.270 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.271
1.272 -val t = TermC.str2term "a + c + b";
1.273 +val t = TermC.parse_test @{context} "a + c + b";
1.274 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.275 if UnparseC.term t = "a + b + c" then ()
1.276 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.277
1.278 "======= rewrite goes into subterms";
1.279 -val t = TermC.str2term "a + c + b + d ::real";
1.280 +val t = TermC.parse_test @{context} "a + c + b + d ::real";
1.281 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.282 if UnparseC.term t = "a + b + c + d" then ()
1.283 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.284
1.285 -val t = TermC.str2term "a + c + d + b";
1.286 +val t = TermC.parse_test @{context} "a + c + d + b";
1.287 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
1.288 if UnparseC.term t = "a + b + c + d" then ()
1.289 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.290
1.291 "======= here we see rew_sub going into subterm with cond.rew....";
1.292 -val t = TermC.str2term "b + a + c + d";
1.293 +val t = TermC.parse_test @{context} "b + a + c + d";
1.294 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
1.295 if UnparseC.term t = "a + b + c + d" then ()
1.296 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.297
1.298 "======= compile rls for the most complicated terms";
1.299 -val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.300 +val t = TermC.parse_test @{context} "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.301 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.302 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t;
1.303 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.304 @@ -316,7 +316,7 @@
1.305 "----------- build fasse_zusammen --------------------------------";
1.306 "----------- build fasse_zusammen --------------------------------";
1.307 "----------- build fasse_zusammen --------------------------------";
1.308 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.309 +val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.310 val SOME (t,_) = rewrite_set_ ctxt false fasse_zusammen t;
1.311 if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
1.312 else error "polyminus.sml: fasse_zusammen finished";
1.313 @@ -324,7 +324,7 @@
1.314 "----------- build verschoenere ----------------------------------";
1.315 "----------- build verschoenere ----------------------------------";
1.316 "----------- build verschoenere ----------------------------------";
1.317 -val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g";
1.318 +val t = TermC.parse_test @{context} "3 + - 2 * e + 2 * f + 2 * g";
1.319 val SOME (t,_) = rewrite_set_ ctxt false verschoenere t;
1.320 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.321 else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
1.322 @@ -524,16 +524,16 @@
1.323 "----- 2 \<up> ";
1.324 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.325 val erls = erls_ordne_alphabetisch;
1.326 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.327 +val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.328 val SOME (t',_) =
1.329 rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
1.330 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
1.331
1.332 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.333 +val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.334 val NONE =
1.335 rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
1.336
1.337 -val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.338 +val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.339 val SOME (t',_) =
1.340 rewrite_set_ ctxt false ordne_alphabetisch t;
1.341 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.342 @@ -598,7 +598,7 @@
1.343 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.344 val thy = @{theory};
1.345 val rls = klammern_ausmultiplizieren;
1.346 -val t = TermC.str2term "(3 * a + 2) * (4 * a - 1::real)";
1.347 +val t = TermC.parse_test @{context} "(3 * a + 2) * (4 * a - 1::real)";
1.348 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.349 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
1.350 val rls = discard_parentheses;
1.351 @@ -608,7 +608,7 @@
1.352 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.353 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
1.354 (*
1.355 -val t = TermC.str2term "3 * a * 4 * a";
1.356 +val t = TermC.parse_test @{context} "3 * a * 4 * a";
1.357 val rls = ordne_monome;
1.358 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
1.359 *)
1.360 @@ -664,7 +664,7 @@
1.361
1.362 "----- go into details, if it seems not to work -----";
1.363 "--- does the predicate evaluate correctly ?";
1.364 -val t = TermC.str2term
1.365 +val t = TermC.parse_patt_test @{theory}
1.366 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
1.367 val ma = eval_matchsub "" "Prog_Expr.matchsub" t ctxt;
1.368 case ma of
1.369 @@ -688,7 +688,7 @@
1.370 val SOME (t', _) = rewrite_set_ ctxt false prls t;
1.371
1.372 "--- does the respective prls rewrite the whole predicate ?";
1.373 -val t = TermC.str2term
1.374 +val t = TermC.parse_patt_test @{theory}
1.375 "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
1.376 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
1.377 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \