1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Fri Jul 16 07:45:06 2021 +0200
1.3 @@ -0,0 +1,793 @@
1.4 +(* Title: test/Tools/isac/Knowledge/poly-1.sml
1.5 + Author: Walther Neuper
1.6 + Use is subject to license terms.
1.7 +
1.8 +Test of basic functions and application to complex examples.
1.9 +*)
1.10 +
1.11 +"-----------------------------------------------------------------------------------------------";
1.12 +"-----------------------------------------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------------------------------------";
1.14 +"-----------------------------------------------------------------------------------------------";
1.15 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.16 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.17 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.18 +"-------- fun sort_variables -------------------------------------------------------------------";
1.19 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.20 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.21 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.22 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.23 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.24 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.25 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.26 +"-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.27 +"-------- complex examples from textbook Schalk I ----------------------------------------------";
1.28 +"-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.29 +"-----------------------------------------------------------------------------------------------";
1.30 +"-----------------------------------------------------------------------------------------------";
1.31 +
1.32 +
1.33 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.34 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.35 +"-------- fun is_polyexp -----------------------------------------------------------------------";
1.36 +val t = TermC.str2term "x / x";
1.37 +if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
1.38 +
1.39 +val t = TermC.str2term "-1 * A * 3";
1.40 +if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
1.41 +
1.42 +val t = TermC.str2term "-1 * AA * 3";
1.43 +if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
1.44 +
1.45 +val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
1.46 +if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
1.47 +
1.48 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.49 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.50 +"-------- fun has_degree_in --------------------------------------------------------------------";
1.51 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.52 +val t = (Thm.term_of o the o (TermC.parse thy)) "1";
1.53 +if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
1.54 +
1.55 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.56 +val t = (Thm.term_of o the o (TermC.parse thy)) "1";
1.57 +if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
1.58 +
1.59 +(*----------*)
1.60 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.61 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
1.62 +if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
1.63 +
1.64 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.65 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
1.66 +if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
1.67 +
1.68 +(*----------*)
1.69 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.70 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
1.71 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
1.72 +
1.73 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.74 +val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
1.75 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
1.76 +
1.77 +(*----------*)
1.78 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.79 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
1.80 +if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
1.81 +
1.82 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.83 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
1.84 +if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
1.85 +
1.86 +(*----------*)
1.87 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.88 +val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
1.89 +if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
1.90 +
1.91 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.92 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
1.93 +if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
1.94 +
1.95 +(*----------*)
1.96 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.97 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
1.98 +if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
1.99 +
1.100 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.101 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
1.102 +if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
1.103 +
1.104 +(*----------*)
1.105 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.106 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
1.107 +if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
1.108 +
1.109 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.110 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
1.111 +if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
1.112 +
1.113 +(*----------*)
1.114 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.115 +val t = (Thm.term_of o the o (TermC.parse thy)) "x";
1.116 +if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
1.117 +
1.118 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.119 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.120 +if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
1.121 +
1.122 +(*----------*)
1.123 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.124 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
1.125 +if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
1.126 +
1.127 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.128 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.129 +if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
1.130 +
1.131 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.132 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.133 +"-------- fun mono_deg_in ----------------------------------------------------------------------";
1.134 +val v = (Thm.term_of o the o (TermC.parse thy)) "x";
1.135 +
1.136 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
1.137 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
1.138 +
1.139 +val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
1.140 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
1.141 +
1.142 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
1.143 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
1.144 +
1.145 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
1.146 +if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
1.147 +
1.148 +val t = (Thm.term_of o the o (TermC.parse thy)) "x";
1.149 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
1.150 +
1.151 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
1.152 +if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
1.153 +
1.154 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
1.155 +if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
1.156 +
1.157 +(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
1.158 +val thy = @{theory Partial_Fractions}
1.159 +val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.160 +
1.161 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
1.162 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
1.163 +
1.164 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
1.165 +if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
1.166 +
1.167 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
1.168 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
1.169 +
1.170 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
1.171 +if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
1.172 +
1.173 +val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
1.174 +if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
1.175 +
1.176 +val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
1.177 +if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
1.178 +
1.179 +val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
1.180 +if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
1.181 +
1.182 +
1.183 +"-------- fun sort_variables -------------------------------------------------------------------";
1.184 +"-------- fun sort_variables -------------------------------------------------------------------";
1.185 +"-------- fun sort_variables -------------------------------------------------------------------";
1.186 +if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
1.187 +else error "lexicographic order CHANGED";
1.188 +
1.189 +(*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
1.190 +val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
1.191 +val t' = sort_variables t;
1.192 +if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
1.193 +else error "sort_variables 3 * b + a * 2 CHANGED";
1.194 +
1.195 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.196 + val ll = map monom2list (poly2list t);
1.197 +
1.198 +(*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
1.199 +(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
1.200 +(*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
1.201 +(*+*) ] = map monom2list (poly2list t);
1.202 +
1.203 + val lls = map sort_varList ll;
1.204 +
1.205 +(*+*)case map sort_varList ll of
1.206 +(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
1.207 +(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
1.208 +(*+*) ] => ()
1.209 +(*+*)| _ => error "map sort_varList CHANGED";
1.210 +
1.211 + val T = type_of t;
1.212 + val ls = map (create_monom T) lls;
1.213 +
1.214 +(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
1.215 +(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
1.216 +
1.217 +(*+*)case map (create_monom T) lls of
1.218 +(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
1.219 +(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
1.220 +(*+*) ] => ()
1.221 +(*+*)| _ => error "map (create_monom T) CHANGED";
1.222 +
1.223 + val xxx = (*in*) create_polynom T ls (*end*);
1.224 +
1.225 +(*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
1.226 +(*+*)else error "create_polynom CHANGED";
1.227 +(* done by rewriting> 2 * a + 3 * b ? *)
1.228 +
1.229 +(*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
1.230 +val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
1.231 +val t' = sort_variables t;
1.232 +if UnparseC.term t' = "3 * a + - 2 * a" then ()
1.233 +else error "sort_variables 3 * a + - 2 * a CHANGED";
1.234 +
1.235 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.236 + val ll = map monom2list (poly2list t);
1.237 +
1.238 +(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.239 +(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
1.240 +(*+*) ] = map monom2list (poly2list t);
1.241 +
1.242 + val lls = map
1.243 + sort_varList ll;
1.244 +
1.245 +(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
1.246 +(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
1.247 +(*+*) ] = map sort_varList ll;
1.248 +
1.249 + map sort_varList ll;
1.250 +"~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
1.251 +val sorted = sort var_ord ts;
1.252 +
1.253 +(*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
1.254 +(*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
1.255 +
1.256 +
1.257 +(*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
1.258 +(*+*)then () else error "get_basStr - 2 CHANGED";
1.259 +(*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
1.260 +(*+*)then () else error "get_basStr a CHANGED";
1.261 +
1.262 +
1.263 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.264 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.265 +"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
1.266 +val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1.267 +Rewrite.trace_on := false;
1.268 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.269 + UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.270 +if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1.271 +else error "poly.sml: diff.behav. in make_polynomial 23";
1.272 +
1.273 +(** )
1.274 +## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
1.275 +### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
1.276 +###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
1.277 +####### try calc: "Poly.is_addUnordered"
1.278 +######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
1.279 + True" (*isa2*)
1.280 +####### calc. to: False (*isa*)
1.281 + True (*isa2*)
1.282 +( **)
1.283 + if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
1.284 +else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
1.285 +"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
1.286 + ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
1.287 +
1.288 +(*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
1.289 +
1.290 +(*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
1.291 +"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
1.292 + val ll = map monom2list (poly2list t);
1.293 + val lls = sort_monList ll;
1.294 +
1.295 +(*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
1.296 +(*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
1.297 +
1.298 +"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
1.299 +(* we check all elements at once..*)
1.300 +val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
1.301 +val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
1.302 +
1.303 +(*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
1.304 +(*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
1.305 +(*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
1.306 +(*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
1.307 +(* isa -- isa2:
1.308 +(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
1.309 +(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
1.310 +(*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
1.311 +
1.312 +(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
1.313 +
1.314 +(*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
1.315 +
1.316 +(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
1.317 +(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
1.318 +(*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
1.319 +val it = true: bool
1.320 +val it = true: bool
1.321 +val it = true: bool
1.322 +val it = true: bool*)
1.323 +
1.324 +"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
1.325 +(*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
1.326 +(*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
1.327 +(*{a = "int_ord (4, 10003) = ", z = LESS} isa
1.328 + {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
1.329 +(*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
1.330 +(*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
1.331 +(* isa -- isa2:
1.332 +(*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
1.333 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.334 +(*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
1.335 +(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
1.336 +(*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
1.337 +(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
1.338 +(*1*){a = "dict_cond_ord ([], [])"} (*isa*)
1.339 +
1.340 +(*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
1.341 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.342 + {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
1.343 +(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
1.344 +
1.345 +(*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
1.346 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.347 + {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
1.348 +(*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
1.349 +
1.350 +(*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
1.351 + {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
1.352 +(*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
1.353 +(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
1.354 +(*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
1.355 +(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
1.356 +(*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
1.357 +
1.358 +val it = true: bool
1.359 +val it = false: bool
1.360 +val it = false: bool
1.361 +val it = true: bool
1.362 +*)
1.363 +
1.364 +(*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
1.365 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
1.366 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.367 + (*if*) (is_nums x) (*else*);
1.368 + val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.369 + (*case*) x (*of*);
1.370 +(*+*)UnparseC.term x = "x \<up> 2";
1.371 + (*if*) TermC.is_num t (*then*);
1.372 +
1.373 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.374 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.375 + (*if*) (is_nums x) (*else*);
1.376 + val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.377 + (*case*) x (*of*);
1.378 +(*+*)UnparseC.term x = "y \<up> 2";
1.379 + (*if*) TermC.is_num t (*then*);
1.380 +
1.381 + val return =
1.382 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.383 +if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
1.384 +( *---------------------------------------------------------------------------------OPEN local/*)
1.385 +
1.386 +(*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
1.387 +else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
1.388 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
1.389 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
1.390 + (*if*) (is_nums x) (*else*);
1.391 +val (Const ("Transcendental.powr", _) $ Free _ $ t) =
1.392 + (*case*) x (*of*);
1.393 +(*+*)UnparseC.term x = "x \<up> 3";
1.394 + (*if*) TermC.is_num t (*then*);
1.395 +
1.396 + counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.397 +"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
1.398 + (*if*) (is_nums x) (*else*);
1.399 +val _ = (*the default case*)
1.400 + (*case*) x (*of*);
1.401 +( *---------------------------------------------------------------------------------OPEN local/*)
1.402 +
1.403 +"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
1.404 +val xxx = dict_cond_ord var_ord_revPow is_nums;
1.405 +(*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
1.406 +(*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
1.407 +(*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
1.408 +(*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
1.409 +
1.410 +
1.411 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.412 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.413 +"-------- check make_polynomial with simple terms ----------------------------------------------";
1.414 +"----- check 1 ---";
1.415 +val t = TermC.str2term "2*3*a";
1.416 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.417 +if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
1.418 +
1.419 +"----- check 2 ---";
1.420 +val t = TermC.str2term "2*a + 3*a";
1.421 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.422 +if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
1.423 +
1.424 +"----- check 3 ---";
1.425 +val t = TermC.str2term "2*a + 3*a + 3*a";
1.426 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.427 +if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
1.428 +
1.429 +"----- check 4 ---";
1.430 +val t = TermC.str2term "3*a - 2*a";
1.431 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.432 +if UnparseC.term t = "a" then () else error "check make_polynomial 4";
1.433 +
1.434 +"----- check 5 ---";
1.435 +val t = TermC.str2term "4*(3*a - 2*a)";
1.436 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.437 +if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
1.438 +
1.439 +"----- check 6 ---";
1.440 +val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
1.441 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.442 +if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
1.443 +
1.444 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.445 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.446 +"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
1.447 +val thy = @{theory "Isac_Knowledge"};
1.448 +"===== works for a simple example, see rewrite.sml -- fun app_rev ===";
1.449 +val t = TermC.str2term "x \<up> 2 * x";
1.450 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
1.451 +if UnparseC.term t' = "x * x \<up> 2" then ()
1.452 +else error "poly.sml Poly.is_multUnordered doesn't work";
1.453 +
1.454 +(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
1.455 +### rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +
1.456 + (-48 * x \<up> 4 + 8))
1.457 +###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
1.458 +####### try calc: Poly.is_multUnordered'
1.459 +======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
1.460 +*)
1.461 +val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))";
1.462 +
1.463 +"----- is_multUnordered ---";
1.464 +val tsort = sort_variables t;
1.465 +UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n-1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n-1 * (-1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";
1.466 +is_polyexp t;
1.467 +tsort = t;
1.468 +is_polyexp t andalso not (t = sort_variables t);
1.469 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
1.470 +
1.471 +"----- eval_is_multUnordered ---";
1.472 +val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
1.473 +case eval_is_multUnordered "testid" "" tm thy of
1.474 + SOME (_, Const ("HOL.Trueprop", _) $
1.475 + (Const ("HOL.eq", _) $
1.476 + (Const ("Poly.is_multUnordered", _) $ _) $
1.477 + Const ("HOL.True", _))) => ()
1.478 + | _ => error "poly.sml diff. eval_is_multUnordered";
1.479 +
1.480 +"----- rewrite_set_ STILL DIDN'T WORK";
1.481 +val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
1.482 +UnparseC.term t;
1.483 +
1.484 +
1.485 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.486 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.487 +"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
1.488 +val thy = @{theory "Isac_Knowledge"};
1.489 +val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
1.490 +
1.491 +(*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
1.492 +(*+*) andalso not (is_multUnordered arg)
1.493 +(*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
1.494 +
1.495 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.496 + SOME
1.497 + ("xxx 3 * a + - 2 * a_",
1.498 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.499 + Const ("HOL.False", _))) => ()
1.500 +(* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
1.501 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.502 +
1.503 +"----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
1.504 +val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
1.505 +
1.506 +(*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
1.507 +(*+*) andalso not (is_multUnordered arg)
1.508 +(*+*)then () else error "sort_variables - 2 * a CHANGED";
1.509 +
1.510 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.511 + SOME
1.512 + ("xxx - 2 * a_",
1.513 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.514 + Const ("HOL.False", _))) => ()
1.515 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.516 +
1.517 +"----- is_multUnordered --- (a) is_multUnordered = False";
1.518 +val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
1.519 +
1.520 +(*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
1.521 +(*+*) andalso not (is_multUnordered arg)
1.522 +(*+*)then () else error "sort_variables a CHANGED";
1.523 +
1.524 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.525 + SOME
1.526 + ("xxx a_",
1.527 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.528 + Const ("HOL.False", _))) => ()
1.529 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.530 +
1.531 +"----- is_multUnordered --- (- 2) is_multUnordered = False";
1.532 +val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
1.533 +
1.534 +(*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
1.535 +(*+*) andalso not (is_multUnordered arg)
1.536 +(*+*)then () else error "sort_variables - 2 CHANGED";
1.537 +
1.538 +case eval_is_multUnordered "xxx " "yyy " t thy of
1.539 + SOME
1.540 + ("xxx - 2_",
1.541 + Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
1.542 + Const ("HOL.False", _))) => ()
1.543 +| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
1.544 +
1.545 +
1.546 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.547 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.548 +"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
1.549 +(* ca.line 45 of Rewrite.trace_on:
1.550 +## rls: order_mult_rls_ on:
1.551 + x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
1.552 +### rls: order_mult_ on:
1.553 + x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
1.554 +###### rls: Rule_Set.empty-is_multUnordered on:
1.555 + 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.556 +####### try calc: "Poly.is_multUnordered"
1.557 +######## eval asms:
1.558 +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.559 +-------------------------------------------------------------------------------------------------==
1.560 +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.561 +####### calc. to: True
1.562 +####### try calc: "Poly.is_multUnordered"
1.563 +####### try calc: "Poly.is_multUnordered"
1.564 +### rls: order_mult_ on:
1.565 +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.566 +--------+--------------------------+---------------------------------+---------------------------<>
1.567 +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.568 +-------------------------------------------------------------------------------------------------<>
1.569 +*)
1.570 +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.571 +(*
1.572 +"~~~~~ fun is_multUnordered
1.573 +"~~~~~~~ fun sort_variables
1.574 +"~~~~~~~~~ val sort_varList
1.575 +*)
1.576 +"~~~~~ fun is_multUnordered , args:"; val (t) = (t);
1.577 + is_polyexp t = true;
1.578 +
1.579 + val return =
1.580 + sort_variables t;
1.581 +(*+*)if UnparseC.term return =
1.582 +(*+*) "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.583 +(*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
1.584 +
1.585 +"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
1.586 + val ll = map monom2list (poly2list t);
1.587 + val lls = map sort_varList ll;
1.588 +
1.589 +(*+*)val ori3 = nth 3 ll;
1.590 +(*+*)val mon3 = nth 3 lls;
1.591 +
1.592 +(*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
1.593 +(*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
1.594 +(*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
1.595 +(*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
1.596 +
1.597 +(*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
1.598 +(*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
1.599 +(*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
1.600 +(*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
1.601 +
1.602 +"~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
1.603 +(* Output below with:
1.604 +val sort_varList = sort var_ord;
1.605 +fun var_ord (a,b: term) =
1.606 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1.607 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1.608 + prod_ord string_ord string_ord
1.609 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1.610 +);
1.611 +*)
1.612 +(*+*)val xxx = sort_varList ori3;
1.613 +(*
1.614 +{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
1.615 +{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
1.616 +
1.617 +isa isa2
1.618 +{a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
1.619 + {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
1.620 +{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1.621 + {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1.622 +{a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
1.623 + {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
1.624 + ^^^ ^^^
1.625 +
1.626 +{a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
1.627 + {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
1.628 + ^^^ ^^^
1.629 +{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1.630 + {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1.631 +{a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
1.632 + {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
1.633 +*)
1.634 +
1.635 +
1.636 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.637 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.638 +"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1.639 +val t = TermC.str2term "b * a * a";
1.640 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.641 +if UnparseC.term t = "a \<up> 2 * b" then ()
1.642 +else error "poly.sml: diff.behav. in make_polynomial 21";
1.643 +
1.644 +"~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
1.645 + ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
1.646 +
1.647 +(*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
1.648 +"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
1.649 + (*if*) TermC.is_num num (*else*);
1.650 +
1.651 +"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
1.652 + (*if*) TermC.is_num num (*else*);
1.653 + (*if*) TermC.is_variable num (*then*);
1.654 +
1.655 + val xxx = sort_variables t;
1.656 +(*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
1.657 +
1.658 +
1.659 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.660 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.661 +"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1.662 +val t = TermC.str2term "2*3*a";
1.663 +val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
1.664 +(*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
1.665 +(*
1.666 +## try calc: "Groups.times_class.times"
1.667 +## rls: order_mult_rls_ on: 6 * a
1.668 +### rls: order_mult_ on: 6 * a
1.669 +###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
1.670 +####### try calc: "Poly.is_multUnordered"
1.671 +######## eval asms: "6 * a is_multUnordered = True" (*isa*)
1.672 + = False" (*isa2*)
1.673 +####### calc. to: True (*isa*)
1.674 + False (*isa2*)
1.675 +*)
1.676 +val t = TermC.str2term "(6 * a) is_multUnordered";
1.677 +val SOME
1.678 + (_, t') =
1.679 + eval_is_multUnordered "xxx" () t @{theory};
1.680 +(*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
1.681 +(*+*)else error "6 * a is_multUnordered = False CHANGED";
1.682 +
1.683 +"~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
1.684 + (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
1.685 + (*if*) is_multUnordered arg (*else*);
1.686 +
1.687 +"~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
1.688 + val return =
1.689 + ((is_polyexp t) andalso not (t = sort_variables t));
1.690 +
1.691 +(*+*)return = false; (*isa*)
1.692 +(*+*) is_polyexp t = true; (*isa*)
1.693 +(*+*) not (t = sort_variables t) = false; (*isa*)
1.694 +
1.695 + val xxx = sort_variables t;
1.696 +(*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
1.697 +
1.698 +"-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.699 +"-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.700 +"-------- norm_Poly with AlgEin ----------------------------------------------------------------";
1.701 +val thy = @{theory AlgEin};
1.702 +
1.703 +val SOME (f',_) = rewrite_set_ thy false norm_Poly
1.704 +(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1.705 +if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
1.706 +then ((*norm_Poly NOT COMPLETE -- TODO MG*))
1.707 +else error "norm_Poly changed behavior";
1.708 +(* isa:
1.709 +## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1.710 +### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1.711 +###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1.712 +oben is_addUnordered
1.713 +####### try calc: "Poly.is_addUnordered"
1.714 +######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1.715 +oben is_addUnordered = True"
1.716 +####### calc. to: True
1.717 +####### try calc: "Poly.is_addUnordered"
1.718 +####### try calc: "Poly.is_addUnordered"
1.719 +### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
1.720 +*)
1.721 +"~~~~~ fun sort_monoms , args:"; val (t) =
1.722 + (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
1.723 +(*+*)val t' =
1.724 + sort_monoms t;
1.725 +(*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
1.726 +
1.727 +
1.728 +"-------- complex examples from textbook Schalk I ----------------------------------------------";
1.729 +"-------- complex examples from textbook Schalk I ----------------------------------------------";
1.730 +"-------- complex examples from textbook Schalk I ----------------------------------------------";
1.731 +val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
1.732 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.733 +if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"
1.734 +then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1.735 +
1.736 +"-----SPB Schalk I p.64 No.296a ---";
1.737 +val t = TermC.str2term "(x - a) \<up> 3";
1.738 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.739 +if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"
1.740 +then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.741 +
1.742 +"-----SPB Schalk I p.64 No.296c ---";
1.743 +val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1.744 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.745 +if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
1.746 +then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.747 +
1.748 +"-----SPB Schalk I p.62 No.242c ---";
1.749 +val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
1.750 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.751 +if (UnparseC.term t) = "1"
1.752 +then () else error "poly.sml: diff.behav. in make_polynomial 12";
1.753 +
1.754 +"-----SPB Schalk I p.60 No.209a ---";
1.755 +val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
1.756 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.757 +if UnparseC.term t = "a \<up> 7"
1.758 +then () else error "poly.sml: diff.behav. in make_polynomial 13";
1.759 +
1.760 +"-----SPB Schalk I p.60 No.209d ---";
1.761 +val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1.762 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.763 +if UnparseC.term t = "d \<up> 3"
1.764 +then () else error "poly.sml: diff.behav. in make_polynomial 14";
1.765 +
1.766 +
1.767 +"-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.768 +"-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.769 +"-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
1.770 +"-----SPO ---";
1.771 +val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1.772 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.773 +if UnparseC.term t = "1" then ()
1.774 +else error "poly.sml: diff.behav. in make_polynomial 15";
1.775 +
1.776 +"-----SPO ---";
1.777 +val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
1.778 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.779 +if UnparseC.term t = "a \<up> 2" then ()
1.780 +else error "poly.sml: diff.behav. in make_polynomial 18";
1.781 +"-----SPO ---";
1.782 +val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1.783 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.784 +if (UnparseC.term t) = "1" then ()
1.785 +else error "poly.sml: diff.behav. in make_polynomial 19";
1.786 +"-----SPO ---";
1.787 +val t = TermC.str2term "b + a - b";
1.788 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1.789 +if (UnparseC.term t) = "a" then ()
1.790 +else error "poly.sml: diff.behav. in make_polynomial 20";
1.791 +
1.792 +"-----SPO ---";
1.793 +val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
1.794 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1.795 +if (UnparseC.term t) = "a \<up> 4" then ()
1.796 +else error "poly.sml: diff.behav. in make_polynomial 24";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Fri Jul 16 07:45:06 2021 +0200
2.3 @@ -0,0 +1,709 @@
2.4 +(* Knowledge/poly.sml
2.5 + author: Matthias Goldgruber 2003
2.6 + (c) due to copyright terms
2.7 +
2.8 +LEGEND:
2.9 +WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
2.10 + examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
2.11 +*)
2.12 +
2.13 +"-----------------------------------------------------------------------------------------------";
2.14 +"-----------------------------------------------------------------------------------------------";
2.15 +"table of contents -----------------------------------------------------------------------------";
2.16 +"-----------------------------------------------------------------------------------------------";
2.17 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
2.18 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
2.19 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
2.20 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
2.21 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
2.22 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
2.23 +"-------- examples from textbook Schalk I ------------------------------------------------------";
2.24 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
2.25 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
2.26 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
2.27 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
2.28 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
2.29 +"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
2.30 +"-------- ord_make_polynomial ------------------------------------------------------------------";
2.31 +"-----------------------------------------------------------------------------------------------";
2.32 +"-----------------------------------------------------------------------------------------------";
2.33 +"-----------------------------------------------------------------------------------------------";
2.34 +
2.35 +
2.36 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
2.37 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
2.38 +"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
2.39 +(* indentation indicates call hierarchy:
2.40 +"~~~~~ fun is_addUnordered
2.41 +"~~~~~~~ fun is_polyexp
2.42 +"~~~~~~~ fun sort_monoms
2.43 +"~~~~~~~~~ fun sort_monList
2.44 +"~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
2.45 +"~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
2.46 +"~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
2.47 +"~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
2.48 +"~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
2.49 +"~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
2.50 +"~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
2.51 +"~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
2.52 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
2.53 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
2.54 +"~~~~~ fun is_multUnordered
2.55 +"~~~~~~~ fun sort_variables
2.56 +"~~~~~~~~~ fun sort_varList
2.57 +"~~~~~~~~~~~ fun var_ord
2.58 +"~~~~~~~~~~~~~ fun get_basStr used twice --^^
2.59 +"~~~~~~~~~~~~~ fun get_potStr used twice --^^
2.60 +
2.61 +fun int_ord (i1, i2) =
2.62 +(@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
2.63 + Int.compare (i1, i2)
2.64 +);
2.65 +fun var_ord (a, b) =
2.66 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
2.67 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
2.68 + prod_ord string_ord string_ord
2.69 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
2.70 +);
2.71 +fun var_ord_revPow (a, b: term) =
2.72 +(@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
2.73 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
2.74 + prod_ord string_ord string_ord_rev
2.75 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
2.76 +);
2.77 +fun sort_varList ts =
2.78 +(@{print} {a = "sort_varList", args = UnparseC.terms ts};
2.79 + sort var_ord ts
2.80 +);
2.81 +fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
2.82 + | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
2.83 + | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
2.84 + | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
2.85 + (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
2.86 + is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
2.87 + case (cond x, cond y) of
2.88 + (false, false) =>
2.89 + (case elem_ord (x, y) of
2.90 + EQUAL => dict_cond_ord elem_ord cond (xs, ys)
2.91 + | ord => ord)
2.92 + | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
2.93 + | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
2.94 + | (true, true) => dict_cond_ord elem_ord cond (xs, ys)
2.95 +);
2.96 +fun compare_koeff_ord (xs, ys) =
2.97 +(@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
2.98 + sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
2.99 + string_ord
2.100 + ((koeff2ordStr o get_koeff_of_mon) xs,
2.101 + (koeff2ordStr o get_koeff_of_mon) ys)
2.102 +);
2.103 +fun var_ord (a,b: term) =
2.104 +(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
2.105 + sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
2.106 + prod_ord string_ord string_ord
2.107 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
2.108 +);
2.109 +*)
2.110 +
2.111 +
2.112 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
2.113 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
2.114 +"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
2.115 +(* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
2.116 +
2.117 + sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
2.118 +@{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
2.119 +val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
2.120 +val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
2.121 +
2.122 +val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac;
2.123 +if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*))
2.124 +else error "thm - ?z = - 1 * ?z loops with new numerals";
2.125 +
2.126 +
2.127 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
2.128 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
2.129 +"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
2.130 +val thy = @{theory Partial_Fractions}
2.131 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
2.132 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
2.133 +
2.134 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
2.135 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
2.136 +
2.137 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
2.138 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
2.139 +"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
2.140 +val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
2.141 +val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
2.142 +if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
2.143 + andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
2.144 +then () else error "eval_is_expanded_in x ..changed";
2.145 +
2.146 +val thy = @{theory Partial_Fractions}
2.147 +val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
2.148 +val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
2.149 +if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
2.150 + andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
2.151 +then () else error "eval_is_expanded_in AA ..changed";
2.152 +
2.153 +
2.154 +val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
2.155 +val SOME (id, t') = eval_is_poly_in 0 0 t 0;
2.156 +if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
2.157 + andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
2.158 +then () else error "is_poly_in x ..changed";
2.159 +
2.160 +val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
2.161 +val SOME (id, t') = eval_is_poly_in 0 0 t 0;
2.162 +if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
2.163 + andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
2.164 +then () else error "is_poly_in AA ..changed";
2.165 +
2.166 +
2.167 +val thy = @{theory Partial_Fractions}
2.168 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
2.169 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
2.170 +
2.171 +val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
2.172 +val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
2.173 +
2.174 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
2.175 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
2.176 +"-------- investigate (new 2002) uniary minus --------------------------------------------------";
2.177 +val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
2.178 +TermC.atomty t;
2.179 +(*
2.180 +*** Const (HOL.Trueprop, bool => prop)
2.181 +*** . Const (HOL.eq, real => real => bool)
2.182 +*** . . Const (Groups.minus_class.minus, real => real => real)
2.183 +*** . . . Const (Groups.zero_class.zero, real)
2.184 +*** . . . Var ((x, 0), real)
2.185 +*** . . Const (Groups.uminus_class.uminus, real => real)
2.186 +*** . . . Var ((x, 0), real)
2.187 +*)
2.188 +case t of
2.189 + Const ("HOL.Trueprop", _) $
2.190 + (Const ("HOL.eq", _) $
2.191 + (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
2.192 + Var (("x", 0), _)) $
2.193 + (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
2.194 +| _ => error "internal representation of \"0 - ?x = - ?x\" changed";
2.195 +
2.196 +
2.197 +val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
2.198 +TermC.atomty t;
2.199 +(*
2.200 +***
2.201 +*** Free (-1, real)
2.202 +***
2.203 +*)
2.204 +case t of
2.205 + Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
2.206 +| _ => error "internal representation of \"- 1\" changed";
2.207 +
2.208 +"======= these external values all have the same internal representation";
2.209 +(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
2.210 +(*----------------------------------- vvvvv -------------------------------------------*)
2.211 +val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
2.212 +TermC.atomty t;
2.213 +(**** -------------
2.214 +*** Free ( -x, real)*)
2.215 +case t of
2.216 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
2.217 +| _ => error "internal representation of \"-x\" changed";
2.218 +(*----------------------------------- vvvvv -------------------------------------------*)
2.219 +val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
2.220 +TermC.atomty t;
2.221 +(**** -------------
2.222 +*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
2.223 +case t of
2.224 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
2.225 +| _ => error "internal representation of \"- x\" changed";
2.226 +(*----------------------------------- vvvvvv ------------------------------------------*)
2.227 +val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
2.228 +TermC.atomty t;
2.229 +(**** -------------
2.230 +*** Free ( -x, real)*)
2.231 +case t of
2.232 + Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
2.233 +| _ => error "internal representation of \"-(x)\" changed";
2.234 +
2.235 +
2.236 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
2.237 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
2.238 +"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
2.239 +(* indentation partially indicates call hierarchy:
2.240 +"~~~~~ fun is_addUnordered
2.241 +"~~~~~~~ fun is_polyexp
2.242 +"~~~~~~~ fun sort_monoms
2.243 +"~~~~~~~~~ fun sort_monList
2.244 +"~~~~~~~~~~~ fun koeff_degree_ord
2.245 +"~~~~~~~~~~~~~ fun degree_ord
2.246 +"~~~~~~~~~~~~~~~ fun dict_cond_ord
2.247 +"~~~~~~~~~~~~~~~~~ fun var_ord_revPow
2.248 +"~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
2.249 +"~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
2.250 +"~~~~~~~~~~~~~~~ fun monom_degree
2.251 +"~~~~~~~~~~~~~ fun compare_koeff_ord
2.252 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon
2.253 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr
2.254 +"~~~~~ fun is_multUnordered
2.255 +"~~~~~~~ fun sort_variables
2.256 +"~~~~~~~~~ fun sort_varList
2.257 +"~~~~~~~~~~~ fun var_ord
2.258 +"~~~~~~~~~~~~~ fun get_basStr used twice --^^
2.259 +"~~~~~~~~~~~~~ fun get_potStr used twice --^^
2.260 +*)
2.261 +val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
2.262 +
2.263 + eval_is_addUnordered "xxx" "yyy" t @{theory};
2.264 +"~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
2.265 + (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =
2.266 + ("xxx", "yyy", t, @{theory});
2.267 +
2.268 + (*if*) is_addUnordered arg;
2.269 +"~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
2.270 + ((is_polyexp t) andalso not (t = sort_monoms t));
2.271 +
2.272 + (t = sort_monoms t);
2.273 +"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
2.274 + val ll = map monom2list (poly2list t);
2.275 + val lls =
2.276 +
2.277 + sort_monList ll;
2.278 +"~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
2.279 + val xxx =
2.280 +
2.281 + sort koeff_degree_ord ll(*return value*);
2.282 +"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
2.283 + koeff_degree_ord: term list * term list -> order;
2.284 +(*we check all elements at once..*)
2.285 +val eee1 = ll |> nth 1;
2.286 +val eee2 = ll |> nth 2;
2.287 +val eee3 = ll |> nth 3;
2.288 +val eee3 = ll |> nth 3;
2.289 +val eee4 = ll |> nth 4;
2.290 +
2.291 +if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
2.292 +if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
2.293 +if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
2.294 +if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
2.295 +
2.296 +if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
2.297 +if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
2.298 +if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
2.299 +if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
2.300 +
2.301 +if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
2.302 +if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
2.303 +if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
2.304 +if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
2.305 +
2.306 +if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
2.307 +if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
2.308 +if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
2.309 +if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
2.310 +
2.311 +if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
2.312 +if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
2.313 +if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
2.314 +if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
2.315 +
2.316 +"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
2.317 + degree_ord: term list * term list -> order;
2.318 +
2.319 +if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
2.320 +if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
2.321 +if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
2.322 +if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
2.323 +
2.324 +if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
2.325 +if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
2.326 +if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
2.327 +if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
2.328 +
2.329 +if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
2.330 +if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
2.331 +if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
2.332 +if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
2.333 +
2.334 +if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
2.335 +if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
2.336 +if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
2.337 +if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
2.338 +
2.339 +"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
2.340 +dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
2.341 +dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
2.342 +dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
2.343 +val xxx = dict_cond_ord var_ord_revPow is_nums;
2.344 +(* output from:
2.345 +fun var_ord_revPow (a,b: term) =
2.346 + (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
2.347 + @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
2.348 + prod_ord string_ord string_ord_rev
2.349 + ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
2.350 +*)
2.351 +if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
2.352 +if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
2.353 +if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
2.354 +if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
2.355 +(*-------------------------------------------------------------------------------------*)
2.356 +if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
2.357 +if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
2.358 +if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
2.359 +if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
2.360 +(*-------------------------------------------------------------------------------------*)
2.361 +if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
2.362 +if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
2.363 +if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
2.364 +if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
2.365 +(*-------------------------------------------------------------------------------------*)
2.366 +if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
2.367 +if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
2.368 +if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
2.369 +if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
2.370 +(*-------------------------------------------------------------------------------------*)
2.371 +
2.372 +"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
2.373 +(* we check all at once//*)
2.374 +if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
2.375 +if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
2.376 +if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
2.377 +if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
2.378 +
2.379 +"~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
2.380 + compare_koeff_ord: term list * term list -> order;
2.381 +(* we check all at once//*)
2.382 +if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
2.383 +if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
2.384 +if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
2.385 +if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
2.386 +
2.387 +if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
2.388 +if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
2.389 +if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
2.390 +if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
2.391 +
2.392 +if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
2.393 +if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
2.394 +if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
2.395 +if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
2.396 +
2.397 +if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
2.398 +if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
2.399 +if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
2.400 +if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
2.401 +
2.402 +"~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
2.403 + get_koeff_of_mon: term list -> term option;
2.404 +
2.405 +val SOME xxx1 = get_koeff_of_mon eee1;
2.406 +val SOME xxx2 = get_koeff_of_mon eee2;
2.407 +val SOME xxx3 = get_koeff_of_mon eee3;
2.408 +val NONE = get_koeff_of_mon eee4;
2.409 +
2.410 +if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
2.411 +if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
2.412 +if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
2.413 +
2.414 +"~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
2.415 + koeff2ordStr: term option -> string;
2.416 +if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
2.417 +if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
2.418 +if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
2.419 +if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
2.420 +
2.421 +
2.422 +"-------- examples from textbook Schalk I ------------------------------------------------------";
2.423 +"-------- examples from textbook Schalk I ------------------------------------------------------";
2.424 +"-------- examples from textbook Schalk I ------------------------------------------------------";
2.425 +"-----SPB Schalk I p.63 No.267b ---";
2.426 +val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
2.427 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.428 +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"
2.429 +then () else error "poly.sml: diff.behav. in make_polynomial 1";
2.430 +
2.431 +"-----SPB Schalk I p.63 No.275b ---";
2.432 +val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
2.433 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.434 +if UnparseC.term t =
2.435 + "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"
2.436 +then () else error "poly.sml: diff.behav. in make_polynomial 2";
2.437 +
2.438 +"-----SPB Schalk I p.63 No.279b ---";
2.439 +val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
2.440 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.441 +if UnparseC.term t =
2.442 + ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
2.443 + "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
2.444 + "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
2.445 + " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
2.446 +then () else error "poly.sml: diff.behav. in make_polynomial 3";
2.447 +(*associate poly*)
2.448 +
2.449 +"-----SPB Schalk I p.63 No.291 ---";
2.450 +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)))";
2.451 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.452 +if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
2.453 +then () else error "poly.sml: diff.behav. in make_polynomial 4";
2.454 +
2.455 +"-----SPB Schalk I p.64 No.295c ---";
2.456 +val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
2.457 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.458 +if UnparseC.term t =
2.459 + "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"
2.460 +then ()else error "poly.sml: diff.behav. in make_polynomial 5";
2.461 +
2.462 +"-----SPB Schalk I p.64 No.299a ---";
2.463 +val t = TermC.str2term "(x - y)*(x + y)";
2.464 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.465 +if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
2.466 +then () else error "poly.sml: diff.behav. in make_polynomial 6";
2.467 +
2.468 +"-----SPB Schalk I p.64 No.300c ---";
2.469 +val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
2.470 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.471 +if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
2.472 +then () else error "poly.sml: diff.behav. in make_polynomial 7";
2.473 +
2.474 +"-----SPB Schalk I p.64 No.302 ---";
2.475 +val t = TermC.str2term
2.476 + "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
2.477 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
2.478 +if UnparseC.term t = "0"
2.479 +then () else error "poly.sml: diff.behav. in make_polynomial 8";
2.480 +(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
2.481 +
2.482 +"-----SPB Schalk I p.64 No.306a ---";
2.483 +val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
2.484 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.485 +if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
2.486 +else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";
2.487 +
2.488 +(*WN071729 when reducing "rls reduce_012_" for Schaerding,
2.489 +the above resulted in the term below ... but reduces from then correctly*)
2.490 +val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
2.491 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.492 +if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
2.493 +then () else error "poly.sml: diff.behav. in make_polynomial 9b";
2.494 +
2.495 +"-----SPB Schalk I p.64 No.296a ---";
2.496 +val t = TermC.str2term "(x - a) \<up> 3";
2.497 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.498 +
2.499 +val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc";
2.500 +
2.501 +if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
2.502 +then () else error "poly.sml: diff.behav. in make_polynomial 10";
2.503 +
2.504 +"-----SPB Schalk I p.64 No.296c ---";
2.505 +val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
2.506 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.507 +if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
2.508 +then () else error "poly.sml: diff.behav. in make_polynomial 11";
2.509 +
2.510 +"-----SPB Schalk I p.62 No.242c ---";
2.511 +val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
2.512 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.513 +if UnparseC.term t = "1"
2.514 +then () else error "poly.sml: diff.behav. in make_polynomial 12";
2.515 +
2.516 +"-----SPB Schalk I p.60 No.209a ---";
2.517 +val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
2.518 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.519 +if UnparseC.term t = "a \<up> 7"
2.520 +then () else error "poly.sml: diff.behav. in make_polynomial 13";
2.521 +
2.522 +"-----SPB Schalk I p.60 No.209d ---";
2.523 +val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
2.524 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.525 +if UnparseC.term t = "d \<up> 3"
2.526 +then () else error "poly.sml: diff.behav. in make_polynomial 14";
2.527 +
2.528 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
2.529 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
2.530 +"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
2.531 +"-----Schalk I p.64 No.303 ---";
2.532 +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)";
2.533 +(*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
2.534 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.535 +if UnparseC.term t = "1280 * b \<up> 4"
2.536 +then () else error "poly.sml: diff.behav. in make_polynomial 14b";
2.537 +(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
2.538 +(*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
2.539 +
2.540 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
2.541 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
2.542 +"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
2.543 +"-----SPO ---";
2.544 +val t = TermC.str2term "a + a + a";
2.545 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.546 +if UnparseC.term t = "3 * a" then ()
2.547 +else error "poly.sml: diff.behav. in make_polynomial 16";
2.548 +"-----SPO ---";
2.549 +val t = TermC.str2term "a + b + b + b";
2.550 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.551 +if UnparseC.term t = "a + 3 * b" then ()
2.552 +else error "poly.sml: diff.behav. in make_polynomial 17";
2.553 +"-----SPO ---";
2.554 +val t = TermC.str2term "b * a * a";
2.555 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.556 +if UnparseC.term t = "a \<up> 2 * b" then ()
2.557 +else error "poly.sml: diff.behav. in make_polynomial 21";
2.558 +"-----SPO ---";
2.559 +val t = TermC.str2term "(a \<up> 2) \<up> 3";
2.560 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.561 +if UnparseC.term t = "a \<up> 6" then ()
2.562 +else error "poly.sml: diff.behav. in make_polynomial 22";
2.563 +"-----SPO ---";
2.564 +val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
2.565 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
2.566 +if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
2.567 +else error "poly.sml: diff.behav. in make_polynomial 23";
2.568 +"-----SPO ---";
2.569 +val t = TermC.str2term "a * b * b \<up> (-1) + a";
2.570 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
2.571 +if UnparseC.term t = "2 * a" then ()
2.572 +else error "poly.sml: diff.behav. in make_polynomial 25";
2.573 +"-----SPO ---";
2.574 +val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
2.575 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
2.576 +if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
2.577 +then () else error "poly.sml: diff.behav. in make_polynomial 26";
2.578 +
2.579 +(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
2.580 +"-----SPO ---";
2.581 +val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
2.582 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
2.583 +if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
2.584 +then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
2.585 +
2.586 +val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
2.587 +val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
2.588 +if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
2.589 +then () else error "poly.sml: diff.behav. in make_polynomial 28";
2.590 +
2.591 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
2.592 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
2.593 +"-------- check pbl 'polynomial simplification' -----------------------------------------------";
2.594 +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"];
2.595 +"-----0 ---";
2.596 +case Refine.refine fmz ["polynomial", "simplification"] of
2.597 + [M_Match.Matches (["polynomial", "simplification"], _)] => ()
2.598 + | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
2.599 +(*...if there is an error, then ...*)
2.600 +
2.601 +"-----1 ---";
2.602 +(*default_print_depth 7;*)
2.603 +val pbt = Problem.from_store ["polynomial", "simplification"];
2.604 +(*default_print_depth 3;*)
2.605 +(*if there is ...
2.606 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
2.607 +... then Rewrite.trace_on:*)
2.608 +
2.609 +"-----2 ---";
2.610 +Rewrite.trace_on := false;
2.611 +M_Match.match_pbl fmz pbt;
2.612 +Rewrite.trace_on := false;
2.613 +(*... if there is no rewrite, then there is something wrong with prls*)
2.614 +
2.615 +"-----3 ---";
2.616 +(*default_print_depth 7;*)
2.617 +val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];
2.618 +(*default_print_depth 3;*)
2.619 +val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
2.620 +val SOME (t',_) = rewrite_set_ thy false prls t;
2.621 +if t' = @{term True} then ()
2.622 +else error "poly.sml: diff.behav. in check pbl 'polynomial..";
2.623 +(*... if this works, but --1-- does still NOT work, check types:*)
2.624 +
2.625 +"-----4 ---";
2.626 +(*show_types:=true;*)
2.627 +(*
2.628 +> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
2.629 +val wh = [False "(t_::real => real) (is_polyexp::real)"]
2.630 +...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
2.631 +val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
2.632 +(*show_types:=false;*)
2.633 +
2.634 +
2.635 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
2.636 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
2.637 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
2.638 +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"];
2.639 +val (dI',pI',mI') =
2.640 + ("Poly",["polynomial", "simplification"],
2.641 + ["simplification", "for_polynomials"]);
2.642 +val p = e_pos'; val c = [];
2.643 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.644 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)
2.645 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
2.646 +
2.647 +(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
2.648 +(*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"
2.649 +(*+*)then () else error "No.267b: I_Model.T CHANGED";
2.650 +( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
2.651 +
2.652 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
2.653 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
2.654 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
2.655 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
2.656 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
2.657 +
2.658 +(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
2.659 +(*+*)then () else error "";
2.660 +
2.661 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
2.662 +
2.663 +(*+*)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"
2.664 +(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
2.665 +
2.666 +(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
2.667 +
2.668 +
2.669 +
2.670 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
2.671 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
2.672 +"-------- interSteps for Schalk 299a -----------------------------------------------------------";
2.673 +reset_states ();
2.674 +CalcTree
2.675 +[(["Term ((x - y)*(x + (y::real)))", "normalform N"],
2.676 + ("Poly",["polynomial", "simplification"],
2.677 + ["simplification", "for_polynomials"]))];
2.678 +Iterator 1;
2.679 +moveActiveRoot 1;
2.680 +autoCalculate 1 CompleteCalc;
2.681 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
2.682 +
2.683 +interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
2.684 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
2.685 +if existpt' ([1,1], Frm) pt then ()
2.686 +else error "poly.sml: interSteps doesnt work again 1";
2.687 +
2.688 +interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
2.689 +val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
2.690 +(*============ inhibit exn WN120316 ==============================================
2.691 +if existpt' ([1,1,1], Frm) pt then ()
2.692 +else error "poly.sml: interSteps doesnt work again 2";
2.693 +============ inhibit exn WN120316 ==============================================*)
2.694 +
2.695 +"-------- ord_make_polynomial ------------------------------------------------------------------";
2.696 +"-------- ord_make_polynomial ------------------------------------------------------------------";
2.697 +"-------- ord_make_polynomial ------------------------------------------------------------------";
2.698 +val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
2.699 +val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
2.700 +
2.701 +if ord_make_polynomial true thy [] (t1, t2) then ()
2.702 +else error "poly.sml: diff.behav. in ord_make_polynomial";
2.703 +(*SO: WHY IS THERE NO REWRITING ...*)
2.704 +
2.705 +val term = TermC.str2term "2*b + (3*a + 3*b)";
2.706 +(*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
2.707 +(*
2.708 +WHY IS THERE NO REWRITING ?!?
2.709 +most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
2.710 +while order_add_mult uses isac's rewriter -- and this is used rarely!
2.711 +*)
2.712 +
3.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri Jul 16 06:57:34 2021 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,1439 +0,0 @@
3.4 -(* Knowledge/poly.sml
3.5 - author: Matthias Goldgruber 2003
3.6 - (c) due to copyright terms
3.7 -
3.8 -LEGEND:
3.9 -WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
3.10 - examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
3.11 -*)
3.12 -
3.13 -"-----------------------------------------------------------------------------------------------";
3.14 -"-----------------------------------------------------------------------------------------------";
3.15 -"table of contents -----------------------------------------------------------------------------";
3.16 -"-----------------------------------------------------------------------------------------------";
3.17 -"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
3.18 -"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
3.19 -"-------- fun is_polyexp -----------------------------------------------------------------------";
3.20 -"-------- fun has_degree_in --------------------------------------------------------------------";
3.21 -"-------- fun mono_deg_in ----------------------------------------------------------------------";
3.22 -"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
3.23 -"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
3.24 -"-------- investigate (new 2002) uniary minus --------------------------------------------------";
3.25 -"-------- fun sort_variables -------------------------------------------------------------------";
3.26 -"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
3.27 -"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
3.28 -"-------- check make_polynomial with simple terms ----------------------------------------------";
3.29 -"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
3.30 -"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
3.31 -"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
3.32 -"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
3.33 -"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
3.34 -"-------- examples from textbook Schalk I ------------------------------------------------------";
3.35 -"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
3.36 -"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
3.37 -"-------- check pbl 'polynomial simplification' -----------------------------------------------";
3.38 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
3.39 -"-------- interSteps for Schalk 299a -----------------------------------------------------------";
3.40 -"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
3.41 -"-------- ord_make_polynomial ------------------------------------------------------------------";
3.42 -"-----------------------------------------------------------------------------------------------";
3.43 -"-----------------------------------------------------------------------------------------------";
3.44 -"-----------------------------------------------------------------------------------------------";
3.45 -
3.46 -
3.47 -"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
3.48 -"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
3.49 -"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
3.50 -(* indentation indicates call hierarchy:
3.51 -"~~~~~ fun is_addUnordered
3.52 -"~~~~~~~ fun is_polyexp
3.53 -"~~~~~~~ fun sort_monoms
3.54 -"~~~~~~~~~ fun sort_monList
3.55 -"~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
3.56 -"~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
3.57 -"~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
3.58 -"~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
3.59 -"~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
3.60 -"~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
3.61 -"~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
3.62 -"~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
3.63 -"~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
3.64 -"~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
3.65 -"~~~~~ fun is_multUnordered
3.66 -"~~~~~~~ fun sort_variables
3.67 -"~~~~~~~~~ fun sort_varList
3.68 -"~~~~~~~~~~~ fun var_ord
3.69 -"~~~~~~~~~~~~~ fun get_basStr used twice --^^
3.70 -"~~~~~~~~~~~~~ fun get_potStr used twice --^^
3.71 -
3.72 -fun int_ord (i1, i2) =
3.73 -(@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
3.74 - Int.compare (i1, i2)
3.75 -);
3.76 -fun var_ord (a, b) =
3.77 -(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
3.78 - sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
3.79 - prod_ord string_ord string_ord
3.80 - ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
3.81 -);
3.82 -fun var_ord_revPow (a, b: term) =
3.83 -(@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
3.84 - sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
3.85 - prod_ord string_ord string_ord_rev
3.86 - ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
3.87 -);
3.88 -fun sort_varList ts =
3.89 -(@{print} {a = "sort_varList", args = UnparseC.terms ts};
3.90 - sort var_ord ts
3.91 -);
3.92 -fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
3.93 - | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
3.94 - | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
3.95 - | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
3.96 - (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
3.97 - is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
3.98 - case (cond x, cond y) of
3.99 - (false, false) =>
3.100 - (case elem_ord (x, y) of
3.101 - EQUAL => dict_cond_ord elem_ord cond (xs, ys)
3.102 - | ord => ord)
3.103 - | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
3.104 - | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
3.105 - | (true, true) => dict_cond_ord elem_ord cond (xs, ys)
3.106 -);
3.107 -fun compare_koeff_ord (xs, ys) =
3.108 -(@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
3.109 - sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
3.110 - string_ord
3.111 - ((koeff2ordStr o get_koeff_of_mon) xs,
3.112 - (koeff2ordStr o get_koeff_of_mon) ys)
3.113 -);
3.114 -fun var_ord (a,b: term) =
3.115 -(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
3.116 - sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
3.117 - prod_ord string_ord string_ord
3.118 - ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
3.119 -);
3.120 -*)
3.121 -
3.122 -
3.123 -"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
3.124 -"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
3.125 -"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
3.126 -(* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
3.127 -
3.128 - sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
3.129 -@{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
3.130 -val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
3.131 -val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
3.132 -
3.133 -val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac;
3.134 -if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*))
3.135 -else error "thm - ?z = - 1 * ?z loops with new numerals";
3.136 -
3.137 -
3.138 -"-------- fun is_polyexp -----------------------------------------------------------------------";
3.139 -"-------- fun is_polyexp -----------------------------------------------------------------------";
3.140 -"-------- fun is_polyexp -----------------------------------------------------------------------";
3.141 -val t = TermC.str2term "x / x";
3.142 -if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
3.143 -
3.144 -val t = TermC.str2term "-1 * A * 3";
3.145 -if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
3.146 -
3.147 -val t = TermC.str2term "-1 * AA * 3";
3.148 -if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
3.149 -
3.150 -val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
3.151 -if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
3.152 -
3.153 -"-------- fun has_degree_in --------------------------------------------------------------------";
3.154 -"-------- fun has_degree_in --------------------------------------------------------------------";
3.155 -"-------- fun has_degree_in --------------------------------------------------------------------";
3.156 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.157 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
3.158 -if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
3.159 -
3.160 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.161 -val t = (Thm.term_of o the o (TermC.parse thy)) "1";
3.162 -if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
3.163 -
3.164 -(*----------*)
3.165 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.166 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
3.167 -if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
3.168 -
3.169 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.170 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
3.171 -if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
3.172 -
3.173 -(*----------*)
3.174 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.175 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
3.176 -if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
3.177 -
3.178 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.179 -val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
3.180 -if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
3.181 -
3.182 -(*----------*)
3.183 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.184 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
3.185 -if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
3.186 -
3.187 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.188 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
3.189 -if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
3.190 -
3.191 -(*----------*)
3.192 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.193 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
3.194 -if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
3.195 -
3.196 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.197 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
3.198 -if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
3.199 -
3.200 -(*----------*)
3.201 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.202 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
3.203 -if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
3.204 -
3.205 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.206 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
3.207 -if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
3.208 -
3.209 -(*----------*)
3.210 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.211 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
3.212 -if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
3.213 -
3.214 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.215 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
3.216 -if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
3.217 -
3.218 -(*----------*)
3.219 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.220 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
3.221 -if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
3.222 -
3.223 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.224 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.225 -if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
3.226 -
3.227 -(*----------*)
3.228 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.229 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
3.230 -if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
3.231 -
3.232 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.233 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
3.234 -if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
3.235 -
3.236 -"-------- fun mono_deg_in ----------------------------------------------------------------------";
3.237 -"-------- fun mono_deg_in ----------------------------------------------------------------------";
3.238 -"-------- fun mono_deg_in ----------------------------------------------------------------------";
3.239 -val v = (Thm.term_of o the o (TermC.parse thy)) "x";
3.240 -
3.241 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
3.242 -if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
3.243 -
3.244 -val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
3.245 -if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
3.246 -
3.247 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
3.248 -if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
3.249 -
3.250 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
3.251 -if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
3.252 -
3.253 -val t = (Thm.term_of o the o (TermC.parse thy)) "x";
3.254 -if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
3.255 -
3.256 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
3.257 -if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
3.258 -
3.259 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
3.260 -if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
3.261 -
3.262 -(*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
3.263 -val thy = @{theory Partial_Fractions}
3.264 -val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.265 -
3.266 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
3.267 -if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
3.268 -
3.269 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
3.270 -if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
3.271 -
3.272 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
3.273 -if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
3.274 -
3.275 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
3.276 -if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
3.277 -
3.278 -val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
3.279 -if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
3.280 -
3.281 -val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
3.282 -if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
3.283 -
3.284 -val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
3.285 -if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
3.286 -
3.287 -"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
3.288 -"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
3.289 -"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
3.290 -val thy = @{theory Partial_Fractions}
3.291 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
3.292 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
3.293 -
3.294 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
3.295 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
3.296 -
3.297 -"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
3.298 -"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
3.299 -"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
3.300 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
3.301 -val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
3.302 -if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
3.303 - andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
3.304 -then () else error "eval_is_expanded_in x ..changed";
3.305 -
3.306 -val thy = @{theory Partial_Fractions}
3.307 -val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
3.308 -val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
3.309 -if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
3.310 - andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
3.311 -then () else error "eval_is_expanded_in AA ..changed";
3.312 -
3.313 -
3.314 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
3.315 -val SOME (id, t') = eval_is_poly_in 0 0 t 0;
3.316 -if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
3.317 - andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
3.318 -then () else error "is_poly_in x ..changed";
3.319 -
3.320 -val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
3.321 -val SOME (id, t') = eval_is_poly_in 0 0 t 0;
3.322 -if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
3.323 - andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
3.324 -then () else error "is_poly_in AA ..changed";
3.325 -
3.326 -
3.327 -val thy = @{theory Partial_Fractions}
3.328 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
3.329 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
3.330 -
3.331 -val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
3.332 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
3.333 -
3.334 -"-------- investigate (new 2002) uniary minus --------------------------------------------------";
3.335 -"-------- investigate (new 2002) uniary minus --------------------------------------------------";
3.336 -"-------- investigate (new 2002) uniary minus --------------------------------------------------";
3.337 -val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
3.338 -TermC.atomty t;
3.339 -(*
3.340 -*** Const (HOL.Trueprop, bool => prop)
3.341 -*** . Const (HOL.eq, real => real => bool)
3.342 -*** . . Const (Groups.minus_class.minus, real => real => real)
3.343 -*** . . . Const (Groups.zero_class.zero, real)
3.344 -*** . . . Var ((x, 0), real)
3.345 -*** . . Const (Groups.uminus_class.uminus, real => real)
3.346 -*** . . . Var ((x, 0), real)
3.347 -*)
3.348 -case t of
3.349 - Const ("HOL.Trueprop", _) $
3.350 - (Const ("HOL.eq", _) $
3.351 - (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
3.352 - Var (("x", 0), _)) $
3.353 - (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
3.354 -| _ => error "internal representation of \"0 - ?x = - ?x\" changed";
3.355 -
3.356 -
3.357 -val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
3.358 -TermC.atomty t;
3.359 -(*
3.360 -***
3.361 -*** Free (-1, real)
3.362 -***
3.363 -*)
3.364 -case t of
3.365 - Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
3.366 -| _ => error "internal representation of \"- 1\" changed";
3.367 -
3.368 -"======= these external values all have the same internal representation";
3.369 -(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
3.370 -(*----------------------------------- vvvvv -------------------------------------------*)
3.371 -val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
3.372 -TermC.atomty t;
3.373 -(**** -------------
3.374 -*** Free ( -x, real)*)
3.375 -case t of
3.376 - Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.377 -| _ => error "internal representation of \"-x\" changed";
3.378 -(*----------------------------------- vvvvv -------------------------------------------*)
3.379 -val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
3.380 -TermC.atomty t;
3.381 -(**** -------------
3.382 -*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
3.383 -case t of
3.384 - Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.385 -| _ => error "internal representation of \"- x\" changed";
3.386 -(*----------------------------------- vvvvvv ------------------------------------------*)
3.387 -val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
3.388 -TermC.atomty t;
3.389 -(**** -------------
3.390 -*** Free ( -x, real)*)
3.391 -case t of
3.392 - Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
3.393 -| _ => error "internal representation of \"-(x)\" changed";
3.394 -
3.395 -
3.396 -"-------- fun sort_variables -------------------------------------------------------------------";
3.397 -"-------- fun sort_variables -------------------------------------------------------------------";
3.398 -"-------- fun sort_variables -------------------------------------------------------------------";
3.399 -if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
3.400 -else error "lexicographic order CHANGED";
3.401 -
3.402 -(*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
3.403 -val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
3.404 -val t' = sort_variables t;
3.405 -if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
3.406 -else error "sort_variables 3 * b + a * 2 CHANGED";
3.407 -
3.408 -"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
3.409 - val ll = map monom2list (poly2list t);
3.410 -
3.411 -(*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
3.412 -(*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
3.413 -(*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
3.414 -(*+*) ] = map monom2list (poly2list t);
3.415 -
3.416 - val lls = map sort_varList ll;
3.417 -
3.418 -(*+*)case map sort_varList ll of
3.419 -(*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
3.420 -(*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
3.421 -(*+*) ] => ()
3.422 -(*+*)| _ => error "map sort_varList CHANGED";
3.423 -
3.424 - val T = type_of t;
3.425 - val ls = map (create_monom T) lls;
3.426 -
3.427 -(*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
3.428 -(*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
3.429 -
3.430 -(*+*)case map (create_monom T) lls of
3.431 -(*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
3.432 -(*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
3.433 -(*+*) ] => ()
3.434 -(*+*)| _ => error "map (create_monom T) CHANGED";
3.435 -
3.436 - val xxx = (*in*) create_polynom T ls (*end*);
3.437 -
3.438 -(*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
3.439 -(*+*)else error "create_polynom CHANGED";
3.440 -(* done by rewriting> 2 * a + 3 * b ? *)
3.441 -
3.442 -(*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
3.443 -val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
3.444 -val t' = sort_variables t;
3.445 -if UnparseC.term t' = "3 * a + - 2 * a" then ()
3.446 -else error "sort_variables 3 * a + - 2 * a CHANGED";
3.447 -
3.448 -"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
3.449 - val ll = map monom2list (poly2list t);
3.450 -
3.451 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
3.452 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
3.453 -(*+*) ] = map monom2list (poly2list t);
3.454 -
3.455 - val lls = map
3.456 - sort_varList ll;
3.457 -
3.458 -(*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
3.459 -(*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
3.460 -(*+*) ] = map sort_varList ll;
3.461 -
3.462 - map sort_varList ll;
3.463 -"~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
3.464 -val sorted = sort var_ord ts;
3.465 -
3.466 -(*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
3.467 -(*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
3.468 -
3.469 -
3.470 -(*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
3.471 -(*+*)then () else error "get_basStr - 2 CHANGED";
3.472 -(*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
3.473 -(*+*)then () else error "get_basStr a CHANGED";
3.474 -
3.475 -
3.476 -"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
3.477 -"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
3.478 -"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
3.479 -(* indentation partially indicates call hierarchy:
3.480 -"~~~~~ fun is_addUnordered
3.481 -"~~~~~~~ fun is_polyexp
3.482 -"~~~~~~~ fun sort_monoms
3.483 -"~~~~~~~~~ fun sort_monList
3.484 -"~~~~~~~~~~~ fun koeff_degree_ord
3.485 -"~~~~~~~~~~~~~ fun degree_ord
3.486 -"~~~~~~~~~~~~~~~ fun dict_cond_ord
3.487 -"~~~~~~~~~~~~~~~~~ fun var_ord_revPow
3.488 -"~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
3.489 -"~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
3.490 -"~~~~~~~~~~~~~~~ fun monom_degree
3.491 -"~~~~~~~~~~~~~ fun compare_koeff_ord
3.492 -"~~~~~~~~~~~~~~~ fun get_koeff_of_mon
3.493 -"~~~~~~~~~~~~~~~~~ fun koeff2ordStr
3.494 -"~~~~~ fun is_multUnordered
3.495 -"~~~~~~~ fun sort_variables
3.496 -"~~~~~~~~~ fun sort_varList
3.497 -"~~~~~~~~~~~ fun var_ord
3.498 -"~~~~~~~~~~~~~ fun get_basStr used twice --^^
3.499 -"~~~~~~~~~~~~~ fun get_potStr used twice --^^
3.500 -*)
3.501 -val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
3.502 -
3.503 - eval_is_addUnordered "xxx" "yyy" t @{theory};
3.504 -"~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
3.505 - (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =
3.506 - ("xxx", "yyy", t, @{theory});
3.507 -
3.508 - (*if*) is_addUnordered arg;
3.509 -"~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
3.510 - ((is_polyexp t) andalso not (t = sort_monoms t));
3.511 -
3.512 - (t = sort_monoms t);
3.513 -"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
3.514 - val ll = map monom2list (poly2list t);
3.515 - val lls =
3.516 -
3.517 - sort_monList ll;
3.518 -"~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
3.519 - val xxx =
3.520 -
3.521 - sort koeff_degree_ord ll(*return value*);
3.522 -"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
3.523 - koeff_degree_ord: term list * term list -> order;
3.524 -(*we check all elements at once..*)
3.525 -val eee1 = ll |> nth 1;
3.526 -val eee2 = ll |> nth 2;
3.527 -val eee3 = ll |> nth 3;
3.528 -val eee3 = ll |> nth 3;
3.529 -val eee4 = ll |> nth 4;
3.530 -
3.531 -if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
3.532 -if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
3.533 -if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
3.534 -if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
3.535 -
3.536 -if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
3.537 -if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
3.538 -if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
3.539 -if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
3.540 -
3.541 -if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
3.542 -if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
3.543 -if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
3.544 -if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
3.545 -
3.546 -if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
3.547 -if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
3.548 -if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
3.549 -if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
3.550 -
3.551 -if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
3.552 -if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
3.553 -if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
3.554 -if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
3.555 -
3.556 -"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
3.557 - degree_ord: term list * term list -> order;
3.558 -
3.559 -if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
3.560 -if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
3.561 -if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
3.562 -if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
3.563 -
3.564 -if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
3.565 -if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
3.566 -if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
3.567 -if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
3.568 -
3.569 -if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
3.570 -if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
3.571 -if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
3.572 -if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
3.573 -
3.574 -if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
3.575 -if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
3.576 -if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
3.577 -if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
3.578 -
3.579 -"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
3.580 -dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
3.581 -dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
3.582 -dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
3.583 -val xxx = dict_cond_ord var_ord_revPow is_nums;
3.584 -(* output from:
3.585 -fun var_ord_revPow (a,b: term) =
3.586 - (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
3.587 - @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
3.588 - prod_ord string_ord string_ord_rev
3.589 - ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
3.590 -*)
3.591 -if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
3.592 -if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
3.593 -if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
3.594 -if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
3.595 -(*-------------------------------------------------------------------------------------*)
3.596 -if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
3.597 -if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
3.598 -if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
3.599 -if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
3.600 -(*-------------------------------------------------------------------------------------*)
3.601 -if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
3.602 -if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
3.603 -if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
3.604 -if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
3.605 -(*-------------------------------------------------------------------------------------*)
3.606 -if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
3.607 -if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
3.608 -if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
3.609 -if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
3.610 -(*-------------------------------------------------------------------------------------*)
3.611 -
3.612 -"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
3.613 -(* we check all at once//*)
3.614 -if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
3.615 -if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
3.616 -if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
3.617 -if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
3.618 -
3.619 -"~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
3.620 - compare_koeff_ord: term list * term list -> order;
3.621 -(* we check all at once//*)
3.622 -if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
3.623 -if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
3.624 -if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
3.625 -if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
3.626 -
3.627 -if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
3.628 -if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
3.629 -if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
3.630 -if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
3.631 -
3.632 -if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
3.633 -if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
3.634 -if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
3.635 -if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
3.636 -
3.637 -if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
3.638 -if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
3.639 -if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
3.640 -if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
3.641 -
3.642 -"~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
3.643 - get_koeff_of_mon: term list -> term option;
3.644 -
3.645 -val SOME xxx1 = get_koeff_of_mon eee1;
3.646 -val SOME xxx2 = get_koeff_of_mon eee2;
3.647 -val SOME xxx3 = get_koeff_of_mon eee3;
3.648 -val NONE = get_koeff_of_mon eee4;
3.649 -
3.650 -if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
3.651 -if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
3.652 -if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
3.653 -
3.654 -"~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
3.655 - koeff2ordStr: term option -> string;
3.656 -if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
3.657 -if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
3.658 -if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
3.659 -if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
3.660 -
3.661 -
3.662 -"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
3.663 -"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
3.664 -"-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
3.665 -val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
3.666 -Rewrite.trace_on := false;
3.667 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.668 - UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
3.669 -if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
3.670 -else error "poly.sml: diff.behav. in make_polynomial 23";
3.671 -
3.672 -(** )
3.673 -## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
3.674 -### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
3.675 -###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
3.676 -####### try calc: "Poly.is_addUnordered"
3.677 -######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
3.678 - True" (*isa2*)
3.679 -####### calc. to: False (*isa*)
3.680 - True (*isa2*)
3.681 -( **)
3.682 - if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
3.683 -else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
3.684 -"~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
3.685 - ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
3.686 -
3.687 -(*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
3.688 -
3.689 -(*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
3.690 -"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
3.691 - val ll = map monom2list (poly2list t);
3.692 - val lls = sort_monList ll;
3.693 -
3.694 -(*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
3.695 -(*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
3.696 -
3.697 -"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
3.698 -(* we check all elements at once..*)
3.699 -val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
3.700 -val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
3.701 -
3.702 -(*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
3.703 -(*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
3.704 -(*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
3.705 -(*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
3.706 -(* isa -- isa2:
3.707 -(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
3.708 -(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
3.709 -(*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
3.710 -
3.711 -(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
3.712 -
3.713 -(*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
3.714 -
3.715 -(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
3.716 -(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
3.717 -(*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
3.718 -val it = true: bool
3.719 -val it = true: bool
3.720 -val it = true: bool
3.721 -val it = true: bool*)
3.722 -
3.723 -"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
3.724 -(*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
3.725 -(*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
3.726 -(*{a = "int_ord (4, 10003) = ", z = LESS} isa
3.727 - {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
3.728 -(*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
3.729 -(*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
3.730 -(* isa -- isa2:
3.731 -(*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
3.732 - {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
3.733 -(*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
3.734 -(*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
3.735 -(*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
3.736 -(*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
3.737 -(*1*){a = "dict_cond_ord ([], [])"} (*isa*)
3.738 -
3.739 -(*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
3.740 - {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
3.741 - {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
3.742 -(*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
3.743 -
3.744 -(*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
3.745 - {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
3.746 - {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
3.747 -(*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
3.748 -
3.749 -(*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
3.750 - {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
3.751 -(*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
3.752 -(*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
3.753 -(*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
3.754 -(*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
3.755 -(*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
3.756 -
3.757 -val it = true: bool
3.758 -val it = false: bool
3.759 -val it = false: bool
3.760 -val it = true: bool
3.761 -*)
3.762 -
3.763 -(*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
3.764 -"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
3.765 -"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
3.766 - (*if*) (is_nums x) (*else*);
3.767 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
3.768 - (*case*) x (*of*);
3.769 -(*+*)UnparseC.term x = "x \<up> 2";
3.770 - (*if*) TermC.is_num t (*then*);
3.771 -
3.772 - counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
3.773 -"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
3.774 - (*if*) (is_nums x) (*else*);
3.775 - val (Const ("Transcendental.powr", _) $ Free _ $ t) =
3.776 - (*case*) x (*of*);
3.777 -(*+*)UnparseC.term x = "y \<up> 2";
3.778 - (*if*) TermC.is_num t (*then*);
3.779 -
3.780 - val return =
3.781 - counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
3.782 -if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
3.783 -( *---------------------------------------------------------------------------------OPEN local/*)
3.784 -
3.785 -(*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
3.786 -else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
3.787 -"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
3.788 -"~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
3.789 - (*if*) (is_nums x) (*else*);
3.790 -val (Const ("Transcendental.powr", _) $ Free _ $ t) =
3.791 - (*case*) x (*of*);
3.792 -(*+*)UnparseC.term x = "x \<up> 3";
3.793 - (*if*) TermC.is_num t (*then*);
3.794 -
3.795 - counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
3.796 -"~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
3.797 - (*if*) (is_nums x) (*else*);
3.798 -val _ = (*the default case*)
3.799 - (*case*) x (*of*);
3.800 -( *---------------------------------------------------------------------------------OPEN local/*)
3.801 -
3.802 -"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
3.803 -val xxx = dict_cond_ord var_ord_revPow is_nums;
3.804 -(*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
3.805 -(*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
3.806 -(*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
3.807 -(*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
3.808 -
3.809 -
3.810 -"-------- check make_polynomial with simple terms ----------------------------------------------";
3.811 -"-------- check make_polynomial with simple terms ----------------------------------------------";
3.812 -"-------- check make_polynomial with simple terms ----------------------------------------------";
3.813 -"----- check 1 ---";
3.814 -val t = TermC.str2term "2*3*a";
3.815 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.816 -if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
3.817 -
3.818 -"----- check 2 ---";
3.819 -val t = TermC.str2term "2*a + 3*a";
3.820 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.821 -if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
3.822 -
3.823 -"----- check 3 ---";
3.824 -val t = TermC.str2term "2*a + 3*a + 3*a";
3.825 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.826 -if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
3.827 -
3.828 -"----- check 4 ---";
3.829 -val t = TermC.str2term "3*a - 2*a";
3.830 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.831 -if UnparseC.term t = "a" then () else error "check make_polynomial 4";
3.832 -
3.833 -"----- check 5 ---";
3.834 -val t = TermC.str2term "4*(3*a - 2*a)";
3.835 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.836 -if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
3.837 -
3.838 -"----- check 6 ---";
3.839 -val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
3.840 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
3.841 -if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
3.842 -
3.843 -"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
3.844 -"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
3.845 -"-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
3.846 -val thy = @{theory "Isac_Knowledge"};
3.847 -"===== works for a simple example, see rewrite.sml -- fun app_rev ===";
3.848 -val t = TermC.str2term "x \<up> 2 * x";
3.849 -val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
3.850 -if UnparseC.term t' = "x * x \<up> 2" then ()
3.851 -else error "poly.sml Poly.is_multUnordered doesn't work";
3.852 -
3.853 -(* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
3.854 -### rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +
3.855 - (-48 * x \<up> 4 + 8))
3.856 -###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
3.857 -####### try calc: Poly.is_multUnordered'
3.858 -======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
3.859 -*)
3.860 -val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))";
3.861 -
3.862 -"----- is_multUnordered ---";
3.863 -val tsort = sort_variables t;
3.864 -UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n-1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n-1 * (-1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";
3.865 -is_polyexp t;
3.866 -tsort = t;
3.867 -is_polyexp t andalso not (t = sort_variables t);
3.868 -if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
3.869 -
3.870 -"----- eval_is_multUnordered ---";
3.871 -val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
3.872 -case eval_is_multUnordered "testid" "" tm thy of
3.873 - SOME (_, Const ("HOL.Trueprop", _) $
3.874 - (Const ("HOL.eq", _) $
3.875 - (Const ("Poly.is_multUnordered", _) $ _) $
3.876 - Const ("HOL.True", _))) => ()
3.877 - | _ => error "poly.sml diff. eval_is_multUnordered";
3.878 -
3.879 -"----- rewrite_set_ STILL DIDN'T WORK";
3.880 -val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
3.881 -UnparseC.term t;
3.882 -
3.883 -
3.884 -"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
3.885 -"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
3.886 -"-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
3.887 -val thy = @{theory "Isac_Knowledge"};
3.888 -val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
3.889 -
3.890 -(*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
3.891 -(*+*) andalso not (is_multUnordered arg)
3.892 -(*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
3.893 -
3.894 -case eval_is_multUnordered "xxx " "yyy " t thy of
3.895 - SOME
3.896 - ("xxx 3 * a + - 2 * a_",
3.897 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
3.898 - Const ("HOL.False", _))) => ()
3.899 -(* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
3.900 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
3.901 -
3.902 -"----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
3.903 -val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
3.904 -
3.905 -(*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
3.906 -(*+*) andalso not (is_multUnordered arg)
3.907 -(*+*)then () else error "sort_variables - 2 * a CHANGED";
3.908 -
3.909 -case eval_is_multUnordered "xxx " "yyy " t thy of
3.910 - SOME
3.911 - ("xxx - 2 * a_",
3.912 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
3.913 - Const ("HOL.False", _))) => ()
3.914 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
3.915 -
3.916 -"----- is_multUnordered --- (a) is_multUnordered = False";
3.917 -val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
3.918 -
3.919 -(*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
3.920 -(*+*) andalso not (is_multUnordered arg)
3.921 -(*+*)then () else error "sort_variables a CHANGED";
3.922 -
3.923 -case eval_is_multUnordered "xxx " "yyy " t thy of
3.924 - SOME
3.925 - ("xxx a_",
3.926 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
3.927 - Const ("HOL.False", _))) => ()
3.928 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
3.929 -
3.930 -"----- is_multUnordered --- (- 2) is_multUnordered = False";
3.931 -val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
3.932 -
3.933 -(*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
3.934 -(*+*) andalso not (is_multUnordered arg)
3.935 -(*+*)then () else error "sort_variables - 2 CHANGED";
3.936 -
3.937 -case eval_is_multUnordered "xxx " "yyy " t thy of
3.938 - SOME
3.939 - ("xxx - 2_",
3.940 - Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
3.941 - Const ("HOL.False", _))) => ()
3.942 -| _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
3.943 -
3.944 -
3.945 -"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
3.946 -"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
3.947 -"-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
3.948 -(* ca.line 45 of Rewrite.trace_on:
3.949 -## rls: order_mult_rls_ on:
3.950 - x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
3.951 -### rls: order_mult_ on:
3.952 - x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
3.953 -###### rls: Rule_Set.empty-is_multUnordered on:
3.954 - 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
3.955 -####### try calc: "Poly.is_multUnordered"
3.956 -######## eval asms:
3.957 -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"
3.958 --------------------------------------------------------------------------------------------------==
3.959 -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"
3.960 -####### calc. to: True
3.961 -####### try calc: "Poly.is_multUnordered"
3.962 -####### try calc: "Poly.is_multUnordered"
3.963 -### rls: order_mult_ on:
3.964 -N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3
3.965 ---------+--------------------------+---------------------------------+---------------------------<>
3.966 -O:x \<up> 3 + -1 * (3 * (a * x \<up> 2)) + -1 \<up> 2 * (3 * (a \<up> 2 * x)) + -1 \<up> 3 * a \<up> 3
3.967 --------------------------------------------------------------------------------------------------<>
3.968 -*)
3.969 -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";
3.970 -(*
3.971 -"~~~~~ fun is_multUnordered
3.972 -"~~~~~~~ fun sort_variables
3.973 -"~~~~~~~~~ val sort_varList
3.974 -*)
3.975 -"~~~~~ fun is_multUnordered , args:"; val (t) = (t);
3.976 - is_polyexp t = true;
3.977 -
3.978 - val return =
3.979 - sort_variables t;
3.980 -(*+*)if UnparseC.term return =
3.981 -(*+*) "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"
3.982 -(*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
3.983 -
3.984 -"~~~~~~~ fun sort_variables , args:"; val (t) = (t);
3.985 - val ll = map monom2list (poly2list t);
3.986 - val lls = map sort_varList ll;
3.987 -
3.988 -(*+*)val ori3 = nth 3 ll;
3.989 -(*+*)val mon3 = nth 3 lls;
3.990 -
3.991 -(*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
3.992 -(*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
3.993 -(*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
3.994 -(*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
3.995 -
3.996 -(*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
3.997 -(*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
3.998 -(*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
3.999 -(*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
3.1000 -
3.1001 -"~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
3.1002 -(* Output below with:
3.1003 -val sort_varList = sort var_ord;
3.1004 -fun var_ord (a,b: term) =
3.1005 -(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
3.1006 - sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
3.1007 - prod_ord string_ord string_ord
3.1008 - ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
3.1009 -);
3.1010 -*)
3.1011 -(*+*)val xxx = sort_varList ori3;
3.1012 -(*
3.1013 -{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
3.1014 -{a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
3.1015 -
3.1016 -isa isa2
3.1017 -{a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
3.1018 - {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
3.1019 -{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
3.1020 - {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
3.1021 -{a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
3.1022 - {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
3.1023 - ^^^ ^^^
3.1024 -
3.1025 -{a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
3.1026 - {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
3.1027 - ^^^ ^^^
3.1028 -{a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
3.1029 - {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
3.1030 -{a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
3.1031 - {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
3.1032 -*)
3.1033 -
3.1034 -
3.1035 -"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
3.1036 -"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
3.1037 -"-------- fun is_multUnordered b * a * a ------------------------------------------------------";
3.1038 -val t = TermC.str2term "b * a * a";
3.1039 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1040 -if UnparseC.term t = "a \<up> 2 * b" then ()
3.1041 -else error "poly.sml: diff.behav. in make_polynomial 21";
3.1042 -
3.1043 -"~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
3.1044 - ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
3.1045 -
3.1046 -(*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
3.1047 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
3.1048 - (*if*) TermC.is_num num (*else*);
3.1049 -
3.1050 -"~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
3.1051 - (*if*) TermC.is_num num (*else*);
3.1052 - (*if*) TermC.is_variable num (*then*);
3.1053 -
3.1054 - val xxx = sort_variables t;
3.1055 -(*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
3.1056 -
3.1057 -
3.1058 -"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
3.1059 -"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
3.1060 -"-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
3.1061 -val t = TermC.str2term "2*3*a";
3.1062 -val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
3.1063 -(*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
3.1064 -(*
3.1065 -## try calc: "Groups.times_class.times"
3.1066 -## rls: order_mult_rls_ on: 6 * a
3.1067 -### rls: order_mult_ on: 6 * a
3.1068 -###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
3.1069 -####### try calc: "Poly.is_multUnordered"
3.1070 -######## eval asms: "6 * a is_multUnordered = True" (*isa*)
3.1071 - = False" (*isa2*)
3.1072 -####### calc. to: True (*isa*)
3.1073 - False (*isa2*)
3.1074 -*)
3.1075 -val t = TermC.str2term "(6 * a) is_multUnordered";
3.1076 -val SOME
3.1077 - (_, t') =
3.1078 - eval_is_multUnordered "xxx" () t @{theory};
3.1079 -(*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
3.1080 -(*+*)else error "6 * a is_multUnordered = False CHANGED";
3.1081 -
3.1082 -"~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
3.1083 - (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
3.1084 - (*if*) is_multUnordered arg (*else*);
3.1085 -
3.1086 -"~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
3.1087 - val return =
3.1088 - ((is_polyexp t) andalso not (t = sort_variables t));
3.1089 -
3.1090 -(*+*)return = false; (*isa*)
3.1091 -(*+*) is_polyexp t = true; (*isa*)
3.1092 -(*+*) not (t = sort_variables t) = false; (*isa*)
3.1093 -
3.1094 - val xxx = sort_variables t;
3.1095 -(*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
3.1096 -
3.1097 -
3.1098 -"-------- examples from textbook Schalk I ------------------------------------------------------";
3.1099 -"-------- examples from textbook Schalk I ------------------------------------------------------";
3.1100 -"-------- examples from textbook Schalk I ------------------------------------------------------";
3.1101 -"-----SPB Schalk I p.63 No.267b ---";
3.1102 -val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
3.1103 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1104 -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"
3.1105 -then () else error "poly.sml: diff.behav. in make_polynomial 1";
3.1106 -
3.1107 -"-----SPB Schalk I p.63 No.275b ---";
3.1108 -val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
3.1109 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1110 -if UnparseC.term t =
3.1111 - "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"
3.1112 -then () else error "poly.sml: diff.behav. in make_polynomial 2";
3.1113 -
3.1114 -"-----SPB Schalk I p.63 No.279b ---";
3.1115 -val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
3.1116 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1117 -if UnparseC.term t =
3.1118 - ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
3.1119 - "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
3.1120 - "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
3.1121 - " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
3.1122 -then () else error "poly.sml: diff.behav. in make_polynomial 3";
3.1123 -(*associate poly*)
3.1124 -
3.1125 -"-----SPB Schalk I p.63 No.291 ---";
3.1126 -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)))";
3.1127 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1128 -if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
3.1129 -then () else error "poly.sml: diff.behav. in make_polynomial 4";
3.1130 -
3.1131 -"-----SPB Schalk I p.64 No.295c ---";
3.1132 -val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
3.1133 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1134 -if UnparseC.term t =
3.1135 - "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"
3.1136 -then ()else error "poly.sml: diff.behav. in make_polynomial 5";
3.1137 -
3.1138 -"-----SPB Schalk I p.64 No.299a ---";
3.1139 -val t = TermC.str2term "(x - y)*(x + y)";
3.1140 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1141 -if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
3.1142 -then () else error "poly.sml: diff.behav. in make_polynomial 6";
3.1143 -
3.1144 -"-----SPB Schalk I p.64 No.300c ---";
3.1145 -val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
3.1146 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1147 -if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
3.1148 -then () else error "poly.sml: diff.behav. in make_polynomial 7";
3.1149 -
3.1150 -"-----SPB Schalk I p.64 No.302 ---";
3.1151 -val t = TermC.str2term
3.1152 - "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
3.1153 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
3.1154 -if UnparseC.term t = "0"
3.1155 -then () else error "poly.sml: diff.behav. in make_polynomial 8";
3.1156 -(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
3.1157 -
3.1158 -"-----SPB Schalk I p.64 No.306a ---";
3.1159 -val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
3.1160 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1161 -if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
3.1162 -else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";
3.1163 -
3.1164 -(*WN071729 when reducing "rls reduce_012_" for Schaerding,
3.1165 -the above resulted in the term below ... but reduces from then correctly*)
3.1166 -val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
3.1167 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1168 -if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
3.1169 -then () else error "poly.sml: diff.behav. in make_polynomial 9b";
3.1170 -
3.1171 -"-----SPB Schalk I p.64 No.296a ---";
3.1172 -val t = TermC.str2term "(x - a) \<up> 3";
3.1173 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1174 -
3.1175 -val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc";
3.1176 -
3.1177 -if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
3.1178 -then () else error "poly.sml: diff.behav. in make_polynomial 10";
3.1179 -
3.1180 -"-----SPB Schalk I p.64 No.296c ---";
3.1181 -val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
3.1182 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1183 -if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
3.1184 -then () else error "poly.sml: diff.behav. in make_polynomial 11";
3.1185 -
3.1186 -"-----SPB Schalk I p.62 No.242c ---";
3.1187 -val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
3.1188 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1189 -if UnparseC.term t = "1"
3.1190 -then () else error "poly.sml: diff.behav. in make_polynomial 12";
3.1191 -
3.1192 -"-----SPB Schalk I p.60 No.209a ---";
3.1193 -val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
3.1194 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1195 -if UnparseC.term t = "a \<up> 7"
3.1196 -then () else error "poly.sml: diff.behav. in make_polynomial 13";
3.1197 -
3.1198 -"-----SPB Schalk I p.60 No.209d ---";
3.1199 -val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
3.1200 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1201 -if UnparseC.term t = "d \<up> 3"
3.1202 -then () else error "poly.sml: diff.behav. in make_polynomial 14";
3.1203 -
3.1204 -"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
3.1205 -"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
3.1206 -"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
3.1207 -"-----Schalk I p.64 No.303 ---";
3.1208 -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)";
3.1209 -(*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
3.1210 -val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1211 -if UnparseC.term t = "1280 * b \<up> 4"
3.1212 -then () else error "poly.sml: diff.behav. in make_polynomial 14b";
3.1213 -(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
3.1214 -(*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
3.1215 -
3.1216 -"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
3.1217 -"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
3.1218 -"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
3.1219 -"-----SPO ---";
3.1220 -val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
3.1221 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1222 -if UnparseC.term t = "1" then ()
3.1223 -else error "poly.sml: diff.behav. in make_polynomial 15";
3.1224 -"-----SPO ---";
3.1225 -val t = TermC.str2term "a + a + a";
3.1226 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1227 -if UnparseC.term t = "3 * a" then ()
3.1228 -else error "poly.sml: diff.behav. in make_polynomial 16";
3.1229 -"-----SPO ---";
3.1230 -val t = TermC.str2term "a + b + b + b";
3.1231 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1232 -if UnparseC.term t = "a + 3 * b" then ()
3.1233 -else error "poly.sml: diff.behav. in make_polynomial 17";
3.1234 -"-----SPO ---";
3.1235 -val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
3.1236 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1237 -if UnparseC.term t = "a \<up> 2" then ()
3.1238 -else error "poly.sml: diff.behav. in make_polynomial 18";
3.1239 -"-----SPO ---";
3.1240 -val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
3.1241 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1242 -if (UnparseC.term t) = "1" then ()
3.1243 -else error "poly.sml: diff.behav. in make_polynomial 19";
3.1244 -"-----SPO ---";
3.1245 -val t = TermC.str2term "b + a - b";
3.1246 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1247 -if (UnparseC.term t) = "a" then ()
3.1248 -else error "poly.sml: diff.behav. in make_polynomial 20";
3.1249 -"-----SPO ---";
3.1250 -val t = TermC.str2term "b * a * a";
3.1251 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1252 -if UnparseC.term t = "a \<up> 2 * b" then ()
3.1253 -else error "poly.sml: diff.behav. in make_polynomial 21";
3.1254 -"-----SPO ---";
3.1255 -val t = TermC.str2term "(a \<up> 2) \<up> 3";
3.1256 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1257 -if UnparseC.term t = "a \<up> 6" then ()
3.1258 -else error "poly.sml: diff.behav. in make_polynomial 22";
3.1259 -"-----SPO ---";
3.1260 -val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
3.1261 -val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
3.1262 -if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
3.1263 -else error "poly.sml: diff.behav. in make_polynomial 23";
3.1264 -"-----SPO ---";
3.1265 -val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
3.1266 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
3.1267 -if (UnparseC.term t) = "a \<up> 4" then ()
3.1268 -else error "poly.sml: diff.behav. in make_polynomial 24";
3.1269 -"-----SPO ---";
3.1270 -val t = TermC.str2term "a * b * b \<up> (-1) + a";
3.1271 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
3.1272 -if UnparseC.term t = "2 * a" then ()
3.1273 -else error "poly.sml: diff.behav. in make_polynomial 25";
3.1274 -"-----SPO ---";
3.1275 -val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
3.1276 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
3.1277 -if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
3.1278 -then () else error "poly.sml: diff.behav. in make_polynomial 26";
3.1279 -
3.1280 -(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
3.1281 -"-----SPO ---";
3.1282 -val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
3.1283 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
3.1284 -if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
3.1285 -then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
3.1286 -
3.1287 -val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
3.1288 -val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
3.1289 -if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
3.1290 -then () else error "poly.sml: diff.behav. in make_polynomial 28";
3.1291 -
3.1292 -"-------- check pbl 'polynomial simplification' -----------------------------------------------";
3.1293 -"-------- check pbl 'polynomial simplification' -----------------------------------------------";
3.1294 -"-------- check pbl 'polynomial simplification' -----------------------------------------------";
3.1295 -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"];
3.1296 -"-----0 ---";
3.1297 -case Refine.refine fmz ["polynomial", "simplification"] of
3.1298 - [M_Match.Matches (["polynomial", "simplification"], _)] => ()
3.1299 - | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
3.1300 -(*...if there is an error, then ...*)
3.1301 -
3.1302 -"-----1 ---";
3.1303 -(*default_print_depth 7;*)
3.1304 -val pbt = Problem.from_store ["polynomial", "simplification"];
3.1305 -(*default_print_depth 3;*)
3.1306 -(*if there is ...
3.1307 -> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
3.1308 -... then Rewrite.trace_on:*)
3.1309 -
3.1310 -"-----2 ---";
3.1311 -Rewrite.trace_on := false;
3.1312 -M_Match.match_pbl fmz pbt;
3.1313 -Rewrite.trace_on := false;
3.1314 -(*... if there is no rewrite, then there is something wrong with prls*)
3.1315 -
3.1316 -"-----3 ---";
3.1317 -(*default_print_depth 7;*)
3.1318 -val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];
3.1319 -(*default_print_depth 3;*)
3.1320 -val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
3.1321 -val SOME (t',_) = rewrite_set_ thy false prls t;
3.1322 -if t' = @{term True} then ()
3.1323 -else error "poly.sml: diff.behav. in check pbl 'polynomial..";
3.1324 -(*... if this works, but --1-- does still NOT work, check types:*)
3.1325 -
3.1326 -"-----4 ---";
3.1327 -(*show_types:=true;*)
3.1328 -(*
3.1329 -> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
3.1330 -val wh = [False "(t_::real => real) (is_polyexp::real)"]
3.1331 -...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
3.1332 -val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
3.1333 -(*show_types:=false;*)
3.1334 -
3.1335 -
3.1336 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
3.1337 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
3.1338 -"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
3.1339 -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"];
3.1340 -val (dI',pI',mI') =
3.1341 - ("Poly",["polynomial", "simplification"],
3.1342 - ["simplification", "for_polynomials"]);
3.1343 -val p = e_pos'; val c = [];
3.1344 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.1345 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)
3.1346 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
3.1347 -
3.1348 -(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
3.1349 -(*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"
3.1350 -(*+*)then () else error "No.267b: I_Model.T CHANGED";
3.1351 -( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
3.1352 -
3.1353 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
3.1354 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
3.1355 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
3.1356 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
3.1357 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
3.1358 -
3.1359 -(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
3.1360 -(*+*)then () else error "";
3.1361 -
3.1362 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
3.1363 -
3.1364 -(*+*)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"
3.1365 -(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
3.1366 -
3.1367 -(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
3.1368 -
3.1369 -
3.1370 -
3.1371 -"-------- interSteps for Schalk 299a -----------------------------------------------------------";
3.1372 -"-------- interSteps for Schalk 299a -----------------------------------------------------------";
3.1373 -"-------- interSteps for Schalk 299a -----------------------------------------------------------";
3.1374 -reset_states ();
3.1375 -CalcTree
3.1376 -[(["Term ((x - y)*(x + (y::real)))", "normalform N"],
3.1377 - ("Poly",["polynomial", "simplification"],
3.1378 - ["simplification", "for_polynomials"]))];
3.1379 -Iterator 1;
3.1380 -moveActiveRoot 1;
3.1381 -autoCalculate 1 CompleteCalc;
3.1382 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
3.1383 -
3.1384 -interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
3.1385 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
3.1386 -if existpt' ([1,1], Frm) pt then ()
3.1387 -else error "poly.sml: interSteps doesnt work again 1";
3.1388 -
3.1389 -interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
3.1390 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
3.1391 -(*============ inhibit exn WN120316 ==============================================
3.1392 -if existpt' ([1,1,1], Frm) pt then ()
3.1393 -else error "poly.sml: interSteps doesnt work again 2";
3.1394 -============ inhibit exn WN120316 ==============================================*)
3.1395 -
3.1396 -"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
3.1397 -"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
3.1398 -"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
3.1399 -val thy = @{theory AlgEin};
3.1400 -
3.1401 -val SOME (f',_) = rewrite_set_ thy false norm_Poly
3.1402 -(TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
3.1403 -if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
3.1404 -then ((*norm_Poly NOT COMPLETE -- TODO MG*))
3.1405 -else error "norm_Poly changed behavior";
3.1406 -(* isa:
3.1407 -## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
3.1408 -### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
3.1409 -###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
3.1410 -oben is_addUnordered
3.1411 -####### try calc: "Poly.is_addUnordered"
3.1412 -######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
3.1413 -oben is_addUnordered = True"
3.1414 -####### calc. to: True
3.1415 -####### try calc: "Poly.is_addUnordered"
3.1416 -####### try calc: "Poly.is_addUnordered"
3.1417 -### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
3.1418 -*)
3.1419 -"~~~~~ fun sort_monoms , args:"; val (t) =
3.1420 - (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
3.1421 -(*+*)val t' =
3.1422 - sort_monoms t;
3.1423 -(*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
3.1424 -
3.1425 -"-------- ord_make_polynomial ------------------------------------------------------------------";
3.1426 -"-------- ord_make_polynomial ------------------------------------------------------------------";
3.1427 -"-------- ord_make_polynomial ------------------------------------------------------------------";
3.1428 -val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
3.1429 -val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
3.1430 -
3.1431 -if ord_make_polynomial true thy [] (t1, t2) then ()
3.1432 -else error "poly.sml: diff.behav. in ord_make_polynomial";
3.1433 -(*SO: WHY IS THERE NO REWRITING ...*)
3.1434 -
3.1435 -val term = TermC.str2term "2*b + (3*a + 3*b)";
3.1436 -(*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
3.1437 -(*
3.1438 -WHY IS THERE NO REWRITING ?!?
3.1439 -most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
3.1440 -while order_add_mult uses isac's rewriter -- and this is used rarely!
3.1441 -*)
3.1442 -