1.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Jun 01 15:41:23 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly.sml Sat Jul 03 16:21:07 2021 +0200
1.3 @@ -1,56 +1,155 @@
1.4 -(* testexamples for Poly, polynomials
1.5 +(* Knowledge/poly.sml
1.6 author: Matthias Goldgruber 2003
1.7 (c) due to copyright terms
1.8
1.9 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.10 - 10 20 30 40 50 60 70 80
1.11 LEGEND:
1.12 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
1.13 examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
1.14 *)
1.15
1.16 -"--------------------------------------------------------";
1.17 -"--------------------------------------------------------";
1.18 -"table of contents --------------------------------------";
1.19 -"--------------------------------------------------------";
1.20 -"----------- fun is_polyexp --------------------------------------------------------------------";
1.21 -"----------- fun has_degree_in -----------------------------------------------------------------";
1.22 -"----------- fun mono_deg_in -------------------------------------------------------------------";
1.23 -"----------- fun mono_deg_in -------------------------------------------------------------------";
1.24 -"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
1.25 -"-------- investigate (new 2002) uniary minus -----------";
1.26 -"----------- fun sort_variables ----------------------------------------------------------------";
1.27 -"-------- check make_polynomial with simple terms -------";
1.28 -"-------- fun is_multUnordered --------------------------";
1.29 -"-------- examples from textbook Schalk I ---------------";
1.30 -"-------- check pbl 'polynomial simplification' --------";
1.31 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.32 -"-------- interSteps for Schalk 299a --------------------";
1.33 -"-------- norm_Poly NOT COMPLETE ------------------------";
1.34 -"-------- ord_make_polynomial ---------------------------";
1.35 -"--------------------------------------------------------";
1.36 -"--------------------------------------------------------";
1.37 -"--------------------------------------------------------";
1.38 +"-----------------------------------------------------------------------------------------------";
1.39 +"-----------------------------------------------------------------------------------------------";
1.40 +"table of contents -----------------------------------------------------------------------------";
1.41 +"-----------------------------------------------------------------------------------------------";
1.42 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
1.43 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
1.44 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.45 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.46 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.47 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
1.48 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
1.49 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
1.50 +"-------- fun sort_variables -------------------------------------------------------------------";
1.51 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
1.52 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.53 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.54 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.55 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.56 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.57 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.58 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.59 +"-------- examples from textbook Schalk I ------------------------------------------------------";
1.60 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.61 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.62 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
1.63 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1.64 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
1.65 +"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1.66 +"-------- ord_make_polynomial ------------------------------------------------------------------";
1.67 +"-----------------------------------------------------------------------------------------------";
1.68 +"-----------------------------------------------------------------------------------------------";
1.69 +"-----------------------------------------------------------------------------------------------";
1.70
1.71
1.72 -"----------- fun is_polyexp --------------------------------------------------------------------";
1.73 -"----------- fun is_polyexp --------------------------------------------------------------------";
1.74 -"----------- fun is_polyexp --------------------------------------------------------------------";
1.75 -val thy = @{theory Partial_Fractions};
1.76 -val ctxt = Proof_Context.init_global thy;
1.77 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
1.78 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
1.79 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
1.80 +(* indentation indicates call hierarchy:
1.81 +"~~~~~ fun is_addUnordered
1.82 +"~~~~~~~ fun is_polyexp
1.83 +"~~~~~~~ fun sort_monoms
1.84 +"~~~~~~~~~ fun sort_monList
1.85 +"~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
1.86 +"~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
1.87 +"~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
1.88 +"~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
1.89 +"~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
1.90 +"~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
1.91 +"~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
1.92 +"~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
1.93 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
1.94 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
1.95 +"~~~~~ fun is_multUnordered
1.96 +"~~~~~~~ fun sort_variables
1.97 +"~~~~~~~~~ fun sort_varList
1.98 +"~~~~~~~~~~~ fun var_ord
1.99 +"~~~~~~~~~~~~~ fun get_basStr used twice --^^
1.100 +"~~~~~~~~~~~~~ fun get_potStr used twice --^^
1.101
1.102 -val t = (the o (parseNEW ctxt)) "x / x";
1.103 +fun int_ord (i1, i2) =
1.104 +(@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
1.105 + Int.compare (i1, i2)
1.106 +);
1.107 +fun var_ord (a, b) =
1.108 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1.109 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.110 + prod_ord string_ord string_ord
1.111 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1.112 +);
1.113 +fun var_ord_revPow (a, b: term) =
1.114 +(@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1.115 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.116 + prod_ord string_ord string_ord_rev
1.117 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1.118 +);
1.119 +fun sort_varList ts =
1.120 +(@{print} {a = "sort_varList", args = UnparseC.terms ts};
1.121 + sort var_ord ts
1.122 +);
1.123 +fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
1.124 + | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
1.125 + | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
1.126 + | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1.127 + (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
1.128 + is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
1.129 + case (cond x, cond y) of
1.130 + (false, false) =>
1.131 + (case elem_ord (x, y) of
1.132 + EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1.133 + | ord => ord)
1.134 + | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1.135 + | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1.136 + | (true, true) => dict_cond_ord elem_ord cond (xs, ys)
1.137 +);
1.138 +fun compare_koeff_ord (xs, ys) =
1.139 +(@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
1.140 + sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
1.141 + string_ord
1.142 + ((koeff2ordStr o get_koeff_of_mon) xs,
1.143 + (koeff2ordStr o get_koeff_of_mon) ys)
1.144 +);
1.145 +fun var_ord (a,b: term) =
1.146 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1.147 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.148 + prod_ord string_ord string_ord
1.149 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1.150 +);
1.151 +*)
1.152 +
1.153 +
1.154 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
1.155 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
1.156 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
1.157 +(* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
1.158 +
1.159 + sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
1.160 +@{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
1.161 +val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
1.162 +val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
1.163 +
1.164 +val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac;
1.165 +if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*))
1.166 +else error "thm - ?z = - 1 * ?z loops with new numerals";
1.167 +
1.168 +
1.169 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.170 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.171 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.172 +val t = TermC.str2term "x / x";
1.173 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
1.174
1.175 -val t = (the o (parseNEW ctxt)) "-1 * A * 3";
1.176 +val t = TermC.str2term "-1 * A * 3";
1.177 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
1.178
1.179 -val t = (the o (parseNEW ctxt)) "-1 * AA * 3";
1.180 +val t = TermC.str2term "-1 * AA * 3";
1.181 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
1.182
1.183 -"----------- fun has_degree_in -----------------------------------------------------------------";
1.184 -"----------- fun has_degree_in -----------------------------------------------------------------";
1.185 -"----------- fun has_degree_in -----------------------------------------------------------------";
1.186 +val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
1.187 +if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
1.188 +
1.189 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.190 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.191 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.192 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.193 val t = (Thm.term_of o the o (TermC.parse thy)) "1";
1.194 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
1.195 @@ -131,9 +230,9 @@
1.196 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.197 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
1.198
1.199 -"----------- fun mono_deg_in -------------------------------------------------------------------";
1.200 -"----------- fun mono_deg_in -------------------------------------------------------------------";
1.201 -"----------- fun mono_deg_in -------------------------------------------------------------------";
1.202 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.203 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.204 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.205 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.206
1.207 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
1.208 @@ -182,9 +281,9 @@
1.209 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.210 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
1.211
1.212 -"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
1.213 -"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
1.214 -"----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
1.215 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
1.216 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
1.217 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
1.218 val thy = @{theory Partial_Fractions}
1.219 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.220 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
1.221 @@ -192,9 +291,9 @@
1.222 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
1.223 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
1.224
1.225 -"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
1.226 -"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
1.227 -"----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
1.228 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
1.229 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
1.230 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
1.231 val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.232 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
1.233 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
1.234 @@ -229,10 +328,9 @@
1.235 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
1.236 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
1.237
1.238 -"-------- investigate (new 2002) uniary minus -----------";
1.239 -"-------- investigate (new 2002) uniary minus -----------";
1.240 -"-------- investigate (new 2002) uniary minus -----------";
1.241 -(*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
1.242 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
1.243 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
1.244 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
1.245 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
1.246 TermC.atomty t;
1.247 (*
1.248 @@ -252,15 +350,7 @@
1.249 (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
1.250 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
1.251
1.252 -(*----------------------------------- vvvv --------------------------------------------*)
1.253 -val t = (Thm.term_of o the o (TermC.parse thy)) "-1";
1.254 -TermC.atomty t;
1.255 -(*** -------------
1.256 -*** Free ( -1, real) *)
1.257 -case t of
1.258 - Free ("-1", _) => ()
1.259 -| _ => error "internal representation of \"-1\" changed";
1.260 -(*----------------------------------- vvvvv -------------------------------------------*)
1.261 +
1.262 val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
1.263 TermC.atomty t;
1.264 (*
1.265 @@ -269,7 +359,7 @@
1.266 ***
1.267 *)
1.268 case t of
1.269 - Free ("-1", _) => ()
1.270 + Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
1.271 | _ => error "internal representation of \"- 1\" changed";
1.272
1.273 "======= these external values all have the same internal representation";
1.274 @@ -299,9 +389,424 @@
1.275 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
1.276 | _ => error "internal representation of \"-(x)\" changed";
1.277
1.278 -"-------- check make_polynomial with simple terms -------";
1.279 -"-------- check make_polynomial with simple terms -------";
1.280 -"-------- check make_polynomial with simple terms -------";
1.281 +
1.282 +"-------- fun sort_variables -------------------------------------------------------------------";
1.283 +"-------- fun sort_variables -------------------------------------------------------------------";
1.284 +"-------- fun sort_variables -------------------------------------------------------------------";
1.285 +if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
1.286 +else error "lexicographic order CHANGED";
1.287 +
1.288 +(*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
1.289 +val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
1.290 +val t' = sort_variables t;
1.291 +if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
1.292 +else error "sort_variables 3 * b + a * 2 CHANGED";
1.293 +
1.294 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.295 + val ll = map monom2list (poly2list t);
1.296 +
1.297 +(*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
1.298 +(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
1.299 +(*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
1.300 +(*+*) ] = map monom2list (poly2list t);
1.301 +
1.302 + val lls = map sort_varList ll;
1.303 +
1.304 +(*+*)case map sort_varList ll of
1.305 +(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
1.306 +(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
1.307 +(*+*) ] => ()
1.308 +(*+*)| _ => error "map sort_varList CHANGED";
1.309 +
1.310 + val T = type_of t;
1.311 + val ls = map (create_monom T) lls;
1.312 +
1.313 +(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
1.314 +(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
1.315 +
1.316 +(*+*)case map (create_monom T) lls of
1.317 +(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
1.318 +(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
1.319 +(*+*) ] => ()
1.320 +(*+*)| _ => error "map (create_monom T) CHANGED";
1.321 +
1.322 + val xxx = (*in*) create_polynom T ls (*end*);
1.323 +
1.324 +(*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
1.325 +(*+*)else error "create_polynom CHANGED";
1.326 +(* done by rewriting> 2 * a + 3 * b ? *)
1.327 +
1.328 +(*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
1.329 +val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
1.330 +val t' = sort_variables t;
1.331 +if UnparseC.term t' = "3 * a + - 2 * a" then ()
1.332 +else error "sort_variables 3 * a + - 2 * a CHANGED";
1.333 +
1.334 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.335 + val ll = map monom2list (poly2list t);
1.336 +
1.337 +(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.338 +(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
1.339 +(*+*) ] = map monom2list (poly2list t);
1.340 +
1.341 + val lls = map
1.342 + sort_varList ll;
1.343 +
1.344 +(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.345 +(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
1.346 +(*+*) ] = map sort_varList ll;
1.347 +
1.348 + map sort_varList ll;
1.349 +"~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
1.350 +val sorted = sort var_ord ts;
1.351 +
1.352 +(*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
1.353 +(*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
1.354 +
1.355 +
1.356 +(*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
1.357 +(*+*)then () else error "get_basStr - 2 CHANGED";
1.358 +(*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
1.359 +(*+*)then () else error "get_basStr a CHANGED";
1.360 +
1.361 +
1.362 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
1.363 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
1.364 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
1.365 +(* indentation partially indicates call hierarchy:
1.366 +"~~~~~ fun is_addUnordered
1.367 +"~~~~~~~ fun is_polyexp
1.368 +"~~~~~~~ fun sort_monoms
1.369 +"~~~~~~~~~ fun sort_monList
1.370 +"~~~~~~~~~~~ fun koeff_degree_ord
1.371 +"~~~~~~~~~~~~~ fun degree_ord
1.372 +"~~~~~~~~~~~~~~~ fun dict_cond_ord
1.373 +"~~~~~~~~~~~~~~~~~ fun var_ord_revPow
1.374 +"~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
1.375 +"~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
1.376 +"~~~~~~~~~~~~~~~ fun monom_degree
1.377 +"~~~~~~~~~~~~~ fun compare_koeff_ord
1.378 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon
1.379 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr
1.380 +"~~~~~ fun is_multUnordered
1.381 +"~~~~~~~ fun sort_variables
1.382 +"~~~~~~~~~ fun sort_varList
1.383 +"~~~~~~~~~~~ fun var_ord
1.384 +"~~~~~~~~~~~~~ fun get_basStr used twice --^^
1.385 +"~~~~~~~~~~~~~ fun get_potStr used twice --^^
1.386 +*)
1.387 +val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
1.388 +
1.389 + eval_is_addUnordered "xxx" "yyy" t @{theory};
1.390 +"~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
1.391 + (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =
1.392 + ("xxx", "yyy", t, @{theory});
1.393 +
1.394 + (*if*) is_addUnordered arg;
1.395 +"~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
1.396 + ((is_polyexp t) andalso not (t = sort_monoms t));
1.397 +
1.398 + (t = sort_monoms t);
1.399 +"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
1.400 + val ll = map monom2list (poly2list t);
1.401 + val lls =
1.402 +
1.403 + sort_monList ll;
1.404 +"~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
1.405 + val xxx =
1.406 +
1.407 + sort koeff_degree_ord ll(*return value*);
1.408 +"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
1.409 + koeff_degree_ord: term list * term list -> order;
1.410 +(*we check all elements at once..*)
1.411 +val eee1 = ll |> nth 1;
1.412 +val eee2 = ll |> nth 2;
1.413 +val eee3 = ll |> nth 3;
1.414 +val eee3 = ll |> nth 3;
1.415 +val eee4 = ll |> nth 4;
1.416 +
1.417 +if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
1.418 +if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
1.419 +if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
1.420 +if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
1.421 +
1.422 +if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
1.423 +if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
1.424 +if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
1.425 +if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
1.426 +
1.427 +if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
1.428 +if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
1.429 +if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
1.430 +if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
1.431 +
1.432 +if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
1.433 +if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
1.434 +if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
1.435 +if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
1.436 +
1.437 +if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
1.438 +if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
1.439 +if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
1.440 +if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
1.441 +
1.442 +"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
1.443 + degree_ord: term list * term list -> order;
1.444 +
1.445 +if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
1.446 +if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
1.447 +if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
1.448 +if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
1.449 +
1.450 +if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
1.451 +if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
1.452 +if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
1.453 +if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
1.454 +
1.455 +if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
1.456 +if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
1.457 +if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
1.458 +if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
1.459 +
1.460 +if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
1.461 +if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
1.462 +if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
1.463 +if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
1.464 +
1.465 +"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
1.466 +dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
1.467 +dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
1.468 +dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
1.469 +val xxx = dict_cond_ord var_ord_revPow is_nums;
1.470 +(* output from:
1.471 +fun var_ord_revPow (a,b: term) =
1.472 + (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
1.473 + @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.474 + prod_ord string_ord string_ord_rev
1.475 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
1.476 +*)
1.477 +if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
1.478 +if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
1.479 +if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
1.480 +if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
1.481 +(*-------------------------------------------------------------------------------------*)
1.482 +if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
1.483 +if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
1.484 +if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
1.485 +if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
1.486 +(*-------------------------------------------------------------------------------------*)
1.487 +if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
1.488 +if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
1.489 +if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
1.490 +if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
1.491 +(*-------------------------------------------------------------------------------------*)
1.492 +if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
1.493 +if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
1.494 +if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
1.495 +if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
1.496 +(*-------------------------------------------------------------------------------------*)
1.497 +
1.498 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
1.499 +(* we check all at once//*)
1.500 +if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
1.501 +if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
1.502 +if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
1.503 +if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
1.504 +
1.505 +"~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
1.506 + compare_koeff_ord: term list * term list -> order;
1.507 +(* we check all at once//*)
1.508 +if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
1.509 +if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
1.510 +if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
1.511 +if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
1.512 +
1.513 +if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
1.514 +if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
1.515 +if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
1.516 +if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
1.517 +
1.518 +if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
1.519 +if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
1.520 +if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
1.521 +if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
1.522 +
1.523 +if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
1.524 +if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
1.525 +if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
1.526 +if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
1.527 +
1.528 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
1.529 + get_koeff_of_mon: term list -> term option;
1.530 +
1.531 +val SOME xxx1 = get_koeff_of_mon eee1;
1.532 +val SOME xxx2 = get_koeff_of_mon eee2;
1.533 +val SOME xxx3 = get_koeff_of_mon eee3;
1.534 +val NONE = get_koeff_of_mon eee4;
1.535 +
1.536 +if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
1.537 +if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
1.538 +if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
1.539 +
1.540 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
1.541 + koeff2ordStr: term option -> string;
1.542 +if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
1.543 +if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
1.544 +if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
1.545 +if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
1.546 +
1.547 +
1.548 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.549 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.550 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.551 +val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.552 +Rewrite.trace_on := false;
1.553 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.554 + UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.555 +if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1.556 +else error "poly.sml: diff.behav. in make_polynomial 23";
1.557 +
1.558 +(** )
1.559 +## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
1.560 +### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
1.561 +###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
1.562 +####### try calc: "Poly.is_addUnordered"
1.563 +######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
1.564 + True" (*isa2*)
1.565 +####### calc. to: False (*isa*)
1.566 + True (*isa2*)
1.567 +( **)
1.568 + if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
1.569 +else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
1.570 +"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
1.571 + ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
1.572 +
1.573 +(*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.574 +
1.575 +(*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
1.576 +"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
1.577 + val ll = map monom2list (poly2list t);
1.578 + val lls = sort_monList ll;
1.579 +
1.580 +(*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
1.581 +(*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
1.582 +
1.583 +"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
1.584 +(* we check all elements at once..*)
1.585 +val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
1.586 +val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
1.587 +
1.588 +(*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
1.589 +(*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
1.590 +(*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
1.591 +(*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
1.592 +(* isa -- isa2:
1.593 +(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
1.594 +(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
1.595 +(*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
1.596 +
1.597 +(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
1.598 +
1.599 +(*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
1.600 +
1.601 +(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
1.602 +(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
1.603 +(*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
1.604 +val it = true: bool
1.605 +val it = true: bool
1.606 +val it = true: bool
1.607 +val it = true: bool*)
1.608 +
1.609 +"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
1.610 +(*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
1.611 +(*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
1.612 +(*{a = "int_ord (4, 10003) = ", z = LESS} isa
1.613 + {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
1.614 +(*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
1.615 +(*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
1.616 +(* isa -- isa2:
1.617 +(*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
1.618 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.619 +(*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
1.620 +(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
1.621 +(*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
1.622 +(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
1.623 +(*1*){a = "dict_cond_ord ([], [])"} (*isa*)
1.624 +
1.625 +(*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
1.626 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.627 + {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
1.628 +(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
1.629 +
1.630 +(*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
1.631 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.632 + {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
1.633 +(*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
1.634 +
1.635 +(*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
1.636 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.637 +(*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
1.638 +(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
1.639 +(*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
1.640 +(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
1.641 +(*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
1.642 +
1.643 +val it = true: bool
1.644 +val it = false: bool
1.645 +val it = false: bool
1.646 +val it = true: bool
1.647 +*)
1.648 +
1.649 +(*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
1.650 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
1.651 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.652 + (*if*) (is_nums x) (*else*);
1.653 + val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.654 + (*case*) x (*of*);
1.655 +(*+*)UnparseC.term x = "x \<up> 2";
1.656 + (*if*) TermC.is_num t (*then*);
1.657 +
1.658 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.659 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.660 + (*if*) (is_nums x) (*else*);
1.661 + val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.662 + (*case*) x (*of*);
1.663 +(*+*)UnparseC.term x = "y \<up> 2";
1.664 + (*if*) TermC.is_num t (*then*);
1.665 +
1.666 + val return =
1.667 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.668 +if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
1.669 +( *---------------------------------------------------------------------------------OPEN local/*)
1.670 +
1.671 +(*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
1.672 +else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
1.673 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
1.674 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.675 + (*if*) (is_nums x) (*else*);
1.676 +val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.677 + (*case*) x (*of*);
1.678 +(*+*)UnparseC.term x = "x \<up> 3";
1.679 + (*if*) TermC.is_num t (*then*);
1.680 +
1.681 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.682 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.683 + (*if*) (is_nums x) (*else*);
1.684 +val _ = (*the default case*)
1.685 + (*case*) x (*of*);
1.686 +( *---------------------------------------------------------------------------------OPEN local/*)
1.687 +
1.688 +"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
1.689 +val xxx = dict_cond_ord var_ord_revPow is_nums;
1.690 +(*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
1.691 +(*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
1.692 +(*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
1.693 +(*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
1.694 +
1.695 +
1.696 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.697 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.698 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.699 "----- check 1 ---";
1.700 val t = TermC.str2term "2*3*a";
1.701 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.702 @@ -332,9 +837,9 @@
1.703 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.704 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
1.705
1.706 -"-------- fun is_multUnordered --------------------------";
1.707 -"-------- fun is_multUnordered --------------------------";
1.708 -"-------- fun is_multUnordered --------------------------";
1.709 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.710 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.711 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.712 val thy = @{theory "Isac_Knowledge"};
1.713 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
1.714 val t = TermC.str2term "x \<up> 2 * x";
1.715 @@ -372,59 +877,271 @@
1.716 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
1.717 UnparseC.term t;
1.718
1.719 -"-------- examples from textbook Schalk I ---------------";
1.720 -"-------- examples from textbook Schalk I ---------------";
1.721 -"-------- examples from textbook Schalk I ---------------";
1.722 +
1.723 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.724 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.725 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.726 +val thy = @{theory "Isac_Knowledge"};
1.727 +val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
1.728 +
1.729 +(*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
1.730 +(*+*) andalso not (is_multUnordered arg)
1.731 +(*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
1.732 +
1.733 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.734 + SOME
1.735 + ("xxx 3 * a + - 2 * a_",
1.736 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.737 + Const ("HOL.False", _))) => ()
1.738 +(* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
1.739 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.740 +
1.741 +"----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
1.742 +val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
1.743 +
1.744 +(*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
1.745 +(*+*) andalso not (is_multUnordered arg)
1.746 +(*+*)then () else error "sort_variables - 2 * a CHANGED";
1.747 +
1.748 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.749 + SOME
1.750 + ("xxx - 2 * a_",
1.751 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.752 + Const ("HOL.False", _))) => ()
1.753 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.754 +
1.755 +"----- is_multUnordered --- (a) is_multUnordered = False";
1.756 +val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
1.757 +
1.758 +(*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
1.759 +(*+*) andalso not (is_multUnordered arg)
1.760 +(*+*)then () else error "sort_variables a CHANGED";
1.761 +
1.762 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.763 + SOME
1.764 + ("xxx a_",
1.765 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.766 + Const ("HOL.False", _))) => ()
1.767 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.768 +
1.769 +"----- is_multUnordered --- (- 2) is_multUnordered = False";
1.770 +val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
1.771 +
1.772 +(*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
1.773 +(*+*) andalso not (is_multUnordered arg)
1.774 +(*+*)then () else error "sort_variables - 2 CHANGED";
1.775 +
1.776 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.777 + SOME
1.778 + ("xxx - 2_",
1.779 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.780 + Const ("HOL.False", _))) => ()
1.781 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.782 +
1.783 +
1.784 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.785 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.786 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.787 +(* ca.line 45 of Rewrite.trace_on:
1.788 +## rls: order_mult_rls_ on:
1.789 + x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
1.790 +### rls: order_mult_ on:
1.791 + x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
1.792 +###### rls: Rule_Set.empty-is_multUnordered on:
1.793 + 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
1.794 +####### try calc: "Poly.is_multUnordered"
1.795 +######## eval asms:
1.796 +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.797 +-------------------------------------------------------------------------------------------------==
1.798 +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.799 +####### calc. to: True
1.800 +####### try calc: "Poly.is_multUnordered"
1.801 +####### try calc: "Poly.is_multUnordered"
1.802 +### rls: order_mult_ on:
1.803 +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.804 +--------+--------------------------+---------------------------------+---------------------------<>
1.805 +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.806 +-------------------------------------------------------------------------------------------------<>
1.807 +*)
1.808 +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.809 +(*
1.810 +"~~~~~ fun is_multUnordered
1.811 +"~~~~~~~ fun sort_variables
1.812 +"~~~~~~~~~ val sort_varList
1.813 +*)
1.814 +"~~~~~ fun is_multUnordered , args:"; val (t) = (t);
1.815 + is_polyexp t = true;
1.816 +
1.817 + val return =
1.818 + sort_variables t;
1.819 +(*+*)if UnparseC.term return =
1.820 +(*+*) "x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) +\n(- 1) \<up> 2 * (3 * (a \<up> 2 * x)) +\n(- 1) \<up> 3 * a \<up> 3"
1.821 +(*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
1.822 +
1.823 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.824 + val ll = map monom2list (poly2list t);
1.825 + val lls = map sort_varList ll;
1.826 +
1.827 +(*+*)val ori3 = nth 3 ll;
1.828 +(*+*)val mon3 = nth 3 lls;
1.829 +
1.830 +(*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
1.831 +(*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
1.832 +(*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
1.833 +(*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
1.834 +
1.835 +(*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
1.836 +(*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
1.837 +(*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
1.838 +(*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
1.839 +
1.840 +"~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
1.841 +(* Output below with:
1.842 +val sort_varList = sort var_ord;
1.843 +fun var_ord (a,b: term) =
1.844 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1.845 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.846 + prod_ord string_ord string_ord
1.847 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1.848 +);
1.849 +*)
1.850 +(*+*)val xxx = sort_varList ori3;
1.851 +(*
1.852 +{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
1.853 +{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
1.854 +
1.855 +isa isa2
1.856 +{a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
1.857 + {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
1.858 +{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1.859 + {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1.860 +{a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
1.861 + {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
1.862 + ^^^ ^^^
1.863 +
1.864 +{a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
1.865 + {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
1.866 + ^^^ ^^^
1.867 +{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1.868 + {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1.869 +{a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
1.870 + {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
1.871 +*)
1.872 +
1.873 +
1.874 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.875 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.876 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.877 +val t = TermC.str2term "b * a * a";
1.878 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.879 +if UnparseC.term t = "a \<up> 2 * b" then ()
1.880 +else error "poly.sml: diff.behav. in make_polynomial 21";
1.881 +
1.882 +"~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
1.883 + ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
1.884 +
1.885 +(*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
1.886 +"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
1.887 + (*if*) TermC.is_num num (*else*);
1.888 +
1.889 +"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
1.890 + (*if*) TermC.is_num num (*else*);
1.891 + (*if*) TermC.is_variable num (*then*);
1.892 +
1.893 + val xxx = sort_variables t;
1.894 +(*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
1.895 +
1.896 +
1.897 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.898 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.899 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.900 +val t = TermC.str2term "2*3*a";
1.901 +val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
1.902 +(*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
1.903 +(*
1.904 +## try calc: "Groups.times_class.times"
1.905 +## rls: order_mult_rls_ on: 6 * a
1.906 +### rls: order_mult_ on: 6 * a
1.907 +###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
1.908 +####### try calc: "Poly.is_multUnordered"
1.909 +######## eval asms: "6 * a is_multUnordered = True" (*isa*)
1.910 + = False" (*isa2*)
1.911 +####### calc. to: True (*isa*)
1.912 + False (*isa2*)
1.913 +*)
1.914 +val t = TermC.str2term "(6 * a) is_multUnordered";
1.915 +val SOME
1.916 + (_, t') =
1.917 + eval_is_multUnordered "xxx" () t @{theory};
1.918 +(*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
1.919 +(*+*)else error "6 * a is_multUnordered = False CHANGED";
1.920 +
1.921 +"~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
1.922 + (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
1.923 + (*if*) is_multUnordered arg (*else*);
1.924 +
1.925 +"~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
1.926 + val return =
1.927 + ((is_polyexp t) andalso not (t = sort_variables t));
1.928 +
1.929 +(*+*)return = false; (*isa*)
1.930 +(*+*) is_polyexp t = true; (*isa*)
1.931 +(*+*) not (t = sort_variables t) = false; (*isa*)
1.932 +
1.933 + val xxx = sort_variables t;
1.934 +(*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
1.935 +
1.936 +
1.937 +"-------- examples from textbook Schalk I ------------------------------------------------------";
1.938 +"-------- examples from textbook Schalk I ------------------------------------------------------";
1.939 +"-------- examples from textbook Schalk I ------------------------------------------------------";
1.940 "-----SPB Schalk I p.63 No.267b ---";
1.941 -(*associate poly* )
1.942 val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
1.943 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.944 -if (UnparseC.term t) = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9"
1.945 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.946 +if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
1.947 then () else error "poly.sml: diff.behav. in make_polynomial 1";
1.948
1.949 "-----SPB Schalk I p.63 No.275b ---";
1.950 val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
1.951 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.952 -if (UnparseC.term t) = ("3 * x \<up> 4 + -2 * x \<up> 3 * y + -5 * x \<up> 2 * y \<up> 2 + " ^
1.953 - "4 * x * y \<up> 3 +\n-2 * y \<up> 4")
1.954 +if UnparseC.term t =
1.955 + "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"
1.956 then () else error "poly.sml: diff.behav. in make_polynomial 2";
1.957
1.958 "-----SPB Schalk I p.63 No.279b ---";
1.959 val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
1.960 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.961 -if (UnparseC.term t) =
1.962 - ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x \<up> 2 +\n" ^
1.963 - "-1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n-1 * a * x \<up> 3 +\n" ^
1.964 - "-1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n-1 * b * x \<up> 3 +\n" ^
1.965 - "c * d * x \<up> 2 +\n-1 * c * x \<up> 3 +\n-1 * d * x \<up> 3 +\nx \<up> 4")
1.966 +if UnparseC.term t =
1.967 + ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
1.968 + "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
1.969 + "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
1.970 + " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
1.971 then () else error "poly.sml: diff.behav. in make_polynomial 3";
1.972 -( *associate poly*)
1.973 +(*associate poly*)
1.974
1.975 "-----SPB Schalk I p.63 No.291 ---";
1.976 val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
1.977 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.978 -if (UnparseC.term t) = "50 + -770 * x + 4520 * x \<up> 2 + -16320 * x \<up> 3 + -26880 * x \<up> 4"
1.979 +if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
1.980 then () else error "poly.sml: diff.behav. in make_polynomial 4";
1.981
1.982 -(*associate poly* )
1.983 "-----SPB Schalk I p.64 No.295c ---";
1.984 val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
1.985 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.986 -if (UnparseC.term t) = ("169 * a \<up> 8 * b \<up> 18 * c \<up> 2 + -312 * a \<up> 7 * b \<up> 15 * c \<up> 10" ^
1.987 - " +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18")
1.988 +if UnparseC.term t =
1.989 + "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"
1.990 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
1.991 -( *associate poly*)
1.992
1.993 "-----SPB Schalk I p.64 No.299a ---";
1.994 val t = TermC.str2term "(x - y)*(x + y)";
1.995 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.996 -if (UnparseC.term t) = "x \<up> 2 + -1 * y \<up> 2"
1.997 +if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
1.998 then () else error "poly.sml: diff.behav. in make_polynomial 6";
1.999
1.1000 "-----SPB Schalk I p.64 No.300c ---";
1.1001 val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
1.1002 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.1003 -if (UnparseC.term t) = "-1 + 9 * x \<up> 4 * y \<up> 2"
1.1004 +if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
1.1005 then () else error "poly.sml: diff.behav. in make_polynomial 7";
1.1006
1.1007 "-----SPB Schalk I p.64 No.302 ---";
1.1008 @@ -438,32 +1155,35 @@
1.1009 "-----SPB Schalk I p.64 No.306a ---";
1.1010 val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
1.1011 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1012 -if (UnparseC.term t) = "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8" then ()
1.1013 +if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
1.1014 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";
1.1015
1.1016 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
1.1017 the above resulted in the term below ... but reduces from then correctly*)
1.1018 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
1.1019 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1020 -if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"
1.1021 +if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
1.1022 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.1023
1.1024 "-----SPB Schalk I p.64 No.296a ---";
1.1025 val t = TermC.str2term "(x - a) \<up> 3";
1.1026 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1027 -if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"
1.1028 +
1.1029 +val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc";
1.1030 +
1.1031 +if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1.1032 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.1033
1.1034 "-----SPB Schalk I p.64 No.296c ---";
1.1035 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1.1036 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1037 -if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
1.1038 +if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1.1039 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.1040
1.1041 "-----SPB Schalk I p.62 No.242c ---";
1.1042 val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
1.1043 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1044 -if (UnparseC.term t) = "1"
1.1045 +if UnparseC.term t = "1"
1.1046 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.1047
1.1048 "-----SPB Schalk I p.60 No.209a ---";
1.1049 @@ -478,19 +1198,21 @@
1.1050 if UnparseC.term t = "d \<up> 3"
1.1051 then () else error "poly.sml: diff.behav. in make_polynomial 14";
1.1052
1.1053 -(*---------------------------------------------------------------------*)
1.1054 -(*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)
1.1055 -(*---------------------------------------------------------------------*)
1.1056 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.1057 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.1058 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1.1059 "-----Schalk I p.64 No.303 ---";
1.1060 val t = TermC.str2term "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
1.1061 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1062 +(*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
1.1063 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1064 if UnparseC.term t = "1280 * b \<up> 4"
1.1065 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
1.1066 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
1.1067 +(*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
1.1068
1.1069 -(*--------------------------------------------------------------------*)
1.1070 -(*----------------------- Eigene Beispiele ---------------------------*)
1.1071 -(*--------------------------------------------------------------------*)
1.1072 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.1073 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.1074 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1.1075 "-----SPO ---";
1.1076 val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1.1077 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1078 @@ -538,38 +1260,38 @@
1.1079 else error "poly.sml: diff.behav. in make_polynomial 23";
1.1080 "-----SPO ---";
1.1081 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
1.1082 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1083 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.1084 if (UnparseC.term t) = "a \<up> 4" then ()
1.1085 else error "poly.sml: diff.behav. in make_polynomial 24";
1.1086 "-----SPO ---";
1.1087 val t = TermC.str2term "a * b * b \<up> (-1) + a";
1.1088 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1089 -if (UnparseC.term t) = "2 * a" then ()
1.1090 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.1091 +if UnparseC.term t = "2 * a" then ()
1.1092 else error "poly.sml: diff.behav. in make_polynomial 25";
1.1093 "-----SPO ---";
1.1094 val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
1.1095 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.1096 -if (UnparseC.term t) = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
1.1097 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.1098 +if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
1.1099 then () else error "poly.sml: diff.behav. in make_polynomial 26";
1.1100
1.1101 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
1.1102 "-----SPO ---";
1.1103 val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
1.1104 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.1105 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
1.1106 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
1.1107 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
1.1108
1.1109 val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
1.1110 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.1111 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
1.1112 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
1.1113 then () else error "poly.sml: diff.behav. in make_polynomial 28";
1.1114
1.1115 -"-------- check pbl 'polynomial simplification' --------";
1.1116 -"-------- check pbl 'polynomial simplification' --------";
1.1117 -"-------- check pbl 'polynomial simplification' --------";
1.1118 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
1.1119 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
1.1120 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
1.1121 val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
1.1122 "-----0 ---";
1.1123 -case Refine.refine fmz ["polynomial", "simplification"]of
1.1124 +case Refine.refine fmz ["polynomial", "simplification"] of
1.1125 [M_Match.Matches (["polynomial", "simplification"], _)] => ()
1.1126 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
1.1127 (*...if there is an error, then ...*)
1.1128 @@ -608,9 +1330,9 @@
1.1129 (*show_types:=false;*)
1.1130
1.1131
1.1132 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.1133 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.1134 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.1135 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1.1136 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1.1137 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1.1138 val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
1.1139 val (dI',pI',mI') =
1.1140 ("Poly",["polynomial", "simplification"],
1.1141 @@ -636,16 +1358,16 @@
1.1142
1.1143 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
1.1144
1.1145 -(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n-8 * x \<up> 9"
1.1146 +(*+*)if f2str f = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
1.1147 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
1.1148
1.1149 (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
1.1150
1.1151
1.1152
1.1153 -"-------- interSteps for Schalk 299a --------------------";
1.1154 -"-------- interSteps for Schalk 299a --------------------";
1.1155 -"-------- interSteps for Schalk 299a --------------------";
1.1156 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
1.1157 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
1.1158 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
1.1159 reset_states ();
1.1160 CalcTree
1.1161 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
1.1162 @@ -668,31 +1390,50 @@
1.1163 else error "poly.sml: interSteps doesnt work again 2";
1.1164 ============ inhibit exn WN120316 ==============================================*)
1.1165
1.1166 -"-------- norm_Poly NOT COMPLETE ------------------------";
1.1167 -"-------- norm_Poly NOT COMPLETE ------------------------";
1.1168 -"-------- norm_Poly NOT COMPLETE ------------------------";
1.1169 +"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1.1170 +"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1.1171 +"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1.1172 val thy = @{theory AlgEin};
1.1173
1.1174 val SOME (f',_) = rewrite_set_ thy false norm_Poly
1.1175 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.1176 -if UnparseC.term f' = "L = senkrecht + oben + 2 * 2 * k + 2 * -4 * q"
1.1177 +if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
1.1178 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
1.1179 else error "norm_Poly changed behavior";
1.1180 +(* isa:
1.1181 +## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1.1182 +### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1.1183 +###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1.1184 +oben is_addUnordered
1.1185 +####### try calc: "Poly.is_addUnordered"
1.1186 +######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1.1187 +oben is_addUnordered = True"
1.1188 +####### calc. to: True
1.1189 +####### try calc: "Poly.is_addUnordered"
1.1190 +####### try calc: "Poly.is_addUnordered"
1.1191 +### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
1.1192 +*)
1.1193 +"~~~~~ fun sort_monoms , args:"; val (t) =
1.1194 + (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
1.1195 +(*+*)val t' =
1.1196 + sort_monoms t;
1.1197 +(*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
1.1198
1.1199 -"-------- ord_make_polynomial ---------------------------";
1.1200 -"-------- ord_make_polynomial ---------------------------";
1.1201 -"-------- ord_make_polynomial ---------------------------";
1.1202 +"-------- ord_make_polynomial ------------------------------------------------------------------";
1.1203 +"-------- ord_make_polynomial ------------------------------------------------------------------";
1.1204 +"-------- ord_make_polynomial ------------------------------------------------------------------";
1.1205 val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
1.1206 -val t2 = TermC.str2term "3 * a + 3 * b + 2 * b";
1.1207 +val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
1.1208
1.1209 if ord_make_polynomial true thy [] (t1, t2) then ()
1.1210 else error "poly.sml: diff.behav. in ord_make_polynomial";
1.1211 +(*SO: WHY IS THERE NO REWRITING ...*)
1.1212
1.1213 -(*WN071202: \<up> why then is there no rewriting ...*)
1.1214 val term = TermC.str2term "2*b + (3*a + 3*b)";
1.1215 -val NONE = rewrite_set_ (@{theory "Isac_Knowledge"}) false order_add_mult term;
1.1216 +(*+++*)val SOME (t', []) = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
1.1217 +(*+++*)if UnparseC.term t' = "a * 3 + (b * 2 + b * 3)" then () else error "no rewriting ?!?";
1.1218 +(* before dropping ThmC.numerals_to_Free this was
1.1219 +val NONE = rewrite_set_ @ {theory "Isac_Knowledge"} false order_add_mult term;
1.1220 +SO: WHY IS THERE NO REWRITING ?!?
1.1221 +*)
1.1222
1.1223 -(*or why is there no rewriting this way...*)
1.1224 -val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
1.1225 -val t2 = TermC.str2term "3 * a + (2 * b + 3 * b)";
1.1226 -