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