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";