1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Apr 19 11:45:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Apr 19 15:02:00 2021 +0200
1.3 @@ -32,32 +32,32 @@
1.4 "----------- fun eval_ist_monom ----------------------------------";
1.5 "----------- fun eval_ist_monom ----------------------------------";
1.6 "----------- fun eval_ist_monom ----------------------------------";
1.7 -ist_monom (str2term "12");
1.8 -case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of
1.9 +ist_monom (TermC.str2term "12");
1.10 +case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
1.11 SOME ("12 ist_monom = True", _) => ()
1.12 | _ => error "polyminus.sml: 12 ist_monom = True";
1.13
1.14 -case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of
1.15 +case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of
1.16 SOME ("a ist_monom = True", _) => ()
1.17 | _ => error "polyminus.sml: a ist_monom = True";
1.18
1.19 -case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of
1.20 +case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of
1.21 SOME ("3 * a ist_monom = True", _) => ()
1.22 | _ => error "polyminus.sml: 3 * a ist_monom = True";
1.23
1.24 -case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of
1.25 +case eval_ist_monom 0 0 (TermC.str2term "(a^^^2) ist_monom") 0 of
1.26 SOME ("a ^^^ 2 ist_monom = True", _) => ()
1.27 | _ => error "polyminus.sml: a^^^2 ist_monom = True";
1.28
1.29 -case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of
1.30 +case eval_ist_monom 0 0 (TermC.str2term "(3*a^^^2) ist_monom") 0 of
1.31 SOME ("3 * a ^^^ 2 ist_monom = True", _) => ()
1.32 | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True";
1.33
1.34 -case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of
1.35 +case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
1.36 SOME ("a * b ist_monom = True", _) => ()
1.37 | _ => error "polyminus.sml: a*b ist_monom = True";
1.38
1.39 -case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of
1.40 +case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of
1.41 SOME ("3 * a * b ist_monom = True", _) => ()
1.42 | _ => error "polyminus.sml: 3*a*b ist_monom = True";
1.43
1.44 @@ -68,7 +68,7 @@
1.45 "----- with these simple variables it works...";
1.46 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.47 Rewrite.trace_on:=false;
1.48 -val t = str2term "((a + d) + c) + b";
1.49 +val t = TermC.str2term "((a + d) + c) + b";
1.50 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.51 if UnparseC.term t = "a + (b + (c + d))" then ()
1.52 else error "polyminus.sml 1 watch order_add_mult";
1.53 @@ -76,7 +76,7 @@
1.54
1.55 "----- the same stepwise...";
1.56 val od = ord_make_polynomial true (@{theory "Poly"});
1.57 -val t = str2term "((a + d) + c) + b";
1.58 +val t = TermC.str2term "((a + d) + c) + b";
1.59 "((a + d) + c) + b";
1.60 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
1.61 "b + ((a + d) + c)";
1.62 @@ -90,7 +90,7 @@
1.63 else error "polyminus.sml 2 watch order_add_mult";
1.64
1.65 "----- if parentheses are right, left_commute is (almost) sufficient...";
1.66 -val t = str2term "a + (d + (c + b))";
1.67 +val t = TermC.str2term "a + (d + (c + b))";
1.68 "a + (d + (c + b))";
1.69 val SOME (t,_) = rewrite_ thy od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
1.70 "a + (c + (d + b))";
1.71 @@ -101,14 +101,14 @@
1.72
1.73 "----- but we do not want the parentheses at right; thus: cond.rew.";
1.74 "WN0712707 complicated monomials do not yet work ...";
1.75 -val t = str2term "((5*a + 4*d) + 3*c) + 2*b";
1.76 +val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
1.77 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.78 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
1.79 else error "polyminus.sml: order_add_mult changed";
1.80
1.81 "----- here we see rew_sub going into subterm with ord.rew....";
1.82 val od = ord_make_polynomial false (@{theory "Poly"});
1.83 -val t = str2term "b + a + c + d";
1.84 +val t = TermC.str2term "b + a + c + d";
1.85 val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.86 val SOME (t,_) = rewrite_ thy od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
1.87 (*@@@ rew_sub gosub: t = d + (b + a + c)
1.88 @@ -124,34 +124,34 @@
1.89 "12" < "3"; (*true !!!*)
1.90
1.91 " a kleiner b ==> (b + a) = (a + b)";
1.92 -str2term "aaa";
1.93 -str2term "222 * aaa";
1.94 +TermC.str2term "aaa";
1.95 +TermC.str2term "222 * aaa";
1.96
1.97 -case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of
1.98 +case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
1.99 SOME ("123 kleiner 32 = False", _) => ()
1.100 | _ => error "polyminus.sml: 12 kleiner 9 = False";
1.101
1.102 -case eval_kleiner 0 0 (str2term "a kleiner b") 0 of
1.103 +case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
1.104 SOME ("a kleiner b = True", _) => ()
1.105 | _ => error "polyminus.sml: a kleiner b = True";
1.106
1.107 -case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of
1.108 +case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
1.109 SOME ("10 * g kleiner f = False", _) => ()
1.110 | _ => error "polyminus.sml: 10 * g kleiner f = False";
1.111
1.112 -case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of
1.113 +case eval_kleiner 0 0 (TermC.str2term "(a^^^2) kleiner b") 0 of
1.114 SOME ("a ^^^ 2 kleiner b = True", _) => ()
1.115 | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True";
1.116
1.117 -case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of
1.118 +case eval_kleiner 0 0 (TermC.str2term "(3*a^^^2) kleiner b") 0 of
1.119 SOME ("3 * a ^^^ 2 kleiner b = True", _) => ()
1.120 | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";
1.121
1.122 -case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of
1.123 +case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
1.124 SOME ("a * b kleiner c = True", _) => ()
1.125 | _ => error "polyminus.sml: a * b kleiner b = True";
1.126
1.127 -case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of
1.128 +case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
1.129 SOME ("3 * a * b kleiner c = True", _) => ()
1.130 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
1.131
1.132 @@ -159,52 +159,52 @@
1.133 val od = dummy_ord;
1.134
1.135 val erls = erls_ordne_alphabetisch;
1.136 -val t = str2term "b + a";
1.137 +val t = TermC.str2term "b + a";
1.138 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.139 if UnparseC.term t = "a + b" then ()
1.140 else error "polyminus.sml: ordne_alphabetisch1 b + a";
1.141
1.142 val erls = Atools_erls;
1.143 -val t = str2term "2*a + 3*a";
1.144 +val t = TermC.str2term "2*a + 3*a";
1.145 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
1.146
1.147 "======= test rewrite_, rewrite_set_";
1.148 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.149 val erls = erls_ordne_alphabetisch;
1.150 -val t = str2term "b + a";
1.151 +val t = TermC.str2term "b + a";
1.152 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.153 if UnparseC.term t = "a + b" then ()
1.154 else error "polyminus.sml: ordne_alphabetisch a + b";
1.155
1.156 -val t = str2term "2*b + a";
1.157 +val t = TermC.str2term "2*b + a";
1.158 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.159 if UnparseC.term t = "a + 2 * b" then ()
1.160 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
1.161
1.162 -val t = str2term "a + c + b";
1.163 +val t = TermC.str2term "a + c + b";
1.164 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.165 if UnparseC.term t = "a + b + c" then ()
1.166 else error "polyminus.sml: ordne_alphabetisch a + b + c";
1.167
1.168 "======= rewrite goes into subterms";
1.169 -val t = str2term "a + c + b + d";
1.170 +val t = TermC.str2term "a + c + b + d";
1.171 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
1.172 if UnparseC.term t = "a + b + c + d" then ()
1.173 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
1.174
1.175 -val t = str2term "a + c + d + b";
1.176 +val t = TermC.str2term "a + c + d + b";
1.177 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.178 if UnparseC.term t = "a + b + c + d" then ()
1.179 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
1.180
1.181 "======= here we see rew_sub going into subterm with cond.rew....";
1.182 -val t = str2term "b + a + c + d";
1.183 +val t = TermC.str2term "b + a + c + d";
1.184 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; UnparseC.term t;
1.185 if UnparseC.term t = "a + b + c + d" then ()
1.186 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
1.187
1.188 "======= compile rls for the most complicated terms";
1.189 -val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.190 +val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
1.191 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
1.192 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t;
1.193 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
1.194 @@ -214,7 +214,7 @@
1.195 "----------- build fasse_zusammen --------------------------------";
1.196 "----------- build fasse_zusammen --------------------------------";
1.197 "----------- build fasse_zusammen --------------------------------";
1.198 -val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.199 +val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
1.200 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;
1.201 if UnparseC.term t = "3 + -2 * e + 2 * f + 2 * g" then ()
1.202 else error "polyminus.sml: fasse_zusammen finished";
1.203 @@ -222,7 +222,7 @@
1.204 "----------- build verschoenere ----------------------------------";
1.205 "----------- build verschoenere ----------------------------------";
1.206 "----------- build verschoenere ----------------------------------";
1.207 -val t = str2term "3 + -2 * e + 2 * f + 2 * g";
1.208 +val t = TermC.str2term "3 + -2 * e + 2 * f + 2 * g";
1.209 val SOME (t,_) = rewrite_set_ thy false verschoenere t;
1.210 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.211 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
1.212 @@ -238,8 +238,8 @@
1.213 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
1.214 \ (Try (Rewrite_Set fasse_zusammen False)) #> \
1.215 \ (Try (Rewrite_Set verschoenere False))) t_t)"
1.216 -val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1.217 -atomty sc;
1.218 +val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
1.219 +TermC.atomty sc;
1.220
1.221 "----------- me simplification.for_polynomials.with_minus";
1.222 "----------- me simplification.for_polynomials.with_minus";
1.223 @@ -345,8 +345,8 @@
1.224 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
1.225 \ (Try (Repeat (Calculate ''PLUS''))) #> \
1.226 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
1.227 -val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
1.228 -atomty sc;
1.229 +val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
1.230 +TermC.atomty sc;
1.231
1.232 "----------- pbl polynom probe -----------------------------------";
1.233 "----------- pbl polynom probe -----------------------------------";
1.234 @@ -422,16 +422,16 @@
1.235 "----- 2 ^^^";
1.236 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.237 val erls = erls_ordne_alphabetisch;
1.238 -val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.239 +val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.240 val SOME (t',_) =
1.241 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
1.242 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
1.243
1.244 -val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.245 +val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.246 val NONE =
1.247 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
1.248
1.249 -val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.250 +val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.251 val SOME (t',_) =
1.252 rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
1.253 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.254 @@ -493,7 +493,7 @@
1.255 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.256 "----------- pbl binom polynom vereinfachen p.39 -----------------";
1.257 val rls = klammern_ausmultiplizieren;
1.258 -val t = str2term "(3 * a + 2) * (4 * a - 1)";
1.259 +val t = TermC.str2term "(3 * a + 2) * (4 * a - 1)";
1.260 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.261 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
1.262 val rls = discard_parentheses;
1.263 @@ -503,7 +503,7 @@
1.264 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.265 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
1.266 (*
1.267 -val t = str2term "3 * a * 4 * a";
1.268 +val t = TermC.str2term "3 * a * 4 * a";
1.269 val rls = ordne_monome;
1.270 val SOME (t,_) = rewrite_set_ thy false rls t; UnparseC.term t;
1.271 *)
1.272 @@ -552,12 +552,12 @@
1.273 "----------- Refine.refine Vereinfache ----------------------------------";
1.274 val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
1.275 (*default_print_depth 11;*)
1.276 -val matches = Refine.refine fmz ["vereinfachen"];
1.277 +val TermC.matches = Refine.refine fmz ["vereinfachen"];
1.278 (*default_print_depth 3;*)
1.279
1.280 "----- go into details, if it seems not to work -----";
1.281 "--- does the predicate evaluate correctly ?";
1.282 -val t = str2term
1.283 +val t = TermC.str2term
1.284 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
1.285 val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy;
1.286 case ma of
1.287 @@ -582,7 +582,7 @@
1.288 Rewrite.trace_on := false;
1.289
1.290 "--- does the respective prls rewrite the whole predicate ?";
1.291 -val t = str2term
1.292 +val t = TermC.str2term
1.293 "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
1.294 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
1.295 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
1.296 @@ -597,8 +597,8 @@
1.297 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
1.298 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
1.299 (*see test/../termC.sml for details*)
1.300 -val t = parse_patt thy "t_t is_polyexp";
1.301 -val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^
1.302 +val t = TermC.parse_patt thy "t_t is_polyexp";
1.303 +val t = TermC.parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^
1.304 " matchsub (?a + (?b - ?c)) t_t | " ^
1.305 " matchsub (?a - (?b + ?c)) t_t | " ^
1.306 " matchsub (?a + (?b - ?c)) t_t )");